In the following snippet:

```
From mathcomp Require Import ssreflect ssrnat.
Goal forall x y, x + y = y + x.
Proof.
move => x y.
elim : y x => [ | y IHy] x.
Search ( _ + 0). (*nothing*)
Fail by []. admit.
rewrite addnS.
by rewrite IHy.
Admitted.
```

There are two problems I am facing, the most obvious one is somehow I cannot prove `_ + 0 = 0 + _`

both LHS and RHS refuse to simplify.

and it feels very very strange not being able to make progress in this simple goal.

Second, there is something I don't like about the two commands:

```
move => x y.
elim : y x => [ | y IHy] x.
```

These two commands does two things reorder `x`

and `y`

, then proceed by induction on `y`

, but the split of roles is not clean. elim contribute to both re-ordering and induction.

So is there a single command (I know I can do it with 2 `move`

commands) that reorder arguments ? I tried `move => x y : y x`

but that did not work.

For the first question:

```
From mathcomp Require Import ssreflect ssrnat.
Goal forall x y, x + y = y + x.
Proof.
move => x y.
elim : y x => [ | y IHy] x.
by rewrite add0n addn0.
rewrite addnS.
by rewrite IHy.
Qed.
```

why are add0n and addn0 not searchable ?

They are defined as e.g. `ssrfun.left_id 0 addn`

...

They are not searchable because they don't have the form you asked (see `Check addn0`

)... searching can become pretty hard if you don't know what you're looking for... which defeats the purpose...

... which defeats the purpose...

Indeed!

https://github.com/math-comp/math-comp/wiki/Search

noted, so search as in search the files manuall xD.

now the other thing I wanted to inquire about is if there is tactic for reordering quantifiers in goal ?

I'm afraid not being able to find `addn0`

is a mathcomp rite of passage. There are other similar cases, such as `idempotent`

and `injective`

. This is really annoying, I think everyone is aware it is really annoying, and IIRC there were people working on improving `Search`

.

In the meantime, my workaround for when I think there really should be a lemma but I can't find it is to reduce the `Search`

to the bare minimum. In this case, I might try `Search 0 addn`

(you can discover the name behind the `_ + _`

notation with `Locate "_ + _"`

). The trick of using the function name instead of its notation arose specifically to deal with cases like this one.

Re: reordering, I'm not aware of a specific way to achieve it. You could `move=> + y; elim: y`

to avoid naming and moving `x`

around, but I don't know if that's much better.

Nevermind, there is something! `move=> /[swap].`

(found here)

Last updated: May 18 2024 at 08:40 UTC