Email Gateway (Aug 22 2022 at 14:09): Email Gateway (Aug 22 2022 at 14:09):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 22 2022 at 14:09):From: Dmitriy Traytel <traytel@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 14:09):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 14:09):From: Manuel Eberl <eberlm@in.tum.de>
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
Last updated: Apr 24 2024 at 08:20 UTC