The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

On Sat, Jun 25, 2011 at 10:51:23AM -0400, Adam Chlipala wrote:
> Georgi Guninski wrote:
> >On Sat, Jun 25, 2011 at 09:34:05AM -0400, Adam Chlipala wrote:
> >>Neither proof is showing an inconsistency in Coq. Rather, you've
> >>shown that [uat_maximal_card] is an inconsistent axiom even by
> >>itself, and [uat_not_maximal_card] is inconsistent with
> >>[eq_rect_eq].
> >If you examine the coq output, you will find out in both cases:
> >~uat_maximal_card = uat_not_maximal_card
> >
> >Any ideas on simplifying your statement?
> 
> I'm not sure what you're asking, but here's a restatement:
> [uat_maximal_card] in full generality is fundamentally incompatible
> with Coq.  [uat_not_maximal_card] in full generality is incompatible
> with another popular axiom.  Thus, you probably don't want to rely
> on either as an axiom!

Dear Adam Chlipala,

Regarding your mad-like doubts about [uat_maximal_card], let me point no 
further than

https://sympa-roc.inria.fr/wws/arc/coq-club/2011-06/msg00099.html

For your convenience, I am including the proof of [uat_maximal_card] (well 
and its negation) here - you can diff(1) against my previous testcases:

(*file 3 *)
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.