Re: [isabelle] Tactic failed for Friends



Hi Manuel,

this is due to a known (to Ondra) weakness of the transfer_prover. Because of this, Andreas Lochbihler always uses his own transfer_proverâ method locally, with which the following works.

method transfer_prover' = (unfold relator_eq[symmetric]; transfer_prover)

type_synonym ae = "(real à real) stream"

corecursive (friend) add_ae :: "ae â ae" where
 "add_ae f = ((fst (shd f), snd (shd f)) ## add_ae (stl f))"
  by transfer_proverâ

We could use transfer_proverâ in Corec by default, but the proper resolution would be to make the transfer_prover to work modulo relator_eq once and for all.

Cheers,
Dmitriy

> On 26 Sep 2016, at 13:17, Manuel Eberl <eberlm at in.tum.de> 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.