-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy patheverything.lean
More file actions
11690 lines (10272 loc) · 493 KB
/
Copy patheverything.lean
File metadata and controls
11690 lines (10272 loc) · 493 KB
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
/-
Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Lars Warren Ericson.
Github: https://github.com/catskillsresearch/scott_models
-/
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Finset.Fold
import Mathlib.Data.Finset.Lattice.Fold
import Mathlib.Data.Set.Basic
import Mathlib.Data.Sum.Order
import Mathlib.Order.CompleteLattice.Basic
import Mathlib.Order.DirSupClosed
import Mathlib.Order.Directed
import Mathlib.Order.FixedPoints
import Mathlib.Order.Hom.Basic
import Mathlib.Order.Hom.WithTopBot
import Mathlib.Order.Ideal
import Mathlib.Order.ScottContinuity
import Mathlib.Order.UpperLower.Basic
import Mathlib.Order.WithBot
import Mathlib.Topology.ContinuousMap.Basic
import Mathlib.Topology.Inseparable
import Mathlib.Topology.Order
import Mathlib.Topology.Order.ScottTopology
import Mathlib.Topology.Separation.Basic
/-!
# Single-file ScottModels
Self-contained flatten of the bridge theorems in `ScottModels/` together
with the transitive vendor modules they import (`vendor/scott1972`,
`vendor/scott1980`, `vendor/scott1982`). Mathlib stays imported.
Regenerate with `python3 scripts/generate_everything.py`.
-/
set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
/-! ## Vendor dependencies -/
-- Vendor 1980 — Scott1980.Neighborhood.Basic (from vendor/scott1980/Scott1980/Neighborhood/Basic.lean)
/-!
# Neighborhood systems (Scott 1981, PRG-19, §1) — foundations
Following Dana Scott, *Lectures on a Mathematical Theory of Computation*, Technical
Monograph PRG-19, Oxford (May 1981), Lecture I, *Domains given by neighbourhoods*.
Scott fixes a non-empty set `Δ` of *tokens* and considers a family `𝒟` of subsets of `Δ`
(the *neighbourhoods*). The order is *reversed* relative to information: a **smaller**
neighbourhood carries **more** information. A finite sequence of neighbourhoods is
*consistent* when it has a common lower bound inside `𝒟` (a `Z ∈ 𝒟` contained in all of
them); a neighbourhood system is closed under intersections of consistent finite sequences.
This file formalizes the very first page of §1:
* **Definition 1.1** — `NeighborhoodSystem`: a family with `Δ ∈ 𝒟` (condition (i)) and
closure under consistent binary intersections (condition (ii)).
* **Factoid 1.1a / 1.1b** — Scott's recursive *convention* for the finite intersection
`⋂_{i < n} Xᵢ` (`interUpTo`): the empty intersection is `Δ`, and the `(n+1)`-fold
intersection peels off the last factor.
* **Theorem 1.1c** — "from (ii) we can extend the intersection property to any finite
sequence", and *consequently* a finite sequence is consistent **iff** its intersection
lies in `𝒟`.
The §1 core is deliberately **constructive**: Scott uses *partial* filters so that the
basic theory avoids maximal-filter existence (Zorn/choice). Every theorem here depends only
on `propext`/`Quot.sound` (no `Classical.choice`).
-/
namespace Scott1980.Neighborhood
/-- **Definition 1.1 (Scott 1981, PRG-19).** A *neighbourhood system* over a token type
`α`. `mem X` means "`X` is a neighbourhood" (`X ∈ 𝒟`), and `master` is Scott's least
informative neighbourhood `Δ` (the whole token set, "ask me no questions").
The two conditions are exactly Scott's:
* (i) `Δ ∈ 𝒟` — `master_mem`;
* (ii) whenever `X, Y, Z ∈ 𝒟` and `Z ⊆ X ∩ Y`, then `X ∩ Y ∈ 𝒟` — `inter_mem`.
We keep `master` as a field (rather than hard-wiring `Set.univ`) to stay faithful to
Scott's `Δ` notation, and record Scott's standing assumption `𝒟 ⊆ 𝒫(Δ)` as the field
`sub_master` (every neighbourhood is a subset of `Δ`). Scott also assumes from the outset
that the token set `Δ` is non-empty; `master_nonempty` records this standing assumption
explicitly. The subset condition is what makes the principal filter `↑X` (Definition 1.7)
contain `Δ`, and underlies the least element `⊥ = ↑Δ`. -/
structure NeighborhoodSystem (α : Type*) where
/-- `mem X` holds iff `X` is a neighbourhood of the system (`X ∈ 𝒟`). -/
mem : Set α → Prop
/-- Scott's distinguished least-informative neighbourhood `Δ`. -/
master : Set α
/-- Scott's standing assumption that the token set `Δ` is non-empty. -/
master_nonempty : master.Nonempty
/-- (i) `Δ ∈ 𝒟`. -/
master_mem : mem master
/-- (ii) Closure under intersection of a *consistent* pair: if `X, Y, Z ∈ 𝒟` with the
witness `Z ⊆ X ∩ Y`, then `X ∩ Y ∈ 𝒟`. -/
inter_mem : ∀ {X Y Z : Set α}, mem X → mem Y → mem Z → Z ⊆ X ∩ Y → mem (X ∩ Y)
/-- Scott's `𝒟 ⊆ 𝒫(Δ)`: every neighbourhood is a subset of the master neighbourhood `Δ`. -/
sub_master : ∀ {X : Set α}, mem X → X ⊆ master
/-- Scott's *"very special circumstance"* (the prose after Examples 1.2–1.4): a family `𝒟`
is **nested-or-disjoint** when any two of its members are either nested (one included in the
other) or disjoint. -/
def NestedOrDisjoint {α : Type*} (mem : Set α → Prop) : Prop :=
∀ ⦃X Y : Set α⦄, mem X → mem Y → X ⊆ Y ∨ Y ⊆ X ∨ X ∩ Y = ∅
/-- **Factoid 1.4a (Scott 1981, PRG-19).** "In these systems two neighbourhoods are either
disjoint or one is included in the other": a family containing `Δ` whose members are pairwise
nested-or-disjoint **is** a neighbourhood system. This uniformly explains why Examples 1.2,
1.3 and 1.4 satisfy Definition 1.1.
The verification of condition (ii) needs no choice: if `X, Y` are nested then `X ∩ Y` is the
smaller (already in `𝒟`); if they are disjoint then the consistency witness `Z ⊆ X ∩ Y = ∅`
forces `Z = ∅`, whence `X ∩ Y = ∅ = Z ∈ 𝒟`. The caller supplies `master_nonempty`
(Scott's standing `Δ ≠ ∅` assumption) and `sub_master` (`𝒟 ⊆ 𝒫(Δ)`) directly. -/
def NeighborhoodSystem.ofNestedOrDisjoint {α : Type*} (mem : Set α → Prop) (master : Set α)
(master_nonempty : master.Nonempty) (master_mem : mem master) (hnd : NestedOrDisjoint mem)
(sub_master : ∀ {X : Set α}, mem X → X ⊆ master) : NeighborhoodSystem α where
mem := mem
master := master
master_nonempty := master_nonempty
master_mem := master_mem
sub_master := sub_master
inter_mem := by
intro X Y Z hX hY hZ hZsub
rcases hnd hX hY with h | h | h
· rwa [Set.inter_eq_left.mpr h]
· rwa [Set.inter_eq_right.mpr h]
· rw [h]
rw [h] at hZsub
rwa [← Set.subset_empty_iff.mp hZsub]
/-- **Exercise 1.19 (Scott 1981, PRG-19) — positivity, condition (ii′).** A neighbourhood
system is *positive* when Scott's (ii) is strengthened to the biconditional **(ii′)**: for
`X, Y ∈ 𝒟`, the intersection `X ∩ Y` is a neighbourhood **iff** it is non-empty. -/
def NeighborhoodSystem.IsPositive {α : Type*} (V : NeighborhoodSystem α) : Prop :=
∀ ⦃X Y : Set α⦄, V.mem X → V.mem Y → (V.mem (X ∩ Y) ↔ (X ∩ Y).Nonempty)
/-- **Exercise 1.19 — a positive system is a neighbourhood system.** Scott: "*prove that a
positive neighbourhood system is indeed a neighbourhood system*". From the raw data — (i)
`Δ ∈ 𝒟`, `𝒟 ⊆ 𝒫(Δ)`, and the positivity axiom (ii′) — condition (ii) follows: a consistency
witness `Z ⊆ X ∩ Y` with `Z ∈ 𝒟` is itself non-empty (apply (ii′) to `Z ∩ Z = Z`), so
`X ∩ Y ⊇ Z` is non-empty, whence `X ∩ Y ∈ 𝒟` by (ii′). Choice-free. -/
def NeighborhoodSystem.ofPositive {α : Type*} (mem : Set α → Prop) (master : Set α)
(master_nonempty : master.Nonempty) (master_mem : mem master)
(sub_master : ∀ {X : Set α}, mem X → X ⊆ master)
(pos : ∀ ⦃X Y : Set α⦄, mem X → mem Y → (mem (X ∩ Y) ↔ (X ∩ Y).Nonempty)) :
NeighborhoodSystem α where
mem := mem
master := master
master_nonempty := master_nonempty
master_mem := master_mem
sub_master := sub_master
inter_mem := by
intro X Y Z hX hY hZ hZsub
have hZZ : mem (Z ∩ Z) := by rwa [Set.inter_self]
have hZne : (Z ∩ Z).Nonempty := (pos hZ hZ).mp hZZ
rw [Set.inter_self] at hZne
exact (pos hX hY).mpr (hZne.mono hZsub)
/-- The system built by `ofPositive` is indeed positive. -/
theorem NeighborhoodSystem.ofPositive_isPositive {α : Type*} (mem : Set α → Prop)
(master : Set α) (master_nonempty : master.Nonempty) (master_mem : mem master)
(sub_master : ∀ {X : Set α}, mem X → X ⊆ master)
(pos : ∀ ⦃X Y : Set α⦄, mem X → mem Y → (mem (X ∩ Y) ↔ (X ∩ Y).Nonempty)) :
(NeighborhoodSystem.ofPositive mem master master_nonempty master_mem sub_master pos).IsPositive :=
pos
namespace NeighborhoodSystem
variable {α : Type*} (V : NeighborhoodSystem α)
/-- The finite intersection `⋂_{i < n} Xᵢ` of the first `n` terms of a sequence of
neighbourhoods, defined by Scott's recursive convention (**Factoid 1.1a / 1.1b**):
* `n = 0` : the empty intersection is `Δ` (`master`);
* `n + 1` : `(⋂_{i < n} Xᵢ) ∩ Xₙ`.
(See `interUpTo_zero` and `interUpTo_succ` for the two defining equations as lemmas.) -/
def interUpTo (V : NeighborhoodSystem α) (X : ℕ → Set α) : ℕ → Set α
| 0 => V.master
| (n + 1) => interUpTo V X n ∩ X n
/-- **Factoid 1.1a.** The intersection of the empty sequence of neighbourhoods is `Δ`:
`⋂_{i < 0} Xᵢ = Δ`. -/
@[simp] theorem interUpTo_zero (X : ℕ → Set α) : V.interUpTo X 0 = V.master := rfl
/-- **Factoid 1.1b.** The intersection of the first `n + 1` neighbourhoods peels off the
last factor: `⋂_{i < n+1} Xᵢ = (⋂_{i < n} Xᵢ) ∩ Xₙ`. -/
@[simp] theorem interUpTo_succ (X : ℕ → Set α) (n : ℕ) :
V.interUpTo X (n + 1) = V.interUpTo X n ∩ X n := rfl
/-- The finite intersection is contained in each of its factors: `⋂_{i < n} Xᵢ ⊆ Xⱼ` for
`j < n`. (Supporting lemma: this is what makes `⋂_{i < n} Xᵢ` a common lower bound of the
sequence, the intuition behind consistency.) -/
theorem interUpTo_subset (X : ℕ → Set α) :
∀ {n j : ℕ}, j < n → V.interUpTo X n ⊆ X j := by
intro n
induction n with
| zero => intro j h; exact absurd h (Nat.not_lt_zero j)
| succ n ih =>
intro j h
rw [interUpTo_succ]
rcases Nat.eq_or_lt_of_le (Nat.lt_succ_iff.mp h) with h' | h'
· subst h'; exact Set.inter_subset_right
· exact Set.inter_subset_left.trans (ih h')
/-- A finite sequence `X₀, …, Xₙ₋₁` of neighbourhoods is *consistent in* `𝒟` when it has a
common lower bound inside `𝒟`: some `Z ∈ 𝒟` contained in the intersection `⋂_{i < n} Xᵢ`
(equivalently, contained in every `Xⱼ`, `j < n`). This is Scott's notion of consistency,
generalized from pairs to finite sequences. -/
def Consistent (X : ℕ → Set α) (n : ℕ) : Prop :=
∃ Z, V.mem Z ∧ Z ⊆ V.interUpTo X n
/-- **Theorem 1.1c (extension of the intersection property).** Scott: "from (ii), we can
extend the intersection property to any finite sequence." If `Xᵢ ∈ 𝒟` for every `i < n`
and the sequence is consistent, then the finite intersection `⋂_{i < n} Xᵢ` is again a
neighbourhood (`∈ 𝒟`). Proved by induction on `n`; the inductive step is one application of
condition (ii). -/
theorem interUpTo_mem (X : ℕ → Set α) :
∀ {n : ℕ}, (∀ i, i < n → V.mem (X i)) → V.Consistent X n →
V.mem (V.interUpTo X n) := by
intro n
induction n with
| zero => intro _ _; exact V.master_mem
| succ n ih =>
intro hX hcons
obtain ⟨Z, hZmem, hZsub⟩ := hcons
have hZsub' : Z ⊆ V.interUpTo X n ∩ X n := by rwa [interUpTo_succ] at hZsub
-- The same witness `Z` shows the length-`n` prefix is consistent.
have hconsn : V.Consistent X n :=
⟨Z, hZmem, hZsub'.trans Set.inter_subset_left⟩
have hmemn : V.mem (V.interUpTo X n) :=
ih (fun i hi => hX i (Nat.lt_succ_of_lt hi)) hconsn
have hXn : V.mem (X n) := hX n (Nat.lt_succ_self n)
rw [interUpTo_succ]
exact V.inter_mem hmemn hXn hZmem hZsub'
/-- **Theorem 1.1c (consistency characterization).** "Consequently, `X₀, …, Xₙ₋₁` is
consistent in `𝒟` iff `⋂_{i < n} Xᵢ ∈ 𝒟`." (Given `Xᵢ ∈ 𝒟` for all `i < n`.)
* `→` is the extension property `interUpTo_mem`;
* `←` is immediate: the intersection is its own common lower bound. -/
theorem consistent_iff_interUpTo_mem (X : ℕ → Set α) {n : ℕ}
(hX : ∀ i, i < n → V.mem (X i)) :
V.Consistent X n ↔ V.mem (V.interUpTo X n) := by
constructor
· exact V.interUpTo_mem X hX
· intro h; exact ⟨V.interUpTo X n, h, Set.Subset.refl _⟩
/-- **Definition 1.6 (Scott 1981, PRG-19).** An (ideal) *element* of a neighbourhood system:
a subfamily `x ⊆ 𝒟` that is a *filter* — (i) `Δ ∈ x`, (ii) closed under intersection, (iii)
upward closed within `𝒟`. The domain is the type `Element` of all such filters, ordered by
inclusion. -/
structure Element where
/-- `mem X` holds iff the neighbourhood `X` belongs to the filter `x`. -/
mem : Set α → Prop
/-- `x` is a subfamily of `𝒟`. -/
sub : ∀ {X}, mem X → V.mem X
/-- (i) `Δ ∈ x`. -/
master_mem : mem V.master
/-- (ii) `X, Y ∈ x ⟹ X ∩ Y ∈ x`. -/
inter_mem : ∀ {X Y}, mem X → mem Y → mem (X ∩ Y)
/-- (iii) `X ∈ x` and `X ⊆ Y ∈ 𝒟 ⟹ Y ∈ x`. -/
up_mem : ∀ {X Y}, mem X → V.mem Y → X ⊆ Y → mem Y
/-- Two elements with the same membership predicate are equal (the remaining fields are `Prop`s). -/
theorem Element.ext {x y : V.Element} (h : ∀ X, x.mem X ↔ y.mem X) : x = y := by
rcases x with ⟨xmem, _, _, _, _⟩
rcases y with ⟨ymem, _, _, _, _⟩
have hmem : xmem = ymem := funext fun X => propext (h X)
subst hmem
rfl
/-- A filter (`Element`) is closed under the finite intersection `⋂_{i<n} Xᵢ`: if every factor
`Xᵢ` (`i < n`) lies in the filter `x`, so does `interUpTo X n`. Used in Exercises 1.18 and 1.21.
Base case `x.master_mem`; inductive step one `x.inter_mem`. -/
theorem Element.mem_interUpTo {α : Type*} {V : NeighborhoodSystem α} (x : V.Element)
(X : ℕ → Set α) :
∀ {n : ℕ}, (∀ i, i < n → x.mem (X i)) → x.mem (V.interUpTo X n) := by
intro n
induction n with
| zero => intro _; exact x.master_mem
| succ n ih =>
intro h
rw [interUpTo_succ]
exact x.inter_mem (ih (fun i hi => h i (Nat.lt_succ_of_lt hi))) (h n (Nat.lt_succ_self n))
/-- Membership of the finite intersection in a filter, as a biconditional (given all factors
are neighbourhoods). `→` is upward closure along `interUpTo X n ⊆ Xᵢ` (`interUpTo_subset`); `←`
is `Element.mem_interUpTo`. -/
theorem Element.mem_interUpTo_iff {α : Type*} {V : NeighborhoodSystem α} (x : V.Element)
(X : ℕ → Set α) {n : ℕ} (hX : ∀ i, i < n → V.mem (X i)) :
x.mem (V.interUpTo X n) ↔ ∀ i, i < n → x.mem (X i) := by
constructor
· intro h i hi
exact x.up_mem h (hX i hi) (V.interUpTo_subset X hi)
· exact x.mem_interUpTo X
/-- Filter-inclusion order on elements (Scott's approximation order, Definition 1.8).
Named so Palomar can lock the `PartialOrder` relation without inlining it. -/
def element_le (x y : V.Element) : Prop :=
∀ X, x.mem X → y.mem X
/-- Reflexivity of the filter-inclusion order. Named so Palomar can lock the
`PartialOrder` instance without a generated `._proof_N`. -/
theorem element_le_refl (x : V.Element) : ∀ X, x.mem X → x.mem X :=
fun _ h => h
/-- Transitivity of the filter-inclusion order. -/
theorem element_le_trans (x y z : V.Element)
(hxy : ∀ X, x.mem X → y.mem X) (hyz : ∀ X, y.mem X → z.mem X) :
∀ X, x.mem X → z.mem X :=
fun X h => hyz X (hxy X h)
/-- Antisymmetry of the filter-inclusion order. -/
theorem element_le_antisymm (x y : V.Element)
(hxy : ∀ X, x.mem X → y.mem X) (hyx : ∀ X, y.mem X → x.mem X) :
x = y :=
@Element.ext α V x y fun X => ⟨hxy X, hyx X⟩
/-- Elements are ordered by inclusion of their membership predicates (Scott's approximation
order, Definition 1.8). -/
instance instPartialOrderElement : PartialOrder V.Element where
le := element_le V
le_refl := element_le_refl V
le_trans := element_le_trans V
le_antisymm := element_le_antisymm V
/-- The **limit family** of a sequence of neighbourhoods (Scott, the prose before Definition
1.6): `x = {Z ∈ 𝒟 ∣ Xₙ ⊆ Z for some n}` — the family of all neighbourhoods eventually reached
by `⟨Xₙ⟩`. This is the construction Scott uses to motivate the (ideal) elements of `|𝒟|`. -/
def limitFamily (X : ℕ → Set α) : Set (Set α) := {Z | V.mem Z ∧ ∃ n, X n ⊆ Z}
/-- Two sequences of neighbourhoods are **equivalent** ("each goes equally deep as the other"):
for every `Yₘ` some `Xₙ ⊆ Yₘ`, and for every `Xₙ` some `Yₘ ⊆ Xₙ`. -/
def SeqEquiv (X Y : ℕ → Set α) : Prop :=
(∀ m, ∃ n, X n ⊆ Y m) ∧ (∀ n, ∃ m, Y m ⊆ X n)
/-- **Factoid 1.5b (Scott 1981, PRG-19).** "It is easy to prove that … the two families are
*equal* if and only if the sequences are *equivalent*." Given that every term of each sequence
is a neighbourhood, the limit families coincide exactly when the sequences are equivalent. -/
theorem limitFamily_eq_iff (X Y : ℕ → Set α)
(hX : ∀ n, V.mem (X n)) (hY : ∀ m, V.mem (Y m)) :
V.limitFamily X = V.limitFamily Y ↔ SeqEquiv X Y := by
constructor
· intro hEq
refine ⟨fun m => ?_, fun n => ?_⟩
· have hmem : Y m ∈ V.limitFamily Y := ⟨hY m, m, subset_rfl⟩
rw [← hEq] at hmem
obtain ⟨_, n, hn⟩ := hmem
exact ⟨n, hn⟩
· have hmem : X n ∈ V.limitFamily X := ⟨hX n, n, subset_rfl⟩
rw [hEq] at hmem
obtain ⟨_, m, hm⟩ := hmem
exact ⟨m, hm⟩
· rintro ⟨h1, h2⟩
apply Set.ext
intro Z
constructor
· rintro ⟨hZ, n, hn⟩
obtain ⟨m, hm⟩ := h2 n
exact ⟨hZ, m, hm.trans hn⟩
· rintro ⟨hZ, m, hm⟩
obtain ⟨n, hn⟩ := h1 m
exact ⟨hZ, n, hn.trans hm⟩
/-- **Definition 1.7 (Scott 1981, PRG-19).** The *principal filter* `↑X` determined by a
neighbourhood `X ∈ 𝒟`:
`↑X = {Y ∈ 𝒟 ∣ X ⊆ Y}`.
These are Scott's *finite elements* of `|𝒟|`. The four filter conditions:
* `sub` is the first projection (`Y ∈ ↑X ⟹ Y ∈ 𝒟`);
* `master_mem` needs `X ⊆ Δ`, supplied by `V.sub_master` (Scott's `𝒟 ⊆ 𝒫(Δ)`);
* `inter_mem` uses `Set.subset_inter` (from `X ⊆ Y₁`, `X ⊆ Y₂`) with `X` itself as the
consistency witness for `V.inter_mem`;
* `up_mem` is transitivity of `⊆`. -/
def principal {X : Set α} (hX : V.mem X) : V.Element where
mem Y := V.mem Y ∧ X ⊆ Y
sub h := h.1
master_mem := ⟨V.master_mem, V.sub_master hX⟩
inter_mem h1 h2 :=
⟨V.inter_mem h1.1 h2.1 hX (Set.subset_inter h1.2 h2.2), Set.subset_inter h1.2 h2.2⟩
up_mem h hY hsub := ⟨hY, h.2.trans hsub⟩
@[simp] theorem mem_principal {X Y : Set α} (hX : V.mem X) :
(V.principal hX).mem Y ↔ V.mem Y ∧ X ⊆ Y := Iff.rfl
/-- **Factoid 1.7a (Scott 1981, PRG-19) — inclusion-*reversing*.** "It is obvious that the
correspondence between `X` and `↑X` is one-one and inclusion *reversing*." The order on `↑`:
`↑X ⊑ ↑Y ↔ Y ⊆ X` (equivalently Scott's `X ⊆ Y ↔ ↑Y ⊑ ↑X`).
`→` tests at `Z = X` (`X ∈ ↑X` since `X ⊆ X`), reading off `Y ⊆ X` from `X ∈ ↑Y`; `←` chains
`Y ⊆ X ⊆ Z`. -/
theorem principal_le_iff {X Y : Set α} (hX : V.mem X) (hY : V.mem Y) :
V.principal hX ≤ V.principal hY ↔ Y ⊆ X := by
constructor
· intro h
exact (h X ⟨hX, subset_rfl⟩).2
· intro hYX Z hZ
exact ⟨hZ.1, hYX.trans hZ.2⟩
/-- **Factoid 1.7a (Scott 1981, PRG-19) — one-one.** The correspondence `X ↦ ↑X` is injective:
`↑X = ↑Y ⟹ X = Y`. Antisymmetry applied to `principal_le_iff` in both directions. -/
theorem principal_injective {X Y : Set α} (hX : V.mem X) (hY : V.mem Y)
(h : V.principal hX = V.principal hY) : X = Y := by
have hYX : Y ⊆ X := (V.principal_le_iff hX hY).mp (le_of_eq h)
have hXY : X ⊆ Y := (V.principal_le_iff hY hX).mp (le_of_eq h.symm)
exact Set.Subset.antisymm hXY hYX
/-- **Factoid 1.7b (Scott 1981, PRG-19).** "It is also obvious from the definitions that for each
`x ∈ |𝒟|`, `x = ⋃ {↑X ∣ X ∈ x}`." In membership form (the union over a `Set (Set α)` made
concrete): a neighbourhood `Z` is in `x` iff `Z` lies in the principal filter `↑X` of *some*
member `X` of `x`.
`→` uses `X = Z` (`Z ∈ ↑Z` as `Z ⊆ Z`); `←` is upward closure `up_mem` (`X ⊆ Z`, `Z ∈ 𝒟`). -/
theorem eq_iUnion_principal (x : V.Element) {Z : Set α} :
x.mem Z ↔ ∃ X, ∃ hX : x.mem X, (V.principal (x.sub hX)).mem Z := by
constructor
· intro hZ
exact ⟨Z, hZ, x.sub hZ, subset_rfl⟩
· rintro ⟨X, hX, hVZ, hXZ⟩
exact x.up_mem hX hVZ hXZ
/-- **Definition 1.8 (Scott 1981, PRG-19) — `⊥`.** The least defined element `⊥ = {Δ}`,
"read: *bottom*". It is the principal filter of the master neighbourhood `Δ`: `⊥ = ↑Δ`. -/
def bot : V.Element := V.principal V.master_mem
/-- **Definition 1.8 — `⊥ = {Δ}` literally.** Scott's `⊥` is the *singleton* `{Δ}`: a
neighbourhood `Y` belongs to `⊥` iff `Y = Δ`.
`→`: `Y ∈ ⊥ = ↑Δ` gives `Y ∈ 𝒟` and `Δ ⊆ Y`; `V.sub_master` gives the reverse `Y ⊆ Δ`, so
`Y = Δ` by antisymmetry. `←`: `Δ ∈ 𝒟` and `Δ ⊆ Δ`. -/
@[simp] theorem mem_bot {Y : Set α} : V.bot.mem Y ↔ Y = V.master := by
constructor
· rintro ⟨hY, hΔY⟩
exact Set.Subset.antisymm (V.sub_master hY) hΔY
· rintro rfl
exact ⟨V.master_mem, subset_rfl⟩
/-- **Factoid 1.8a (Scott 1981, PRG-19).** "The element that approximates all others, `{Δ}`,
is called `⊥`": `⊥` is the least element of `|𝒟|`, `⊥ ⊑ x` for every `x`.
Given `Y ∈ ⊥`, i.e. `Y = Δ`, membership `Δ ∈ x` is filter condition (i) (`x.master_mem`). -/
theorem bot_le (x : V.Element) : V.bot ≤ x := by
intro Y hY
rw [mem_bot] at hY
subst hY
exact x.master_mem
/-- **Factoid 1.8a, packaged.** `⊥` is an `OrderBot` for the approximation order, so the `⊥`
notation refers to `{Δ}`. Constructive (`bot_le` is `[propext, Quot.sound]`). -/
instance : OrderBot V.Element where
bot := V.bot
bot_le := V.bot_le
/-- **Definition 1.8 (Scott 1981, PRG-19) — *total* elements.** "Elements maximal with respect
to the approximation relation are called *total elements*." `x` is total iff it is maximal: any
`y` it approximates approximates it back. This is the *predicate* only; the *existence* of total
elements above a given `x` (Exercise 1.24) is choice-dependent and out of scope here. -/
def IsTotal (x : V.Element) : Prop := ∀ y, x ≤ y → y ≤ x
/-- **Factoid 1.8b (Scott 1981, PRG-19) — "Examples 1.2–1.5 revisited".** "Any explicitly given
filter `x` is principal … the minimal `X ∈ x` tells us all we need to know." Stated honestly: if
the filter `x` has a `⊆`-minimum member `X` (one contained in every member of `x`), then `x` is
exactly the principal filter `↑X`. In a *finite* system every filter has such a minimum (the
intersection of its finitely many members, itself in `x` by closure), so every element is
principal; that finiteness step is the only classical ingredient and is left implicit here — this
constructive core captures the content.
`⊆`: any `Z ∈ x` satisfies `X ⊆ Z` by minimality, so `Z ∈ ↑X`. `⊇`: `Z ∈ ↑X` means `Z ∈ 𝒟` and
`X ⊆ Z`, so `Z ∈ x` by upward closure from `X ∈ x`. -/
theorem eq_principal_of_isMin (x : V.Element) {X : Set α} (hX : x.mem X)
(hmin : ∀ Y, x.mem Y → X ⊆ Y) : x = V.principal (x.sub hX) := by
apply Element.ext
intro Z
constructor
· intro hZ
exact ⟨x.sub hZ, hmin Z hZ⟩
· rintro ⟨hZmem, hXZ⟩
exact x.up_mem hX hZmem hXZ
end NeighborhoodSystem
/-- **Definition 1.9 (Scott 1981, PRG-19).** Two neighbourhood systems `𝒟₀` and `𝒟₁` (over possibly
*different* token types) *determine isomorphic domains* iff there is a one-one, inclusion-preserving
correspondence between `|𝒟₀|` and `|𝒟₁|`. We package "one-one + preserves inclusion (both ways)" as
mathlib's order-isomorphism `≃o`: an `OrderIso` is automatically a bijection that *reflects* as well
as preserves `⊑` (`map_rel_iff`), which is exactly Scott's requirement. -/
abbrev DomainIso {α β : Type*} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : Type _ :=
V₀.Element ≃o V₁.Element
/-- Scott's `𝒟₀ ≅ 𝒟₁`: the domains are isomorphic (there *exists* a `DomainIso`). -/
def Isomorphic {α β : Type*} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : Prop :=
Nonempty (DomainIso V₀ V₁)
@[inherit_doc] infix:25 " ≅ᴰ " => Isomorphic
/-- `≅ᴰ` is reflexive (`OrderIso.refl`). -/
theorem Isomorphic.refl {α : Type*} (V : NeighborhoodSystem α) : V ≅ᴰ V :=
⟨OrderIso.refl _⟩
/-- `≅ᴰ` is symmetric (`OrderIso.symm`). -/
theorem Isomorphic.symm {α β : Type*} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β}
(h : V₀ ≅ᴰ V₁) : V₁ ≅ᴰ V₀ :=
h.elim fun e => ⟨e.symm⟩
/-- `≅ᴰ` is transitive (`OrderIso.trans`). -/
theorem Isomorphic.trans {α β γ : Type*} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β}
{V₂ : NeighborhoodSystem γ} (h₀ : V₀ ≅ᴰ V₁) (h₁ : V₁ ≅ᴰ V₂) : V₀ ≅ᴰ V₂ :=
h₀.elim fun e₀ => h₁.elim fun e₁ => ⟨e₀.trans e₁⟩
end Scott1980.Neighborhood
-- Vendor 1982 — Scott1982.InfoSys (from vendor/scott1982/Scott1982/InfoSys.lean)
/-!
# Scott Information Systems
Following Dana Scott, *"Domains for Denotational Semantics"* (ICALP 1982) and the
compact presentation in Glynn Winskel, *The Formal Semantics of Programming
Languages*, Chapter 8.
Following Scott's **Definition 2.1**, an information system is a structure
`(P, Δ, Con, ⊢)` where
* `P` is a set of *data objects* / *propositions* (our token type `α`);
* `Δ ∈ P` is a distinguished *least informative* object (here the field `bot`);
* `Con` is a set of finite subsets of `P`, the *consistent* sets; and
* `⊢` (entailment, here `Ent`) relates a finite set to a token it forces.
Scott's six axioms (Def. 2.1) are, for finite `u, v ⊆ P` and `X ∈ P`:
* (i) `u ∈ Con` whenever `u ⊆ v ∈ Con` — `con_subset`
* (ii) `{X} ∈ Con` — `con_sing`
* (iii) `u ∪ {X} ∈ Con` whenever `u ⊢ X` — `ent_con`
* (iv) `u ⊢ Δ` — `ent_bot`
* (v) `u ⊢ X` whenever `X ∈ u` — `ent_refl`
* (vi) if `v ⊢ Y` for all `Y ∈ u` and `u ⊢ X` then `v ⊢ X` — `ent_trans`
The **domain** determined by an information system is the poset of its *elements*
(a.k.a. *ideals*): sets of tokens that are consistent on every finite subset and
closed under entailment, ordered by inclusion. This file sets up the structure, the
notion of element, and the partial order; later files build the function, product,
and sum spaces.
This is the **1982** presentation; the development is kept choice-free (constructive),
matching Scott's emphasis on the constructive nature of the definitions.
-/
namespace Scott1982
universe u
/-- A Scott information system on a type of tokens `α`, following Scott's Definition 2.1
in *"Domains for Denotational Semantics"* (ICALP 1982).
`DecidableEq α` is required so that finite token sets support union (`X ∪ {a}`) and the
other `Finset` operations the axioms mention. -/
structure InfoSys (α : Type u) [DecidableEq α] where
/-- The distinguished least-informative object `Δ`. -/
bot : α
/-- The consistent finite sets of tokens. -/
Con : Set (Finset α)
/-- Entailment: `Ent u a` means the consistent set `u` forces the token `a`. -/
Ent : Finset α → α → Prop
/-- (i) Consistency is downward closed under `⊆`. -/
con_subset : ∀ {u v : Finset α}, u ∈ Con → v ⊆ u → v ∈ Con
/-- (ii) Every singleton is consistent. -/
con_sing : ∀ a : α, {a} ∈ Con
/-- (iii) A set entailing `a` stays consistent when `a` is added. Scott writes this as
`u ∪ {a} ∈ Con`; we use the definitionally identical `insert a u`, because mathlib's
`Finset` union instance (unlike `insert`) depends on `Classical.choice`, which would
break the constructive development. -/
ent_con : ∀ {u : Finset α} {a : α}, Ent u a → insert a u ∈ Con
/-- (iv) The least token `Δ` is entailed by every consistent set. -/
ent_bot : ∀ {u : Finset α}, u ∈ Con → Ent u bot
/-- (v) Entailment is reflexive on members of a consistent set. -/
ent_refl : ∀ {u : Finset α} {a : α}, u ∈ Con → a ∈ u → Ent u a
/-- (vi) Entailment is transitive (cut): if a consistent `v` entails every member of a
consistent `u`, and `u ⊢ c`, then `v ⊢ c`. -/
ent_trans : ∀ {u v : Finset α} {c : α},
v ∈ Con → u ∈ Con → (∀ y ∈ u, Ent v y) → Ent u c → Ent v c
namespace InfoSys
variable {α : Type u} [DecidableEq α] (sys : InfoSys α)
/-- An *element* (ideal) of the domain: a set of tokens that is consistent on every
finite subset and closed under entailment. -/
structure Element where
/-- The underlying set of tokens. -/
carrier : Set α
/-- Every finite subset of the element is consistent. -/
consistent : ∀ Y : Finset α, (Y : Set α) ⊆ carrier → Y ∈ sys.Con
/-- The element is closed under entailment. -/
closed : ∀ (Y : Finset α) (a : α), (Y : Set α) ⊆ carrier → sys.Ent Y a → a ∈ carrier
/-- Extensional equality of elements. -/
theorem Element.ext {x y : sys.Element} (h : x.carrier = y.carrier) : x = y := by
cases x
cases y
subst h
rfl
/-- Reflexivity of the carrier-inclusion order. -/
theorem element_le_refl (x : sys.Element) : x.carrier ⊆ x.carrier :=
Set.Subset.refl _
/-- Transitivity of the carrier-inclusion order. -/
theorem element_le_trans (x y z : sys.Element)
(hxy : x.carrier ⊆ y.carrier) (hyz : y.carrier ⊆ z.carrier) :
x.carrier ⊆ z.carrier :=
Set.Subset.trans hxy hyz
/-- Antisymmetry of the carrier-inclusion order. -/
theorem element_le_antisymm (x y : sys.Element)
(hxy : x.carrier ⊆ y.carrier) (hyx : y.carrier ⊆ x.carrier) :
x = y :=
Element.ext sys (Set.Subset.antisymm hxy hyx)
/-- Elements are ordered by inclusion of their carriers; this is the Scott ordering. -/
instance instPartialOrderElement : PartialOrder sys.Element where
le x y := x.carrier ⊆ y.carrier
le_refl := element_le_refl sys
le_trans := element_le_trans sys
le_antisymm := element_le_antisymm sys
/-- Empty set is consistent (subset of any singleton). -/
theorem con_empty : (∅ : Finset α) ∈ sys.Con :=
sys.con_subset (sys.con_sing sys.bot) (Finset.empty_subset _)
end InfoSys
end Scott1982
-- Vendor 1982 — Scott1982.Constructive (from vendor/scott1982/Scott1982/Constructive.lean)
/-!
# A choice-free `Finset` prelude
One of the project's goals (Goal 3) is to certify that the *information-system*
presentation of Scott domains can be developed in a **purely constructive** fragment of
Lean: every result must have a `#print axioms` footprint contained in
`[propext, Quot.sound]`, with **no `Classical.choice`** and no use of the law of excluded
middle.
This is harder than it looks, because several of mathlib's `Finset` *operations* and even
a few basic *lemmas* transitively depend on `Classical.choice` (through the
`Multiset.dedup` / quotient machinery), in version `v4.30.0`:
* tainted operations: `(· ∪ ·)`, `Finset.image`, `(· ×ˢ ·)`, `Finset.biUnion`, `(· \ ·)`,
and mathlib's `Finset.decidableEq` (via `Multiset` quotients);
* tainted lemmas: e.g. `Finset.insert_comm`, `Finset.singleton_subset_iff`;
* tainted *tactics*: `tauto`, `aesop` (they close goals via classical reasoning).
By contrast the following are choice-free and form our working toolkit: `insert`,
`(· ∩ ·)`, `Finset.filter`, `Finset.fold`, `Multiset.foldr`, the membership/subset lemmas
(`Finset.mem_insert`, `Finset.mem_singleton`, `Finset.subset_iff`, `Finset.mem_coe`,
`Finset.coe_subset`, `Finset.mem_inter`, `Finset.ext`), set-level unions/intersections,
and explicit term-mode/`rintro`/`constructor` proofs.
This file provides the finite-set operations the development needs but mathlib only
offers in choice-tainted form: a **binary union of `Finset`s**, built choice-free by
folding `insert`, and a **decidable equality** for `Finset` via subset antisymmetry.
Every declaration here is audited to depend only on
`[propext, Quot.sound]`.
-/
namespace Scott1982.Constructive
variable {α : Type*} [DecidableEq α]
/-- Choice-free commutativity of `insert` (mathlib's `Finset.insert_comm` is choice-tainted).
Needed to fold `insert` over a `Multiset`. -/
theorem insert_comm' (a b : α) (s : Finset α) :
insert a (insert b s) = insert b (insert a s) := by
ext x
simp only [Finset.mem_insert]
constructor
· rintro (h | h | h)
exacts [Or.inr (Or.inl h), Or.inl h, Or.inr (Or.inr h)]
· rintro (h | h | h)
exacts [Or.inr (Or.inl h), Or.inl h, Or.inr (Or.inr h)]
instance instLeftCommutativeInsert :
LeftCommutative (insert : α → Finset α → Finset α) := ⟨insert_comm'⟩
/-- Choice-free binary union of finite sets, obtained by folding `insert` over the second
argument's underlying multiset. Definitionally equal in content to `u ∪ v`, but — unlike
mathlib's `(· ∪ ·)` — free of any `Classical.choice` dependency. -/
def funion (u v : Finset α) : Finset α := Multiset.foldr insert u v.1
@[inherit_doc] infixl:65 " ∪' " => funion
theorem mem_foldr_insert (a : α) (u : Finset α) (s : Multiset α) :
a ∈ Multiset.foldr insert u s ↔ a ∈ u ∨ a ∈ s := by
refine Multiset.induction_on s ?_ ?_
· simp
· intro b t ih
simp only [Multiset.foldr_cons, Finset.mem_insert, ih, Multiset.mem_cons]
constructor
· rintro (h | h | h)
exacts [Or.inr (Or.inl h), Or.inl h, Or.inr (Or.inr h)]
· rintro (h | h | h)
exacts [Or.inr (Or.inl h), Or.inl h, Or.inr (Or.inr h)]
@[simp] theorem mem_funion {a : α} {u v : Finset α} :
a ∈ u ∪' v ↔ a ∈ u ∨ a ∈ v := mem_foldr_insert a u v.1
/-- The coercion of `u ∪' v` to a `Set` is the (choice-free) set union of the coercions. -/
theorem coe_funion (u v : Finset α) :
(↑(u ∪' v) : Set α) = (↑u : Set α) ∪ ↑v := by
ext x
simp only [Set.mem_union, Finset.mem_coe, mem_funion]
theorem subset_funion_left (u v : Finset α) : u ⊆ u ∪' v := fun _ hx => mem_funion.2 (Or.inl hx)
theorem subset_funion_right (u v : Finset α) : v ⊆ u ∪' v := fun _ hx => mem_funion.2 (Or.inr hx)
@[simp] theorem funion_empty_right (u : Finset α) : u ∪' (∅ : Finset α) = u := by
ext x
simp only [mem_funion, Finset.notMem_empty, or_false]
/-- Universal property of the union: `u ∪' v ⊆ w` iff both `u ⊆ w` and `v ⊆ w`. -/
theorem funion_subset_iff {u v w : Finset α} : u ∪' v ⊆ w ↔ u ⊆ w ∧ v ⊆ w := by
constructor
· intro h
exact ⟨fun x hx => h (subset_funion_left u v hx),
fun x hx => h (subset_funion_right u v hx)⟩
· rintro ⟨hu, hv⟩ x hx
rcases mem_funion.1 hx with h | h
exacts [hu h, hv h]
omit [DecidableEq α] in
/-- If mutual subset holds, the finsets are equal. -/
theorem decidableEq_finset_eq_of_subset (s t : Finset α) (h : s ⊆ t ∧ t ⊆ s) : s = t :=
Finset.Subset.antisymm h.1 h.2
omit [DecidableEq α] in
/-- Mutual subset is required for finset equality in this decidable instance. -/
theorem decidableEq_finset_false_of_ne (s t : Finset α) (h : ¬(s ⊆ t ∧ t ⊆ s)) (heq : s = t) :
False := by
subst heq
exact h ⟨Finset.Subset.refl _, Finset.Subset.refl _⟩
/-- Choice-free decidable equality for `Finset`.
mathlib's `Finset.decidableEq` goes through `Multiset` quotients and pulls
`Classical.choice`; this version uses only decidable membership and subset. -/
def decidableEq_finset {α : Type*} [DecidableEq α] : DecidableEq (Finset α) :=
fun s t =>
if h : s ⊆ t ∧ t ⊆ s then
isTrue (decidableEq_finset_eq_of_subset s t h)
else
isFalse (decidableEq_finset_false_of_ne s t h)
end Scott1982.Constructive
-- Vendor 1982 — Scott1982.Definition22 (from vendor/scott1982/Scott1982/Definition22.lean)
/-!
# Definition 2.2 — set-level entailment
**Scott 1982, Definition 2.2.** For `u, v ∈ Con` we write `u ⊢ v` to mean that
`u ⊢ X` for all `X ∈ v`.
-/
namespace Scott1982
namespace InfoSys
universe u
variable {α : Type u} [DecidableEq α] (sys : InfoSys α)
/-- **Definition 2.2 (Scott 1982).** Set-level entailment: `EntSet u v` means
`u ⊢ X` for every `X ∈ v`. -/
def EntSet (u v : Finset α) : Prop := ∀ X ∈ v, sys.Ent u X
theorem entSet_empty (u : Finset α) : sys.EntSet u (∅ : Finset α) := by
intro X hX
exact False.elim (Finset.notMem_empty X hX)
theorem entSet_singleton {u : Finset α} {X : α} :
sys.EntSet u {X} ↔ sys.Ent u X := by
constructor
· intro h
exact h X (Finset.mem_singleton_self X)
· intro h Y hY
rw [Finset.mem_singleton] at hY
subst hY
exact h
end InfoSys
end Scott1982
-- Vendor 1982 — Scott1982.Proposition23 (from vendor/scott1982/Scott1982/Proposition23.lean)
/-!
# Proposition 2.3 — elementary properties of set-level entailment
**Scott 1982, Proposition 2.3.** For all `u, v, w, u', v' ∈ Con`:
(i) `∅ ⊢ {Δ}`; (ii) `u ⊢ v ⇒ u ∪ v ∈ Con`; (iii) `u ⊢ u`;
(iv) transitivity; (v) monotonicity; (vi) `u ⊢ v ∧ u ⊢ v' ⇒ u ⊢ v ∪ v'`.
-/
namespace Scott1982
open Scott1982.Constructive
namespace InfoSys
variable {α : Type*} [DecidableEq α] (sys : InfoSys α)
/-- `u ∪' insert a t = insert a (u ∪' t)`. -/
theorem funion_insert (u : Finset α) (a : α) (t : Finset α) :
u ∪' insert a t = insert a (u ∪' t) := by
ext x
constructor
· intro hx
rcases mem_funion.mp hx with hu | hins
· exact Finset.mem_insert_of_mem (mem_funion.mpr (Or.inl hu))
· rcases Finset.mem_insert.mp hins with ha | ht
· exact Finset.mem_insert.mpr (Or.inl ha)
· exact Finset.mem_insert_of_mem (mem_funion.mpr (Or.inr ht))
· intro hx
rcases Finset.mem_insert.mp hx with ha | h
· exact mem_funion.mpr (Or.inr (Finset.mem_insert.mpr (Or.inl ha)))
· rcases mem_funion.mp h with hu | ht
· exact mem_funion.mpr (Or.inl hu)
· exact mem_funion.mpr (Or.inr (Finset.mem_insert.mpr (Or.inr ht)))
/-- **Proposition 2.3(i).** `∅ ⊢ {Δ}`. -/
theorem proposition_2_3_i : sys.EntSet ∅ ({sys.bot} : Finset α) := by
intro X hX
rw [Finset.mem_singleton] at hX
subst hX
exact sys.ent_bot sys.con_empty
/-- **Proposition 2.3(iii).** `u ⊢ u`. -/
theorem proposition_2_3_iii {u : Finset α} (hu : u ∈ sys.Con) : sys.EntSet u u :=
fun _X hX => sys.ent_refl hu hX
/-- **Proposition 2.3(iv).** Transitivity of `EntSet`. -/
theorem proposition_2_3_iv {u v w : Finset α}
(hu : u ∈ sys.Con) (hv : v ∈ sys.Con)
(huv : sys.EntSet u v) (hvw : sys.EntSet v w) : sys.EntSet u w :=
fun X hX => sys.ent_trans hu hv huv (hvw X hX)
/-- **Proposition 2.3(v).** Monotonicity: `u ⊆ u'`, `u ⊢ v`, `v' ⊆ v` ⇒ `u' ⊢ v'`. -/
theorem proposition_2_3_v {u u' v v' : Finset α}
(hu : u ∈ sys.Con) (hu' : u' ∈ sys.Con)
(hsubu : u ⊆ u') (huv : sys.EntSet u v) (hsubv : v' ⊆ v) :
sys.EntSet u' v' := by
intro X hX
have hEnt : sys.Ent u X := huv X (hsubv hX)
refine sys.ent_trans hu' hu ?_ hEnt
intro y hy
exact sys.ent_refl hu' (hsubu hy)
/-- **Proposition 2.3(vi).** `u ⊢ v` and `u ⊢ v'` imply `u ⊢ v ∪' v'`. -/
theorem proposition_2_3_vi {u v v' : Finset α}
(huv : sys.EntSet u v) (huv' : sys.EntSet u v') : sys.EntSet u (v ∪' v') := by
intro X hX
rcases mem_funion.mp hX with h | h
· exact huv X h
· exact huv' X h
/-- **Proposition 2.3(ii).** `u ⊢ v` implies `u ∪' v ∈ Con`. -/
theorem proposition_2_3_ii {u v : Finset α} (hu : u ∈ sys.Con) (h : sys.EntSet u v) :
u ∪' v ∈ sys.Con := by
have : ∀ s : Finset α, (∀ x ∈ s, x ∈ v) → u ∪' s ∈ sys.Con := by
intro s
refine Finset.induction_on s ?_ ?_
· intro _
-- foldr insert u 0 = u
simpa [funion_empty_right] using hu
· intro a t _ha ih hmem
have hEnt_u_a : sys.Ent u a := h a (hmem a (Finset.mem_insert_self a t))
have hut : u ∪' t ∈ sys.Con := ih fun x hx => hmem x (Finset.mem_insert_of_mem hx)
have hEnt : sys.Ent (u ∪' t) a :=
sys.ent_trans hut hu (fun y hy => sys.ent_refl hut (subset_funion_left u t hy))
hEnt_u_a
have hins : insert a (u ∪' t) ∈ sys.Con := sys.ent_con hEnt
simpa [funion_insert] using hins
exact this v fun _ hx => hx
end InfoSys
end Scott1982
-- Vendor 1982 — Scott1982.Factoid35 (from vendor/scott1982/Scott1982/Factoid35.lean)
/-!
# Factoid 3.5 — finite elements as entailment closures
**Factoid 3.5 (inventory).** For `u ∈ Con`, the closure
`ū = {X ∣ u ⊢ X}` is an element of `|A|` (a *finite element*).
-/
namespace Scott1982
open Scott1982.Constructive
namespace InfoSys
variable {α : Type*} [DecidableEq α] (sys : InfoSys α)
/-- **Factoid 3.5.** Entailment closure of a consistent set. -/
def closure (u : Finset α) (hu : u ∈ sys.Con) : sys.Element where
carrier := {X | sys.Ent u X}
consistent := by
intro Y hY
have hEnt : sys.EntSet u Y := fun X hX => hY (Finset.mem_coe.2 hX)
exact sys.con_subset (proposition_2_3_ii sys hu hEnt) (subset_funion_right _ _)
closed := by
intro Y a hY hEnt
have hYcon : Y ∈ sys.Con := by
have hEntY : sys.EntSet u Y := fun X hX => hY (Finset.mem_coe.2 hX)
exact sys.con_subset (proposition_2_3_ii sys hu hEntY) (subset_funion_right _ _)
exact sys.ent_trans hu hYcon (fun y hy => hY (Finset.mem_coe.2 hy)) hEnt
theorem mem_closure_iff {u : Finset α} (hu : u ∈ sys.Con) {X : α} :
X ∈ (sys.closure u hu).carrier ↔ sys.Ent u X := Iff.rfl
/-- `u ⊆ ū`. -/
theorem subset_closure {u : Finset α} (hu : u ∈ sys.Con) :
↑u ⊆ (sys.closure u hu).carrier :=
fun _ hX => sys.ent_refl hu (Finset.mem_coe.1 hX)
end InfoSys
end Scott1982
-- Vendor 1982 — Scott1982.Approximable (from vendor/scott1982/Scott1982/Approximable.lean)
/-!
# Approximable mappings — Definitions 5.1 and 5.2
Adapted from the PRG-19 approximable-map pattern, rewritten for Scott 1982
information systems (relations on `Con × Con`).
-/
namespace Scott1982
open Scott1982.Constructive
namespace InfoSys
universe u v
variable {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β]
/-- **Definition 5.1 (Scott 1982).** Approximable mapping between information systems. -/
structure ApproximableMap (A : InfoSys α) (B : InfoSys β) where
rel : Finset α → Finset β → Prop
rel_dom : ∀ {u v}, rel u v → u ∈ A.Con
rel_cod : ∀ {u v}, rel u v → v ∈ B.Con
empty_rel : rel ∅ ∅
union_right : ∀ {u v v'}, rel u v → rel u v' → rel u (v ∪' v')
mono : ∀ {u u' v v'},
rel u v → A.EntSet u' u → B.EntSet v v' → u' ∈ A.Con → v' ∈ B.Con → rel u' v'
namespace ApproximableMap
variable {A : InfoSys α} {B : InfoSys β}
theorem ext {f g : ApproximableMap A B} (h : ∀ u v, f.rel u v ↔ g.rel u v) : f = g := by
obtain ⟨rf, _, _, _, _, _⟩ := f
obtain ⟨rg, _, _, _, _, _⟩ := g
have : rf = rg := by
funext u v
exact propext (h u v)
subst this
rfl
private theorem Approximable_singleton_funion_eq (a : β) (s : Finset β) :
({a} : Finset β) ∪' s = insert a s := by
ext x
constructor
· intro hx
rcases mem_funion.mp hx with ha | hs
· exact Finset.mem_insert.mpr (Or.inl (Finset.mem_singleton.mp ha))
· exact Finset.mem_insert_of_mem hs
· intro hx
rcases Finset.mem_insert.mp hx with ha | hs
· exact mem_funion.mpr (Or.inl (Finset.mem_singleton.mpr ha))
· exact mem_funion.mpr (Or.inr hs)
/-- Given `↑Y ⊆ f(x).carrier`, produce `u ⊆ x` with `u f Y`. -/
theorem exists_rel_of_subset_image (f : ApproximableMap A B) (x : A.Element)
(Y : Finset β)