# Library Coq.Logic.Berardi

This file formalizes Berardi's paradox which says that in the calculus of constructions, excluded middle (EM) and axiom of choice (AC) imply proof irrelevance (PI). Here, the axiom of choice is not necessary because of the use of inductive types.
```@article{Barbanera-Berardi:JFP96,
author    = {F. Barbanera and S. Berardi},
title     = {Proof-irrelevance out of Excluded-middle and Choice
in the Calculus of Constructions},
journal   = {Journal of Functional Programming},
year      = {1996},
volume    = {6},
number    = {3},
pages     = {519-525}
}
```

Set Implicit Arguments.

Excluded middle
Hypothesis EM : forall P:Prop, P \/ ~ P.

Conditional on any proposition.
Definition IFProp (P B:Prop) (e1 e2:P) :=
match EM B with
| or_introl _ => e1
| or_intror _ => e2
end.

Axiom of choice applied to disjunction. Provable in Coq because of dependent elimination.
Lemma AC_IF :
forall (P B:Prop) (e1 e2:P) (Q:P -> Prop),
(B -> Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2).

We assume a type with two elements. They play the role of booleans. The main theorem under the current assumptions is that T=F
Variable Bool : Prop.
Variable T : Bool.
Variable F : Bool.

The powerset operator
Definition pow (P:Prop) := P -> Bool.

A piece of theory about retracts
Section Retracts.

Variables A B : Prop.

Record retract : Prop :=
{i : A -> B; j : B -> A; inv : forall a:A, j (i a) = a}.
Record retract_cond : Prop :=
{i2 : A -> B; j2 : B -> A; inv2 : retract -> forall a:A, j2 (i2 a) = a}.

The dependent elimination above implies the axiom of choice:

Lemma AC : forall r:retract_cond, retract -> forall a:A, r.(j2) (r.(i2) a) = a.

End Retracts.

This lemma is basically a commutation of implication and existential quantification: (EX x | A -> P(x)) <=> (A -> EX x | P(x)) which is provable in classical logic ( => is already provable in intuitionistic logic).

Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B).

Definition U := forall P:Prop, pow P.

Bijection between U and (pow U)
Definition f (u:U) : pow U := u U.

Definition g (h:pow U) : U :=
fun X => let lX := j2 (L1 X U) in let rU := i2 (L1 U U) in lX (rU h).

We deduce that the powerset of U is a retract of U. This lemma is stated in Berardi's article, but is not used afterwards.