Is the Daniel Schepler's inconsistency real?

Post by Georgi Guninski
Is the Daniel Schepler's inconsistency real?

No, his code does not demonstrate an inconsistency.

Post by Georgi Guninski
Daniel Schepler proved [1][2] both T and ~T using only a plausible axiom and I couldn't find any cheating in his proof (I admit I am dumb).
Possibly due to a coq ``anomaly'' (read a bug) coq gives strange error when using both T and ~T (well maybe coded on purpose)

The fact that it seems strange to you doesn't mean that it isn't a key
part of maintaining Coq's consistency. ;)

Georgi Guninski

2011-06-25 13:21:12 UTC

Post by Georgi Guninski
Is the Daniel Schepler's inconsistency real?

No, his code does not demonstrate an inconsistency.

if you read the message you would realize i was asking about
*modifications* of his code. here are two files - one takes T as axiom,
the other takes ~T as axiom and in both cases False is proven (one of
the proofs should be real unless i miss something)

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

Axiom 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.
*)

Lemma not_power_inj: forall X (f:(X->Prop)->X), ~ injective f.
Proof.
intros.
intro Hinj.
pose (S0 := fun x:X => exists S:X->Prop, ~ S x /\ f S = x).
pose (x0 := f S0).
assert (~ S0 x0).
intro.
unfold S0 in H.
destruct H as [S' []].
unfold x0 in H0.
apply Hinj in H0.
rewrite H0 in H.
unfold S0 in H.
contradiction H.
exists S0.
split; trivial.

pose proof H.
unfold S0 in H0.
contradiction H0.
exists S0.
split; trivial.
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].
exact (not_power_inj _ _ H0).
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. (* Done *)

(*file 2*)

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.

Lemma not_power_inj: forall X (f:(X->Prop)->X), ~ injective f.
Proof.
intros.
intro Hinj.
pose (S0 := fun x:X => exists S:X->Prop, ~ S x /\ f S = x).
pose (x0 := f S0).
assert (~ S0 x0).
intro.
unfold S0 in H.
destruct H as [S' []].
unfold x0 in H0.
apply Hinj in H0.
rewrite H0 in H.
unfold S0 in H.
contradiction H.
exists S0.
split; trivial.

pose proof H.
unfold S0 in H0.
contradiction H0.
exists S0.
split; trivial.
Qed.

Axiom 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].
exact (not_power_inj _ _ H0).
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. (* Done *)

Adam Chlipala

2011-06-25 13:34:05 UTC

Post by Georgi Guninski
if you read the message you would realize i was asking about
*modifications* of his code. here are two files - one takes T as axiom,
the other takes ~T as axiom and in both cases False is proven (one of
the proofs should be real unless i miss something)

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].

The key thing to understand here is that, in Coq, proofs may change
theorem statements, even the statements of past, already-proved
theorems! Every occurrence of [Type] is implicitly annotated with a
universe variable. Any part of a development that depends on such a
variable may add constraints on it, in a very "imperative" way.
Checking these constraints is crucial for consistency.

Daniel's proofs tweak universe variables in a way that makes your
"axioms" weaker. The untweaked versions are strong enough to be
inconsistent, but the tweaked ones are fine.

The moral of the story is to try to avoid axioms whenever you can. ;)

Georgi Guninski

2011-06-25 14:37:50 UTC

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?

Note I probably need excluded middle.

Note that you can try to prove axioms by removing the comments...

Adam Chlipala

2011-06-25 14:51:23 UTC

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].

~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!

Georgi Guninski

2011-06-25 15:44:12 UTC

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].

~uat_maximal_card = uat_not_maximal_card
Any ideas on simplifying your statement?

