## Tuesday, 27 October 2009

### Cantors Diagonalization Proof in Coq

`Axiom b : (nat -> nat) -> nat.Axiom b' : nat -> (nat -> nat).Axiom bijection : forall f, b' (b f) = f.Axiom bijection' : forall x, b (b' x) = x.Definition Stream A := nat -> A.Definition Map {A B} (f : A -> B) : Stream A -> Stream B :=  fun sa =>    fun i =>      f (sa i).Definition l : Stream (nat -> nat) -> Stream nat :=  Map b.Definition l' : Stream nat -> Stream (nat -> nat) :=  Map b'.Definition isnt x :=  match x with    | O => S O    | S _ => O  end.Theorem isn't_isnt {x} : isnt x <> x.  destruct x; discriminate.Qed.Definition Diagonal {A} (s : Stream (Stream A)) : Stream A:=  fun i => s i i.Definition Diagonalization (sequences : Stream (nat -> nat)) : Stream nat :=  Map isnt (Diagonal sequences).Theorem isn't_in {sequences} : forall i, Diagonalization sequences <> sequences i.intros; intro.pose (f_equal (fun f => f i) H) as H'.unfold Diagonalization in H'.unfold Diagonal in H'.unfold Map in H'.revert H'.apply isn't_isnt.Qed.Definition pink_elephant : Stream nat := fun i => i.Definition sequence_enumeration : Stream (nat -> nat) := l' pink_elephant.Theorem every_sequence : forall s, exists i, s = sequence_enumeration i.intro s; exists (b s).unfold sequence_enumeration.unfold pink_elephant.unfold l'.unfold Map.rewrite bijection.reflexivity.Qed.Theorem Cantor : False.destruct (every_sequence (Diagonalization sequence_enumeration)) as [i iPrf].pose (@isn't_in sequence_enumeration i).contradiction.Qed.`