Maybe this is a naive question, but, when writing a definition as follows, which produces an obligation in each branch,
Equations uncons {A n} : t A (Ps n) -> A * t A n :=
uncons (exist _ xs _) with dequeue_internal.uncons xs => {
uncons (exist _ xs _) None _ := _;
uncons (exist _ xs _) (Some (x, xs')) _ := (x, exist _ xs' _)
}.
in each obligation, the information that dequeue_internal.uncons xs = None
or dequeue_internal.uncons xs = Some (x, xs')
has been lost. Is there a way of writing the code to get this information back in the obligations?
It sounds like you want the inspect idiom. I'm not sure there's any Equations-specific documentation, but the Agda documentation should get you going. Equations doesn't have simultaneous with
, as far as I'm aware, but it's often good enough to do sequential with
s in the opposite order.
ah, very good! thanks for the pointer, it does indeed look like what I'm looking for
In Equations lingo it's also called inspect
:
Definition inspect {A} (x : A) : { y : A | y = x } := exist x eq_refl.
I also think I saw @Yannick Forster use a nice parse-only notation for it. Something like
Notation "x 'eqn:' e" := (exist x e) (only parsing).
Yep, and inspect is now part of the Equations .v files, so you will not need to redefine it in future versions. Also in the direction { y : A | x = y }
which seems more natural (to me at least ;)
@James Wood Equations does support multiple-with (separated by ,
)
I think this is equivalent to two with
s in sequence, though, rather than a simultaneous with
.
It probably doesn't make a difference for this use case. Indeed, here we only need the simple inspect idiom, because nothing in the goal and context mentions the term we are taking cases of. So there's no use for the simultaneous with
-based inspect idiom.
FWIW, Equations does have some docs for this: https://github.com/mattam82/Coq-Equations/blob/82dc46c6c0ed1e28436ab48f8a28fe7618f2da40/examples/Basics.v#L506-L538
posting here because @Traian Florin Șerbănuță just run into this again.
Thanks, that really helps!
I have another question about inspect (btw, it's working great so far): I'm trying to use the eqn:
notation, but it seems to sometimes conflict with the eqn:
associated to standard tactics like destruct
. Any suggestions about how to deal with things like that?
I guess you have to disambiguate because destruct
expects a term
and an optional eqn:ident
, so it's a direct clash in the grammar
Maybe use eq:
instead?
Yes, eq:
would work; now I see that inspect
and eqn:
are part of the examples, not exported by the library.
Are there any plans to export inspect
and eqn:
(well, maybe renamed) as equation definition helpers in the future?
maybe the right thing to ask is: is a PR which adds exporting inspect
and eqn
(possibly renamed) to all Equations users welcome?
as a start, we could extract out the key definitions into a standalone file and try copying it into a couple of projects
We did merge already a definition of inspect
https://github.com/mattam82/Coq-Equations/pull/481/files
Adding an eq:
notation (in some module that's not exported by default for safety) would be fine with me, what do you think @Yannick Forster @Théo Winterhalter @Kenji Maillard ?
This sounds great!
Last updated: May 28 2023 at 18:29 UTC