Hello, I want to use Equations with a wf and a "with" case analysis on the result of another function's call on the argument, such as the following:

```
From Equations Require Import Equations.
Equations? f (x : nat) : nat by wf x lt :=
f 0 := 1 ;
f x with 0 + x := {
| O := O;
| S y := f y;
}.
```

However the wf obligation seems to lack an equality, here `0 + x`

and the pattern `S y`

. Do you know how to make Equations provide this information? Thank you!

You should apply the inspect pattern described in this example to `0 + x`

.

Oh, indeed, thank you Kenji!

Btw there are now new tutorials for Equations https://github.com/Zimmi48/platform-docs/tree/main/src including one specifically about Equations + wf. Among others, the inspect method is explained in it.

Indeed Thomas, I did see your tutorial when searching for "wf" here, but I did not find the information. I should have thought of searching for the "remember" keyword... Thank you for the tutorial!

it's unfortunate that the `inspect`

definition and notation are not available in some module after installing the `coq-equations`

package. This means that everyone (1) has to discover that they need it and (2) copy-paste their own version into their local project

specifically:

```
Definition inspect {A} (a : A) : {b | a = b} :=
exist _ a eq_refl.
Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20).
```

probably there should be some scope to make the notation optional and avoid clashes

since I don't have cycles personally I will open an Equations issue about this, and some volunteer hopefully chips in

https://github.com/mattam82/Coq-Equations/issues/613

`inspect`

is in Equations.Logic but not exported indeed...

I think the notation is problematic as it clashes with `destruct x eqn:H`

no?

well, it could be renamed then? I think the key point is that Equations users and tutorials are all copy-pasting this, so a new central recommended solution doesn't have to use the old stuff verbatim

Yep, but I don't known how to best fix the notation at the moment, the clash with destruct is really sad because they are basically doing the same thing but cannot be notated the same way. Using `eq:`

instead seems dangerous

I updated the issue to reflect all this

@Jean-Marie Madiot So I guess it is an issue of finding information. Did the sum up at the beginning and the toc not complete / clear enough ?

@Thomas Lamiaux no no I think it is clear enough, I just didn't spend enough time on it, it was one of many tabs in my search for an answer and I decided to cut it short too soon. I was looking for some kind of `as`

syntax next to the `with`

, though I'm surprised the `eqn:`

did not catch my eye.

ok, if in your work you encounter other methods you regularly use / folklore you would like to see turned into knowledge and is not in the documentation don't hesitate to say so

Last updated: Oct 13 2024 at 01:02 UTC