## 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 `with`s 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 `with`s 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 24 2024 at 22:02 UTC