Skip to content

perf(DomainTheory): narrow imports and factor repeated proofs #720

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Vilin97 wants to merge 1 commit into
base: main
Choose a base branch
from
Open

perf(DomainTheory): narrow imports and factor repeated proofs #720

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
194 changes: 65 additions & 129 deletions LeanPool/DomainTheory.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,155 +5,91 @@ Authors: Catskills Research Company
-/
module

public import LeanPool.DomainTheory.Constructive
public import LeanPool.DomainTheory.InfoSys
public import LeanPool.DomainTheory.ContinuousLattice.Injective
public import LeanPool.DomainTheory.ContinuousLattice.WayBelow
public import LeanPool.DomainTheory.ContinuousLattice.Specialization
public import LeanPool.DomainTheory.ContinuousLattice.ScottMaps
public import LeanPool.DomainTheory.ContinuousLattice.MilnerCorrection
public import LeanPool.DomainTheory.ContinuousLattice.Constructions
public import LeanPool.DomainTheory.ContinuousLattice.FunctionSpaces
public import LeanPool.DomainTheory.ContinuousLattice.Theorem212
public import LeanPool.DomainTheory.ContinuousLattice.InverseLimits
-- Terminal imports retain the complete public API. Start with the long independent branches.
public import LeanPool.DomainTheory.Neighborhood.Exercise617Gen
public import LeanPool.DomainTheory.Neighborhood.Theorem76
public import LeanPool.DomainTheory.ContinuousLattice.FunctionSpaceTower
public import LeanPool.DomainTheory.Neighborhood.Basic
public import LeanPool.DomainTheory.Neighborhood.Example12
public import LeanPool.DomainTheory.Neighborhood.Example13
public import LeanPool.DomainTheory.Neighborhood.Exercise623
public import LeanPool.DomainTheory.Neighborhood.Exercise509
public import LeanPool.DomainTheory.Neighborhood.Theorem56Full
public import LeanPool.DomainTheory.Neighborhood.Proposition77
public import LeanPool.DomainTheory.Neighborhood.Exercise516Overlap
public import LeanPool.DomainTheory.Neighborhood.Theorem616
public import LeanPool.DomainTheory.Neighborhood.Exercise415
public import LeanPool.DomainTheory.Neighborhood.Example14
public import LeanPool.DomainTheory.Neighborhood.Example15
public import LeanPool.DomainTheory.Neighborhood.ExampleB
public import LeanPool.DomainTheory.Neighborhood.Theorem110
public import LeanPool.DomainTheory.Neighborhood.Theorem111
public import LeanPool.DomainTheory.Neighborhood.Exercise112
public import LeanPool.DomainTheory.Neighborhood.Theorem614
public import LeanPool.DomainTheory.Neighborhood.Exercise215
public import LeanPool.DomainTheory.Neighborhood.Exercise327
public import LeanPool.DomainTheory.Neighborhood.Exercise422
public import LeanPool.DomainTheory.Neighborhood.Exercise626
public import LeanPool.DomainTheory.Neighborhood.Exercise514
public import LeanPool.DomainTheory.Neighborhood.Proposition53
public import LeanPool.DomainTheory.Neighborhood.Exercise618
public import LeanPool.DomainTheory.Neighborhood.Exercise627
public import LeanPool.DomainTheory.Neighborhood.Exercise113
public import LeanPool.DomainTheory.Neighborhood.Exercise114
public import LeanPool.DomainTheory.Neighborhood.Exercise119
public import LeanPool.DomainTheory.Neighborhood.Exercise121
public import LeanPool.DomainTheory.Neighborhood.Example13
public import LeanPool.DomainTheory.Neighborhood.Exercise508
public import LeanPool.DomainTheory.Neighborhood.Exercise622
public import LeanPool.DomainTheory.Neighborhood.Exercise629
public import LeanPool.DomainTheory.Neighborhood.Example62A
public import LeanPool.DomainTheory.ContinuousLattice.Theorem212
public import LeanPool.DomainTheory.Neighborhood.Exercise126
public import LeanPool.DomainTheory.Neighborhood.Exercise625
public import LeanPool.DomainTheory.Neighborhood.Exercise115
public import LeanPool.DomainTheory.Neighborhood.Exercise317
public import LeanPool.DomainTheory.Neighborhood.Exercise328
public import LeanPool.DomainTheory.Neighborhood.Exercise112
public import LeanPool.DomainTheory.Neighborhood.Exercise116
public import LeanPool.DomainTheory.Neighborhood.Exercise220
public import LeanPool.DomainTheory.Neighborhood.Exercise324Iter
public import LeanPool.DomainTheory.Neighborhood.Exercise325
public import LeanPool.DomainTheory.Neighborhood.Theorem56
public import LeanPool.DomainTheory.Neighborhood.Exercise515
public import LeanPool.DomainTheory.Neighborhood.Proposition611
public import LeanPool.DomainTheory.Neighborhood.Exercise117
public import LeanPool.DomainTheory.Neighborhood.Exercise118
public import LeanPool.DomainTheory.Neighborhood.Exercise119
public import LeanPool.DomainTheory.Neighborhood.Exercise120
public import LeanPool.DomainTheory.Neighborhood.Exercise121
public import LeanPool.DomainTheory.Neighborhood.Exercise122
public import LeanPool.DomainTheory.Neighborhood.Exercise123
public import LeanPool.DomainTheory.Neighborhood.Exercise124
public import LeanPool.DomainTheory.Neighborhood.Exercise125
public import LeanPool.DomainTheory.Neighborhood.Exercise126
public import LeanPool.DomainTheory.Neighborhood.Exercise127
public import LeanPool.DomainTheory.Neighborhood.Approximable
public import LeanPool.DomainTheory.Neighborhood.ApproximableExercises
public import LeanPool.DomainTheory.Neighborhood.Example23
public import LeanPool.DomainTheory.Neighborhood.Example24
public import LeanPool.DomainTheory.Neighborhood.Exercise213
public import LeanPool.DomainTheory.Neighborhood.Exercise214
public import LeanPool.DomainTheory.Neighborhood.Exercise215
public import LeanPool.DomainTheory.Neighborhood.Exercise216
public import LeanPool.DomainTheory.Neighborhood.Exercise218
public import LeanPool.DomainTheory.Neighborhood.Exercise220
public import LeanPool.DomainTheory.Neighborhood.Exercise221
public import LeanPool.DomainTheory.Neighborhood.Exercise222
public import LeanPool.DomainTheory.Neighborhood.Product
public import LeanPool.DomainTheory.Neighborhood.FunctionSpace
public import LeanPool.DomainTheory.Neighborhood.Exercise314
public import LeanPool.DomainTheory.Neighborhood.Exercise315
public import LeanPool.DomainTheory.Neighborhood.Exercise318
public import LeanPool.DomainTheory.Neighborhood.Exercise319
public import LeanPool.DomainTheory.Neighborhood.Exercise319Sum
public import LeanPool.DomainTheory.Neighborhood.Exercise321
public import LeanPool.DomainTheory.Neighborhood.Exercise322
public import LeanPool.DomainTheory.Neighborhood.Exercise323
public import LeanPool.DomainTheory.Neighborhood.Exercise324
public import LeanPool.DomainTheory.Neighborhood.Exercise316
public import LeanPool.DomainTheory.Neighborhood.Exercise317
public import LeanPool.DomainTheory.Neighborhood.Exercise324Iter
public import LeanPool.DomainTheory.Neighborhood.Exercise324Distrib
public import LeanPool.DomainTheory.Neighborhood.Exercise325
public import LeanPool.DomainTheory.Neighborhood.Exercise327
public import LeanPool.DomainTheory.Neighborhood.Exercise326
public import LeanPool.DomainTheory.Neighborhood.Exercise326Sum
public import LeanPool.DomainTheory.Neighborhood.Exercise328
public import LeanPool.DomainTheory.Neighborhood.Theorem41
public import LeanPool.DomainTheory.Neighborhood.Example43
public import LeanPool.DomainTheory.Neighborhood.Example44
public import LeanPool.DomainTheory.Neighborhood.Theorem46
public import LeanPool.DomainTheory.Neighborhood.Exercise407
public import LeanPool.DomainTheory.Neighborhood.Exercise408
public import LeanPool.DomainTheory.Neighborhood.Exercise409
public import LeanPool.DomainTheory.Neighborhood.Exercise410
public import LeanPool.DomainTheory.Neighborhood.Exercise411
public import LeanPool.DomainTheory.Neighborhood.Exercise412
public import LeanPool.DomainTheory.Neighborhood.Exercise413
public import LeanPool.DomainTheory.Neighborhood.Exercise414
public import LeanPool.DomainTheory.Neighborhood.Exercise415
public import LeanPool.DomainTheory.Neighborhood.Exercise416
public import LeanPool.DomainTheory.Neighborhood.Exercise417
public import LeanPool.DomainTheory.Neighborhood.Exercise418
public import LeanPool.DomainTheory.Neighborhood.Exercise419
public import LeanPool.DomainTheory.Neighborhood.Exercise420
public import LeanPool.DomainTheory.Neighborhood.Exercise421
public import LeanPool.DomainTheory.Neighborhood.Exercise422
public import LeanPool.DomainTheory.Neighborhood.Theorem51
public import LeanPool.DomainTheory.Neighborhood.Proposition54
public import LeanPool.DomainTheory.Neighborhood.Exercise624
public import LeanPool.DomainTheory.Neighborhood.Exercise628
public import LeanPool.DomainTheory.Constructive
public import LeanPool.DomainTheory.Neighborhood.Exercise120
public import LeanPool.DomainTheory.Neighborhood.Exercise324Distrib
public import LeanPool.DomainTheory.Neighborhood.Exercise423
public import LeanPool.DomainTheory.Neighborhood.Exercise424
public import LeanPool.DomainTheory.Neighborhood.Exercise425
public import LeanPool.DomainTheory.Neighborhood.Table55
public import LeanPool.DomainTheory.Neighborhood.Theorem51
public import LeanPool.DomainTheory.Neighborhood.Theorem52
public import LeanPool.DomainTheory.Neighborhood.Proposition53
public import LeanPool.DomainTheory.Neighborhood.Proposition54
public import LeanPool.DomainTheory.Neighborhood.Theorem56
public import LeanPool.DomainTheory.Neighborhood.Theorem56Full
public import LeanPool.DomainTheory.Neighborhood.Exercise507
public import LeanPool.DomainTheory.Neighborhood.Exercise508
public import LeanPool.DomainTheory.Neighborhood.Exercise509
public import LeanPool.DomainTheory.Neighborhood.Exercise510
public import LeanPool.DomainTheory.Neighborhood.Exercise511
public import LeanPool.DomainTheory.Neighborhood.Exercise512
public import LeanPool.DomainTheory.Neighborhood.Exercise513
public import LeanPool.DomainTheory.Neighborhood.Exercise514
public import LeanPool.DomainTheory.Neighborhood.Exercise515
public import LeanPool.DomainTheory.Neighborhood.Exercise516
public import LeanPool.DomainTheory.Neighborhood.Exercise516ThueMorse
public import LeanPool.DomainTheory.Neighborhood.Exercise516Overlap
public import LeanPool.DomainTheory.Neighborhood.Example61
public import LeanPool.DomainTheory.Neighborhood.Example62
public import LeanPool.DomainTheory.Neighborhood.Example62C
public import LeanPool.DomainTheory.Neighborhood.Example62A
public import LeanPool.DomainTheory.Neighborhood.Example62Regular
public import LeanPool.DomainTheory.Neighborhood.Definition63
public import LeanPool.DomainTheory.InfoSys
public import LeanPool.DomainTheory.Neighborhood.Exercise218
public import LeanPool.DomainTheory.Neighborhood.Exercise324
public import LeanPool.DomainTheory.Neighborhood.Exercise409
public import LeanPool.DomainTheory.Neighborhood.Exercise420
public import LeanPool.DomainTheory.Neighborhood.Exercise512
public import LeanPool.DomainTheory.Neighborhood.Exercise322
public import LeanPool.DomainTheory.Neighborhood.Exercise418
public import LeanPool.DomainTheory.Neighborhood.Exercise214
public import LeanPool.DomainTheory.Neighborhood.Exercise216
public import LeanPool.DomainTheory.Neighborhood.Exercise417
public import LeanPool.DomainTheory.ContinuousLattice.MilnerCorrection
public import LeanPool.DomainTheory.Neighborhood.Exercise323
public import LeanPool.DomainTheory.Neighborhood.Exercise114
public import LeanPool.DomainTheory.Neighborhood.Example24
public import LeanPool.DomainTheory.Neighborhood.Exercise424
public import LeanPool.DomainTheory.Neighborhood.Exercise412
public import LeanPool.DomainTheory.Neighborhood.Proposition66
public import LeanPool.DomainTheory.Neighborhood.Example15
public import LeanPool.DomainTheory.Neighborhood.Exercise314
public import LeanPool.DomainTheory.Neighborhood.Exercise213
public import LeanPool.DomainTheory.Neighborhood.Proposition67
public import LeanPool.DomainTheory.Neighborhood.Definition68
public import LeanPool.DomainTheory.Neighborhood.Theorem69
public import LeanPool.DomainTheory.Neighborhood.Definition610
public import LeanPool.DomainTheory.Neighborhood.Proposition611
public import LeanPool.DomainTheory.Neighborhood.Proposition612
public import LeanPool.DomainTheory.Neighborhood.Definition613
public import LeanPool.DomainTheory.Neighborhood.Theorem614
public import LeanPool.DomainTheory.Neighborhood.Lemma615
public import LeanPool.DomainTheory.Neighborhood.Theorem616
public import LeanPool.DomainTheory.Neighborhood.Exercise617
public import LeanPool.DomainTheory.Neighborhood.Exercise617Gen
public import LeanPool.DomainTheory.Neighborhood.Exercise618
public import LeanPool.DomainTheory.Neighborhood.Exercise619
public import LeanPool.DomainTheory.Neighborhood.Exercise619PartB
public import LeanPool.DomainTheory.Neighborhood.Exercise621
public import LeanPool.DomainTheory.Neighborhood.Exercise622
public import LeanPool.DomainTheory.Neighborhood.Exercise623
public import LeanPool.DomainTheory.Neighborhood.Exercise624
public import LeanPool.DomainTheory.Neighborhood.Exercise625
public import LeanPool.DomainTheory.Neighborhood.Exercise626
public import LeanPool.DomainTheory.Neighborhood.Exercise627
public import LeanPool.DomainTheory.Neighborhood.Exercise628
public import LeanPool.DomainTheory.Neighborhood.Exercise629
public import LeanPool.DomainTheory.Neighborhood.Recursive
public import LeanPool.DomainTheory.Neighborhood.Definition71
public import LeanPool.DomainTheory.Neighborhood.Definition72
public import LeanPool.DomainTheory.Neighborhood.Theorem74
public import LeanPool.DomainTheory.Neighborhood.Theorem75
public import LeanPool.DomainTheory.Neighborhood.Theorem76
public import LeanPool.DomainTheory.Neighborhood.Proposition77
import Mathlib.Data.Rat.Floor

