Stream: Equations devs & users

Topic: Equations simultaneous `with`


view this post on Zulip James Wood (Feb 28 2022 at 16:57):

Does Equations support simultaneous with-abstraction, and in particular the inspect idiom?

view this post on Zulip Notification Bot (Feb 28 2022 at 16:59):

This topic was moved here from #Coq users > Equations simultaneous with by Karl Palmskog.

view this post on Zulip Paolo Giarrusso (Feb 28 2022 at 18:10):

I think the inspect idiom appears in examples, even by name

view this post on Zulip Paolo Giarrusso (Feb 28 2022 at 18:14):

E.g. https://github.com/mattam82/Coq-Equations/blob/82dc46c6c0ed1e28436ab48f8a28fe7618f2da40/examples/Basics.v#L506-L538

OTOH, I can't find examples with multiple with clauses :-|... the grammar in the manual might suggest that | works?

view this post on Zulip Paolo Giarrusso (Feb 28 2022 at 18:15):

No sorry, it should be , , see the last line:
image.png

view this post on Zulip 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!

view this post on Zulip Kenji Maillard (Feb 28 2022 at 21:11):

The only example I know uses multiple with clauses (in this file from metacoq)

view this post on Zulip 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 => _
  }.

view this post on Zulip James Wood (Mar 02 2022 at 10:52):

However, this seems to be good enough for the (full) inspect idiom, or at least my use case.

view this post on Zulip 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: Jan 29 2023 at 15:02 UTC