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))
*)

Fin is injective

Inductive Fin : nat -> Set :=
| fz : forall n, Fin (S n)
| fs : forall n, Fin n -> Fin (S n).
Implicit Arguments fz [n].
Implicit Arguments fs [n].
(* Fin is the family of finite types
 * Fin n is the type with 'n' distinct elements
 * Fin 0 ~ void
 * Fin 1 ~ unit
 * Fin 2 ~ bool
 *)

Inductive sumdys (A:Prop) (B:Type) : Type :=
| dyleft : A -> sumdys A B
| dyright : B -> sumdys A B.
(* Just because I prefer the Prop case to come first *)

Definition fz_or_fs n (f : Fin (S n)) : sumdys (f = fz) { f' | f = fs f' }.
intros; set (P n :=
  match n return Fin n -> Set with
    | O => fun _ => unit
    | S n => fun f => sumdys (f = fz) { f' | f = fs f' }
  end).

change (P (S n) f);
  destruct f;
    [ left; reflexivity |
      right; exists f; reflexivity ].
Defined.
Implicit Arguments fz_or_fs [n].

Lemma no_fin0 : Fin 0 -> forall P, P.
  intros f; refine
    match f in Fin n' return
      match n' with
        | O => forall P, P
        | S _ => True
      end
      with
      | fz _ => I
      | fs _ _ => I
    end.
Qed.

(* Destruct a fin down one level *)
Ltac fin_case f :=
  destruct (fz_or_fs f);
    match goal with
      | eq : f = fz |- _ =>
        try (rewrite eq in *; clear eq)
      | Ex : { f' | f = fs f' } |- _ =>
        destruct Ex;
          match goal with
            | eq : f = fs ?f' |- _ =>
              try (rewrite eq in *; clear eq)
          end end.