/-!
# DomainTheory
Expand Down
15 changes: 8 additions & 7 deletions LeanPool/DomainTheory/ContinuousLattice/Constructions.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,7 +117,7 @@ theorem proposition_2_9_a {ι : Type*} (E : ι → Type*) [∀ i, CompleteLattic
· rw [hei]; exact Set.mem_Ici.1 (hUsub hz)
· rw [he, Function.update_of_ne hji]; exact bot_le
have hle : e i ≤ b i := (hb hcyl) i
simp_all
simp_all only [mem_ofPred_eq, Function.update_self]

/-! ### Proposition 2.9(b): the induced topology of a product is the product
topology
Expand Down Expand Up @@ -159,8 +159,9 @@ theorem update_preservesDirectedSup {ι : Type*} [DecidableEq ι] {E : ι → Ty
rw [sSup_apply_eq_sSup_image, Set.image_image]
rcases eq_or_ne j i with hji | hji
· rw [hji, Function.update_self]
simp_all
· simp_all
simp_all only [Function.eval, Function.update_self, image_id']
· simp_all only [ne_eq, not_false_eq_true, Function.update_of_ne, Function.eval,
Nonempty.image_const, sSup_singleton]

/-- A way-below relation in a product projects to each coordinate: if `a ≪ z` in
`∏ᵢ Eᵢ` then
Expand All @@ -174,7 +175,7 @@ theorem wayBelow_proj {ι : Type*} {E : ι → Type*} [∀ i, CompleteLattice (E
obtain ⟨W, hW, hzW, hWsub⟩ := h
refine ⟨(fun v : E i => Function.update z i v) ⁻¹' W, ?_, ?_, ?_⟩
· exact scottOpen_preimage (update_preservesDirectedSup z i) hW
· simp_all
· simp_all only [mem_preimage, Function.update_eq_self]
· intro v hv
have hav : a ≤ Function.update z i v := Set.mem_Ici.1 (hWsub hv)
have := hav i
Expand Down Expand Up @@ -216,13 +217,13 @@ theorem wayBelow_finite_support {ι : Type*} {E : ι → Type*} [∀ i, Complete
· rw [Pi.le_def]; intro j
rw [sSup_apply_eq_sSup_image]
refine le_sSup ⟨Z {j}, ⟨{j}, rfl⟩, ?_⟩
simp [hZ, Function.eval]
simp only [Function.eval, hZ, Finset.mem_singleton, ↓reduceIte]
rw [← hsup] at h
obtain ⟨d, hd𝒵, had⟩ := (wayBelow_sSup_iff h𝒵ne h𝒵dir).1 h
obtain ⟨F, rfl⟩ := hd𝒵
refine ⟨F, fun j hjF => ?_⟩
have hj := had.le j
simp_all
simp_all only [↓reduceIte, le_bot_iff]

/-- **Scott 1972, Proposition 2.9(b).** For a family of continuous lattices, the
Scott topology of
Expand Down Expand Up @@ -267,7 +268,7 @@ theorem proposition_2_9_b {ι : Type*} (E : ι → Type*) [∀ i, CompleteLattic
exact iInf_le
(fun i => TopologicalSpace.induced (fun w : ∀ j, E j => w i) scottTopologicalSpace) i _ hind
· -- the box contains `z`
simp_all
simp_all only [mem_iInter, mem_preimage, implies_true]

/-- **Scott 1972, Proposition 2.9 (full statement).** The product of a family of
continuous lattices
Expand Down
Loading
Loading