(* Robert Dockins, 2007 *)
(* Public Domain *)

Set Implicit Arguments.
Require Import Bool.

(* A bijection is a function from A to B together
   with its inverse *)
Structure bijection (A B:Type) : Type :=
  { bijMap : A -> B
  ; bijInv : B -> A
  ; bijId  : forall a:A, bijInv (bijMap a) = a
  }.

(* A type is countably infinite iff it can be placed
   into a bijection with the natral numbers *)
Definition countable (U:Type) := bijection U nat.

(* The type of infinite binary streams *)
CoInductive boolStream : Set :=
  | BCons : bool -> boolStream -> boolStream.

Definition Unfold_boolStream (x:boolStream) :=
   match x with
   | BCons x z => BCons x z
   end.

Lemma unfold_boolStream : forall x, x = Unfold_boolStream x.
  intro x; case x; simpl; auto.
 Qed.

Fixpoint b_nth (n:nat) (x:boolStream) { struct n } : bool :=
  match n, x with
  | 0,    BCons z _  => z
  | S n', BCons _ x' => b_nth n' x'
  end.


(* We wish to show that the boolean streams are uncountable; thus,
   assume they are countable and therefrom derive a contradiction.
   We proceed using the classic diagonalization argument.
*)
Section boolStream_uncountable.
  Variable bCount : countable boolStream.

  CoFixpoint diag' (n:nat) : boolStream :=
     BCons (negb (b_nth n (bijInv bCount n))) (diag' (S n)).

  Definition diag := diag' 0.

  Lemma b_nth_diag : forall n m, b_nth n (diag' m) = negb (b_nth (n+m) (bijInv bCount (n+m))).
    induction n; simpl; intros; auto.
    pattern (diag' (S m)); rewrite unfold_boolStream; simpl.
    destruct n; simpl; auto.
    replace (b_nth n (diag' (S (S m)))) with
         (b_nth (S n) (diag' (S m)));
       [| simpl; auto ].
    rewrite IHn.
    simpl.
    replace (S (n + S m)) with (S (S (n+m))); auto.
    replace (n + S m) with (S (n+m)); auto.
   Qed.

  Lemma diag_nth_neq : forall n, b_nth n (bijInv bCount n) <> b_nth n diag.
    unfold diag; intro n.
    rewrite b_nth_diag.
    replace (n+0) with n; auto.    
    intro H; refine (no_fixpoint_negb (b_nth n (bijInv bCount n)) _); auto.
   Qed.

  Lemma diag_neq : forall n, bijInv bCount n <> diag.
    intros n H; apply (diag_nth_neq n); rewrite <- H; auto.
   Qed.

  (* From the assumption that the boolean streams are countable,
     we derive a proof of the absurd proposition "False" *)
  Theorem uncountable : False.
    generalize (bijId bCount diag); intro H; apply (diag_neq _ H).
   Qed.
End boolStream_uncountable.

Check uncountable.