The Coinduction library allows for parametrized coinduction proofs on the shallow definition of ag
but we have no way to do the same kind of proof in the deep definition, for example
We need to unfold entailsF only to do the parametrized coinduction underneath. This exposes the low-level details to the user of the deep embedding. We shouldn't do that and related #29 entailsF should be opaque.
One attempt at defining AG_coind' requires explicitly providing the coinductive relation, which is extremely tedious and cancels all the benefits of parametrized coinduction.
What would it take to do parametrized coinduction proofs without unfolding entailsF and without defining the relation R manually?
The Coinduction library allows for parametrized coinduction proofs on the shallow definition of
agbut we have no way to do the same kind of proof in the deep definition, for exampleWe need to unfold
entailsFonly to do the parametrized coinduction underneath. This exposes the low-level details to the user of the deep embedding. We shouldn't do that and related #29entailsFshould be opaque. One attempt at definingAG_coind'requires explicitly providing the coinductive relation, which is extremely tedious and cancels all the benefits of parametrized coinduction.What would it take to do parametrized coinduction proofs without unfolding
entailsFand without defining the relation R manually?