--- Day changed Sat Feb 10 2018
apostolishttp://lpaste.net/36233510/02 18:02
apostolisCan anyone help me with coinduction and instance arguments?10/02 18:02
apostolisI made a simple test program. Unfortunately the coinductive proof is not constructed with instance resolution.10/02 18:03
apostolishttp://lpaste.net/36233610/02 18:11
{AS}apostolis: did you try to construct the proof manually?10/02 19:05
{AS}apostolis: in any case10/02 19:06
{AS}you want the recursive arguments to your constructors to also use {{ }}10/02 19:07
{AS}if you want instance resolution to succeed10/02 19:07
{AS}Agda as far as I recall will not recursively search for explicit arguments10/02 19:07
apostolis{AS} I did construct it manually.10/02 19:09
{AS}apostolis: how does it look?10/02 19:09
apostolisCheck line 8510/02 19:09
apostolisFrom the second lpaste. I did omit {{}} in the first.10/02 19:10
{AS}apostolis: Hmm, this requires a bit complex recursion10/02 19:10
{AS}I do not know whether Agda can do this10/02 19:10
{AS}Maybe someone else knows10/02 19:10
{AS}apostolis: Maybe if you can add some kind of coinduction principle and make it take instance argumetns?10/02 19:11
{AS}I am not sure whether this is possible :)10/02 19:11
apostolisYea, I couldn't find anything on the internet either :)10/02 19:12
apostolis{AS} Maybe If I create a generic function that creates the proof and then tag that function as instance. I think this will work.10/02 20:03
{AS}apostolis: yeah10/02 21:10
apostolisWell, I think that it is impossible to prove that by using a generic function. In coinductive proofs, you know the pattern, this is why you can provide the proof.10/02 22:50
apostolisI am pretty sure that instance resolutions searches blindly for a proof, thus it will not be able to do what I want for coinduction. 10/02 22:53

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!