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