← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to test-suite/failure/universes-buraliforti.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
test-suite/failure/universes-buraliforti.v
 
1
(* Check that Burali-Forti paradox does not go through *)
 
2
 
 
3
(* Source: contrib/Rocq/PARADOX/{Logics,BuraliForti},v *)
 
4
 
 
5
(* Some properties about relations on objects in Type *)
 
6
 
 
7
  Inductive ACC (A : Type) (R : A -> A -> Prop) : A -> Prop :=
 
8
      ACC_intro :
 
9
        forall x : A, (forall y : A, R y x -> ACC A R y) -> ACC A R x.
 
10
 
 
11
  Lemma ACC_nonreflexive :
 
12
   forall (A : Type) (R : A -> A -> Prop) (x : A),
 
13
   ACC A R x -> R x x -> False.
 
14
simple induction 1; intros.
 
15
exact (H1 x0 H2 H2).
 
16
Qed.
 
17
 
 
18
  Definition WF (A : Type) (R : A -> A -> Prop) := forall x : A, ACC A R x.
 
19
 
 
20
 
 
21
Section Inverse_Image.
 
22
 
 
23
  Variables (A B : Type) (R : B -> B -> Prop) (f : A -> B).
 
24
 
 
25
  Definition Rof (x y : A) : Prop := R (f x) (f y).
 
26
 
 
27
  Remark ACC_lemma :
 
28
   forall y : B, ACC B R y -> forall x : A, y = f x -> ACC A Rof x.
 
29
    simple induction 1; intros.
 
30
    constructor; intros.
 
31
    apply (H1 (f y0)); trivial.
 
32
    elim H2 using eq_ind_r; trivial.
 
33
    Qed.
 
34
 
 
35
  Lemma ACC_inverse_image : forall x : A, ACC B R (f x) -> ACC A Rof x.
 
36
    intros; apply (ACC_lemma (f x)); trivial.
 
37
    Qed.
 
38
 
 
39
  Lemma WF_inverse_image : WF B R -> WF A Rof.
 
40
    red in |- *; intros; apply ACC_inverse_image; auto.
 
41
    Qed.
 
42
 
 
43
End Inverse_Image.
 
44
 
 
45
 
 
46
(* Remark: the paradox is written in Type, but also works in Prop or Set. *)
 
47
 
 
48
Section Burali_Forti_Paradox.
 
49
 
 
50
  Definition morphism (A : Type) (R : A -> A -> Prop) 
 
51
    (B : Type) (S : B -> B -> Prop) (f : A -> B) :=
 
52
    forall x y : A, R x y -> S (f x) (f y).
 
53
 
 
54
  (* The hypothesis of the paradox:
 
55
     assumes there exists an universal system of notations, i.e:
 
56
      - A type A0
 
57
      - An injection i0 from relations on any type into A0
 
58
      - The proof that i0 is injective modulo morphism 
 
59
   *)
 
60
  Variable A0 : Type.                     (* Type_i *)
 
61
  Variable i0 : forall X : Type, (X -> X -> Prop) -> A0. (* X: Type_j *)
 
62
  Hypothesis
 
63
    inj :
 
64
      forall (X1 : Type) (R1 : X1 -> X1 -> Prop) (X2 : Type)
 
65
        (R2 : X2 -> X2 -> Prop),
 
66
      i0 X1 R1 = i0 X2 R2 -> exists f : X1 -> X2, morphism X1 R1 X2 R2 f.
 
67
 
 
68
  (* Embedding of x in y: x and y are images of 2 well founded relations
 
69
     R1 and R2, the ordinal of R2 being strictly greater than that of R1.
 
70
   *)
 
71
  Record emb (x y : A0) : Prop := 
 
72
    {X1 : Type;
 
73
     R1 : X1 -> X1 -> Prop;
 
74
     eqx : x = i0 X1 R1;
 
75
     X2 : Type;
 
76
     R2 : X2 -> X2 -> Prop;
 
77
     eqy : y = i0 X2 R2;
 
78
     W2 : WF X2 R2;
 
79
     f : X1 -> X2;
 
80
     fmorph : morphism X1 R1 X2 R2 f;
 
81
     maj : X2;
 
82
     majf : forall z : X1, R2 (f z) maj}.
 
83
 
 
84
 
 
85
  Lemma emb_trans : forall x y z : A0, emb x y -> emb y z -> emb x z.
 
86
intros.
 
87
case H; intros.
 
88
case H0; intros.
 
89
generalize eqx0; clear eqx0.
 
90
elim eqy using eq_ind_r; intro.
 
91
case (inj _ _ _ _ eqx0); intros.
 
92
exists X1 R1 X3 R3 (fun x : X1 => f0 (x0 (f x))) maj0; trivial.
 
93
red in |- *; auto.
 
94
Defined.
 
95
 
 
96
 
 
97
  Lemma ACC_emb :
 
98
   forall (X : Type) (R : X -> X -> Prop) (x : X),
 
99
   ACC X R x ->
 
100
   forall (Y : Type) (S : Y -> Y -> Prop) (f : Y -> X),
 
101
   morphism Y S X R f -> (forall y : Y, R (f y) x) -> ACC A0 emb (i0 Y S).
 
102
simple induction 1; intros.
 
103
constructor; intros.
 
104
case H4; intros.
 
105
elim eqx using eq_ind_r.
 
106
case (inj X2 R2 Y S).
 
107
apply sym_eq; assumption.
 
