Stream: Coq users

Topic: Why does this rewrite fail ?


view this post on Zulip 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, as it should, 1 + _ against 1 + n but somehow, the second one fails to match 1 + (S 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre Rousselin (Oct 09 2022 at 19:27):

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 09 2022 at 22:31):

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