Stream: Equations devs & users

Topic: getting equalities out of with clauses


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

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

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

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

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

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

view this post on Zulip Matthieu Sozeau (Jul 05 2022 at 09:35):

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

view this post on Zulip James Wood (Jul 05 2022 at 09:36):

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

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

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

view this post on Zulip Paolo Giarrusso (Jul 20 2022 at 14:34):

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

view this post on Zulip Traian Florin Șerbănuță (Jul 20 2022 at 14:36):

Thanks, that really helps!

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

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

view this post on Zulip Matthieu Sozeau (Sep 05 2022 at 12:58):

Maybe use eq: instead?

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

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

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

view this post on Zulip Matthieu Sozeau (Sep 07 2022 at 12:44):

We did merge already a definition of inspect

view this post on Zulip Matthieu Sozeau (Sep 07 2022 at 12:46):

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

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

view this post on Zulip Théo Winterhalter (Sep 07 2022 at 13:04):

This sounds great!


Last updated: Jan 29 2023 at 16:02 UTC