The Coq mailing list

[casteran AT labri.fr]

Selon Venanzio Capretta 
<Venanzio.Capretta AT mathstat.uottawa.ca>:


Hi Venanzio,

Hello  Venanzio,


There was indeed some problem with the semantics of "match ... term"
and "fail i" in Ltac.

In the current CVS version, the "match term with" evaluates immediately
the tactics it produces. Then your example works perfectly.
Hugo will add an option for lazy evaluation of match term in case it is
needed.




In Coq V8.0 (with lazy evaluation of match term with)
, your "strange example" works if you replace the "fail 1" with a
"fail 0".
Notice that, in the current coqCVS, replacing "fail 1" with "fail 0"
makes your example loop.

Hugo, am I right?


Now, Yves and I must put something about that in our book site (in the
errata of chapter 7).

For your second example :

Ltac S_to_plus_simpl_mult :=
  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_mult
      end
  | |- _ => idtac
  end.

Let us replace the last successor in strange example
by something else.

Theorem strange_example':
  forall n k:nat, (S n)*(S k) = S n + k*0.
Proof.
intros.
S_to_plus_simpl_mult.

  n : nat
  k : nat
  ============================
   S n * (k + 1) = S n + k * 0


You  can see that not "all" the terms "S ..." were replaced.

Only the terms having some occurrence at the right of
a multiplication were replaced.

Another way to "debug" the tactic is to write a non recursive version
of this tactic and look at each step.


So its seems correct to me.


Regards,

Pierre









> 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
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>




----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.