Transport.lean

1 import ProofPath.Extension
2 
3 /-!
4 An explicit interpretation contract between declared rule fields.
5 It transports actual inductive derivations and pulls target models back.
6 -/
7 namespace ProofPath
8 variable {ι κ ν J K M : Type*}
9 
10 structure RuleTransport (F : Field ι J) (G : Field κ K) where
11   node : ι → κ
12   rule : J → K
13   leaves : ∀ v, v ∈ F.leaf → node v ∈ G.leaf
14   certified : ∀ j, F.certified j → G.certified (rule j)
15   premises : ∀ j w, w ∈ G.premises (rule j) → ∃ v, v ∈ F.premises j ∧ node v = w
16   conclusion : ∀ j, node (F.conclusion j) = G.conclusion (rule j)
17 
18 namespace RuleTransport
19 variable {F : Field ι J} {G : Field κ K} {H : Field ν M}
20 
21 def identity (F : Field ι J) : RuleTransport F F where
22   node := id
23   rule := id
24   leaves := fun _ h => h
25   certified := fun _ h => h
26   premises := fun _ w h => ⟨w, h, rfl⟩
27   conclusion := fun _ => rfl
28 
29 def comp (a : RuleTransport F G) (b : RuleTransport G H) : RuleTransport F H where
30   node := b.node ∘ a.node
31   rule := b.rule ∘ a.rule
32   leaves := fun v h => b.leaves _ (a.leaves v h)
33   certified := fun j h => b.certified _ (a.certified j h)
34   premises := by
35     intro j w hw
36     obtain ⟨u, hu, he⟩ := b.premises (a.rule j) w hw
37     obtain ⟨v, hv, hvu⟩ := a.premises j u hu
38     exact ⟨v, hv, (congrArg b.node hvu).trans he⟩
39   conclusion := fun j => (congrArg b.node (a.conclusion j)).trans (b.conclusion (a.rule j))
40 
41 @[ext] theorem ext (a b : RuleTransport F G)
42     (hn : a.node = b.node) (hr : a.rule = b.rule) : a = b := by
43   cases a
44   cases b
45   cases hn
46   cases hr
47   rfl
48 
49 theorem identity_comp (a : RuleTransport F G) : comp (identity F) a = a := by
50   apply ext <;> rfl
51 
52 theorem comp_identity (a : RuleTransport F G) : comp a (identity G) = a := by
53   apply ext <;> rfl
54 
55 theorem comp_assoc {ω N : Type*} {Q : Field ω N}
56     (a : RuleTransport F G) (b : RuleTransport G H) (c : RuleTransport H Q) :
57     comp (comp a b) c = comp a (comp b c) := by
58   apply ext <;> rfl
59 
60 theorem derives_map (a : RuleTransport F G) {v : ι} (hv : F.Derives v) :
61     G.Derives (a.node v) := by
62   induction hv with
63   | leaf h => exact Field.Derives.leaf (a.leaves _ h)
64   | step j hc _ ih =>
65     rw [a.conclusion j]
66     apply Field.Derives.step (a.rule j) (a.certified j hc)
67     intro w hw
68     obtain ⟨v, hv, h⟩ := a.premises j w hw
69     rw [← h]
70     exact ih v hv
71 
72 theorem model_pullback (a : RuleTransport F G) {x : κ → Prop} (hx : G.Model x) :
73     F.Model (x ∘ a.node) := by
74   constructor
75   · exact fun v hv => hx.1 _ (a.leaves v hv)
76   · intro j hc hp
77     change x (a.node (F.conclusion j))
78     rw [a.conclusion j]
79     apply hx.2 (a.rule j) (a.certified j hc)
80     intro w hw
81     obtain ⟨v, hv, he⟩ := a.premises j w hw
82     rw [← he]
83     exact hp v hv
84 
85 theorem extension_pullback (a : RuleTransport F G) (S N : Set ι)
86     {x : κ → Prop} (hx : G.Extends (a.node '' S) (a.node '' N) x) :
87     F.Extends S N (x ∘ a.node) := by
88   refine ⟨a.model_pullback hx.1, ?_, ?_⟩
89   · exact fun v hv => hx.2.1 _ ⟨v, hv, rfl⟩
90   · exact fun v hv => hx.2.2 _ ⟨v, hv, rfl⟩
91 
92 /-- Infeasibility transports in the direction opposite to model pullback. -/
93 theorem obstruction_pushforward (a : RuleTransport F G) (S N : Set ι)
94     (h : ¬ ∃ x, F.Extends S N x) :
95     ¬ ∃ x, G.Extends (a.node '' S) (a.node '' N) x := by
96   rintro ⟨x, hx⟩
97   exact h ⟨x ∘ a.node, a.extension_pullback S N hx⟩
98 
99 /-- Semantic soundness is transported, not manufactured by the node labels. -/
100 theorem semantic_transport (a : RuleTransport F G) (meaning : κ → Prop)
101     (hm : G.Model meaning) {v : ι} (hv : F.Derives v) : meaning (a.node v) :=
102   G.derives_sound hm (a.derives_map hv)
103 
104 /-- Positive observations are transported as admitted data, not renamed conclusions. -/
105 def seeded (a : RuleTransport F G) (S : Set ι) :
106     RuleTransport (F.seeded S) (G.seeded (a.node '' S)) where
107   node := a.node
108   rule := a.rule
109   leaves := by
110     intro v hv
111     rcases hv with hv | hv
112     · exact Or.inl (a.leaves v hv)
113     · exact Or.inr ⟨v, hv, rfl⟩
114   certified := a.certified
115   premises := a.premises
116   conclusion := a.conclusion
117 
118 theorem closure_map (a : RuleTransport F G) (S : Set ι) {v : ι}
119     (hv : v ∈ F.closure S) : a.node v ∈ G.closure (a.node '' S) :=
120   (a.seeded S).derives_map hv
121 
122 theorem obstruction_witness_map (a : RuleTransport F G) (S N : Set ι) {v : ι}
123     (hn : v ∈ N) (hv : v ∈ F.closure S) :
124     a.node v ∈ a.node '' N ∧ a.node v ∈ G.closure (a.node '' S) :=
125   ⟨⟨v, hn, rfl⟩, a.closure_map S hv⟩
126 
127 end RuleTransport
128 end ProofPath

Back to source controls