Field.lean

1 import Mathlib.Data.Set.Lattice.Indexed
2 
3 /-!
4 The proof field induces a contravariant system of local Horn models.
5 Support coverage is coverage of whole justifications, not pairwise edges.
6 -/
7 namespace ProofPath
8 
9 structure Field (ι J : Type*) where
10   leaf : Set ι
11   premises : J → Set ι
12   conclusion : J → ι
13   certified : J → Prop
14 
15 namespace Field
16 variable {ι J I : Type*} (F : Field ι J)
17 
18 def support (j : J) : Set ι := insert (F.conclusion j) (F.premises j)
19 
20 inductive Derives : ι → Prop where
21   | leaf {v} : v ∈ F.leaf → Derives v
22   | step (j) : F.certified j → (∀ v, v ∈ F.premises j → Derives v) →
23       Derives (F.conclusion j)
24 
25 def Model (x : ι → Prop) : Prop :=
26   (∀ v, v ∈ F.leaf → x v) ∧
27   (∀ j, F.certified j → (∀ v, v ∈ F.premises j → x v) → x (F.conclusion j))
28 
29 theorem derives_sound {x : ι → Prop} (hx : F.Model x) {v : ι}
30     (h : F.Derives v) : x v := by
31   induction h with
32   | leaf h => exact hx.1 _ h
33   | step j hc _ ih => exact hx.2 j hc ih
34 
35 theorem derives_model : F.Model F.Derives :=
36   ⟨fun _ h => Derives.leaf h, fun j hc hp => Derives.step j hc hp⟩
37 
38 theorem derives_iff_all_models (v : ι) :
39     F.Derives v ↔ ∀ x, F.Model x → x v := by
40   exact ⟨fun h _ hx => F.derives_sound hx h, fun h => h F.Derives F.derives_model⟩
41 
42 theorem nonderivable_countermodel {v : ι} (h : ¬ F.Derives v) :
43     ∃ x, F.Model x ∧ ¬ x v :=
44   ⟨F.Derives, F.derives_model, h⟩
45 
46 /-- New exploratory rules cannot destroy an old certified derivation. -/
47 theorem derives_mono (G : Field ι J)
48     (hleaf : F.leaf ⊆ G.leaf)
49     (hpre : ∀ j, G.premises j = F.premises j)
50     (hcon : ∀ j, G.conclusion j = F.conclusion j)
51     (hcert : ∀ j, F.certified j → G.certified j)
52     {v : ι} (hv : F.Derives v) : G.Derives v := by
53   induction hv with
54   | leaf h => exact Derives.leaf (hleaf h)
55   | step j hc _ ih =>
56     rw [← hcon j]
57     exact Derives.step j (hcert j hc) (by simpa [hpre j] using ih)
58 
59 /-- Outside values are normalized to false, so there are no hidden coordinates. -/
60 structure Local (U : Set ι) where
61   val : ι → Prop
62   outside : ∀ v, v ∉ U → ¬ val v
63   leaves : ∀ v, v ∈ F.leaf → v ∈ U → val v
64   rules : ∀ j, F.certified j → F.support j ⊆ U →
65     (∀ v, v ∈ F.premises j → val v) → val (F.conclusion j)
66 
67 @[ext] theorem Local.ext {U : Set ι} {a b : F.Local U}
68     (h : ∀ v, a.val v ↔ b.val v) : a = b := by
69   cases a with
70   | mk a ao al ar =>
71     cases b with
72     | mk b bo bl br =>
73       have hab : a = b := funext fun v => propext (h v)
74       cases hab
75       rfl
76 
77 def restrict {U V : Set ι} (hUV : U ⊆ V) (x : F.Local V) : F.Local U where
78   val v := v ∈ U ∧ x.val v
79   outside _ hv h := hv h.1
80   leaves v hv hu := ⟨hu, x.leaves v hv (hUV hu)⟩
81   rules j hc hs hp :=
82     ⟨hs (Set.mem_insert _ _),
83       x.rules j hc (fun _ h => hUV (hs h)) (fun v hv => (hp v hv).2)⟩
84 
85 theorem restrict_identity {U : Set ι} (x : F.Local U) :
86     F.restrict (fun _ h => h) x = x := by
87   apply Local.ext
88   intro v
89   constructor
90   · exact fun h => h.2
91   · intro h
92     exact ⟨by by_contra hn; exact x.outside v hn h, h⟩
93 
94 theorem restrict_composition {U V W : Set ι} (hUV : U ⊆ V) (hVW : V ⊆ W)
95     (x : F.Local W) :
96     F.restrict hUV (F.restrict hVW x) = F.restrict (fun _ h => hVW (hUV h)) x := by
97   apply Local.ext
98   intro v
99   exact ⟨fun h => ⟨h.1, h.2.2⟩, fun h => ⟨h.1, hUV h.1, h.2⟩⟩
100 
101 def localize (x : ι → Prop) (hx : F.Model x) (U : Set ι) : F.Local U where
102   val v := v ∈ U ∧ x v
103   outside _ hv h := hv h.1
104   leaves _ hl hu := ⟨hu, hx.1 _ hl⟩
105   rules j hc hs hp :=
106     ⟨hs (Set.mem_insert _ _), hx.2 j hc (fun v hv => (hp v hv).2)⟩
107 
108 def Matching (U : I → Set ι) (s : ∀ i, F.Local (U i)) : Prop :=
109   ∀ i j v, v ∈ U i → v ∈ U j → ((s i).val v ↔ (s j).val v)
110 
111 def gluedValue (U : I → Set ι) (s : ∀ i, F.Local (U i)) (v : ι) : Prop :=
112   ∃ i, v ∈ U i ∧ (s i).val v
113 
114 theorem glued_agrees (U : I → Set ι) (s : ∀ i, F.Local (U i))
115     (hm : F.Matching U s) (i : I) {v : ι} (hv : v ∈ U i) :
116     F.gluedValue U s v ↔ (s i).val v := by
117   constructor
118   · rintro ⟨j, hj, hs⟩
119     exact (hm j i v hj hv).mp hs
120   · exact fun h => ⟨i, hv, h⟩
121 
122 theorem support_cover_gluing (U : I → Set ι) (s : ∀ i, F.Local (U i))
123     (hcov : ∀ v, ∃ i, v ∈ U i)
124     (hsup : ∀ j, F.certified j → ∃ i, F.support j ⊆ U i)
125     (hm : F.Matching U s) :
126     ∃! x : ι → Prop, F.Model x ∧
127       ∀ i v, v ∈ U i → (x v ↔ (s i).val v) := by
128   have agree := F.glued_agrees U s hm
129   refine ⟨F.gluedValue U s, ⟨?_, ?_⟩, ?_⟩
130   · constructor
131     · intro v hl
132       obtain ⟨i, hi⟩ := hcov v
133       exact ⟨i, hi, (s i).leaves v hl hi⟩
134     · intro j hc hp
135       obtain ⟨i, hi⟩ := hsup j hc
136       have hcon : F.conclusion j ∈ U i := hi (Set.mem_insert _ _)
137       apply (agree i hcon).mpr
138       apply (s i).rules j hc hi
139       intro v hv
140       exact (agree i (hi (Set.mem_insert_of_mem _ hv))).mp (hp v hv)
141   · intro i v hv
142     exact agree i hv
143   · intro x hx
144     apply funext
145     intro v
146     obtain ⟨i, hi⟩ := hcov v
147     exact propext ((hx.2 i v hi).trans (agree i hi).symm)
148 
149 /-- The intended truth interpretation remains an explicit, checkable contract. -/
150 theorem semantic_soundness (meaning : ι → Prop)
151     (leaves_true : ∀ v, v ∈ F.leaf → meaning v)
152     (rules_sound : ∀ j, F.certified j →
153       (∀ v, v ∈ F.premises j → meaning v) → meaning (F.conclusion j))
154     {v : ι} (hv : F.Derives v) : meaning v :=
155   F.derives_sound ⟨leaves_true, rules_sound⟩ hv
156 
157 end Field
158 end ProofPath

Back to source controls