aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/1918.v
blob: 9d92fe12b8f506378377d762a664c23326b6d785 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
(** Occur-check for Meta (up to delta) *)

(** LNMItPredShort.v Version 2.0 July 2008 *)
(** does not need impredicative Set, runs under V8.2, tested with SVN 11296 *)

(** Copyright Ralph Matthes, I.R.I.T.,  C.N.R.S. & University of Toulouse*)


Set Implicit Arguments.

(** the universe of all monotypes *)
Definition k0 := Set.

(** the type of all type transformations *)
Definition k1 := k0 -> k0.

(** the type of all rank-2 type transformations *)
Definition k2 := k1 -> k1.

(** polymorphic identity *)
Definition id : forall (A:Set), A -> A := fun A x => x.

(** composition *)
Definition comp (A B C:Set)(g:B->C)(f:A->B) : A->C := fun x => g (f x).

Infix "o" := comp (at level 90).

Definition sub_k1 (X Y:k1) : Type :=
     forall A:Set, X A -> Y A.

Infix "c_k1" := sub_k1 (at level 60).

(** monotonicity *)
Definition mon (X:k1) : Type := forall (A B:Set), (A -> B) -> X A -> X B.

(** extensionality *)
Definition ext (X:k1)(h: mon X): Prop :=
  forall (A B:Set)(f g:A -> B),
        (forall a, f a = g a) -> forall r, h _ _ f r = h _ _ g r.

(** first functor law *)
Definition fct1 (X:k1)(m: mon X) : Prop :=
  forall (A:Set)(x:X A), m _ _ (id(A:=A)) x = x.

(** second functor law *)
Definition fct2 (X:k1)(m: mon X) : Prop :=
 forall (A B C:Set)(f:A -> B)(g:B -> C)(x:X A),
       m _ _ (g o f) x = m _ _ g (m _ _ f x).

(** pack up the good properties of the approximation into
  the notion of an extensional functor *)
Record EFct (X:k1) : Type := mkEFct
  { m : mon X;
     e : ext m;
     f1 : fct1 m;
     f2 : fct2 m }.

(** preservation of extensional functors *)
Definition pEFct (F:k2) : Type :=
  forall (X:k1), EFct X -> EFct (F X).


(** we show some closure properties of pEFct, depending on such properties
      for EFct *)

Definition moncomp (X Y:k1)(mX:mon X)(mY:mon Y): mon (fun A => X(Y A)).
Proof.
  red.
  intros A B f x.
  exact (mX (Y A)(Y B) (mY A B f) x).
Defined.

(** closure under composition *)
Lemma compEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X(Y A)).
Proof.
  intros ef1 ef2.
  apply (mkEFct(m:=moncomp (m ef1) (m ef2))); red; intros; unfold moncomp.
(* prove ext *)
  apply (e ef1).
  intro.
  apply (e ef2); trivial.
(* prove fct1 *)
  rewrite (e ef1 (m ef2 (id (A:=A))) (id(A:=Y A))).
  apply (f1 ef1).
  intro.
  apply (f1 ef2).
(* prove fct2 *)
  rewrite (e ef1 (m ef2 (g o f))((m ef2 g)o(m ef2 f))).
  apply (f2 ef1).
  intro.
  unfold comp at 2.
  apply (f2 ef2).
Defined.

Corollary comppEFct (F G:k2): pEFct F -> pEFct G ->
      pEFct (fun X A => F X (G X A)).
Proof.
  red.
  intros.
  apply compEFct; auto.
Defined.

(** closure under sums *)
Lemma sumEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A + Y A)%type.
Proof.
  intros ef1 ef2.
  set (m12:=fun (A B:Set)(f:A->B) x => match x with
    | inl y => inl _ (m ef1 f y)
    | inr y => inr _ (m ef2 f y)
  end).
  apply (mkEFct(m:=m12)); red; intros.
(* prove ext *)
  destruct r.
  simpl.
  apply (f_equal (fun x=>inl (A:=X B) (Y B) x)).
  apply (e ef1); trivial.
  simpl.
  apply (f_equal (fun x=>inr (X B) (B:=Y B) x)).
  apply (e ef2); trivial.
