coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: casteran AT labri.fr
- To: Venanzio Capretta <Venanzio.Capretta AT mathstat.uottawa.ca>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] tactic bug
- Date: Fri, 19 Nov 2004 15:20:35 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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.
- [Coq-Club] tactic bug, Venanzio Capretta
- Re: [Coq-Club] tactic bug,
casteran
- Re: [Coq-Club] tactic bug, Hugo Herbelin
- Re: [Coq-Club] tactic bug, casteran
- Re: [Coq-Club] tactic bug, Venanzio Capretta
- Re: [Coq-Club] tactic bug,
casteran
Archive powered by MhonArc 2.6.16.