Accessing Ackermann

(* The Ackermann function is defined by the equations:
 *
 *          n+1             m=0
 * A(m,n) = A(m-1,1)        m>0 n=0
 *          A(m-1,A(m,n-1)) m>0 n>0
 *)

(* It's an example of something not structurally recursive,
 * that means it's going to be a lot of fun to try and define
 * in type theory.
 *)

(* A simple example to look at first is double: *)
Fixpoint double (n : nat) : nat :=
  match n with
    | O => O
    | S m => S (S (double m))
  end.

(* From the definition you can see that every application of double
 * is done with m = S n
 *)

Definition nat_struct n m := m = S n.

(* This is a well founded relation *)

Theorem well_founded_nat_struct : well_founded nat_struct.
  unfold well_founded.
  (* forall a : nat, Acc nat_struct a *)
  Print Acc.
  (* Inductive Acc (A : Type) (R : A -> A -> Prop) (x : A) : Prop :=
         Acc_intro : (forall y : A, R y x -> Acc R y) -> Acc R x
   *)
  (* For some relation to be well founded, every element must be
     accessable
   *)
  induction a.
  (*
     ============================
     Acc nat_struct 0
     
     subgoal 2 is:
     Acc nat_struct (S a)
   *)
  apply Acc_intro; intros.
  discriminate.
  
  apply Acc_intro; intros.
  injection H; intros.
  (*
     a : nat
     IHa : Acc nat_struct a
     y : nat
     H : nat_struct y (S a)
     H0 : a = y
     ============================
     Acc nat_struct y
   *)
  rewrite <- H0; assumption.
Defined.
(* Must used Defined. instead of Qed. here if you want to be
 * able to use the computational properties of any definition
 * given by well_founded_induction on nat_struct
 *)

Definition double' : nat -> nat.
apply (well_founded_induction well_founded_nat_struct).
(*  ============================
   forall x : nat, (forall y : nat, nat_struct y x -> nat) -> nat
 *)
