Re: [isabelle] Tactic failed for Friends



Thanks for the explanation (also to Dmitriy).

I, of course, cannot say who of the people involved is more obligated to change their tool in order to make this work. This isn't a very pressing issue for me either, and now that I know of the workaround, it's not a big problem for me anymore either.

Nevertheless, it would probably be good if this could be resolved soon, lest others without knowledge of the internals of the codatatype package fall into the same trap as I did.

Cheers,

Manuel


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

"corec (friend)" internally uses transfer_prover, which has its problems with equality on compound types. In detail, corec generates a parametricity proof obligation and passes it to transfer_prover. In your example, this goal contains "op =" on tuples of reals, which transfer_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 change transfer_prover or corec such that their tools work together smoothly. Or you just use the long form

  corecursive (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 my naÃvetÃ, I simply added "(friend)" to a reasonably friendly-looking corecursive definition and expected it to work. Instead, it looped. A minimal non-working example is the following:

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 my original definition is
the 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 to get there. The command
defining the function I originally had in mind has not terminated yet.


Cheers,

Manuel




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.