Inductive Ack  : nat->nat->nat->Prop :=
      AckO : forall n:nat ,(Ack O n (S n))
    | AcknO : forall n m:nat ,(Ack n (S O) m)->(Ack (S n) O m)
    | AckSS : forall n m p q:nat ,
               (Ack (S n) m q)->(Ack n q p)->(Ack (S n) (S m) p).

Hint Constructors Ack.

Require Export Arith.

Lemma inv:forall n m, (Ack (S n) 0 m)->(Ack n (S 0) m).
intros.
inversion H.
assumption.
Qed.

Lemma prev1: forall p,(Ack 0 0 p)-> p=1.
intros p H.
inversion H.
auto.
Qed.

Lemma prev2:forall p n, (Ack 0 n p)->p= S n.
intros p n H.
inversion H;auto.
Qed.


Theorem ack: forall n m:nat,{p:nat | (Ack n m p)}.
Proof.
induction n; induction m.
 split with 1; auto.
 split with (S (S m));auto.
  
 case (IHn 1); intros.
   split with x; auto.
   
 case IHm; intros.
   case (IHn x); intros.
   split with x0;auto.
   apply (AckSS n m x0 x); auto.
Defined.



Definition pr1 (A : Set) (P : A -> Prop) (H : {x : A | P x}) :=
  let (a, p) := H in a.
Implicit Arguments pr1 [A].
Hint Rewrite pr1:mio.
Lemma proy:forall (A : Set) (P : A -> Prop) (H : {x : A | P x})  ,
pr1  P (let (a,p):=H in (exist (fun x:A=> P x) a p)) = pr1 P H.
intros.
case H;intros;auto.
Qed.
Hint Rewrite proy:mio.
Definition pr2 (A : Set) (P : A -> Prop) (H : {x : A | P x}) :=
  let (a, p) return (P (pr1 P H)) := H in p.
Implicit Arguments pr2 [A].
Hint Rewrite pr2:mio.




Definition ackm (n m:nat):=let P:= (Ack n m) in (pr1 P (ack n m)).


Lemma cumple:forall n m, (Ack n m (ackm n m)).
intros.
exact (pr2 (Ack n m) (ack n m)).
Qed.

 Eval compute in (ackm 1 3).

Extraction "/home/freire/md2/c08-09/ackerman" ack.