(* prove fct1 *)
  destruct x.
  simpl.
  apply (f_equal (fun x=>inl (A:=X A) (Y A) x)).
  apply (f1 ef1).
  simpl.
  apply (f_equal (fun x=>inr (X A) (B:=Y A) x)).
  apply (f1 ef2).
(* prove fct2 *)
  destruct x.
  simpl.
  rewrite (f2 ef1); reflexivity.
  simpl.
  rewrite (f2 ef2); reflexivity.
Defined.

Corollary sumpEFct (F G:k2): pEFct F -> pEFct G ->
      pEFct (fun X A => F X A + G X A)%type.
Proof.
  red.
  intros.
  apply sumEFct; auto.
Defined.

(** closure under products *)
Lemma prodEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A * Y A)%type.
Proof.
  intros ef1 ef2.
  set (m12:=fun (A B:Set)(f:A->B) x => match x with
    (x1,x2) => (m ef1 f x1, m ef2 f x2) end).
  apply (mkEFct(m:=m12)); red; intros.
(* prove ext *)
  destruct r as [x1 x2].
  simpl.
  apply injective_projections; simpl.
  apply (e ef1); trivial.
  apply (e ef2); trivial.
(* prove fct1 *)
  destruct x as [x1 x2].
  simpl.
  apply injective_projections; simpl.
  apply (f1 ef1).
  apply (f1 ef2).
(* prove fct2 *)
  destruct x as [x1 x2].
  simpl.
  apply injective_projections; simpl.
  apply (f2 ef1).
  apply (f2 ef2).
Defined.

Corollary prodpEFct (F G:k2): pEFct F -> pEFct G ->
      pEFct (fun X A => F X A * G X A)%type.
Proof.
  red.
  intros.
  apply prodEFct; auto.
Defined.

(** the identity in k2 preserves extensional functors *)
Lemma idpEFct: pEFct (fun X => X).
Proof.
  red.
  intros.
  assumption.
Defined.

(** a variant for the eta-expanded identity *)
Lemma idpEFct_eta: pEFct (fun X A => X A).
Proof.
  red.
  intros X ef.
  destruct ef as [m0 e0 f01 f02].
  change (mon X) with (mon (fun A => X A)) in m0.
  apply (mkEFct (m:=m0) e0 f01 f02).
Defined.

(** the identity in k1 "is" an extensional functor *)
Lemma idEFct: EFct (fun A => A).
Proof.
  set (mId:=fun A B (f:A->B)(x:A) => f x).
  apply (mkEFct(m:=mId)).
  red.
  intros.
  unfold mId.
  apply H.
  red.
  reflexivity.
  red.
  reflexivity.
Defined.

(** constants in k2 *)
Lemma constpEFct (X:k1): EFct X  -> pEFct (fun _ => X).
Proof.
  red.
  intros.
  assumption.
Defined.

(** constants in k1 *)
Lemma constEFct (C:Set): EFct (fun _ => C).
Proof.
  set (mC:=fun A B (f:A->B)(x:C) => x).
  apply (mkEFct(m:=mC)); red; intros; unfold mC; reflexivity.
Defined.


(** the option type *)
Lemma optionEFct: EFct (fun (A:Set) => option A).
  apply (mkEFct (X:=fun (A:Set) => option A)(m:=option_map)); red; intros.
  destruct r.
  simpl.
  rewrite H.
  reflexivity.
  reflexivity.
  destruct x; reflexivity.
  destruct x; reflexivity.
Defined.


(** natural transformations from (X,mX) to (Y,mY) *)
Definition NAT(X Y:k1)(j:X c_k1 Y)(mX:mon X)(mY:mon Y) : Prop :=
  forall (A B:Set)(f:A->B)(t:X A), j B (mX A B f t) = mY _ _ f (j A t).


Module Type LNMIt_Type.

Parameter F:k2.
Parameter FpEFct: pEFct F.
Parameter mu20: k1.
Definition  mu2: k1:= fun A => mu20 A.
Parameter mapmu2: mon mu2.
Definition MItType: Type :=
  forall G : k1, (forall X : k1, X c_k1 G -> F X c_k1 G) -> mu2 c_k1 G.
Parameter MIt0 : MItType.
Definition MIt : MItType:= fun G s A t => MIt0 s t.
Definition InType : Type :=
    forall (X:k1)(ef:EFct X)(j: X c_k1 mu2),
        NAT j (m ef) mapmu2 -> F X c_k1 mu2.
