The Coq mailing list

[Venanzio Capretta <Venanzio.Capretta AT mathstat.uottawa.ca>]

Hi,
 I was reading Chapter 7 of the book by Yves Bertot and Pierre Casteran
about defining tactics. They give an example of definition of a tactic
by contextual pattern-matching "S_to_plus_simpl" that replaces all the
occurrences of (S x) with (x+1), provided that x is not 0.

I think the following shows a bug in the execution of tactics:

--------------------------------------------------------------------------------------
Require Import Arith.

Theorem S_to_plus_one : forall n:nat, S n = n+1.
Proof.
 intros; rewrite plus_comm; reflexivity.
Qed.

Ltac S_to_plus_simpl :=
 match goal with
 | |-  context [(S ?X1)] =>
     match X1 with
     | 0%nat => fail 1
     | ?X2 => rewrite (S_to_plus_one X2); S_to_plus_simpl
     end
 | |- _ => idtac
 end.

Theorem strange_example:
 forall n k:nat, (S n)*(S k) = (S n) + k*(S n).
Proof.
intros.
S_to_plus_simpl.
-----------------------------------------------------------------------------------------

Here I expected (S k) to be changed to (k+1) too, but it isn't. Why?

Even stranger: I tried to change the pattern to force the reduction when
the successor is on the right of the multiplication symbol:
--------------------------------------------------------------------------------------
Ltac S_to_plus_simpl :=
 match goal with
 | |-  context [(mult ?X3 (S ?X1))] =>
     match X1 with
     | 0%nat => fail 1
     | ?X2 => rewrite (S_to_plus_one X2); S_to_plus_simpl
     end
 | |- _ => idtac
 end.
---------------------------------------------------------------------------------------

Now, when I try to use the tactic in the proof of strange_example, "all"
successors are replaced, even those that are not on the right of a
multiplication !?

Venanzio