Discussion:
[isabelle] Tactic failed for Friends
Manuel Eberl
2016-09-26 11:21:27 UTC
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
Dmitriy Traytel
2016-09-26 12:07:10 UTC
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
Post by Manuel Eberl
Hallo,
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))"
Tactic failed
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".
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
Andreas Lochbihler
2016-09-26 12:08:01 UTC
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
Post by Manuel Eberl
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
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))"
Tactic failed
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
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
Manuel Eberl
2016-09-26 13:06:29 UTC
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
Post by Andreas Lochbihler
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)
by(fold relator_eq) transfer_prover
Hope this helps,
Andreas
Post by Manuel Eberl
Hallo,
I don't know awfully much about friends and corecursion, but in my
"(friend)" to a reasonably friendly-looking corecursive definition and expected it to
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))"
Tactic failed
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
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