The Coq mailing list

[casteran AT labri.fr]

Hi,

 I tried to work on the example below, but I couldn't program the
behaviour you suggest (replacing (S x) with x+1 in the term pointed
by match context and not elsewhere).



The syntax of Ltac admits context variables, so that one can
 use a pattern  variable like C :
[context C [(mult ?X3 (S ?X1))] and use it to fill C with any term.



What I would like to do is using C to apply the "pattern" tactic and then
a rewrite, something like :

  pattern (mult X3 (S X1)) at C

or better
  pattern (S X1) at C::3 (or something like that)

but pattern ... at  expects occurrence numbers.

I tried :

Ltac S_to_plus_simpl_2 :=
  match goal with
  | |-  context C [(mult ?X3 (S ?X1))] =>
      let f := fresh in
        let e' := context C [(mult X3 f)])) in
            change ((fun f:nat => e') (S X1));
            rewrite (S_to_plus_one X1)
        end.

But it doesn't work.



Pierre


Selon Venanzio Capretta 
<Venanzio.Capretta AT mathstat.uottawa.ca>:
>
> 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.