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

*)

## Saturday, 20 September 2008

### Accessing Ackermann

Labels:
Ackermann,
Coq,
Extraction,
Induction,
Well Founded Relation

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

(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

Subscribe to:
Posts (Atom)