The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Fri, Jun 24, 2011 at 6:03 AM, Bruno Barras <bruno.barras AT inria.fr> wrote:

Who can address this challenge: find a "simple" statement T (simple in the sense that anyone with a minimal background in logics can understand) such that you can prove both T and ~T in Coq.

Bruno.

Here's something close: it purports to prove that classic + constructive_definite_description (+ eq_rect_eq which is implied by classic) gives a contradiction.

Inductive union_of_all_types : Type :=
| type_inc: forall {X:Type}, X -> union_of_all_types.

Definition injective {X Y:Type} (f:X->Y) : Prop :=
  forall x1 x2:X, f x1 = f x2 -> x1 = x2.

Lemma uat_maximal_card: forall (X:Type), exists f:X->union_of_all_types,
  injective f.
Proof.
intros.
exists (@type_inc X).
red; intros.
injection H.
Require Import Eqdep.
apply inj_pair2.
Qed.

Require Import Description.
Require Import Classical.

Lemma classic_dec : forall P:Prop, {P} + {~P}.
Proof.
intro P.
assert ({b:bool | if b then P else ~P}).
apply constructive_definite_description.
destruct (classic P); [ exists true | exists false ]; split; trivial;
  destruct x'; intros; try contradiction; reflexivity.
destruct H as [[|]]; [ left | right ]; trivial.
Qed.

Program Definition inj_left_inv {X Y:Type} (f:X->Y) (x0:X)
  (Hinj:injective f) : Y -> X :=
fun y:Y => if (classic_dec (exists x:X, f x = y)) then
    proj1_sig (constructive_definite_description (fun x:X => f x = y) _) else
    x0.
Next Obligation.
rename H into x.
exists x.
split; trivial.
intros.
apply Hinj; symmetry; trivial.
Qed.

Lemma inj_left_inv_left_inv: forall X Y (f:X->Y) x0 Hinj x,
  inj_left_inv f x0 Hinj (f x) = x.
Proof.
intros.
unfold inj_left_inv.
destruct classic_dec.
destruct constructive_definite_description.
simpl.
apply Hinj; trivial.
contradict n.
exists x; trivial.
Qed.

Lemma inj_left_inv_surj: forall X Y (f:X->Y) x0 Hinj (x:X),
  exists y:Y, inj_left_inv f x0 Hinj y = x.
Proof.
intros.
exists (f x).
apply inj_left_inv_left_inv.
Qed.

Lemma uat_not_maximal_card:
  ~ forall (X:Type), exists f:X->union_of_all_types, injective f.
Proof.
intro.
destruct (H (union_of_all_types -> Prop)) as [f].
pose (g := inj_left_inv f (fun _ => True) H0).
assert (forall S:union_of_all_types -> Prop, exists x:union_of_all_types,
  g x = S) by apply inj_left_inv_surj.
destruct (H1 (fun x:union_of_all_types => ~ g x x)) as [x].
Require Import FunctionalExtensionality. (* for equal_f only *)
pose proof (equal_f H2 x).
simpl in H3.
assert (~ g x x).
intro.
assert (~ g x x).
rewrite <- H3.
trivial.
contradiction.
assert (g x x).
rewrite H3.
trivial.
contradiction.
Qed.

Print Assumptions uat_maximal_card.
Print Assumptions uat_not_maximal_card.

Lemma contradiction: False.
Proof.
exact (uat_not_maximal_card uat_maximal_card).
Qed.  (* this is where Coq prints a universe inconsistency *)