intros x double'.
refine (match x as x' return x = x' -> nat
             (* the trick here ^ is one of many that gives me more
                information about the pattern match than I would get
                normally *)
          with
          | O => fun eq => O
          | S n => fun eq => S (S (double' n _))
                      (* the underscore here ^ is a proof obligation *)
        end (refl_equal x)).
(* x : nat
   double' : forall y : nat, nat_struct y x -> nat
   n : nat
   eq : x = S n
   ============================
   nat_struct n x
*)
unfold nat_struct.
(* x : nat
   double' : forall y : nat, nat_struct y x -> nat
   n : nat
   eq : x = S n
   ============================
   x = S n
 *)
congruence.
Defined.

Print double'.
(*
double' = 
well_founded_induction well_founded_nat_struct (fun _ : nat => nat)
  (fun (x : nat) (double' : forall y : nat, nat_struct y x -> nat) =>
   match x as x' return (x = x' -> nat) with
   | 0 => fun _ : x = 0 => 0
   | S n => fun eq : x = S n => S (S (double' n eq))
   end (refl_equal x))
     : nat -> nat
*)

Eval compute in (double' 6).
(*     = 12
       : nat *)

Extraction double'.
(* let rec double' = function
 *   | O -> O
 *   | S n -> S (S (double' n))
 *)

(* The extraction is very very clean, which is excellent!
 * It's just that one would like to know -why- the extraction
 * doesn't have any 'Acc' or 'well_founded_induction' in it.
 * It's not to do with Prop vs Set or Defined/Qed, the reason is
 *
 * Coq/contrib/extraction/mlutil.ml:

let manual_inline_list = 
  let mp = MPfile (dirpath_of_string "Coq.Init.Wf") in 
  List.map (fun s -> (make_con mp empty_dirpath (mk_label s)))
    [ "well_founded_induction_type"; "well_founded_induction"; 
      "Acc_rect"; "Acc_rec" ; "Acc_iter" ; "Fix" ]
 
 *
 * I wish I knew why this was in here, I can only assume it's
 * some kind of historical artifact, anyway,

Extraction Inline foo bar baz.
 
 * works fine if I were to defined my own Acc type thing.
 *)


(* So now we know _what_ to do, it's just a simple matter of doing it
 * I must define a relation that is Well Founded (and prove that),
 * and is suitable for defining the Ackermann function with
 *)

Definition lt_prod_lt : nat * nat -> nat * nat -> Prop :=
  fun pq mn =>
    let (p,q) := pq in
    let (m,n) := mn in
         p < m
      \/ p = m /\ q < n.

Require Import Omega.

Theorem well_founded_lt_prod_lt : well_founded lt_prod_lt.
  (* ... long ugly proof omitted ... *)
Defined.

Definition Ackermann : nat -> nat -> nat.
intros m n; generalize (m,n); clear m n. (* currying *)
apply (well_founded_induction well_founded_lt_prod_lt).
destruct x as (m,n).
intro Ackermann.
refine
  (match m as m', n as n' return m = m' -> n = n' -> nat with
     | 0,   n   => fun _ _ => S n
     | S m, 0   => fun eq eq' => Ackermann (m, 1) _
     | S m, S n => fun eq eq' => let x := Ackermann (S m, n) _ in Ackermann (m, x) _
   end (refl_equal m) (refl_equal n));
  rewrite eq; rewrite eq'; unfold lt_prod_lt; auto with arith.
Defined.

Eval vm_compute in (Ackermann 3 4).
(*     = 125
 *     : nat *)

Extraction Ackermann.
(*
let ackermann m n =
  let rec f = function
    | Pair (m0, n0) ->
        (match m0 with
           | O -> S n0
           | S m1 ->
               (match n0 with
                  | O -> f (Pair (m1, (S O)))
                  | S n1 -> f (Pair (m1, (f (Pair ((S m1), n1)))))))
  in f (Pair (m, n))
*)

(* Lots of fabulous tupling and untupling,
 * Actually, I don't like that, so I have defined a curried
 * Acc2 and given similar definitions as the Wf does
 *)

Require Import Acc2.

Definition lexi : nat -> nat ->
                  nat -> nat ->
                  Prop :=
  fun p q m n =>
       p < m
    \/ p = m /\ q < n.

Theorem well_founded2_lexi : well_founded2 lexi.
  unfold well_founded2; unfold lexi.
  induction m.
   induction n.
    apply Acc2_intro; intros.
     elimtype False; omega.
    apply Acc2_intro; intros.
    destruct H.
     inversion H.
     destruct H.
     destruct (lt_eq_lt_dec q n). destruct s.
      destruct IHn.
      apply H1.
      right; split; auto.
      rewrite H; rewrite e; apply IHn.
      elimtype False; omega.
   induction n.
    apply Acc2_intro; intros.
    destruct H.
     apply Acc2_intro; intros.
     destruct H0.
      destruct (IHm q).
      apply H1.
       left; omega.
      destruct H0.
      rewrite H0.
      destruct (IHm q).
      apply H2.
      destruct (lt_eq_lt_dec p m). destruct s.
       left; assumption.
       right; split; assumption.
       elimtype False; omega.
      destruct H.
      inversion H0.
     apply Acc2_intro; intros.
     destruct H.
      destruct IHn.
      apply H0.
      left; assumption.
     destruct H.
     destruct (lt_eq_lt_dec q n). destruct s.
      rewrite H.
       destruct IHn.
       apply H1.
       right; split; auto.
      rewrite H; rewrite e; apply IHn.
      elimtype False; omega.
Defined.

Definition Ack2 : nat -> nat -> nat.
apply (well_founded2_induction well_founded2_lexi); intros m n Ack2.
refine
  (match m as m', n as n' return m = m' -> n = n' -> nat with
     | 0,   n   => fun eq eq' => S n
     | S m, 0   => fun eq eq' => Ack2 m 1 _
     | S m, S n => fun eq eq' => let x := Ack2 (S m) n _
                                  in Ack2 m x _
   end (refl_equal m) (refl_equal n));
  unfold lexi; rewrite eq; rewrite eq'.
left; auto.
right; auto.
left; auto.
Defined.

(* One thing I don't like, is having this let x := .. but I don't know
 * how to remove that yet, anyway it doesn't matter much
 *)

Extraction Ack2.
(*
let rec ack2 m n =
  match m with
    | O -> S n
    | S m0 ->
        (match n with
           | O -> ack2 m0 (S O)
           | S n0 -> ack2 m0 (ack2 (S m0) n0))
*)
Extraction Language Haskell.
Extraction Ack2.
(*
ack2 :: Nat -> Nat -> Nat
ack2 m n =
  case m of
    O -> S n
    S m0 -> (case n of
               O -> ack2 m0 (S O)
               S n0 -> ack2 m0 (ack2 (S m0) n0))
*)