Extension.lean

1 import ProofPath.Field
2 
3 /-!
4 Protected extensions of the actual declared rule field.
5 Positive observations are extra leaves; negative observations are forbidden nodes.
6 -/
7 namespace ProofPath
8 namespace Field
9 variable {ι J : Type*} (F : Field ι J)
10 
11 def seeded (S : Set ι) : Field ι J := { F with leaf := F.leaf ∪ S }
12 
13 def closure (S : Set ι) : Set ι := {v | (F.seeded S).Derives v}
14 
15 def Extends (S N : Set ι) (x : ι → Prop) : Prop :=
16   F.Model x ∧ (∀ v, v ∈ S → x v) ∧ (∀ v, v ∈ N → ¬ x v)
17 
18 theorem closure_contains_seed (S : Set ι) : S ⊆ F.closure S := by
19   intro v hv
20   exact Derives.leaf (Or.inr hv)
21 
22 theorem closure_is_model (S : Set ι) : F.Model (F.closure S) := by
23   constructor
24   · intro v hv
25     exact Derives.leaf (Or.inl hv)
26   · intro j hc hp
27     exact Derives.step j hc hp
28 
29 theorem closure_le_model (S : Set ι) {x : ι → Prop}
30     (hx : F.Model x) (hs : ∀ v, v ∈ S → x v) :
31     ∀ v, v ∈ F.closure S → x v := by
32   intro v hv
33   apply (F.seeded S).derives_sound ?_ hv
34   refine ⟨?_, hx.2⟩
35   intro w hw
36   rcases hw with hw | hw
37   · exact hx.1 w hw
38   · exact hs w hw
39 
40 theorem closure_mono {S T : Set ι} (hst : S ⊆ T) :
41     F.closure S ⊆ F.closure T := by
42   exact F.closure_le_model S (F.closure_is_model T)
43     (fun _ hv => F.closure_contains_seed T (hst hv))
44 
45 theorem closure_idempotent (S : Set ι) :
46     F.closure (F.closure S) = F.closure S := by
47   apply Set.Subset.antisymm
48   · exact F.closure_le_model _ (F.closure_is_model S) (fun _ hv => hv)
49   · exact F.closure_contains_seed _
50 
51 /-- Existence of a protected extension is decided by one least closure. -/
52 theorem extension_iff_avoids_closure (S N : Set ι) :
53     (∃ x, F.Extends S N x) ↔ ∀ v, v ∈ N → v ∉ F.closure S := by
54   constructor
55   · rintro ⟨x, hx, hs, hn⟩ v hv hc
56     exact hn v hv (F.closure_le_model S hx hs v hc)
57   · intro h
58     exact ⟨F.closure S, F.closure_is_model S,
59       fun _ hv => F.closure_contains_seed S hv, h⟩
60 
61 theorem extension_iff_closed_interval (S N : Set ι) (x : ι → Prop) :
62     F.Extends S N x ↔
63       F.Model x ∧ (∀ v, v ∈ F.closure S → x v) ∧ (∀ v, v ∈ N → ¬ x v) := by
64   constructor
65   · rintro ⟨hx, hs, hn⟩
66     exact ⟨hx, F.closure_le_model S hx hs, hn⟩
67   · rintro ⟨hx, hs, hn⟩
68     exact ⟨hx, fun _ hv => hs _ (F.closure_contains_seed S hv), hn⟩
69 
70 /-- This is a refutation of the fixed extension problem, not of an arbitrary theorem. -/
71 theorem infeasible_iff_forbidden_derivation (S N : Set ι) :
72     ¬ (∃ x, F.Extends S N x) ↔ ∃ v, v ∈ N ∧ v ∈ F.closure S := by
73   rw [extension_iff_avoids_closure]
74   push Not
75   rfl
76 
77 /-- A partial valuation prescribes both true and false values on its patch. -/
78 theorem partial_extension_iff (U S : Set ι) (hsu : S ⊆ U) :
79     (∃ x, F.Model x ∧ ∀ v, v ∈ U → (x v ↔ v ∈ S)) ↔
80       F.closure S ∩ U = S := by
81   constructor
82   · rintro ⟨x, hx, hagree⟩
83     apply Set.Subset.antisymm
84     · intro v hv
85       have hseed : ∀ w, w ∈ S → x w := fun w hw => (hagree w (hsu hw)).mpr hw
86       exact (hagree v hv.2).mp (F.closure_le_model S hx hseed v hv.1)
87     · exact fun v hv => ⟨F.closure_contains_seed S hv, hsu hv⟩
88   · intro he
89     refine ⟨F.closure S, F.closure_is_model S, ?_⟩
90     intro v hv
91     constructor
92     · intro hc
93       have hm : v ∈ F.closure S ∩ U := ⟨hc, hv⟩
94       rw [he] at hm
95       exact hm
96     · exact fun hs => F.closure_contains_seed S hs
97 
98 /-- Closing earlier positive data before adding later data changes no result. -/
99 theorem staged_closure (S T : Set ι) :
100     F.closure (F.closure S ∪ T) = F.closure (S ∪ T) := by
101   apply Set.Subset.antisymm
102   · apply F.closure_le_model _ (F.closure_is_model (S ∪ T))
103     intro v hv
104     rcases hv with hv | hv
105     · exact F.closure_mono (Set.subset_union_left) hv
106     · exact F.closure_contains_seed (S ∪ T) (Or.inr hv)
107   · apply F.closure_mono
108     intro v hv
109     rcases hv with hv | hv
110     · exact Or.inl (F.closure_contains_seed S hv)
111     · exact Or.inr hv
112 
113 /-- More observations shrink the extension fiber. -/
114 theorem extends_antitone {S T N M : Set ι} (hst : S ⊆ T) (hnm : N ⊆ M)
115     {x : ι → Prop} (hx : F.Extends T M x) : F.Extends S N x :=
116   ⟨hx.1, fun _ hv => hx.2.1 _ (hst hv), fun _ hv => hx.2.2 _ (hnm hv)⟩
117 
118 theorem obstruction_persists {S T N M : Set ι} (hst : S ⊆ T) (hnm : N ⊆ M)
119     (h : ¬ ∃ x, F.Extends S N x) : ¬ ∃ x, F.Extends T M x := by
120   rintro ⟨x, hx⟩
121   exact h ⟨x, F.extends_antitone hst hnm hx⟩
122 
123 end Field
124 end ProofPath

Back to source controls