108
 
 
109
intros.
 
110
apply H1 with (y := f (x1 maj)) (f := fun x : X1 => f (x1 (f0 x)));
 
111
 try red in |- *; auto.
 
112
Defined.
 
113
 
 
114
  (* The embedding relation is well founded *)
 
115
  Lemma WF_emb : WF A0 emb.
 
116
constructor; intros.
 
117
case H; intros.
 
118
elim eqx using eq_ind_r.
 
119
apply ACC_emb with (X := X2) (R := R2) (x := maj) (f := f); trivial.
 
120
Defined.
 
121
 
 
122
 
 
123
  (* The following definition enforces Type_j >= Type_i *)
 
124
  Definition Omega : A0 := i0 A0 emb.
 
125
 
 
126
 
 
127
Section Subsets.
 
128
 
 
129
  Variable a : A0.
 
130
 
 
131
  (* We define the type of elements of A0 smaller than a w.r.t embedding.
 
132
     The Record is in Type, but it is possible to avoid such structure. *)
 
133
  Record sub : Type :=  {witness : A0; emb_wit : emb witness a}.
 
134
 
 
135
  (* F is its image through i0 *)
 
136
  Definition F : A0 := i0 sub (Rof _ _ emb witness).
 
137
 
 
138
  (* F is embedded in Omega:
 
139
     - the witness projection is a morphism
 
140
     - a is an upper bound because emb_wit proves that witness is
 
141
       smaller than a.
 
142
   *)
 
143
  Lemma F_emb_Omega : emb F Omega.
 
144
exists sub (Rof _ _ emb witness) A0 emb witness a; trivial.
 
145
exact WF_emb.
 
146
 
 
147
red in |- *; trivial.
 
148
 
 
149
exact emb_wit.
 
150
Defined.
 
151
 
 
152
End Subsets.
 
153
 
 
154
 
 
155
  Definition fsub (a b : A0) (H : emb a b) (x : sub a) : 
 
156
    sub b := Build_sub _ (witness _ x) (emb_trans _ _ _ (emb_wit _ x) H).
 
157
 
 
158
  (* F is a morphism: a < b => F(a) < F(b)
 
159
      - the morphism from F(a) to F(b) is fsub above
 
160
      - the upper bound is a, which is in F(b) since a < b
 
161
   *)
 
162
  Lemma F_morphism : morphism A0 emb A0 emb F.
 
163
red in |- *; intros.
 
164
exists
 
165
 (sub x)
 
166
   (Rof _ _ emb (witness x))
 
167
   (sub y)
 
168
   (Rof _ _ emb (witness y))
 
169
   (fsub x y H)
 
170
   (Build_sub _ x H); trivial.
 
171
apply WF_inverse_image.
 
172
exact WF_emb.
 
173
 
 
174
unfold morphism, Rof, fsub in |- *; simpl in |- *; intros.
 
175
trivial.
 
176
 
 
177
unfold Rof, fsub in |- *; simpl in |- *; intros.
 
178
apply emb_wit.
 
179
Defined.
 
180
 
 
181
 
 
182
  (* Omega is embedded in itself:
 
183
     - F is a morphism
 
184
     - Omega is an upper bound of the image of F
 
185
   *)
 
186
  Lemma Omega_refl : emb Omega Omega.
 
187
exists A0 emb A0 emb F Omega; trivial.
 
188
exact WF_emb.
 
189
 
 
190
exact F_morphism.
 
191
 
 
192
exact F_emb_Omega.
 
193
Defined.
 
194
 
 
195
  (* The paradox is that Omega cannot be embedded in itself, since
 
196
     the embedding relation is well founded.
 
197
   *)
 
198
  Theorem Burali_Forti : False.
 
199
apply ACC_nonreflexive with A0 emb Omega.
 
200
apply WF_emb.
 
201
 
 
202
exact Omega_refl.
 
203
 
 
204
Defined.
 
205
 
 
206
End Burali_Forti_Paradox.
 
207
 
 
208
 
 
209
  (* The following type seems to satisfy the hypothesis of the paradox.
 
210
     But it does not!
 
211
   *)
 
212
  Record A0 : Type :=  (* Type_i' *)
 
213
    i0 {X0 : Type; R0 : X0 -> X0 -> Prop}. (* X0: Type_j' *)
 
214
 
 
215
 
 
216
  (* Note: this proof uses a large elimination of A0. *)
 
217
  Lemma inj :
 
218
   forall (X1 : Type) (R1 : X1 -> X1 -> Prop) (X2 : Type)
 
219
     (R2 : X2 -> X2 -> Prop),
 
220
   i0 X1 R1 = i0 X2 R2 -> exists f : X1 -> X2, morphism X1 R1 X2 R2 f.
 
221
intros.
 
222
change
 
223
  match i0 X1 R1, i0 X2 R2 with
 
224
  | i0 x1 r1, i0 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f
 
225
  end in |- *.
 
226
case H; simpl in |- *.
 
227
exists (fun x : X1 => x).
 
228
red in |- *; trivial.
 
229
Defined.
 
230
 
 
231
(* The following command raises 'Error: Universe Inconsistency'.
 
232
   To allow large elimination of A0, i0 must not be a large constructor.
 
233
   Hence, the constraint Type_j' < Type_i' is added, which is incompatible
 
234
   with the constraint j >= i in the paradox.
 
235
*)
 
236
 
 
237
  Definition Paradox : False := Burali_Forti A0 i0 inj.