Re: [isabelle] Tactic failed for Friends



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.