(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.3                                 *)
(*                               July 1st 1999                              *)
(*                                                                          *)
(****************************************************************************)
(*                            DemoAutoRewrite.v                             *)
(****************************************************************************)
(* $Id: DemoAutoRewrite.v,v 1.1 1999/06/30 10:57:48 loiseleu Exp $ *)

(* 1. The Ackerman function *)

Require Arith.

Variable Ack:nat->nat->nat.

Axiom Ack0:(m:nat)(Ack (0) m)=(S m).
Axiom Ack1:(n:nat)(Ack (S n) (0))=(Ack n (1)).
Axiom Ack2:(n,m:nat)(Ack (S n) (S m))=(Ack n (Ack (S n) m)).

HintRewrite base0 [ Ack0 LR 
                Ack1 LR
                Ack2 LR].

Lemma ResAck0:(Ack (2) (1))=(5).
AutoRewrite [base0] Step=[Reflexivity].

(* 2. More complex: the MacCarthy function *)
Require Omega.

Parameter g:nat->nat->nat.

Axiom g0:(m:nat)(g (0) m)=m.
Axiom g1:
  (n,m:nat)(gt n (0))->(gt m (100))->
  (g n m)=(g (pred n) (minus m (10))).
Axiom g2:
  (n,m:nat)(gt n (0))->(le m (100))->(g n m)=(g (S n) (plus m (11))).
HintRewrite base1 [g0 LR g1 LR].
HintRewrite base2 [g2 LR].
Lemma Resg0:(g (1) (90))=(91).
AutoRewrite [base1 base2] 
  Step=[Simpl|Reflexivity] with All
  Rest=[Omega] with Cond 
  Depth=10.
Save.

Reset g.
Parameter g: Z->Z->Z.
Lemma maccarthy_90 : 
  (g0:(m:Z)`(g 0 m)=m`)
  (g1:(n,m:Z)`n > 0`->`m > 100`->`(g n m)=(g (Zpred n) (m - 10))`)
  (g2:(n,m:Z)`n > 0`->`m <= 100`->`(g n m)=(g (Zs n) (m + 11))`)
  `(g 1 90)=91`.
  Intros.
  AutoRewrite [[g0 LR g1 LR] [g2 LR]] 
  Step=[Simpl|Reflexivity] with All
  Rest=[Omega] with Cond 
  Depth=10.
Save.
