diag.v

gistfile1.txt

Definition notb (b : bool) : bool :=
  if b then false else true.
Definition true_neq_false (b : bool) : b = notb b -> False :=
  match b as b return b = notb b -> False with
  | true => fun p =>
    match p in _ = b return
      if b then True else False
    with
    | eq_refl => I
    end
  | false => fun p =>
    match p in _ = b return
      if b then False else True
    with
    | eq_refl => I
    end
  end.

Section Bad.
  Definition Real := nat -> bool.
  Variable id_nat_real : nat = Real.
  Definition f : nat -> Real :=
    match id_nat_real in _ = T return nat -> T with
    | eq_refl => fun n => n
    end.
  Definition r : Real := fun n => notb (f n n).
  Definition diag n : f n = r -> False := fun p =>
    true_neq_false (f n n)
      match p in _ = g return
        f n n = g n
      with
      | eq_refl => eq_refl
      end.
  Definition g : Real -> nat :=
    match id_nat_real in _ = T return T -> nat with
    | eq_refl => fun n => n
    end.
  Definition f_g_id : forall r, f (g r) = r.
    unfold f, g.
    exact (
      match id_nat_real in (_ = T) with
      | eq_refl => fun r => eq_refl
      end
    ).
  Defined.
  Definition bad : False := diag (g r) (f_g_id r).
End Bad.