SemanticCover.lean

1 import ProofPath.Extension
2 
3 /-!
4 An exact semantic replacement for whole-support coverage.
5 No constraint is silently discarded: every discarded rule needs a derivation
6 of its conclusion from its premises in the retained system.
7 -/
8 namespace ProofPath
9 namespace Field
10 variable {ι J I : Type*} (F : Field ι J)
11 
12 def filtered (keep : J → Prop) : Field ι J :=
13   { F with certified := fun j => F.certified j ∧ keep j }
14 
15 theorem filtered_model_of_model (keep : J → Prop) {x : ι → Prop}
16     (hx : F.Model x) : (F.filtered keep).Model x :=
17   ⟨hx.1, fun j hj hp => hx.2 j hj.1 hp⟩
18 
19 /-- Retained rules suffice precisely when each original rule is entailed. -/
20 theorem filtered_models_iff_rule_entailment (keep : J → Prop) :
21     (∀ x, (F.filtered keep).Model x → F.Model x) ↔
22       ∀ j, F.certified j → F.conclusion j ∈ (F.filtered keep).closure (F.premises j) := by
23   constructor
24   · intro h j hc
25     have hx := h _ ((F.filtered keep).closure_is_model (F.premises j))
26     exact hx.2 j hc (fun v hv => (F.filtered keep).closure_contains_seed _ hv)
27   · intro h x hx
28     refine ⟨hx.1, ?_⟩
29     intro j hc hp
30     exact (F.filtered keep).closure_le_model _ hx hp _ (h j hc)
31 
32 /-- A complete entailment check preserves every seeded closure, not just one goal. -/
33 theorem filtered_closures_iff_rule_entailment (keep : J → Prop) :
34     (∀ S, (F.filtered keep).closure S = F.closure S) ↔
35       ∀ j, F.certified j → F.conclusion j ∈ (F.filtered keep).closure (F.premises j) := by
36   constructor
37   · intro h j hc
38     rw [h]
39     exact Derives.step j hc (fun v hv => F.closure_contains_seed _ hv)
40   · intro h S
41     apply Set.Subset.antisymm
42     · exact (F.filtered keep).closure_le_model S
43         (F.filtered_model_of_model keep (F.closure_is_model S))
44         (fun _ hv => F.closure_contains_seed S hv)
45     · exact F.closure_le_model S
46         ((F.filtered_models_iff_rule_entailment keep).mpr h _
47           ((F.filtered keep).closure_is_model S))
48         (fun _ hv => (F.filtered keep).closure_contains_seed S hv)
49 
50 def visible (U : I → Set ι) : Field ι J :=
51   F.filtered (fun j => ∃ i, F.support j ⊆ U i)
52 
53 def SemanticCover (U : I → Set ι) : Prop :=
54   ∀ j, F.certified j → F.conclusion j ∈ (F.visible U).closure (F.premises j)
55 
56 theorem support_cover_is_semantic (U : I → Set ι)
57     (hsup : ∀ j, F.certified j → ∃ i, F.support j ⊆ U i) :
58     F.SemanticCover U := by
59   intro j hc
60   exact Derives.step j ⟨hc, hsup j hc⟩
61     (fun v hv => (F.visible U).closure_contains_seed _ hv)
62 
63 /-- Matching data already satisfy all rules whose supports the patches see. -/
64 theorem matching_visible_model (U : I → Set ι) (s : ∀ i, F.Local (U i))
65     (hcov : ∀ v, ∃ i, v ∈ U i) (hm : F.Matching U s) :
66     (F.visible U).Model (F.gluedValue U s) := by
67   constructor
68   · intro v hl
69     obtain ⟨i, hi⟩ := hcov v
70     exact ⟨i, hi, (s i).leaves v hl hi⟩
71   · rintro j ⟨hc, i, hs⟩ hp
72     apply (F.glued_agrees U s hm i (hs (Set.mem_insert _ _))).mpr
73     apply (s i).rules j hc hs
74     intro v hv
75     exact (F.glued_agrees U s hm i (hs (Set.mem_insert_of_mem _ hv))).mp (hp v hv)
76 
77 theorem semantic_cover_gluing (U : I → Set ι) (s : ∀ i, F.Local (U i))
78     (hcov : ∀ v, ∃ i, v ∈ U i) (hsem : F.SemanticCover U)
79     (hm : F.Matching U s) :
80     ∃! x : ι → Prop, F.Model x ∧
81       ∀ i v, v ∈ U i → (x v ↔ (s i).val v) := by
82   have hx := (F.filtered_models_iff_rule_entailment _).mpr hsem _
83     (F.matching_visible_model U s hcov hm)
84   refine ⟨F.gluedValue U s, ⟨hx, ?_⟩, ?_⟩
85   · intro i v hv
86     exact F.glued_agrees U s hm i hv
87   · intro y hy
88     funext v
89     obtain ⟨i, hi⟩ := hcov v
90     exact propext ((hy.2 i v hi).trans (F.glued_agrees U s hm i hi).symm)
91 
92 /-- A visible model restricts to genuine local models of the original field. -/
93 def visibleLocal (U : I → Set ι) (x : ι → Prop)
94     (hx : (F.visible U).Model x) (i : I) : F.Local (U i) where
95   val v := v ∈ U i ∧ x v
96   outside _ hv h := hv h.1
97   leaves _ hl hu := ⟨hu, hx.1 _ hl⟩
98   rules j hc hs hp :=
99     ⟨hs (Set.mem_insert _ _), hx.2 j ⟨hc, i, hs⟩ (fun v hv => (hp v hv).2)⟩
100 
101 /-- With node coverage, semantic cover is necessary and sufficient for all gluing. -/
102 theorem universal_gluing_iff_semantic_cover (U : I → Set ι)
103     (hcov : ∀ v, ∃ i, v ∈ U i) :
104     (∀ (s : ∀ i, F.Local (U i)), F.Matching U s →
105       ∃! x : ι → Prop, F.Model x ∧ ∀ i v, v ∈ U i → (x v ↔ (s i).val v)) ↔
106       F.SemanticCover U := by
107   constructor
108   · intro hall
109     apply (F.filtered_models_iff_rule_entailment _).mp
110     intro x hx
111     let s := F.visibleLocal U x hx
112     have hm : F.Matching U s := by
113       intro i j v hi hj
114       exact ⟨fun h => ⟨hj, h.2⟩, fun h => ⟨hi, h.2⟩⟩
115     obtain ⟨y, hy, _⟩ := hall s hm
116     have hxy : x = y := by
117       funext v
118       obtain ⟨i, hi⟩ := hcov v
119       apply propext
120       exact ⟨fun h => (hy.2 i v hi).mpr ⟨hi, h⟩,
121         fun h => ((hy.2 i v hi).mp h).2⟩
122     rw [hxy]
123     exact hy.1
124   · intro hsem s hm
125     exact F.semantic_cover_gluing U s hcov hsem hm
126 
127 end Field
128 end ProofPath

Back to source controls