Stream: Equations devs & users

Topic: getting equalities out of with clauses

Armaël Guéneau (Jul 04 2022 at 15:54):

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?

James Wood (Jul 04 2022 at 16:10):

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 withs in the opposite order.

Armaël Guéneau (Jul 04 2022 at 16:12):

ah, very good! thanks for the pointer, it does indeed look like what I'm looking for

Théo Winterhalter (Jul 04 2022 at 16:33):

In Equations lingo it's also called inspect:

Definition inspect {A} (x : A) : { y : A | y = x } := exist x eq_refl.

Théo Winterhalter (Jul 04 2022 at 16:36):

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).

Matthieu Sozeau (Jul 05 2022 at 09:33):

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 ;)

Matthieu Sozeau (Jul 05 2022 at 09:35):

@James Wood Equations does support multiple-with (separated by ,)

James Wood (Jul 05 2022 at 09:36):

I think this is equivalent to two withs in sequence, though, rather than a simultaneous with.

James Wood (Jul 05 2022 at 09:40):

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.

Paolo Giarrusso (Jul 20 2022 at 14:33):

FWIW, Equations does have some docs for this: https://github.com/mattam82/Coq-Equations/blob/82dc46c6c0ed1e28436ab48f8a28fe7618f2da40/examples/Basics.v#L506-L538

Paolo Giarrusso (Jul 20 2022 at 14:34):

posting here because @Traian Florin Șerbănuță just run into this again.

Traian Florin Șerbănuță (Jul 20 2022 at 14:36):

Thanks, that really helps!

Traian Florin Șerbănuță (Sep 05 2022 at 09:04):

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?

Matthieu Sozeau (Sep 05 2022 at 12:58):

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

Matthieu Sozeau (Sep 05 2022 at 12:58):

Maybe use eq: instead?

Traian Florin Șerbănuță (Sep 07 2022 at 12:41):

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?

Karl Palmskog (Sep 07 2022 at 12:42):

maybe the right thing to ask is: is a PR which adds exporting inspect and eqn (possibly renamed) to all Equations users welcome?

Karl Palmskog (Sep 07 2022 at 12:43):

as a start, we could extract out the key definitions into a standalone file and try copying it into a couple of projects

Matthieu Sozeau (Sep 07 2022 at 12:44):

We did merge already a definition of inspect

Matthieu Sozeau (Sep 07 2022 at 12:46):

https://github.com/mattam82/Coq-Equations/pull/481/files

Matthieu Sozeau (Sep 07 2022 at 12:47):

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 ?

Théo Winterhalter (Sep 07 2022 at 13:04):

This sounds great!

Last updated: May 28 2023 at 18:29 UTC