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?

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.

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

In Equations lingo it's also called `inspect`

:

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

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

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

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

)

I think this is equivalent to two `with`

s in sequence, though, rather than a simultaneous `with`

.

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.

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

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

Thanks, that really helps!

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?

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

Maybe use `eq: `

instead?

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?

maybe the right thing to ask is: is a PR which adds exporting `inspect`

and `eqn`

(possibly renamed) to all Equations users welcome?

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

We did merge already a definition of inspect

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

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 ?

This sounds great!

Last updated: May 24 2024 at 22:02 UTC