## Saturday, 20 September 2008

### 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 -> Natack2 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))*)`

## Wednesday, 17 September 2008

### 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.`

## Saturday, 6 September 2008

### 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