% Unprogramming a permutation machine

stack([],[],[]) --> [].
stack([push|Instrs],[I|IS],SS) --> stack(Instrs,IS,[I|SS]).
stack([pop|Instrs],IS,[S|SS]) --> [S], stack(Instrs,IS,SS).

% ?- phrase(stack(Instructions, [1,2,3,4,5], []), [1,2,4,3,5], []).
% Instructions = [push, pop, push, pop, push, push, pop, pop, push, pop] .

Implementing tactics in Coq

Require Import List.

Section propr.
  Variable Sym : Set.
  Variable lookup : Sym -> Prop.
  Variable eq_Sym_dec : forall s s' : Sym, {s = s'} + {s <> s'}.
  
  Inductive prop : Set :=
  | var : Sym -> prop
  | imp : prop -> prop -> prop.
  
  Fixpoint interpret (p : prop) : Prop :=
    match p with
      | var i => lookup i
      | imp p q => interpret p -> interpret q
    end.
  
  Fixpoint assume (context : list Sym) :=
    match context with
      | nil => True
      | i :: is => lookup i /\ assume is
    end.
  
  Fixpoint contextLookup (i : Sym) (context : list Sym) :=
    match context as context' return option (assume context' -> interpret (var i)) with
      | nil => None
      | j::js =>
        match eq_Sym_dec i j with
          | left eql =>
            match eql with
              | refl_equal =>
                Some (fun hypotheses =>
                  match hypotheses with
                    | conj J _ => J
                  end)
            end
          | right _ =>
            match contextLookup i js with
              | Some Prf =>
                Some (fun hypotheses =>
                  match hypotheses with
                    | conj _ Js => Prf Js
                  end)
              | None => None
            end
        end
    end.
  
  Fixpoint proveable' (p : prop) (context : list Sym) : option (assume context -> interpret p) :=
    match p as p' return option (assume context -> interpret p') with
      | var i => contextLookup i context
      | imp (var i) q =>
        match proveable' q (i :: context) with
          | Some Hypo'X => Some (fun Hyp o => Hypo'X (conj o Hyp))
          | None => None
        end
      | imp _ x => None
    end.
  
  Definition some X (x : option X) :=
    match x with
      | Some _ => True
      | None => False
    end.
  Implicit Arguments some [X].
  
  Theorem proveable'_proveable p : some (proveable' p nil) -> interpret p.
    intro p; destruct (proveable' p nil); [ exact i | simpl; tauto ].
  Qed.

End propr.


Require Import Arith.

Theorem test (X Y Z W : Prop) : X -> Y -> Z -> X -> Y -> Z.
intros X Y Z W.
exact
  (proveable'_proveable
    nat
    (fun i =>
      match i with
        | 0 => X
        | 1 => Y
        | 2 => Z
        | 3 => W
        | _ => False
      end)
    eq_nat_dec
    (imp _ (var _ 0)
      (imp _ (var _ 1)
        (imp _ (var _ 2)
          (imp _ (var _ 0)
            (imp _ (var _ 1) (var _ 2))))))
  I).
Qed.

Print test.
(**************

test = 
fun X Y Z W : Prop =>
proveable'_proveable nat
  (fun i : nat =>
   match i with
   | 0 => X
   | 1 => Y
   | 2 => Z
   | 3 => W
   | S (S (S (S _))) => False
   end) eq_nat_dec
  (imp nat (var nat 0)
     (imp nat (var nat 1)
        (imp nat (var nat 2)
           (imp nat (var nat 0) (imp nat (var nat 1) (var nat 2)))))) I
     : forall X Y Z : Prop, Prop -> X -> Y -> Z -> X -> Y -> Z

 ***************)

eq_fin_dec via NoConfusion

Require Import JMeq.
Infix "==" := JMeq (at level 30).
Notation "X =/= Y" := (X == Y -> False) (at level 30).

Inductive Fin : nat -> Set :=
| fz n : Fin (S n)
| fs n : Fin n -> Fin (S n).

Fixpoint Fin_NoConfusion (P : Type) (n : nat) (f f' : Fin n) {struct f} :=
  match f, f' with
    | fz _, fz _ => P -> P
    | fs _ f, fs _ f' => (f == f' -> P) -> P
    | _, _ => P
  end.

Definition Fin_noConfusion P n (f f' : Fin n) : f == f' -> Fin_NoConfusion P n f f'.
intros P n f f' Eq.
elim Eq.
elim f;
  simpl; intros; tauto.
Defined.

Definition fs_injective (P : Type) (n : nat) (f f' : Fin n)
  : (f == f' -> P) -> (fs n f == fs n f' -> P)
  := fun m Eq =>
    Fin_noConfusion P (S n) (fs n f) (fs n f') Eq m.

Definition fz_fs_clash (P : Type) (n : nat) (f : Fin n)
  : fz n == fs n f -> P
  := fun Eq =>
    Fin_noConfusion P (S n) (fz n) (fs n f) Eq.

Definition eq_fin_dec n : forall f f' : Fin n, {f == f'} + {f =/= f'}.
refine (fix eq_fin_dec n (f f' : Fin n) {struct f'} : {f == f'} + {f =/= f'} :=
  match f in Fin n, f' in Fin n' return n = n' -> {f == f'} + {f =/= f'} with
    | fz _, fz _ => _
    | fs _ _, fz _ => _
    | fz _, fs _ _ => _
    | fs _ _, fs _ _ => _
  end (refl_equal _));
intro Eq; injection Eq; clear Eq; intro Eq.

left; rewrite Eq; reflexivity.

right; rewrite Eq; intro; exact (fz_fs_clash False _ _ H).

right; rewrite <- Eq; intro; exact (fz_fs_clash False _ _ (sym_JMeq H)).

clear f f' n; subst n0.
destruct (eq_fin_dec n1 f0 f1).
left; elim j; reflexivity.
right; intro; apply f; exact (fs_injective _ _ _ _ (fun Eq => Eq) H).
Defined.

A different approach

Just typing out stuff from http://www.cs.nott.ac.uk/~pwm/ .

module Universe where

open import Data.Nat

data SPT : ℕ -> Set1 where
 vz : {n : ℕ} -> SPT (suc n)
 vs : {n : ℕ} -> SPT n -> SPT (suc n)
 _[_] : {n : ℕ} -> SPT (suc n) -> SPT n -> SPT n
 “0” : {n : ℕ} -> SPT n
 “1” : {n : ℕ} -> SPT n
 _“+”_ : {n : ℕ} -> SPT n -> SPT n -> SPT n
 _“×”_ : {n : ℕ} -> SPT n -> SPT n -> SPT n
 _“->”_ : {n : ℕ} -> (K : Set) -> SPT n -> SPT n
 “μ”_ : {n : ℕ} -> SPT (suc n) -> SPT n

data Tel : ℕ -> (ℕ -> Set1) -> Set2 where
 ε : (F : ℕ -> Set1) -> Tel zero F
 _^_ : {F : ℕ -> Set1} -> {n : ℕ} -> F n -> Tel n F -> Tel (suc n) F

data ⟦_⟧_ : {n : ℕ} -> SPT n -> Tel n SPT -> Set2 where
 top : {n : ℕ} -> {T' : Tel n SPT} -> {T : SPT n} ->
   ⟦ T ⟧ T' -> ⟦ vz ⟧ (T ^ T')
 pop : {n : ℕ} -> {T' : Tel n SPT} -> {S T : SPT n} ->
   ⟦ T ⟧ T' -> ⟦ vs T ⟧ (S ^ T')
 def : {n : ℕ} -> {T' : Tel n SPT} -> {A : SPT n} -> {F : SPT (suc n)} ->
   ⟦ F ⟧ (A ^ T') -> ⟦  F [ A ]  ⟧ T'
 void : {n : ℕ} -> {T' : Tel n SPT} ->
   ⟦ “1” ⟧ T'
 inl : {n : ℕ} -> {T' : Tel n SPT} -> {S T : SPT n} ->
   ⟦ S ⟧ T' -> ⟦ S “+” T ⟧ T'
 inr : {n : ℕ} -> {T' : Tel n SPT} -> {S T : SPT n} ->
   ⟦ T ⟧ T' -> ⟦ S “+” T ⟧ T'
 pair : {n : ℕ} -> {T' : Tel n SPT} -> {S T : SPT n} ->
   ⟦ S ⟧ T' -> ⟦ T ⟧ T' -> ⟦ S “×” T ⟧ T'
 funk : {n : ℕ} -> {T' : Tel n SPT} -> {K : Set} -> {T : SPT n} ->
  (f : K -> ⟦ T ⟧ T') -> ⟦ (K “->” T) ⟧ T'
 miso : {n : ℕ} -> {T' : Tel n SPT} -> {F : SPT (suc n)} ->
   ⟦ F ⟧ ((“μ” F) ^ T') -> ⟦ (“μ” F) ⟧ T'



“Nat” : {n : ℕ} -> SPT n
“Nat” = “μ” (“1” “+” vz)

“zero” : {n : ℕ} -> {T' : Tel n SPT} -> ⟦ “Nat” ⟧ T'
“zero” = miso (inl (void))

“succ” : {n : ℕ} -> {T' : Tel n SPT} -> ⟦ “Nat” ⟧ T' -> ⟦ “Nat” ⟧ T'
“succ” x = miso (inr (top x))


data “Nat”-View : {n : ℕ} -> {T' : Tel n SPT} -> ⟦ “Nat” ⟧ T' -> Set2 where
 isZero : {n : ℕ} -> {T' : Tel n SPT} -> “Nat”-View {n} {T'} “zero”
 isSucc : {n : ℕ} -> {T' : Tel n SPT} -> (x : ⟦ “Nat” ⟧ T') -> “Nat”-View {n} {T'} (“succ” x)

viewNat : {n : ℕ} -> {T' : Tel n SPT} -> (n : ⟦ “Nat” ⟧ T') -> “Nat”-View n
viewNat {n} {T'} (miso Q) = aux1 Q
 where aux3 : (r : ⟦ vz ⟧ ((“μ” (“1” “+” vz)) ^ T')) -> “Nat”-View (miso (inr r))
       aux3 (top x) = isSucc x
       aux2 : (l : ⟦ “1” ⟧ ((“μ” (“1” “+” vz)) ^ T')) -> “Nat”-View (miso (inl l))
       aux2 void = isZero
       aux1 : (u : ⟦ “1” “+” vz ⟧ ((“μ” (“1” “+” vz)) ^ T')) -> “Nat”-View (miso u)
       aux1 (inl U) = aux2 U
       aux1 (inr V) = aux3 V

“add” : {n : ℕ} -> {T' : Tel n SPT} -> ⟦ “Nat” ⟧ T' -> ⟦ “Nat” ⟧ T' -> ⟦ “Nat” ⟧ T'
“add” x y with viewNat x
“add” (miso (inl (void))) y | isZero = y
“add” (miso (inr (top x))) y | isSucc .x = “succ” (“add” x y)


test = “add” {zero} {ε SPT}
         (“succ” (“succ” (“succ” “zero”)))
         (“succ” (“succ” “zero”))

{- =
miso
(inr
 (top
  (miso
   (inr
    (top
     (miso
      (inr
       (top
        (miso (inr (top (miso (inr (top (miso (inl void)))))))))))))))) -}

Emulate Agda style pattern matching in Coq using ideas frow Eliminating Dependent Pattern Matching..

Require Import JMeq.
Infix "==" := JMeq (at level 31).
Notation "[ x : X ]  == [ y : Y ]" := (@JMeq X x Y y) (at level 30).
Notation "X =/= Y" := (JMeq _ X _ Y -> False) (at level 30).


Derive NoConfusion nat.
Definition noConfusion_nat (P : Type) (u v : nat) : JMeq u v -> NoConfusion_nat P u v.
intros.
elim H.
elim u;
  simpl; intros; tauto.
Defined.


Inductive SPT : nat -> Type :=
| vz {n} : SPT (S n)
| vs {n} : SPT n -> SPT (S n)
| of {n} : SPT (S n) -> SPT n -> SPT n
| q_zero_q {n} : SPT n
| q_one_q {n} : SPT n
| q_sum_q {n} : SPT n -> SPT n -> SPT n
| q_mul_q {n} : SPT n -> SPT n -> SPT n
| q_arrow_q {n} : Type -> SPT n -> SPT n
| q_mu_q {n} : SPT (S n) -> SPT n.
Derive NoConfusion SPT.
Definition noConfusion_SPT (P : Type) (e1 : nat) (u v : SPT e1) : JMeq u v -> NoConfusion_SPT P e1 u v.
intros.
elim H.
elim u;
  simpl; intros; tauto.
Defined.



Inductive Tel : nat -> (nat -> Type) -> Type :=
| eps : forall {F}, Tel 0 F
| telCons : forall {F} {n}, Tel n F -> F n -> Tel (S n) F.
Infix ";" := telCons (at level 27, left associativity).
Derive NoConfusion Tel.
Definition noConfusion_Tel (P : Type) (e1 : nat) (e2 : nat -> Type) (u v : Tel e1 e2) : JMeq u v -> NoConfusion_Tel P e1 e2 u v.
intros.
elim H.
elim u;
  simpl; intros; tauto.
Defined.



Reserved Notation "⟦  type ⟧ scope" (at level 30, no associativity).
Inductive Interpretation : forall n, SPT n -> Tel n SPT -> Type :=
| top {n} {T' : Tel n SPT} {T : SPT n}
  : ⟦ T ⟧ T' -> ⟦ vz ⟧ (T';T)
| pop {n} {T' : Tel n SPT} {S T : SPT n}
  : ⟦ T ⟧ T' -> ⟦ vs T ⟧ (T';S)
| def {n} {T' : Tel n SPT} {A : SPT n} {F : SPT (S n)}
  : ⟦ F ⟧ (T'; A) -> ⟦ of F A ⟧ T'
| void {n} {T' : Tel n SPT}
  : ⟦ q_one_q ⟧ T'
| inl {n} {T' : Tel n SPT} {S T : SPT n}
  : ⟦ S ⟧ T' -> ⟦ q_sum_q S T ⟧ T'
| inr {n} {T' : Tel n SPT} {S T : SPT n}
  : ⟦ T ⟧ T' -> ⟦ q_sum_q S T ⟧ T'
| pair {n} {T' : Tel n SPT} {S T : SPT n}
  : ⟦ S ⟧ T' -> ⟦ T ⟧ T' -> ⟦ q_mul_q S T ⟧ T'
| funk {n} {T' : Tel n SPT} {K : Type} {T : SPT n}
  : (K -> ⟦ T ⟧ T') -> ⟦ q_arrow_q K T ⟧ T'
| miso {n} {T' : Tel n SPT} {F : SPT (S n)}
  : ⟦ F ⟧ (T';q_mu_q F) -> ⟦ q_mu_q F ⟧ T'
where "⟦  type ⟧ scope" := (Interpretation _ type scope).
Derive NoConfusion Interpretation.
Definition noConfusion_Interpretation (P : Type) (e1 : nat) (e2 : SPT e1) (e3 : Tel e1 SPT) (u v : ⟦e2 ⟧ e3) : JMeq u v -> NoConfusion_Interpretation P e1 e2 e3 u v.
intros.
elim H.
elim u;
  simpl; intros; tauto.
Defined.



Definition mu_injective (P : Type) (e1 : nat) (u v : SPT (S e1))
  : (e1 == e1 -> u == v -> P) -> (q_mu_q u == q_mu_q v -> P)
  := fun m Eq =>
    noConfusion_SPT P _ (q_mu_q u) (q_mu_q v) Eq m.

Definition mu_vz_clash (P : Type) (n : nat) (F : SPT (S (S n)))
  : q_mu_q F == vz -> P
  := fun Eq =>
    noConfusion_SPT P (S n) (q_mu_q F) vz Eq.



Definition q_Nat_q {n} : SPT n := q_mu_q (q_sum_q q_one_q vz).
Definition q_O_q {n} {T' : Tel n SPT} : ⟦ q_Nat_q ⟧ T' := miso (inl void).
Definition q_S_q {n} {T' : Tel n SPT} : ⟦ q_Nat_q ⟧ T' -> ⟦ q_Nat_q ⟧ T' := fun x => miso (inr (top x)).

Inductive q_Nat_q'View {n} {T' : Tel n SPT} : ⟦ q_Nat_q ⟧ T' -> Type :=
| isO : q_Nat_q'View q_O_q
| isS : forall x : ⟦ q_Nat_q ⟧ T', q_Nat_q'View (q_S_q x).



Ltac dpm_lift := repeat match goal with H : _ |- _ => intro Eq; revert H; revert Eq end.
Ltac dpm_prepare :=
  match goal with
    | |- @JMeq _ ?x _ ?x -> _ => intros _; dpm_prepare
    | |- @JMeq _ _ _ _ -> _ => dpm_lift
    | _ => intro; dpm_prepare
  end.

Ltac dpm_subst := intro Eql;
  match type of Eql with @JMeq _ ?x _ ?y =>
    (rewrite Eql; clear x Eql) || (rewrite <- Eql; clear y Eql)
  end.

Ltac dpm_confusion := intro Eql;
  match goal with |- ?P =>
    apply (noConfusion_nat P _ _ Eql)||
    apply (noConfusion_SPT P _ _ _ Eql)||
    apply (noConfusion_Tel P _ _ _ _ Eql)||
    apply (noConfusion_Interpretation P _ _ _ _ _ Eql)
  end.

Ltac dpm_specialize := repeat (dpm_prepare; (dpm_subst||dpm_confusion)).



Definition view'q_Nat_q
  (n : nat) (Ts : Tel n SPT) (x : ⟦ q_Nat_q ⟧ Ts) : (@q_Nat_q'View n Ts x).
intros.

refine
  (Interpretation_rect
    (fun n' S' Ts' x' =>
      n == n' -> @q_Nat_q n == S' -> Ts == Ts' -> x == x' ->
      q_Nat_q'View x)
    _ _ _ _ _ _ _ _ _
               n               q_Nat_q                Ts             x
    (JMeq_refl n) (JMeq_refl (@q_Nat_q n)) (JMeq_refl Ts) (JMeq_refl x));
unfold q_Nat_q in *;
dpm_specialize;
intros _.

refine
  (Interpretation_rect
    (fun n0' S' Ts' i' =>
      S n0 == n0' -> q_sum_q q_one_q vz == S' -> T'; q_mu_q (q_sum_q q_one_q vz) == Ts' -> i == i' ->
      q_Nat_q'View (miso i))
    _ _ _ _ _ _ _ _ _
    (S n0) (q_sum_q q_one_q vz) (T'; q_mu_q (q_sum_q q_one_q vz)) i
    (JMeq_refl (S n0)) (JMeq_refl (q_sum_q q_one_q vz)) (JMeq_refl (T'; q_mu_q (q_sum_q q_one_q vz))) (JMeq_refl i));
dpm_specialize;
intros _.

refine
  (Interpretation_rect
    (fun n0' S' Ts' i0' =>
      S n0 == n0' -> q_one_q == S' -> (T'; q_mu_q (q_sum_q q_one_q vz)) == Ts' -> i0 == i0' ->
      q_Nat_q'View (miso (inl i0)))
    _ _ _ _ _ _ _ _ _
    (S n0) q_one_q (T'; q_mu_q (q_sum_q q_one_q vz)) i0
    (JMeq_refl (S n0)) (JMeq_refl (q_one_q)) (JMeq_refl (T'; q_mu_q (q_sum_q q_one_q vz))) (JMeq_refl i0));
dpm_specialize.

exact isO.

refine
  (Interpretation_rect
    (fun n0' S' Ts' i0' =>
      S n0 == n0' -> vz == S' -> (T'; q_mu_q (q_sum_q q_one_q vz)) == Ts' -> i0 == i0' ->
      q_Nat_q'View (miso (inr i0)))
    _ _ _ _ _ _ _ _ _
    (S n0) vz (T'; q_mu_q (q_sum_q q_one_q vz)) i0
    (JMeq_refl (S n0)) (JMeq_refl vz) (JMeq_refl (T'; q_mu_q (q_sum_q q_one_q vz))) (JMeq_refl i0));
dpm_specialize;
intros _.

exact (isS i).

Defined.

Semigroup/Group proof

Definition associativity (T : Set) (o : T -> T -> T) :=
  forall x y z, (o (o x y) z) = (o x (o y z)).

Record Semigroup : Type := makeSemigroup {
  T : Set;
  o : T -> T -> T;
  assoc : associativity T o
}.

Record Group : Type := makeGroup {
  T' : Set;
  o' : T' -> T' -> T';
  assoc' : associativity T' o';
  I : T';
  unit' : forall u : T', exists v, o' u v = I
}.

(* Any semigroup S with a right unit, and right inverse forall a in
   S is a group *)

Theorem ex10
  (S : Semigroup)
  (right_unit : T S)
  (right_unit_meaning : forall a, (o S) a right_unit = a)
  (right_inverse : forall a, exists b, (o S) a b = right_unit)
: (* --------------------------------------------------------- *)
  exists I : T S,
    forall u : T S, exists v, (o S) u v = I.

intros.
exists right_unit.

intro.

destruct (right_inverse u).
exists x.

assumption.
Qed.

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