*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, cl-isabelle-users at lists.cam.ac.uk, Jasmin Blanchette <jasmin.blanchette at inria.fr>, Dmitriy Traytel <traytel at inf.ethz.ch>*Subject*: Re: [isabelle] Tactic failed for Friends*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Mon, 26 Sep 2016 15:03:35 +0200*In-reply-to*: <00f02c62-4ff3-a8fd-858b-61d019659ecb@inf.ethz.ch>*References*: <0d224229-1202-cf1b-0812-dcea78d11a40@in.tum.de> <00f02c62-4ff3-a8fd-858b-61d019659ecb@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.3.0

Thanks for the explanation (also to Dmitriy).

Cheers, Manuel On 26/09/16 14:05, Andreas Lochbihler wrote:

Dear Manuel,"corec (friend)" internally uses transfer_prover, which has itsproblems with equality on compound types. In detail, corec generates aparametricity proof obligation and passes it to transfer_prover. Inyour example, this goal contains "op =" on tuples of reals, whichtransfer_prover cannot handle, because it expects it to be written as"rel_prod op = op =".Either, you now bug Ondra or (Jasmin or Dmitriy) to changetransfer_prover or corec such that their tools work together smoothly.Or you just use the long formcorecursive (friend) and manually prove the parametricity: by(fold relator_eq) transfer_prover Hope this helps, Andreas On 26/09/16 13:17, Manuel Eberl wrote:Hallo,I don't know awfully much about friends and corecursion, but in mynaÃvetÃ, I simply added"(friend)" to a reasonably friendly-looking corecursive definitionand expected it towork. Instead, it looped. A minimal non-working example is thefollowing:type_synonym ae = "(real Ã real) stream" corec (friend) add_ae :: "ae â ae" where "add_ae f = ((fst (shd f), snd (shd f)) ## add_ae (stl f))" This runs for about 3 seconds and then returns with the following error: Tactic failed The error(s) above occurred for the goal statementâ: rel_fun (rel_prod R (rel_pre_stream op = R)) (rel_pre_stream op = (rel_ssig_stream_v1 R)) (Îf. ((fst (fst (snd f)), snd (fst (snd f))), stream.v1.Oper (stream.v1.Sig (Inr (case snd f of (x1, x2) â stream.v1.VLeaf x2))))) (Îf. ((fst (fst (snd f)), snd (fst (snd f))), stream.v1.Oper (stream.v1.Sig (Inr (case snd f of (x1, x2) â stream.v1.VLeaf x2)))))The problem does not occur if I replace "(fst (shd f), snd (shd f))"with the equivalent"shd f".A similar, slightly less vacuous definition that is closer to myoriginal definition isthe following: corec (friend) add_ae :: "ae â ae â ae" where"add_ae f g = ((fst (shd f) + fst (shd g), snd (shd f)) ## add_ae(stl f) (stl g))"That also causes a similar error, but it takes about 110 seconds toget there. The commanddefining the function I originally had in mind has not terminated yet. Cheers, Manuel

**References**:**[isabelle] Tactic failed for Friends***From:*Manuel Eberl

**Re: [isabelle] Tactic failed for Friends***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Tactic failed for Friends
- Next by Date: Re: [isabelle] Mutual coinduction
- Previous by Thread: Re: [isabelle] Tactic failed for Friends
- Next by Thread: [isabelle] Open Ph.D. position in Formal Methods for Information Security at ETH Zurich
- Cl-isabelle-users September 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list