8.5 AutoRewrite
Example: Here is a basic use of AutoRewrite with the Ackermann function:
Coq < Require Arith.
Coq <
Coq < Variable Ack:nat->nat->nat.
Coq <
Coq < Axiom Ack0:(m:nat)(Ack (0) m)=(S m).
Coq < Axiom Ack1:(n:nat)(Ack (S n) (0))=(Ack n (1)).
Coq < Axiom Ack2:(n,m:nat)(Ack (S n) (S m))=(Ack n (Ack (S n) m)).
Coq < HintRewrite base0 [ Ack0 LR
Coq < Ack1 LR
Coq < Ack2 LR].
Coq <
Coq < Lemma ResAck0:(Ack (2) (1))=(5).
1 subgoal
============================
(Ack (2) (1))=(5)
Coq < AutoRewrite [base0] Step=[Reflexivity].
Subtree proved!
Example: The Mac Carthy function shows a more complex case:
Coq < Require Omega.
Coq <
Coq < Variable g:nat->nat->nat.
Coq <
Coq < Axiom g0:(m:nat)(g (0) m)=m.
Coq < Axiom g1:
Coq < (n,m:nat)(gt n (0))->(gt m (100))->
Coq < (g n m)=(g (pred n) (minus m (10))).
Coq < Axiom g2:
Coq < (n,m:nat)(gt n (0))->(le m (100))->(g n m)=(g (S n) (plus m (11))).
Coq < HintRewrite base1 [ g0 LR g1 LR].
Coq < HintRewrite base2 [g2 LR].
Coq <
Coq < Lemma Resg0:(g (1) (90))=(91).
1 subgoal
============================
(g (1) (90))=(91)
Coq < AutoRewrite [base1 base2]
Coq < Step=[Simpl|Reflexivity] with All
Coq < Rest=[Omega] with Cond
Coq < Depth=10.
Warning: 10 rewriting(s) carried out
Warning: 20 rewriting(s) carried out
Subtree proved!
One can also give the full base definition instead of a name. This is
useful to do rewritings with the hypotheses of current goal:
Coq < Show.
1 subgoal
g3 : (m:nat)(g (0) m)=m
g4 : (n,m:nat)
(gt n (0))->(gt m (100))->(g n m)=(g (pred n) (minus m (10)))
g5 : (n,m:nat)
(gt n (0))->(le m (100))->(g n m)=(g (S n) (plus m (11)))
============================
(g (1) (90))=(91)
Coq < AutoRewrite [[g0 LR g1 LR] [g2 LR]]
Coq < Step=[Simpl|Reflexivity] with All
Coq < Rest=[Omega] with Cond
Coq < Depth=10.
Warning: 10 rewriting(s) carried out
Warning: 20 rewriting(s) carried out
Subtree proved!