Why does this rewrite fail ? · Coq users

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 .

Tactic generated a subgoal identical to the original goal.

Guillaume Melquiond (Oct 04 2022 at 05:14):

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.

Gaëtan Gilbert (Oct 04 2022 at 08:12):

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

Pierre Rousselin (Oct 09 2022 at 18:54):

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 + _.
Importing 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.

Enrico Tassi (Oct 09 2022 at 19:09):

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.

Enrico Tassi (Oct 09 2022 at 19:13):

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.

Pierre Rousselin (Oct 09 2022 at 19:27):

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

Paolo Giarrusso (Oct 09 2022 at 22:16):

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.

Stream: Coq users

Topic: Why does this rewrite fail ?

Pierre Rousselin (Oct 04 2022 at 04:52):