[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.

Adam Chlipala

2011-06-25 15:52:40 UTC

Post by Adam Chlipala
[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!

let me point no further than
https://sympa-roc.inria.fr/wws/arc/coq-club/2011-06/msg00099.html

Your proofs prove different facts. Not all occurrences of the same
source text represent the same formulas in Coq; every occurrence of
[Type] has a hidden universe variable, and those variables end up with
different constraints between the versions.

Mathieu Boespflug

2011-06-25 17:06:45 UTC

let me point no further than
https://sympa-roc.inria.fr/wws/arc/coq-club/2011-06/msg00099.html

Perhaps the

Set Printing Universes.

command should help clear up the confusion. Also,

Print Universes.

to see the current global set of constraints on all universe variables
currently in use by Coq. New constraints to existing variables can
arise as new definitions, theorems, etc are made.

-- Mathieu

gallais @ ensl.org

2011-06-25 13:34:22 UTC

Even if you are using classical Logic, you cannot prove False
from your scripts because you still have the Universe inconsistency
problem:

Require Import Classical.

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 not_power_inj: forall X (f:(X->Prop)->X), ~ injective f.
Proof.
intros.
intro Hinj.
pose (S0 := fun x:X => exists S:X->Prop, ~ S x /\ f S = x).
pose (x0 := f S0).
assert (~ S0 x0).
intro.
unfold S0 in H.
destruct H as [S' []].
unfold x0 in H0.
apply Hinj in H0.
rewrite H0 in H.
unfold S0 in H.
contradiction H.
exists S0.
split; trivial.

pose proof H.
unfold S0 in H0.
contradiction H0.
exists S0.
split; trivial.
Qed.

Lemma contradiction : False.
Proof.
case (classic (forall (X:Type), exists f:X->union_of_all_types,
injective f)) ; intro H.

destruct (H (union_of_all_types -> Prop)) as [f].
exact (not_power_inj _ _ H0).

apply H.
intros.
exists (@type_inc X).
red; intros.
injection H0.
Require Import Eqdep.
apply inj_pair2.
Qed. (** Fail : Universe inconsistency **)

--
gallais

Post by Georgi Guninski
Is the Daniel Schepler's inconsistency real?

No, his code does not demonstrate an inconsistency.

if you read the message you would realize i was asking about
*modifications* of his code. here are two files - one takes T as axiom,
the other takes ~T as axiom and in both cases False is proven (one of
the proofs should be real unless i miss something)
(*file 1*)
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.
Axiom uat_maximal_card: forall (X:Type), exists f:X->union_of_all_types,
injective f.
(*
Proof.
intros.
red; intros.
injection H.
Require Import Eqdep.
apply inj_pair2.
Qed.
*)
Lemma not_power_inj: forall X (f:(X->Prop)->X), ~ injective f.
Proof.
intros.
intro Hinj.
pose (S0 := fun x:X => exists S:X->Prop, ~ S x /\ f S = x).
pose (x0 := f S0).
assert (~ S0 x0).
intro.
unfold S0 in H.
destruct H as [S' []].
unfold x0 in H0.
apply Hinj in H0.
rewrite H0 in H.
unfold S0 in H.
contradiction H.
exists S0.
split; trivial.
pose proof H.
unfold S0 in H0.
contradiction H0.
exists S0.
split; trivial.
Qed.
~ (forall (X:Type), exists f:X->union_of_all_types, injective f).
Proof.
intro.
destruct (H (union_of_all_types -> Prop)) as [f].
exact (not_power_inj _ _ H0).
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. (* Done *)
(*file 2*)
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.
red; intros.
injection H.
Require Import Eqdep.
apply inj_pair2.
Qed.
Lemma not_power_inj: forall X (f:(X->Prop)->X), ~ injective f.
Proof.
intros.
intro Hinj.
pose (S0 := fun x:X => exists S:X->Prop, ~ S x /\ f S = x).
pose (x0 := f S0).
assert (~ S0 x0).
intro.
unfold S0 in H.
destruct H as [S' []].
unfold x0 in H0.
apply Hinj in H0.
rewrite H0 in H.
unfold S0 in H.
contradiction H.
exists S0.
split; trivial.
pose proof H.
unfold S0 in H0.
contradiction H0.
exists S0.
split; trivial.
Qed.
~ (forall (X:Type), exists f:X->union_of_all_types, injective f).
(*
Proof.
intro.
destruct (H (union_of_all_types -> Prop)) as [f].
exact (not_power_inj _ _ H0).
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. (* Done *)

Daniel Schepler

2011-06-25 16:41:11 UTC

Post by Georgi Guninski
Is the Daniel Schepler's inconsistency real?
Daniel Schepler proved [1][2] both T and ~T using only a plausible axiom
and I couldn't find any cheating in his proof (I admit I am dumb).
Possibly due to a coq ``anomaly'' (read a bug) coq gives strange error when
using both T and ~T (well maybe coded on purpose)
In his code T and ~T are [uat_maximal_card] and [uat_not_maximal_card].
Assuming excluded middle, does it mean one of T and ~T is necessarily true
so it can be taken as an axiom?
According to my tests if I take as an axiom one of them, in *both* cases I
can prove False using exactly his approach. One of the proofs will have
axiom False (genuinely proved by him but unusable due to a bug), but the
other must be real inconsistency.
For testing I just replaced [Lemma] by [Axiom] and commented out the
proof (leaving the proof for the contrary).
Is this correct?

Let me try to explain what the "paradox" is that I'm formalizing, and what the
resolution is. I forget the exact name of the paradox, but it's essentially
the Burali-Forti paradox with cardinals instead of ordinals. If you formulate
it in ZFC, getting two contradictory statements about the cardinality of the
collection V of all sets, it's also closely related to the Russell paradox if
you unfold Cantor's diagonalization argument.

Essentially, if you let U be the disjoint union of all types, and consider the
cardinality mu of U, then you can seem to get two contradictory statements
about it. First, for any cardinality kappa which is the cardinality of a type
X, you obviously have an injection from X to U by the inclusion map.
Therefore, kappa <= mu [uat_maximal_card]. But by Cantor diagonalization,
2^mu > mu [uat_not_maximal_card].

Here, the key to resolving the apparent paradox is to consider Coq's type
hierarchy closely. Suppose the Type in the definition of union_of_all_types is
Type(n). Then union_of_all_types is in Type(n+1). Now, in the proof of
uat_maximal_card, we feed X as an argument of type_inc. In order for this to
be valid, the Type in the statement of uat_maximal_card must be at level
Type(n) or lower. On the other hand, in the proof of uat_not_maximal_card, we
feed (union_of_all_types -> Prop) into X, which is in Type(n+1), so for this
statement to be valid the Type here must be Type(n+1) or higher. If you turn
on display of universe levels just before trying to process the Qed of
contradiction, Coq will print an error message like

Error: Universe inconsistency (cannot enforce Top.8 = Top.61).

Here Top.8 is the level of Type in uat_maximal_card and Top.61 is the level of
Type in uat_not_maximal_card. It wants the two levels to be equal in order to
be able to derive the contradiction False, while internally it must have found
restraints that imply that Top.8 < Top.61.

So as another way of saying it, all this argument proves is that it would be
inconsistent to assign union_of_all_types to the same level universe
represented by the Type level in the declaration in type_inc (or lower). But
if you "Print union_of_all_types." with universe level printing on, it shows

Inductive union_of_all_types : Type (* (Top.2)+1 *) :=
type_inc : forall X : Type (* Top.2 *), X -> union_of_all_types

So Coq got the universe level right.

--
Daniel

Daniel Schepler

2011-06-26 17:00:19 UTC

Thank you.
I was asking what was wrong with taking as an axiom one of your statements.
In both cases False is proven and excluded middle appears to guarantee one
of the proofs to be genuine.
btw, setting the lemma as Definition and proving D and ~D doesn't work
for me.

What's wrong with setting one of them as an axiom is that it doesn't generate
the appropriate constraints on the level of Type in the statement.

Maybe it might help understanding to make a couple definitions:

Definition small_univ := Type.
Inductive union_of_all_small_types : small_univ :=
| small_type_inc : forall {X:small_univ},
X -> union_of_all_small_types.

This should give a universe inconsistency error right away.

On the other hand, with:

Definition small_univ := Type.
Definition large_univ := Type.
Inductive union_of_all_small_types : large_univ :=
| small_type_inc: forall {X:small_univ},
X -> union_of_all_small_types.

This should be fine, and just forces that small_univ is at a strictly lower
level in the type hierarchy than large_univ.

Then the correct statements of uat_maximal_card and uat_not_maximal_card are:

Lemma uat_maximal_card: forall X:small_univ, exists f :
X->union_of_all_small_types, injective f.
Lemma uat_not_maximal_card: ~ forall X:large_univ, exists f :
X->union_of_all_small_types, injective f.

But if you declare the original statements as axioms, in uat_maximal_card, for
all Coq knows, the Type occuring there might be large_univ. Similarly, in
not_uat_maximal_card, for all Coq knows, the Type occuring there might be
small_univ. So this would have the same effect as declaring

Axiom uat_maximal_card_ax: forall X:large_univ, exists f :
X->union_of_all_small_types, injective f.

or

Axiom uat_not_maximal_card_ax: ~ forall X:small_univ, exists f :
X->union_of_all_small_types, injective f.

If you set the statement as a definition, that forces there to be a single
instance of Type, with the proofs of uat_maximal_card and uat_not_maximal_card
generating incompatible constraints on the level of this Type compared to the
level of the Type in the definition of union_of_all_types. So you could prove
either one of the statements D or ~D, but not both at the same time. In
trying to adapt this approach to the small_univ / large_univ case, you'd have
to decide whether to put small_univ or large_univ into the definition.
Depending on which you choose, you would be able to prove one or the other of
D or ~D, but not both at the same time.

So one conclusion you can draw from the "paradox" is that small_univ <>
large_univ. Which would look strange on its own given the definitions of
small_univ and large_univ, if you didn't know about the type hierarchy and
that different instances of Type are distinct objects to Coq.

--
Daniel

Georgi Guninski

2011-06-27 16:54:34 UTC

Post by Daniel Schepler
level of the Type in the definition of union_of_all_types. So you could prove
either one of the statements D or ~D, but not both at the same time. In

With a simple trick, one can prove both D and ~D by splitting files.

Basically, put the definition in def.v, the proof of D in D.v and the proof of ~D in notD.v. Compile all of them with coqc (coq fanatics know they should trust the .vo, because the compiler may not see the .v). In D and notD.v do "Require Import def".

So coqchk is quite happy, but coqtop gives error when importing notD after D, why so after coqchk passed, are there incompatible sets of .vo's?

Coq < Require Import D.
Coq < Require Import notD.
Error: Universe inconsistency.

In a new session:

Coq < Require Import notD.
Coq < Require Import D.
Error: Universe inconsistency.

(*def.v*)
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.
Definition D := forall (X:Type), exists f:X->union_of_all_types,
injective f.

(*D.v*)
Require Import def.

Lemma uat_maximal_card: D.

Proof.
compute.
intros.
exists (@type_inc X).
(*red;*) intros.
injection H.
Require Import Eqdep.
apply inj_pair2.
Qed.

(*notD.v*)
Require Import def.
Lemma not_power_inj: forall X (f:(X->Prop)->X), ~ injective f.
Proof.
intros.
intro Hinj.
pose (S0 := fun x:X => exists S:X->Prop, ~ S x /\ f S = x).
pose (x0 := f S0).
assert (~ S0 x0).
intro.
unfold S0 in H.
destruct H as [S' []].
unfold x0 in H0.
apply Hinj in H0.
rewrite H0 in H.
unfold S0 in H.
contradiction H.
exists S0.
split; trivial.

pose proof H.
unfold S0 in H0.
contradiction H0.
exists S0.
split; trivial.
Qed.

Lemma uat_not_maximal_card:
~ D.

Proof.

intro.
destruct (H (union_of_all_types -> Prop)) as [f].
exact (not_power_inj _ _ H0).
Qed.

AUGER Cedric

2011-06-27 16:08:18 UTC

Le Mon, 27 Jun 2011 19:54:34 +0300,

Post by Daniel Schepler
level of the Type in the definition of union_of_all_types. So you
could prove either one of the statements D or ~D, but not both at
the same time. In

Because you haven't yet understood our replies, D and ~D are may be
both true in their universe constraints.

A compiled file has never been said to be "correct" under ANY regular
universe constraints, but under SOME regular universe constraints.

I already posted on this topic last year I believe, when I didn't know
of Coq's universe constraints, but I don't remember exactly when and I
am too lazy to look for it.

Post by Georgi Guninski
Coq < Require Import D.
Coq < Require Import notD.
Error: Universe inconsistency.
Coq < Require Import notD.
Coq < Require Import D.
Error: Universe inconsistency.
(*def.v*)
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.
Definition D := forall (X:Type), exists f:X->union_of_all_types,
injective f.
(*D.v*)
Require Import def.
Lemma uat_maximal_card: D.
Proof.
compute.
intros.
(*red;*) intros.
injection H.
Require Import Eqdep.
apply inj_pair2.
Qed.
(*notD.v*)
Require Import def.
Lemma not_power_inj: forall X (f:(X->Prop)->X), ~ injective f.
Proof.
intros.
intro Hinj.
pose (S0 := fun x:X => exists S:X->Prop, ~ S x /\ f S = x).
pose (x0 := f S0).
assert (~ S0 x0).
intro.
unfold S0 in H.
destruct H as [S' []].
unfold x0 in H0.
apply Hinj in H0.
rewrite H0 in H.
unfold S0 in H.
contradiction H.
exists S0.
split; trivial.
pose proof H.
unfold S0 in H0.
contradiction H0.
exists S0.
split; trivial.
Qed.
~ D.
Proof.
intro.
destruct (H (union_of_all_types -> Prop)) as [f].
exact (not_power_inj _ _ H0).
Qed.

Adam Chlipala

2011-06-27 17:13:39 UTC