The Coq mailing list

[Daniel Schepler <(e29315a54f%hidden_head%e29315a54f)dschepler(e29315a54f%hidden_at%e29315a54f)gmail.com(e29315a54f%hidden_end%e29315a54f)>]

I never really understood the proof from the Coq standard library,
although now that I've seen Hurkens' paper I guess the idea is
something like "if two proofs were distinguishable, that would allow
one to derive a contradiction similar to the Burali-Forti paradox".
So I eventually came up with another proof.

Outline: Suppose we have a proposition "bool" with proofs "true" and "false".
* Given that Prop is impredicative, it's easy to define a projection
function from P to (P -> bool), where P is the product of (X -> bool)
over all propositions X.
* Given classic, it's not too hard to show this function is
surjective: given y:P -> bool, define x:P to be the element where the
P component is y, and other components are a constant function to
true.  (In the actual formalization, we run into the issue that the
eq_rect conversion function isn't necessarily the identity.  We don't
yet know that all equalities x = x are eq_refl -- that's a special
case of what we're trying to prove.  So we need to apply a reverse
eq_rect_r conversion to invert that...)
* By a very minor modification of Cantor's diagonalization argument,
this implies that every function bool -> bool has a fixed point.
* The existence of a fixed point of a natural negation function on
bool implies true = false.

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

Lemma Cantor_fixed_pt : forall (X Y:Type) (g:X->(X->Y)),
  surjective g -> forall f:Y->Y, exists y:Y, f y = y.
Proof.
intros.
set (h x := f (g x x)).
destruct (H h) as [x0 ?].
exists (h x0).
unfold h at 2.
rewrite H0; reflexivity.
Qed.

Lemma eq_rect_r_inv : forall (A:Type) (x:A) (P:A->Type)
  (f:P x) (y:A) (e:x=y), eq_rect_r P (eq_rect x P f y e) e = f.
Proof.
intros.
destruct e.
reflexivity.
Qed.

Section classic_proof_irrelevance.

Hypothesis classic : forall P:Prop, P \/ ~P.

Variable bool : Prop.
Variables true false : bool.

Definition P : Prop := (forall X:Prop, X -> bool).
Definition g : P -> (P -> bool) := fun p:P => p P.

Lemma g_surj : surjective g.
Proof.
intros y.
unfold g.
exists (fun X:Prop =>
  match (classic (P = X)) return (X -> bool) with
  | or_introl e =>
       match (classic (X = X)) with
       | or_introl e' =>
         eq_rect_r _ (eq_rect P (fun P' => P' -> bool) y _ e) e'
       | or_intror ne => False_ind _ (ne (eq_refl X))
       end
  | or_intror _ => fun _ => true
  end).
destruct (classic (P=P)).
exact (eq_rect_r_inv _ _ _ _ _ _).
contradiction n; trivial.
Qed.

Definition negb := fun b:bool =>
  if (classic (b = true)) then false else true.

Lemma notb_fixed_pt : exists b:bool, negb b = b.
Proof.
apply Cantor_fixed_pt with (1:=g_surj).
Qed.

Corollary proof_irrelevance : true = false.
Proof.
destruct notb_fixed_pt as [b].
unfold negb in H.
destruct classic in H; congruence.
Qed.

End classic_proof_irrelevance.

Print Assumptions proof_irrelevance.
(* Closed under the global context *)
-- 
Daniel Schepler