-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathZFcofix.v
1274 lines (1075 loc) · 27 KB
/
ZFcofix.v
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
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
Require Import ZF ZFrelations ZFwfr ZFnats ZFord ZFstable.
(** Decreasing transfinite iteration of a monotonic operator
*)
Definition interb A x := inter(singl A ∪ x).
Lemma interb_def A a x :
x ∈ interb A a <->
(x ∈ A /\ forall y : set, y ∈ a -> x ∈ y).
unfold interb.
split; intros.
split.
apply inter_elim with (1:=H).
apply union2_intro1; apply singl_intro.
intros.
apply inter_elim with (1:=H).
apply union2_intro2; trivial.
destruct H.
apply inter_intro.
intros.
apply union2_elim in H1; destruct H1; auto.
apply singl_elim in H1; rewrite H1; trivial.
exists A.
apply union2_intro1; apply singl_intro.
Qed.
Lemma interb_bound A a : interb A a ⊆ A.
red; intros; apply interb_def in H; destruct H; trivial.
Qed.
Instance interb_morph : morph2 interb.
unfold interb; do 3 red; intros.
rewrite H,H0; reflexivity.
Qed.
Definition infb A I f := interb A (replf I f).
Lemma infb_morph : Proper (eq_set==>eq_set==>(eq_set==>eq_set)==>eq_set) infb.
unfold infb; do 4 red; intros.
apply interb_morph; trivial.
apply replf_morph; auto.
red; intros; apply H1; trivial.
Qed.
Lemma infb_ext A A' I I' f f':
A==A' -> I==I' -> eq_fun I f f' -> infb A I f== infb A' I' f'.
intros.
apply interb_morph; trivial.
apply replf_morph; auto.
Qed.
Lemma infb_ax A I f z :
ext_fun I f ->
(z ∈ infb A I f <->
(z ∈ A /\ forall x, x ∈ I -> z ∈ f x)).
unfold infb; intros.
rewrite interb_def.
apply and_iff_morphism; auto with *.
split; intros.
apply H0.
apply replf_intro with x; auto with *.
apply replf_elim in H1; trivial.
destruct H1 as (x,?,eqy); rewrite eqy; auto.
Qed.
Lemma infb_bound A I f : infb A I f ⊆ A.
apply interb_bound.
Qed.
Lemma infb_incl A I f x :
ext_fun I f ->
x ∈ I -> infb A I f ⊆ f x.
red; intros.
apply infb_ax in H1; trivial.
destruct H1; auto.
Qed.
Lemma infb_glb A I f a :
ext_fun I f ->
a ⊆ A ->
(forall x, x ∈ I -> a ⊆ f x) ->
a ⊆ infb A I f.
red; intros.
apply infb_ax; trivial.
split; intros; auto.
apply H1; trivial.
Qed.
Section CoTransfiniteIteration.
Variable A:set.
Variable F:set->set.
Hypothesis Fmorph : morph1 F.
Let G f o := infb A o (fun o' => F (f o')).
Let Gm : Proper ((eq_set ==> eq_set) ==> eq_set ==> eq_set) G.
do 3 red; intros.
apply infb_morph; auto with *.
red; intros; auto.
Qed.
Let Gmorph : forall o f f', eq_fun o f f' -> G f o == G f' o.
unfold G; intros.
apply infb_ext; auto with *.
red; intros; auto.
Qed.
Definition COTI := TR G.
Instance COTI_morph : morph1 COTI.
unfold COTI; do 2 red; intros.
apply TR_morph0; auto with *.
Qed.
Lemma COTI_fun_ext : forall x, ext_fun x (fun y => F (COTI y)).
do 2 red; intros.
apply Fmorph.
apply COTI_morph; trivial.
Qed.
Hint Resolve COTI_fun_ext.
Lemma COTI_eq : forall o,
isOrd o ->
COTI o == infb A o (fun o' => F (COTI o')).
intros.
unfold COTI.
apply TR_eqn; auto.
Qed.
Lemma COTI_intro o x :
isOrd o ->
x ∈ A ->
(forall o', lt o' o -> x ∈ F (COTI o')) ->
x ∈ COTI o.
intros.
rewrite COTI_eq; trivial.
apply infb_ax; auto.
Qed.
Lemma COTI_bound o : isOrd o -> COTI o ⊆ A.
intros.
rewrite COTI_eq; trivial.
apply infb_bound.
Qed.
Lemma COTI_elim : forall o x,
isOrd o ->
x ∈ COTI o ->
forall o', o' < o -> x ∈ F (COTI o').
intros.
rewrite COTI_eq in H0; trivial.
rewrite infb_ax in H0; auto.
destruct H0; auto.
Qed.
Lemma COTI_initial : COTI zero == A.
rewrite COTI_eq; auto.
apply incl_eq.
apply infb_bound.
red; intros; apply infb_ax; auto.
split; intros; trivial.
apply empty_ax in H0; contradiction.
Qed.
End CoTransfiniteIteration.
Local Hint Resolve COTI_fun_ext.
Global Instance COTI_morph_gen :
Proper (eq_set==>(eq_set==>eq_set)==>eq_set==>eq_set) COTI.
do 4 red; intros.
unfold COTI.
apply TR_morph; trivial.
do 2 red; intros.
apply infb_morph; trivial.
red; intros.
auto.
Qed.
Definition decreasing F :=
forall x y, isOrd x -> isOrd y -> y ⊆ x -> F x ⊆ F y.
Lemma COTI_mono A F : morph1 F -> decreasing (COTI A F).
do 2 red; intros.
apply COTI_intro; intros; auto.
revert H3; apply COTI_bound; trivial.
apply COTI_elim with (3:=H3); auto.
apply H2; trivial.
Qed.
(** * Elementary properties *)
Section IterMonotone.
Variable A : set.
Variable F : set -> set.
Variable Fmono : Proper (incl_set ==> incl_set) F.
Hypothesis Fbound : F A ⊆ A.
Let Fm := Fmono_morph _ Fmono.
Lemma COTI_incl : forall o, isOrd o ->
forall o', o' < o ->
COTI A F o ⊆ COTI A F o'.
intros.
apply COTI_mono; trivial; auto.
apply isOrd_inv with o; trivial.
Qed.
Lemma COTI_mono_succ0 : forall o,
isOrd o ->
COTI A F (osucc o) == A ∩ F (COTI A F o).
intros.
assert (Fext : ext_fun (osucc o) (fun o' => F (COTI A F o'))).
generalize (isOrd_succ _ H); auto.
rewrite COTI_eq; auto.
apply eq_set_ax; intros z.
rewrite infb_ax; auto.
rewrite inter2_def.
apply and_iff_morphism; auto with *.
split; intros.
apply H0; apply lt_osucc; trivial.
revert H0; apply Fmono; apply COTI_mono; auto.
apply isOrd_inv with (osucc o); auto.
apply olts_le in H1; trivial.
Qed.
Lemma COTI_mono_succ : forall o,
isOrd o ->
COTI A F (osucc o) == F (COTI A F o).
intros.
rewrite COTI_mono_succ0; trivial.
apply eq_set_ax; intros z.
rewrite inter2_def.
split;[destruct 1; auto|intros].
split; auto.
apply Fbound.
revert H0; apply Fmono; apply COTI_bound; trivial.
Qed.
Lemma COTI_inv o x :
isOrd o ->
x ∈ COTI A F o ->
forall o', o' ∈ o -> x ∈ COTI A F (osucc o').
intros.
rewrite COTI_mono_succ.
2:apply isOrd_inv with o; trivial.
apply COTI_elim with (3:=H0); auto.
Qed.
Lemma COTI_mono_eq : forall o,
isOrd o ->
COTI A F o == infb A o (fun o' => COTI A F (osucc o')).
intros.
rewrite COTI_eq; auto.
apply infb_ext; auto with *.
red; intros.
rewrite <- COTI_mono_succ.
rewrite H1; reflexivity.
apply isOrd_inv with o; trivial.
Qed.
Lemma COTI_post_fix : forall fx o,
isOrd o ->
fx ⊆ A ->
fx ⊆ F fx ->
fx ⊆ COTI A F o.
intros.
induction H using isOrd_ind; intros.
red; intros.
apply COTI_intro; auto.
intros.
apply H1 in H4.
revert H4; apply Fmono; auto.
Qed.
(** Stability of ordinal-indexed families *)
(*
Definition stable_ord := stable_class isOrd.
Lemma COTI_stable K :
Proper (eq_set ==> iff) K ->
stable_class K F ->
(forall o, isOrd o -> K (COTI A F o)) ->
stable_ord (COTI A F).
intros Km Fs KTI.
cut (forall o, isOrd o ->
forall X, o == inter X ->
(forall x, x ∈ X -> isOrd x) ->
inter (replf X (TI F)) ⊆ TI F (inter X)).
do 2 red; intros.
apply H with (inter X); auto with *.
apply isOrd_inter; auto.
induction 1 using isOrd_ind; red; intros.
assert (eX : ext_fun X (TI F)).
red; red; intros; apply TI_morph; trivial.
assert (eN : forall X, ext_fun X F).
red; red; intros; apply Fm; trivial.
pose (Y := subset (union X) (fun y => z ∈ F (TI F y))).
assert (oY : forall y, y ∈ Y -> isOrd y).
unfold Y; intros.
apply subset_elim1 in H5.
apply union_elim in H5; destruct H5.
eauto using isOrd_inv.
assert (eY : ext_fun Y (TI F)).
red; red; intros.
apply TI_morph; trivial.
assert (wX : exists w, w ∈ X).
destruct inter_non_empty with (1:=H4).
rewrite replf_ax in H5; trivial.
destruct H5.
exists x0; trivial.
destruct wX as (wx,wX).
assert (wY : exists w, w ∈ Y).
assert (z ∈ TI F wx).
apply inter_elim with (1:=H4).
rewrite replf_ax; trivial.
exists wx; auto with *.
apply TI_elim in H5; auto.
destruct H5.
exists x.
apply subset_intro; trivial.
apply union_intro with wx; trivial.
destruct wY as (wy,wY).
assert (ltY : lt (inter Y) (inter X)).
apply inter_intro; eauto.
intros.
assert (z ∈ TI F y0).
apply inter_elim with (1:=H4).
rewrite replf_ax; trivial.
exists y0; auto with *.
apply TI_elim in H6; auto.
destruct H6.
apply isOrd_plump with x; auto.
apply isOrd_inter; auto.
red; intros.
apply inter_elim with (1:=H8).
apply subset_intro; trivial.
apply union_intro with y0; trivial.
assert (inter (replf Y (TI F)) ⊆ TI F (inter Y)).
apply H1 with (inter Y); auto with *.
rewrite H2; trivial.
apply TI_intro with (inter Y); auto.
apply isOrd_inter; auto.
apply Fmono with (1:=H5).
apply Fs.
intros.
rewrite replf_ax in H6; auto with *.
destruct H6.
rewrite H7; auto.
apply inter_intro.
intros.
rewrite replf_ax in H6; trivial.
destruct H6.
rewrite replf_ax in H6; trivial.
destruct H6.
apply subset_elim2 in H6; destruct H6.
setoid_replace y0 with (F (TI F x1)); trivial.
rewrite H7; apply Fm.
rewrite H8; apply TI_morph; trivial.
exists (F (TI F wy)).
rewrite replf_ax; trivial.
exists (TI F wy); auto with *.
rewrite replf_ax; trivial.
exists wy; auto with *.
Qed.
*)
(** * Case of a bounded monotonic operator
*)
(** The intersection of all stages. We will show it is a fixpoint. *)
Definition COFfix := subset A (fun a => forall o, isOrd o -> a ∈ COTI A F o).
Lemma COFfix_inA : COFfix ⊆ A.
red; intros.
apply subset_elim1 in H; trivial.
Qed.
Lemma COTI_Ffix : forall o, isOrd o -> COFfix ⊆ COTI A F o.
intros.
apply isOrd_ind with (2:=H); intros.
red; intros.
apply COTI_intro; auto with *.
apply COFfix_inA; trivial.
intros.
rewrite <- COTI_mono_succ; auto.
2:apply isOrd_inv with y; trivial.
apply subset_ax in H3; destruct H3.
destruct H5 as (z',eqz,?).
rewrite eqz; eauto using isOrd_inv.
Qed.
Lemma COFfix_def : forall a, a ∈ COFfix <-> (forall o, isOrd o -> a ∈ COTI A F o).
unfold COFfix; intros.
rewrite subset_ax.
split; intros.
destruct H.
destruct H1.
rewrite H1; auto.
split.
generalize (H _ isOrd_zero).
apply COTI_bound; auto.
exists a; auto with *.
Qed.
(*
(** Subterms of [a] *)
Definition fsub a :=
subset Ffix (fun b => forall X, X ⊆ Ffix -> a ∈ F X -> b ∈ X).
Instance fsub_morph : morph1 fsub.
unfold fsub; do 2 red; intros.
apply subset_morph; auto with *.
red; intros.
apply fa_morph; intro X.
rewrite H; reflexivity.
Qed.
Lemma fsub_elim : forall x y o,
isOrd o ->
y ∈ TI F o ->
x ∈ fsub y ->
exists2 o', lt o' o & x ∈ TI F o'.
intros.
unfold fsub in H1; rewrite subset_ax in H1.
destruct H1 as (?,(x',?,?)).
apply TI_elim in H0; auto.
destruct H0.
exists x0; trivial.
rewrite H2; apply H3; trivial.
apply TI_Ffix.
apply isOrd_inv with o; trivial.
Qed.
Lemma Ffix_fsub_inv : forall x y,
x ∈ Ffix ->
y ∈ fsub x ->
y ∈ Ffix.
intros.
apply subset_elim1 in H0; trivial.
Qed.
(** Functions defined by recursion on subterms *)
Section Iter.
Variable G : (set -> set) -> set -> set.
Hypothesis Gm : forall x x' g g',
x ∈ Ffix ->
eq_fun (fsub x) g g' ->
x == x' -> G g x == G g' x'.
Definition G' F a :=
cond_set (a ∈ Ffix) (G F a).
Lemma G'm : Proper ((eq_set==>eq_set)==>eq_set==>eq_set) G'.
do 3 red; intros.
apply cond_set_morph2.
rewrite H0; reflexivity.
intros.
apply Gm; trivial.
red; intros.
apply H; trivial.
Qed.
Lemma G'ext : forall x x' g g',
x ∈ Ffix ->
eq_fun (fsub x) g g' ->
x == x' -> G' g x == G' g' x'.
intros.
apply cond_set_morph.
rewrite H1; reflexivity.
apply Gm; trivial.
Qed.
Definition Fix_rec := WFR (fun b a => b ∈ fsub a) G'.
Instance Fix_rec_morph0 : morph1 Fix_rec.
do 2 red; intros.
apply WFR_morph0; auto with *.
Qed.
(*
Lemma fsub_acc o x:
isOrd o ->
x ∈ TI F o ->
Acc (fun b a => b ∈ fsub a) x.
apply Ffix_def in H1; destruct H1 as (o',oo',tyx).
intros oo; revert x; elim oo using isOrd_ind; intros.
constructor; intros.
destruct fsub_elim with (2:=H2) (3:=H3) as (z,lty,tyy0); trivial.
eauto.
Qed.
*)
Lemma Fr_eqn : forall a o,
isOrd o ->
a ∈ TI F o ->
Fix_rec a == G Fix_rec a.
intros.
transitivity (G' Fix_rec a).
unfold Fix_rec.
apply WFR_eqn_gen; intros.
clear; do 3 red; intros; rewrite H,H0; reflexivity.
apply G'm.
apply G'ext; auto with *.
apply Ffix_def.
exists o; trivial.
revert a H0; elim H using isOrd_ind; intros.
constructor; intros.
destruct fsub_elim with (2:=H3) (3:=H4) as (z,ltx,tyy0); eauto.
unfold G'; apply cond_set_ok.
apply TI_Ffix in H0; trivial.
Qed.
Lemma Fix_rec_typ U2 a :
(forall x g, ext_fun (fsub x) g -> x ∈ Ffix ->
(forall y, y ∈ fsub x -> g y ∈ U2) -> G g x ∈ U2) ->
a ∈ Ffix ->
Fix_rec a ∈ U2.
intros.
rewrite Ffix_def in H0; destruct H0.
revert a H1.
induction H0 using isOrd_ind; intros.
rewrite Fr_eqn with (2:=H3); trivial.
apply H.
do 2 red; intros.
apply Fix_rec_morph0; trivial.
apply TI_Ffix with y; trivial.
intros.
apply fsub_elim with (o:=y) in H4; trivial.
destruct H4.
apply H2 with x0; trivial.
Qed.
End Iter.
Definition F_a g x := osup (fsub x) (fun a => osucc (g a)).
Lemma F_a_morph : forall x x' g g',
eq_fun (fsub x) g g' ->
x == x' -> F_a g x == F_a g' x'.
unfold F_a; intros.
apply osup_morph.
rewrite H0; reflexivity.
red; intros.
apply osucc_morph; apply H; trivial.
Qed.
Hint Resolve F_a_morph.
Lemma Fe1 : forall X, ext_fun X (fun b => osucc (Fix_rec F_a b)).
red; red; intros.
rewrite H0; reflexivity.
Qed.
Hint Resolve Fe1.
Lemma F_a_ord : forall a, a ∈ Ffix -> isOrd (Fix_rec F_a a).
intros.
rewrite Ffix_def in H; destruct H.
revert a H0; apply isOrd_ind with (2:=H); intros.
rewrite Fr_eqn with (o:=y); auto.
apply isOrd_osup; trivial.
intros.
apply isOrd_succ.
destruct fsub_elim with (2:=H3) (3:=H4); trivial.
eauto.
Qed.
Hint Resolve F_a_ord.
(** We need stability to prove that Ffix is a fixpoint *)
Hypothesis Fstab : stable_class (fun X => X ⊆ Ffix) F.
Lemma F_intro : forall w,
isOrd w ->
forall a, a ∈ TI F w ->
a ∈ F (fsub a).
intros.
pose (F1a := subset (power Ffix) (fun X => a ∈ F X)).
assert (fx_ok : Ffix ∈ F1a).
apply subset_intro.
apply power_intro; trivial.
apply TI_elim in H0; auto.
destruct H0.
revert H1; apply Fmono.
apply TI_Ffix; trivial.
apply isOrd_inv with w; trivial.
assert (inter (replf F1a (fun X => X)) ⊆ fsub a).
red; intros.
apply subset_intro.
apply inter_elim with (1:=H1).
rewrite replf_ax.
2:red;red;auto.
exists Ffix; auto with *.
intros.
apply inter_elim with (1:=H1).
rewrite replf_ax.
2:red;red;auto.
exists X; auto with *.
apply subset_intro; trivial.
apply power_intro; trivial.
apply Fmono in H1.
apply H1.
apply Fstab.
intros.
rewrite replf_ax in H2.
2:do 2 red; trivial.
destruct H2.
apply subset_elim1 in H2.
rewrite H3; red; intros.
apply power_elim with (1:=H2); trivial.
apply TI_elim in H0; auto.
destruct H0.
apply inter_intro.
intros.
rewrite replf_ax in H3; auto.
destruct H3 as (x',?,?).
rewrite replf_ax in H3.
2:do 2 red; trivial.
destruct H3 as (x'',?,?).
rewrite H4; rewrite H5.
apply subset_elim2 in H3; destruct H3.
rewrite H3; trivial.
exists (F Ffix).
rewrite replf_ax.
2:red;red;auto.
exists Ffix; auto with *.
rewrite replf_ax.
2:red;red;trivial.
exists Ffix; auto with *.
Qed.
Lemma F_a_tot : forall a,
a ∈ Ffix ->
a ∈ TI F (osucc (Fix_rec F_a a)).
intros.
rewrite Ffix_def in H; destruct H.
revert a H0; apply isOrd_ind with (2:=H); intros.
assert (ao : isOrd (Fix_rec F_a a)).
apply F_a_ord; rewrite Ffix_def; exists y; trivial.
rewrite TI_mono_succ; auto.
assert (fsub a ⊆ TI F (Fix_rec F_a a)).
red; intros.
destruct fsub_elim with (2:=H3) (3:=H4); trivial.
assert (xo : isOrd x0).
apply isOrd_inv with y; trivial.
assert (z ∈ TI F (osucc (Fix_rec F_a z))).
apply H2 with x0; trivial.
revert H7; apply TI_mono; auto.
apply isOrd_succ; apply F_a_ord; rewrite Ffix_def; exists x0; trivial.
red; intros.
rewrite Fr_eqn with (o:=y); auto.
unfold F_a.
apply osup_intro with (x:=z); trivial.
apply Fmono in H4.
apply H4.
apply F_intro with y; trivial.
Qed.
(** The closure ordinal *)
Definition Ffix_ord :=
osup Ffix (fun a => osucc (Fix_rec F_a a)).
Lemma Ffix_o_o : isOrd Ffix_ord.
apply isOrd_osup; auto.
Qed.
Hint Resolve Ffix_o_o.
Lemma Ffix_post : forall a,
a ∈ Ffix ->
a ∈ TI F Ffix_ord.
intros.
apply TI_intro with (Fix_rec F_a a); auto.
apply osup_intro with (x:=a); trivial.
apply lt_osucc; auto.
rewrite <- TI_mono_succ; auto.
apply F_a_tot; trivial.
Qed.
Lemma TI_clos_stages o : isOrd o -> TI F o ⊆ TI F Ffix_ord.
intros.
transitivity Ffix.
apply TI_Ffix; trivial.
red; intros; apply Ffix_post; trivial.
Qed.
Lemma TI_clos_fix_eqn : TI F Ffix_ord == F (TI F Ffix_ord).
apply eq_set_ax; intros z.
rewrite <- TI_mono_succ; trivial.
split; intros.
revert H; apply TI_incl; auto.
apply TI_clos_stages in H; auto.
Qed.
Lemma Ffix_closure : Ffix == TI F Ffix_ord.
apply incl_eq.
red; intros; apply Ffix_post; trivial.
apply TI_Ffix; trivial.
Qed.
(** We prove Ffix is a fixpoint *)
Lemma Ffix_eqn : Ffix == F Ffix.
rewrite Ffix_closure.
apply TI_clos_fix_eqn.
Qed.
(*BEGIN alt*)
(** Functions defined by recursion on subterms *)
Section Iter2.
Variable G : (set -> set) -> set -> set.
Hypothesis Gm : forall x x' g g',
x ∈ Ffix ->
eq_fun (fsub x) g g' ->
x == x' -> G g x == G g' x'.
Definition G'' F a :=
cond_set (a ∈ Ffix) (G F a).
Lemma G''m : Proper ((eq_set==>eq_set)==>eq_set==>eq_set) G''.
do 3 red; intros.
apply cond_set_morph2.
rewrite H0; reflexivity.
intros.
apply Gm; trivial.
red; intros.
apply H; trivial.
Qed.
Lemma G''ext : forall x x' g g',
(x ∈ Ffix -> eq_fun (fsub x) g g') ->
x == x' -> G'' g x == G'' g' x'.
intros.
apply cond_set_morph2.
rewrite H0; reflexivity.
intros.
apply Gm; auto.
Qed.
(*
Lemma G''ext : forall x x' g g',
x ∈ Ffix ->
eq_fun (fsub x) g g' ->
x == x' -> G'' g x == G'' g' x'.
intros.
apply cond_set_morph.
rewrite H1; reflexivity.
apply Gm; trivial.
Qed.
*)
Definition Fix_rec' :=
WFR (fun b a => b ∈ Ffix /\ b ∈ fsub a) G''.
Instance Fix_rec_morph0' : morph1 Fix_rec'.
do 2 red; intros.
apply WFR_morph; auto with *.
do 2 red; intros.
rewrite H0,H1; reflexivity.
apply G''m.
Qed.
(*
Lemma fsub_acc o x:
isOrd o ->
x ∈ TI F o ->
Acc (fun b a => b ∈ fsub a) x.
apply Ffix_def in H1; destruct H1 as (o',oo',tyx).
intros oo; revert x; elim oo using isOrd_ind; intros.
constructor; intros.
destruct fsub_elim with (2:=H2) (3:=H3) as (z,lty,tyy0); trivial.
eauto.
Qed.
*)
Lemma Fr_eqn' : forall a o,
isOrd o ->
a ∈ TI F o ->
Fix_rec' a == G Fix_rec' a.
intros.
transitivity (G'' Fix_rec' a).
unfold Fix_rec'.
apply WFR_eqn; intros.
do 3 red; intros.
rewrite H1,H2; reflexivity.
apply G''m.
apply G''ext; auto with *.
clear H1; red; intros.
apply H2; auto.
split; trivial.
apply Ffix_fsub_inv with x; trivial.
revert a H0.
elim H using isOrd_ind; intros.
constructor.
destruct 1; trivial.
destruct fsub_elim with (2:=H3) (3:=H5) as (z,ltx,tyy0); eauto.
unfold G''; apply cond_set_ok.
apply TI_Ffix in H0; trivial.
Qed.
Lemma Fix_rec_typ' U2 a :
(forall x g, ext_fun (fsub x) g -> x ∈ Ffix ->
(forall y, y ∈ fsub x -> g y ∈ U2) -> G g x ∈ U2) ->
a ∈ Ffix ->
Fix_rec' a ∈ U2.
intros.
rewrite Ffix_def in H0; destruct H0.
revert a H1.
induction H0 using isOrd_ind; intros.
rewrite Fr_eqn' with (2:=H3); trivial.
apply H.
do 2 red; intros.
apply Fix_rec_morph0'; trivial.
apply TI_Ffix with y; trivial.
intros.
apply fsub_elim with (o:=y) in H4; trivial.
destruct H4.
apply H2 with x0; trivial.
Qed.
End Iter2.
Lemma Fe1' : forall X, ext_fun X (fun b => osucc (Fix_rec' F_a b)).
red; red; intros.
rewrite H0; reflexivity.
Qed.
Hint Resolve Fe1'.
Lemma F_a_ord' : forall a, a ∈ Ffix -> isOrd (Fix_rec' F_a a).
intros.
rewrite Ffix_def in H; destruct H.
revert a H0; apply isOrd_ind with (2:=H); intros.
rewrite Fr_eqn' with (o:=y); auto.
apply isOrd_osup; trivial.
intros.
apply isOrd_succ.
destruct fsub_elim with (2:=H3) (3:=H4); trivial.
eauto.
Qed.
Hint Resolve F_a_ord'.
Lemma F_a_tot' : forall a,
a ∈ Ffix ->
a ∈ TI F (osucc (Fix_rec' F_a a)).
intros.
rewrite Ffix_def in H; destruct H.
revert a H0; apply isOrd_ind with (2:=H); intros.
assert (ao : isOrd (Fix_rec' F_a a)).
apply F_a_ord'; rewrite Ffix_def; exists y; trivial.
rewrite TI_mono_succ; auto.
assert (fsub a ⊆ TI F (Fix_rec' F_a a)).
red; intros.
destruct fsub_elim with (2:=H3) (3:=H4); trivial.
assert (xo : isOrd x0).
apply isOrd_inv with y; trivial.
assert (z ∈ TI F (osucc (Fix_rec' F_a z))).
apply H2 with x0; trivial.
revert H7; apply TI_mono; auto.
apply isOrd_succ; apply F_a_ord'; rewrite Ffix_def; exists x0; trivial.
red; intros.
rewrite Fr_eqn' with (o:=y); auto.
unfold F_a.
apply osup_intro with (x:=z); trivial.
apply Fmono in H4.
apply H4.
apply F_intro with y; trivial.
Qed.
(** The closure ordinal *)
Definition Ffix_ord' :=
osup Ffix (fun a => osucc (Fix_rec' F_a a)).
Lemma Ffix_o_o' : isOrd Ffix_ord'.
apply isOrd_osup; auto.
Qed.
Hint Resolve Ffix_o_o'.
Lemma Ffix_post' : forall a,
a ∈ Ffix ->
a ∈ TI F Ffix_ord'.
intros.
apply TI_intro with (Fix_rec' F_a a); auto.
apply osup_intro with (x:=a); trivial.
apply lt_osucc; auto.
rewrite <- TI_mono_succ; auto.
apply F_a_tot'; trivial.
Qed.
Lemma TI_clos_stages' o : isOrd o -> TI F o ⊆ TI F Ffix_ord'.
intros.
transitivity Ffix.
apply TI_Ffix; trivial.
red; intros; apply Ffix_post'; trivial.
Qed.
Lemma TI_clos_fix_eqn' : TI F Ffix_ord' == F (TI F Ffix_ord').
apply eq_set_ax; intros z.
rewrite <- TI_mono_succ; trivial.
split; intros.
revert H; apply TI_incl; auto.
apply TI_clos_stages' in H; auto.
Qed.
Lemma Ffix_closure' : Ffix == TI F Ffix_ord'.
apply incl_eq.
red; intros; apply Ffix_post'; trivial.
apply TI_Ffix; trivial.
Qed.
(** We prove Ffix is a fixpoint *)
Lemma Ffix_eqn' : Ffix == F Ffix.
rewrite Ffix_closure'.
apply TI_clos_fix_eqn'.
Qed.
(*END*)
End BoundedOperator.
*)
End IterMonotone.
(*
Lemma TI_mono_gen G G' o o' :
morph1 G ->
morph1 G' ->
(incl_set==>incl_set)%signature G G' ->
isOrd o ->
isOrd o' ->
o ⊆ o' ->
TI G o ⊆ TI G' o'.
intros.
revert o' H3 H4.
elim H2 using isOrd_ind; intros.
red; intros.
apply TI_elim in H8; trivial.
destruct H8 as (y',y'o,?).
apply TI_intro with y'; auto.
apply H7; trivial.
revert H8; apply H1.
apply H5; auto with *.
apply isOrd_inv with y; trivial.
Qed.
Instance Ffix_morph : Proper ((eq_set==>eq_set)==>eq_set==>eq_set) Ffix.
do 3 red; intros.
unfold Ffix.
apply subset_morph; trivial.
red; intros.
apply ex2_morph'; intros.
reflexivity.
apply in_set_morph.
reflexivity.