(** Mathematics for Computer Scientists 2 (G52MC2)
Thorsten Altenkirch
L11 (The omega hotel, diagonalisation)
The material in this file contains coq proofs
which can be read and animated with coqide or xemacs+proofgeneral.
**)
Section wHotel.
Require Import Coq.Arith.Arith.
Definition sn2n (sn : unit + nat) : nat
:= match sn with
| inl tt => 0
| inr n => S n
end.
Definition n2sn (n : nat) : unit + nat
:= match n with
| O => inl nat tt
| S n' => inr unit n'
end.
Definition snn2n (snn : sum nat nat) : nat
:= match snn with
| inl n' => 2*n'
| inr n' => 2*n'+1
end.
Fixpoint n2snn (n:nat) : sum nat nat
:= match n with
| O => inl nat 0
| S O => inr nat 0
| S (S n') => match n2snn n' with
| inl m => inl nat (S m)
| inr m => inr nat (S m)
end
end.
(* The case for nat * nat is left as an exercise *)
End wHotel.
Section diagonalize.
Variable f : nat -> (nat -> nat).
Variable g : (nat -> nat) -> nat.
Hypothesis ginvf : forall h:nat -> nat, f (g h) = h.
Definition d (n : nat) : nat
:= S (f n n).
Lemma diag : f (g d) (g d) = S (f (g d) (g d)).
pattern (f (g d)) at 1.
rewrite ginvf.
unfold d at 1.
reflexivity.
Qed.
Lemma contr : False.
eapply n_Sn.
apply diag.
Qed.