(*

  The following proof shows proof-irrelevance in Martin-Löf's type
theory extended with computational classical logic (hence
inconsistency in Martin-Löf's type theory with universes).

  By "computational classical logic" is intended the presence of a
control operator equipped with the standard reduction rules for
classical control. Here we consider call-cc equipped with its
commutation rule and its simplification rule.

  The proof is formalised in Coq V7.4, but impredicativity is not used.

  The simplification rule is probably the more questionable rule when
considered as a rewriting rule on types. E.g. the semantics of callcc
in the boolean model of propositions for non empty is a choice
function, hence the simplification rule on A asserts that any element
of A is equal to the default representant. Hence the proof-irrelevance.

*)

---------------------------------------------------------------------------
(* Proving proof-irrelevance in Set from strong projections of [sig] *)
(* and call-cc reduction rules (no impredicativity) *)

Set Implicit Arguments.

Implicits proj1_sig [1 2].
Implicits proj2_sig [1 2].

(* Call-cc *)
Parameter callcc : (A:Set)((A->False)->A)->A.

(* Call-cc generic commutation rule: should mention evaluation order, *)
(* otherwise, we get proof-irrelevance directly from non confluence of *)
(* CBN and CBV ! *)
(*
Axiom callcc_commut : (A,B:Set)(E:A->B)(M:(A->False)->A)
  (E (callcc M)) = (callcc [k:B->False](E (M [x:A](k (E x))))).
*)

(* Here is a confluent specialisation of the commutation rule which is *)
(* sufficient for our purpose *)
Axiom callcc_cases_commut : (P:bool->Prop) let A = (sig bool P) in
 (B:Set)(N:(x:bool)(P x)->B) let E = [x:A]Case x of N end in
 (M:(A->False)->A)
 (E (callcc M)) = (callcc [k:B->False](E (M [x:A](k (E x))))).

(* Call-cc simplification rule *)
Axiom callcc_simpl : (A:Set)(M:A)
  (callcc [_:A->False]M) = M.

(* An artifially-classical proof of a trivial constructive statement *)
Lemma detour : { b:bool | true = b }.
Proof.
Apply callcc.
Exists false.
Elim H.
Exists true.
Reflexivity.
Defined.

(* The crux of the constructive classical logic : first projection of
   the classical proof is _always_ the first try [here false] *)
Lemma proj1_detour : (proj1_sig detour) = false.
Proof.
Assert commut := (callcc_cases_commut 1![b]true=b [b;p]b).
Simpl in commut.
Unfold detour proj1_sig.
Rewrite commut.
Simpl.
Apply callcc_simpl.
Defined.

(* Hence, we can change the second-projection type from *)
(* [true=(proj1_sig detour)] to [true=false] *)
Lemma proof_irrelevance : true=false.
Proof.
Rewrite <- proj1_detour.
Apply (proj2_sig detour).
Qed.

(* We derive an inconsistency from true<>false which is provable *)
(* using strong elimination (definition of propositions by cases) *)
Lemma paradox : False.
Proof.
Assert H := proof_irrelevance.
Discriminate H.
Qed.