(* Smash a Fin to bits *)
Ltac destruct_fin f :=
  destruct (fz_or_fs f);
    match goal with
      | eq : f = fz |- _ =>
        try (rewrite eq in *; clear eq)
      | Ex : { f' | f = fs f' } |- _ =>
        destruct Ex;
          match goal with
            | eq : f = fs ?f' |- _ =>
              try (rewrite eq in *; clear eq);
                match type of f' with
                  | Fin 0 => apply (no_fin0 f')
                  | Fin (S _) => destruct_fin f'
                end end end.

Lemma one_fin1 : forall f : Fin 1, f = fz.
  intro f; destruct_fin f; reflexivity.
Qed.

Lemma two_fin2 : forall f : Fin 2, f = fz \/ f = fs fz.
  intro f; destruct_fin f; auto.
Qed.

Definition squish n : Fin (S (S n)) -> Fin (S n) :=
  fun f => match fz_or_fs f with
             | dyleft _ => fz
             | dyright (exist f _) => f
           end.
Implicit Arguments squish [n].
(* squish pushes down on the Fin *)

Fixpoint bump n (f : Fin n) : Fin (S n) :=
  match f with
    | fz _ => fz
    | fs _ f => fs (bump _ f)
  end.
Implicit Arguments bump [n].
(* bump lifts the family a Fin resides in *)

Fixpoint scum n : Fin (S n) :=
  match n with
    | O => fz
    | S n => fs (scum n)
  end.
Implicit Arguments scum [n].
(* scum always floats at the top *)


Lemma fs_injective n (x y : Fin n) : fs x = fs y -> x = y.
  intros; destruct n.
  apply (no_fin0 x).
  change (squish (fs x) = squish (fs y)); congruence.
Qed.
Implicit Arguments fs_injective [n x y].

Lemma bump_isn't_scum n (f : Fin n) : bump f <> scum.
  induction f.
  discriminate.
  contradict IHf.
  simpl in IHf; rewrite (fs_injective IHf).
  reflexivity.
Qed.

Lemma bump_injection n : forall u v : Fin n, bump u = bump v -> u = v.
  intros; induction n.
  apply (no_fin0 u).
  fin_case u; fin_case v.
  reflexivity.
  discriminate.
  discriminate.
  rewrite (IHn _ _ (fs_injective H)).
  reflexivity.
Qed.

Definition fin_eq_dec n (x y : Fin n) : {x = y} + {x <> y}.
intros; induction n.
apply (no_fin0 x).
fin_case x; fin_case y.
left; reflexivity.
right; discriminate.
right; discriminate.
destruct (IHn x0 x1).
left; congruence.
right; contradict n0; pose (fs_injective n0); congruence.
Defined.
Implicit Arguments fin_eq_dec [n].


(* thinning a Fin either lifts it or leaves it where it was,
 * depending on if it was above or below the wedge.
 *)
Definition thin n (wedge : Fin (S n)) : Fin n -> Fin (S n).
induction n.
refine (fun _ e => no_fin0 e _).
refine (fun wedge e =>
  match fz_or_fs wedge with
    | dyleft _ => fs e
    | dyright (exist wedge' _) =>
      match fz_or_fs e with
        | dyleft _ => fz
        | dyright (exist e' _) => fs (IHn wedge' e')
      end
  end).
Defined.

(* thickening a Fin squashes down around a pivot, this is
 * a partial inverse of thin, which will be proven soon.
 *)
Definition thicken n (wedge e : Fin (S n)) : option (Fin n).
induction n.
refine (fun _ _ => None).
refine (fun wedge e =>
  match fz_or_fs wedge with
    | dyleft _ =>
      match fz_or_fs e with
        | dyleft _ => None
        | dyright (exist e' _) => Some e'
      end
    | dyright (exist wedge' _) =>
      match fz_or_fs e with
        | dyleft _ => Some fz
        | dyright (exist e' _) =>
          match IHn wedge' e' with
            | Some e' => Some (fs e')
            | None => None
          end
      end
  end).
Defined.

Theorem thin_injective n o x y : thin n o x = thin n o y -> x = y.
  intros; induction n.
  apply (no_fin0 x).
  fin_case x; fin_case y.
  reflexivity.
  fin_case o; inversion H.
  fin_case o; inversion H.
  destruct n.
  apply (no_fin0 x0).
  fin_case o; rewrite (IHn fz x0 x1); try reflexivity; simpl.
  rewrite (fs_injective H); reflexivity.
  rewrite (IHn _ _ _ (fs_injective H)); reflexivity.
Qed.

Theorem thin_mutate n o e : thin n o e <> o.
  intros; induction n.
  apply (no_fin0 e).
  fin_case o.
  discriminate.
  fin_case e.
  discriminate.
  pose (IHn x x0).
  simpl; contradict n0.
  exact (fs_injective n0).
Qed.

Theorem thin_image n o e : o <> e -> exists e', thin n o e' = e.
  intros; induction n.
  destruct_fin o; destruct_fin e.
  absurd (@fz 1 = fz); auto.
  fin_case o.
  fin_case e.
  absurd (@fz 1 = fz); auto.
  exists x; reflexivity.
  fin_case e.
  exists fz; reflexivity.
  destruct (IHn x x0).
  contradict H; congruence.
  exists (fs x1); simpl; congruence.
Qed.

Theorem thicken_inversion n o e r : thicken n o e = r ->
  (e = o /\ r = None) + { e' | e = thin n o e' /\ r = Some e' }.
  intros; induction n.
  destruct_fin o; destruct_fin e; left; auto.
  fin_case o.
  
  fin_case e.
  left; auto.
  right; exists x; auto.
  
  fin_case e.
  right; exists fz; auto.
  
  destruct r.
  simpl in H.
  case_eq (thicken n x x0).
  intros f' eq.
  rewrite eq in *.
  injection H; clear H; intro H; rewrite <- H in *; clear H.
  destruct (IHn _ _ _ eq).
  destruct a.
  inversion H0.
  destruct s.
  destruct a.
  injection H0; clear H0; intro H0; rewrite <- H0 in *; clear H0.
  right; exists (fs f'); intuition.
  simpl; congruence.
  intro eq; rewrite eq in H; inversion H.
  
  left; intuition.
  destruct (IHn x x0 None).
  simpl in H.
  destruct (thicken n x x0); auto.
  inversion H.
  destruct a; congruence.
  destruct s.
  destruct a.
  inversion H1.
Qed.
(* Why is the proof long? *)


Definition thicken' n (wedge e : Fin (S n)) : wedge <> e -> Fin n.
intros.
pose (thicken n wedge e).
destruct (thicken_inversion n wedge e o (refl_equal _)).
destruct a; absurd (wedge = e); auto.
destruct s.
exact x.
Defined.

Lemma thick_and_thin n o e ne : e = thin n o (thicken' n o e ne).
  intros; unfold thicken'.
  set (k := thicken_inversion _ _ _ (thicken n o e) (refl_equal _)).
  destruct k.
  elimtype False; destruct a; absurd (e = o); auto.
  destruct s.
  destruct a.
  assumption.
Qed.



Require Import List.

Inductive AllDifferent A : list A -> Prop :=
| nil'  :
  AllDifferent A nil
| cons' : forall x xs,
  AllDifferent A xs -> ~In x xs -> AllDifferent A (x :: xs).
Implicit Arguments AllDifferent [A].

Lemma AllDifferent_injection A B (f : A -> B) x : (forall u v, f u = f v -> u = v) -> AllDifferent x -> AllDifferent (map f x).
  intros; induction x; simpl.
  apply nil'.
  apply cons'; inversion H0.
  apply IHx; assumption.
  contradict H4.
  destruct (in_map_iff f x (f a)).
  destruct (H5 H4).
  destruct H7.
  rewrite <- (H _ _ H7).
  assumption.
Qed.


Lemma In_P_reduce X (P : X -> Prop) o xs :
  (forall x : X, In x (o :: xs) -> P x) ->
   forall x : X, In x xs -> P x.
  intros.
  apply H.
  right.
  assumption.
Qed.

Definition map' X Y (P : X -> Prop) (f : forall x : X, P x -> Y) :
  forall xs : list X, (forall x, In x xs -> P x) -> list Y.
fix 5.
intros X Y P f xs P'.
destruct xs.
exact nil.
refine (f x (P' _ _) :: map' _ _ _ f xs (In_P_reduce _ _ _ _ P')).
left; reflexivity.
Defined.

Theorem map'_length X Y P f xs O : length xs = length (map' X Y P f xs O).
  intros; induction xs.
  reflexivity.
  simpl; rewrite (IHxs (In_P_reduce _ _ _ _ O)).
  reflexivity.
Qed.


Lemma thicken_In_inj n o a x H H' :
  In (thicken' n o a H)
     (map' _ _ (fun e => o <> e) (thicken' n o) x H') ->
  In a x.
  intros; induction x.
  inversion H0.
  simpl in H0.
  destruct H0.
  left.
  rewrite (thick_and_thin _ o a H).
  rewrite (thick_and_thin _ o a0 (H' a0 (or_introl (In a0 x) (refl_equal a0)))).
  rewrite H0.
  reflexivity.
  right.
  eapply IHx.
  apply H0.
Qed.

Lemma saturation n : forall x : list (Fin n),
  AllDifferent x -> length x = n -> forall f, In f x.
  intros; induction n.
  apply (no_fin0 f).
  destruct x.
  inversion H0.
  destruct (fin_eq_dec f f0).
  left; congruence.
  right.
  injection H0; clear H0; intro H0.
  inversion H.
  clear H1 H2 x0 xs.
  
  assert (forall e, In e x -> f0 <> e).
  intros; contradict H4; congruence.
  pose (map' _ _ _ (thicken' _ f0) x H1).
  
  Lemma AllDifferent_map'_thicken' n o x (H : (forall e, In e x -> o <> e)) :
    AllDifferent x ->
    (AllDifferent
      (map' _ _
        (fun e => o <> e)
        (thicken' n o) x
        H)).
    intros; induction x.
    apply nil'.
    simpl; apply cons'; inversion H0.
    apply IHx; assumption.
    contradict H4.
    eapply thicken_In_inj.
    apply H4.
  Qed.
  pose (AllDifferent_map'_thicken' _ _ _ H1 H3).
  
  assert (length l = n).
  rewrite <- H0.
  rewrite (map'_length _ _ _ (thicken' n f0) x H1).
  reflexivity.
  
  pose (IHn _ a H2).
  pose (i (thicken' _ f f0 n0)).
  assert (f0 <> f).
  auto.
  pose (thicken_In_inj _ f0 f x H5 H1).
  apply i1.
  apply i.
Qed.

Definition Cardinality : nat -> Set -> Prop :=
  fun n A => exists l : list A, length l = n /\ AllDifferent l.

Theorem pigeonhole_principle m : ~ Cardinality (S m) (Fin m).
  unfold Cardinality.
  intros; intro.
  destruct H; destruct H.
  destruct x.
  inversion H.
  case (In_dec (@fin_eq_dec _) f x); inversion H0.
  contradiction.
  injection H; intro H'.
  pose (saturation _ x H3 H' f).
  contradiction.
Qed.

Theorem Cardinality_n_Fin_n n : Cardinality n (Fin n).
  induction n.
  
  exists nil; split; [ reflexivity | apply nil'].
  
  destruct IHn.
  destruct H.
  exists (scum :: map (@bump _) x); split.
  
  simpl.
  rewrite map_length.
  congruence.
  
  apply cons'.
  apply AllDifferent_injection.
  apply bump_injection.
  assumption.
  clear H H0.
  induction x.
  auto.
  contradict IHx.
  inversion IHx.
  absurd (bump a = scum); auto.
  apply bump_isn't_scum.
  apply H.
Qed.

Theorem not_gt_Cardinality_n_Fin_m n m : n > m -> ~Cardinality n (Fin m).
  intros.
  
  Lemma lt_diff n m : n > m -> exists d, n = S d + m.
    unfold gt; unfold lt.
    intros n m H; induction H.
    exists 0; reflexivity.
    destruct IHle.
    exists (S x).
    rewrite H0.
    reflexivity.
  Qed.
  destruct (lt_diff n m); auto.
  rewrite H0; clear H0 H n.
  induction x.
  
  exact (pigeonhole_principle m).
  
  contradict IHx.
  destruct IHx.
  destruct H.
  inversion H0.
  rewrite <- H1 in H; inversion H.
  exists xs; split; auto.
  rewrite <- H3 in H; injection H.
  auto.
Qed.
(* Another triumph of the pigeonhole principle *)

Require Import Arith.
Theorem fin_different n m : n <> m -> Fin n <> Fin m.
  intros n m ne; intro H.
  destruct (not_eq _ _ ne);
    [ pose (Cardinality_n_Fin_n m) as p; rewrite <- H in p |
      pose (Cardinality_n_Fin_n n) as p; rewrite    H in p ];
    eapply not_gt_Cardinality_n_Fin_m;
      try apply p; auto with arith.
Qed.

Theorem fin_injective n m : Fin n = Fin m -> n = m.
  intros; destruct (eq_nat_dec n m).
  assumption.
  pose (fin_different _ _ n0); contradiction.
Qed.

cycle = concat . repeat = fix . (++)

It's annoying that I don't know how to write this totally point free.

(1)
concat . repeat
 { repeat = fix . (:) }
concat . fix . (:)
 { eta }
\x -> (concat . fix . (:)) x
 { compute }
\x -> concat (fix ((:) x))
 { f (fix g) = fix h <= f . g = h . f }
 { concat . ((:) x) = ((++) x) . concat } <- (2)
\x -> fix ((++) x)
 { eta }
fix . (++)

(2)
concat . ((:) x)
 { concat = foldr (++) [] }
foldr (++) [] . ((:) x)
 { eta }
\xs -> (foldr (++) [] . ((:) x)) xs
 { compute }
\xs -> foldr (++) [] (x:xs)
 { compute }
\xs -> x ++ (foldr (++) [] xs)
 { eta }
((++) x) . foldr (++) []
 { concat = foldr (++) [] }
((++) x) . concat