James Wood (Feb 28 2022 at 16:57): James Wood (Feb 28 2022 at 16:57):Does Equations support simultaneous with-abstraction, and in particular the inspect idiom?
Notification Bot (Feb 28 2022 at 16:59):This topic was moved here from #Coq users > Equations simultaneous with by Karl Palmskog.
Paolo Giarrusso (Feb 28 2022 at 18:10):I think the inspect idiom appears in examples, even by name
Paolo Giarrusso (Feb 28 2022 at 18:14):OTOH, I can't find examples with multiple with clauses :-|... the grammar in the manual might suggest that | works?
Paolo Giarrusso (Feb 28 2022 at 18:15):No sorry, it should be , , see the last line:
image.png
James Wood (Feb 28 2022 at 20:38):The example doesn't abstract over the thing being inspected (the Agda docs explain this fairly well), but I'll give comma a go. Thanks!
Kenji Maillard (Feb 28 2022 at 21:11):The only example I know uses multiple with clauses (in this file from metacoq)
James Wood (Mar 02 2022 at 10:52):So, as far as I can tell, having multiple with-expressions just does a sequence of with-abstractions, rather than one simultaneous with-abstraction. Adapting example f₃ from the Agda docs produces an ill typed term:
From Equations Require Import Equations.
Axiom T : nat -> Set.
Axiom H : forall x y, T (x + y) -> Set.
Equations? f3 : forall x y (t : T (x + y)) (h : H x y t), T (x + y) :=
| x, y, t, h with h, x + y => {
| w2, w1 => _
}.
However, this seems to be good enough for the (full) inspect idiom, or at least my use case.
James Wood (Mar 02 2022 at 14:22):Hmm, maybe it's not enough for my next use case. Is there any way to do a simultaneous with-abstraction in Ltac?
Last updated: Jun 11 2023 at 01:30 UTC