intuitionistic proof that cantor space doesn't surject onto the natural numbers

int.v

Require Import Lia PeanoNat Bool.Bool.

Section Exhaustible.

Definition surj{X Y}(f : X -> Y) :=
  forall y, exists x, f x = y.

Definition dec(P : Prop) := {P} + {~P}.

Definition exh(X : Type) := forall p : X -> bool,
  dec (forall x, p x = true).

Lemma unit_exh : exh unit.
Proof.
  intro p.
  destruct (p tt) eqn:G.
  - left; intros []; exact G.
  - right; intro.
    rewrite H in G.
    discriminate.
Defined.

Lemma bool_exh : exh bool.
Proof.
  intro p.
  destruct (p false) eqn:P0.
  - destruct (p true) eqn:P1.
    + left; intros []; assumption.
    + right; intro.
      rewrite H in P1.
      discriminate.
  - right; intro.
    rewrite H in P0.
    discriminate.
Defined.

Lemma prod_exh : forall X Y, exh X -> exh Y -> exh (X * Y).
Proof.
  intros X Y X_exh Y_exh p.
  pose (p_hat := fun x y => p (x,y)).
  pose (q := fun x =>
    match Y_exh (p_hat x) with
    | left _ => true
    | right _ => false
    end).
  destruct (X_exh q).
  - left; intros [x y].
    pose proof (e x).
    unfold q in H.
    destruct (Y_exh (p_hat x)).
    + apply e0.
    + discriminate.
  - right; intro.
    elim n.
    intro x.
    unfold q.
    destruct (Y_exh (p_hat x)).
    + reflexivity.
    + elim n0.
      intro y.
      apply H.
Defined.

Fixpoint Vec X n : Type :=
  match n with
  | 0 => unit
  | S m => (X * Vec X m)%type
  end.

Lemma Vec_exh : forall X n, exh X -> exh (Vec X n).
Proof.
  intros.
  induction n.
  - apply unit_exh.
  - apply prod_exh.
    + exact X0.
    + exact IHn.
Defined.

Lemma surj_exh : forall X Y (f : X -> Y),
  surj f -> exh X -> exh Y.
Proof.
  intros X Y f f_surj X_exh p.
  destruct (X_exh (fun x => p (f x))).
  - left; intro y.
    destruct (f_surj y) as [x Hx].
    pose (e x).
    rewrite Hx in e0.
    exact e0.
  - right; intro y.
    elim n.
    intro x.
    apply y.
Defined.

End Exhaustible.

Section Intuition.

Variable modulus : ((nat -> bool) -> bool) -> nat.

Hypothesis modulus_property : forall F f g,
  (forall x, x < modulus F -> f x = g x) -> F f = F g.

Lemma nat_nonexh : exh nat -> False.
Proof.
  intro nat_exh.
  unfold exh in nat_exh.
  pose (F := fun p =>
    match nat_exh p with
    | left _ => true
    | right _ => false
    end).
  pose (f := fun x : nat => true).
  pose (g := fun x => negb (Nat.eqb (modulus F) x)).
  absurd (F f = F g).
  - unfold F.
    destruct (nat_exh f).
    + destruct (nat_exh g).
      * pose proof (e0 (modulus F)).
        unfold g in H.
        rewrite Nat.eqb_refl in H.
        discriminate.
      * discriminate.
    + elim n.
      unfold f.
      intro; reflexivity.
  - apply modulus_property.
    intros.
    unfold f,g.
    symmetry; apply negb_true_iff.
    rewrite Nat.eqb_neq.
    lia.
Defined.

Fixpoint to_func{n} : Vec bool n -> nat -> bool :=
  match n with
  | 0 => fun _ _ => false
  | S m => fun v i => match i with
                      | 0 => fst v
                      | S j => to_func (snd v) j
                      end
  end.

Fixpoint prefix{X n} : (nat -> X) -> Vec X n :=
  match n return (nat -> X) -> Vec X n with
  | 0 => fun _ => tt
  | S m => fun f => (f 0, prefix (fun x => f (S x)))
  end.

Lemma to_func_prefix : forall n f x, x < n -> to_func (@prefix _ n f) x = f x.
Proof.
  induction n; intros.
  - lia.
  - destruct x.
    + reflexivity.
    + simpl.
      apply (IHn (fun x => f (S x))).
      lia.
Qed.

Lemma cantor_exh : exh (nat -> bool).
Proof.
  intro p.
  pose (p_hat := fun (v : Vec bool (modulus p)) => p (to_func v)).
  destruct (Vec_exh _ _ bool_exh p_hat).
  - left.
    intro f.
    rewrite <- (e (prefix f)).
    apply modulus_property.
    intros.
    symmetry; apply to_func_prefix; assumption.
  - right.
    intro.
    apply n.
    intro v.
    apply H.
Defined.

Lemma no_surj_cantor_nat : ~ exists f : (nat -> bool) -> nat,
  surj f.
Proof.
  intros [f f_surj].
  apply nat_nonexh.
  exact (surj_exh _ _ f f_surj cantor_exh).
Qed.