The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Mon, 27 Jun 2011 19:54:34 +0300,
Georgi Guninski 
<guninski AT guninski.com>
 a écrit :

> On Sun, Jun 26, 2011 at 10:00:19AM -0700, Daniel Schepler wrote:
> > 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?

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.

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