Parameter In : InType.
Axiom mapmu2Red : forall (A:Set)(X:k1)(ef:EFct X)(j: X c_k1 mu2)
    (n: NAT j (m ef) mapmu2)(t: F X A)(B:Set)(f:A->B),
            mapmu2 f (In ef n t) = In ef n (m (FpEFct ef) f t).
Axiom MItRed : forall (G : k1)
  (s : forall X : k1, X c_k1 G -> F X c_k1 G)(X : k1)(ef:EFct X)(j: X c_k1 mu2)
      (n: NAT j (m ef) mapmu2)(A:Set)(t:F X A),
     MIt s (In ef n t) = s X (fun A => (MIt s (A:=A)) o (j A)) A t.
Definition mu2IndType : Prop :=
  forall (P : (forall A : Set, mu2 A -> Prop)),
       (forall (X : k1)(ef:EFct X)(j : X c_k1 mu2)(n: NAT j (m ef) mapmu2),
          (forall (A : Set) (x : X A), P A (j A x)) ->
        forall (A:Set)(t : F X A), P A (In ef n t)) ->
    forall (A : Set) (r : mu2 A), P A r.
Axiom mu2Ind : mu2IndType.

End LNMIt_Type.

(** BushDepPredShort.v Version 0.2 July 2008 *)
(** does not need impredicative Set, produces stack overflow under V8.2, tested
with SVN 11296 *)

(** Copyright  Ralph Matthes, I.R.I.T.,  C.N.R.S. & University of Toulouse *)

Set Implicit Arguments.

Require Import List.

Definition listk1 (A:Set) : Set := list A.
Open Scope type_scope.

Definition BushF(X:k1)(A:Set) :=  unit + A  * X (X A).

Definition bushpEFct : pEFct BushF.
Proof.
  unfold BushF.
  apply sumpEFct.
  apply constpEFct.
  apply constEFct.
  apply prodpEFct.
  apply constpEFct.
  apply idEFct.
  apply comppEFct.
  apply idpEFct.
  apply idpEFct_eta.
Defined.

Module Type BUSH := LNMIt_Type with Definition F:=BushF
                                                with Definition FpEFct :=
bushpEFct.

Module Bush (BushBase:BUSH).

Definition Bush : k1 := BushBase.mu2.

Definition bush : mon Bush := BushBase.mapmu2.

End Bush.


Definition Id : k1 := fun X => X.

Fixpoint Pow (X:k1)(k:nat){struct k}:k1:=
  match k with 0 => Id
             |  S k' => fun A => X (Pow X k' A)
  end.

Fixpoint POW  (k:nat)(X:k1)(m:mon X){struct k} : mon (Pow X k) :=
  match k return mon (Pow X k)
      with 0 => fun _ _ f  => f
     |  S k' => fun _ _ f  => m _ _ (POW k' m f)
   end.

Module Type BushkToList_Type.

Declare Module Import BP: BUSH.
Definition F:=BushF.
Definition FpEFct:= bushpEFct.
Definition mu20 := mu20.
Definition mu2 := mu2.
Definition mapmu2 := mapmu2.
Definition MItType:= MItType.
Definition MIt0 := MIt0.
Definition MIt := MIt.
Definition InType := InType.
Definition In := In.
Definition mapmu2Red:=mapmu2Red.
Definition MItRed:=MItRed.
Definition mu2IndType:=mu2IndType.
Definition mu2Ind:=mu2Ind.

Definition  Bush:= mu2.
Module BushM := Bush BP.

Parameter BushkToList: forall(k:nat)(A:k0)(t:Pow Bush k A), list A.
Axiom BushkToList0: forall(A:k0)(t:Pow Bush 0 A), BushkToList 0 A t = t::nil.

End BushkToList_Type.

Module BushDep (BushkToListM:BushkToList_Type).

Module Bush := Bush BushkToListM.

Import Bush.
Import BushkToListM.


Lemma BushkToList0NAT: NAT(Y:=listk1) (BushkToList 0) (POW 0 bush) map.
Proof.
  red.
  intros.
  simpl.
  rewrite BushkToList0.
(* stack overflow for coqc and coqtop *)


Abort.