I am writing a low-level example about rewrite and unification.

```
Require Import PeanoNat.
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 n). (* Why do I have to instantiate with n ? *)
rewrite Nat.add_0_l.
reflexivity.
Qed.
```

I don't understand why the second `rewrite`

fails if I don't instantiate it.

With just :

```
Require Import PeanoNat.
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 .
```

The error message is :

```
Tactic generated a subgoal identical to the original goal.
```

For some reason, Coq succeeds in matching `1 + _`

against `S x`

, so it rewrites `S x`

into `S x`

(with `x`

being `1 + n`

). This looks like a bug.

I think rewrite's unification considers constants to be unfoldable

changing that probably leads to other pains

see eg https://github.com/coq/coq/pull/15588 for an attempt to change it for setoid_rewrite

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 `1 + _`

against `1 + (1 + n)`

but somehow, the second one fails to match `1 + 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: Sep 23 2023 at 07:01 UTC