Sorry but bumping it, since I think it should be addressed.

Recall that `Nat.add_1_l`

is :

```
Nat.add_1_l
: forall n : nat, 1 + n = S n
```

The first `rewrite`

matches, as it should, `1 + _`

against `1 + n`

but somehow, the second one fails to match `1 + (S n)`

against `1 + _`

.

`Import`

ing ssreflect works ;

```
Require Import PeanoNat.
Require Import ssreflect.
Theorem exemple_rewrite_thm_unif : forall n : nat, 0 + (1 + (1 + n)) = S (S n).
Proof.
intros n.
rewrite Nat.add_1_l.
rewrite Nat.add_1_l. (* no instantiation needed *)
rewrite Nat.add_0_l.
reflexivity.
Qed.
```

This example is not hand-crafted to expose a `rewrite`

failure, but is actually used in an undergraduate introductory course.

I think you read it ~~wrong~~ right.

The first time, it matches `1 + (1 + n)`

and you get `S (1 + n)`

, then it matches `1 + n`

and you get `S n`

(under the previous `S`

).

The goal is traversed left to right, outside in.

Sorry, I did not read that the problem was using vanilla rewrite. The difference is that SSR looks for the head symbol, if your rule has a pattern `_ + _`

then it will only try it on expressions starting with `+`

. Maybe you can use vanilla rewrite in conjunction with `Set Keyed Unification.`

, but I would recommend you use SSR's rewrite, it is just less surprising.

Enrico Tassi said:

I think you read it

~~wrong~~right.

The first time, it matches`1 + (1 + n)`

and you get`S (1 + n)`

, then it matches`1 + n`

and you get`S n`

(under the previous`S`

).

The goal is traversed left to right, outside in.

Sorry, you're right, edited. Still, I don't understand why the unification fails for the second rewrite in vanilla coq.

and importing SSR changes a lot the behavior of `rewrite`

...

Yes SSR rewrite is a completely separate tactic, thatâ€™s what Enrico was advising. Especially if you are trying to explain precisely what rewrite does.

As being discussed in the neighbor thread (https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/what.20is.20SSReflect.20about.3F/near/303147647), vanilla `rewrite`

's behavior is pretty undocumented

Last updated: Jan 31 2023 at 12:01 UTC