Stream: Coq users

Topic: Why does this rewrite fail ?


view this post on Zulip Pierre Rousselin (Oct 04 2022 at 04:52):

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.

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

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

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

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: Mar 29 2024 at 04:02 UTC