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