]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/static_2/static/lsubf.ma
update in ground and delayed updating
[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / lsubf.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "ground/xoa/ex_3_3.ma".
16 include "ground/xoa/ex_4_3.ma".
17 include "ground/xoa/ex_5_5.ma".
18 include "ground/xoa/ex_5_6.ma".
19 include "ground/xoa/ex_6_5.ma".
20 include "ground/xoa/ex_7_6.ma".
21 include "static_2/notation/relations/lrsubeqf_4.ma".
22 include "ground/relocation/nstream_sor.ma".
23 include "static_2/static/frees.ma".
24
25 (* RESTRICTED REFINEMENT FOR CONTEXT-SENSITIVE FREE VARIABLES ***************)
26
27 inductive lsubf: relation4 lenv pr_map lenv pr_map ≝
28 | lsubf_atom: ∀f1,f2. f1 ≡ f2 → lsubf (⋆) f1 (⋆) f2
29 | lsubf_push: ∀f1,f2,I1,I2,L1,L2. lsubf L1 (f1) L2 (f2) →
30               lsubf (L1.ⓘ[I1]) (⫯f1) (L2.ⓘ[I2]) (⫯f2)
31 | lsubf_bind: ∀f1,f2,I,L1,L2. lsubf L1 f1 L2 f2 →
32               lsubf (L1.ⓘ[I]) (↑f1) (L2.ⓘ[I]) (↑f2)
33 | lsubf_beta: ∀f,f0,f1,f2,L1,L2,W,V. L1 ⊢ 𝐅+❨V❩ ≘ f → f0 ⋓ f ≘ f1 →
34               lsubf L1 f0 L2 f2 → lsubf (L1.ⓓⓝW.V) (↑f1) (L2.ⓛW) (↑f2)
35 | lsubf_unit: ∀f,f0,f1,f2,I1,I2,L1,L2,V. L1 ⊢ 𝐅+❨V❩ ≘ f → f0 ⋓ f ≘ f1 →
36               lsubf L1 f0 L2 f2 → lsubf (L1.ⓑ[I1]V) (↑f1) (L2.ⓤ[I2]) (↑f2)
37 .
38
39 interpretation
40   "local environment refinement (context-sensitive free variables)"
41   'LRSubEqF L1 f1 L2 f2 = (lsubf L1 f1 L2 f2).
42
43 (* Basic inversion lemmas ***************************************************)
44
45 fact lsubf_inv_atom1_aux:
46      ∀f1,f2,L1,L2. ❨L1,f1❩ ⫃𝐅+ ❨L2,f2❩ → L1 = ⋆ →
47      ∧∧ f1 ≡ f2 & L2 = ⋆.
48 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
49 [ /2 width=1 by conj/
50 | #f1 #f2 #I1 #I2 #L1 #L2 #_ #H destruct
51 | #f1 #f2 #I #L1 #L2 #_ #H destruct
52 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct
53 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #H destruct
54 ]
55 qed-.
56
57 lemma lsubf_inv_atom1: ∀f1,f2,L2. ❨⋆,f1❩ ⫃𝐅+ ❨L2,f2❩ → ∧∧ f1 ≡ f2 & L2 = ⋆.
58 /2 width=3 by lsubf_inv_atom1_aux/ qed-.
59
60 fact lsubf_inv_push1_aux:
61      ∀f1,f2,L1,L2. ❨L1,f1❩ ⫃𝐅+ ❨L2,f2❩ →
62      ∀g1,I1,K1. f1 = ⫯g1 → L1 = K1.ⓘ[I1] →
63      ∃∃g2,I2,K2. ❨K1,g1❩ ⫃𝐅+ ❨K2,g2❩ & f2 = ⫯g2 & L2 = K2.ⓘ[I2].
64 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
65 [ #f1 #f2 #_ #g1 #J1 #K1 #_ #H destruct
66 | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J1 #K1 #H1 #H2 destruct
67   <(eq_inv_pr_push_bi … H1) -g1 /2 width=6 by ex3_3_intro/
68 | #f1 #f2 #I #L1 #L2 #_ #g1 #J1 #K1 #H elim (eq_inv_pr_next_push … H)
69 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g1 #J1 #K1 #H elim (eq_inv_pr_next_push … H)
70 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g1 #J1 #K1 #H elim (eq_inv_pr_next_push … H)
71 ]
72 qed-.
73
74 lemma lsubf_inv_push1:
75       ∀g1,f2,I1,K1,L2. ❨K1.ⓘ[I1],⫯g1❩ ⫃𝐅+ ❨L2,f2❩ →
76       ∃∃g2,I2,K2. ❨K1,g1❩ ⫃𝐅+ ❨K2,g2❩ & f2 = ⫯g2 & L2 = K2.ⓘ[I2].
77 /2 width=6 by lsubf_inv_push1_aux/ qed-.
78
79 fact lsubf_inv_pair1_aux:
80      ∀f1,f2,L1,L2. ❨L1,f1❩ ⫃𝐅+ ❨L2,f2❩ →
81      ∀g1,I,K1,X. f1 = ↑g1 → L1 = K1.ⓑ[I]X →
82      ∨∨ ∃∃g2,K2. ❨K1,g1❩ ⫃𝐅+ ❨K2,g2❩ & f2 = ↑g2 & L2 = K2.ⓑ[I]X
83       | ∃∃g,g0,g2,K2,W,V. ❨K1,g0❩ ⫃𝐅+ ❨K2,g2❩ &
84           K1 ⊢ 𝐅+❨V❩ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2 &
85           I = Abbr & X = ⓝW.V & L2 = K2.ⓛW
86       | ∃∃g,g0,g2,J,K2. ❨K1,g0❩ ⫃𝐅+ ❨K2,g2❩ &
87           K1 ⊢ 𝐅+❨X❩ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2 & L2 = K2.ⓤ[J].
88 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
89 [ #f1 #f2 #_ #g1 #J #K1 #X #_ #H destruct
90 | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J #K1 #X #H elim (eq_inv_pr_push_next … H)
91 | #f1 #f2 #I #L1 #L2 #H12 #g1 #J #K1 #X #H1 #H2 destruct
92   <(eq_inv_pr_next_bi … H1) -g1 /3 width=5 by or3_intro0, ex3_2_intro/
93 | #f #f0 #f1 #f2 #L1 #L2 #W #V #Hf #Hf1 #H12 #g1 #J #K1 #X #H1 #H2 destruct
94   <(eq_inv_pr_next_bi … H1) -g1 /3 width=12 by or3_intro1, ex7_6_intro/
95 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #Hf #Hf1 #H12 #g1 #J #K1 #X #H1 #H2 destruct
96   <(eq_inv_pr_next_bi … H1) -g1 /3 width=10 by or3_intro2, ex5_5_intro/
97 ]
98 qed-.
99
100 lemma lsubf_inv_pair1:
101       ∀g1,f2,I,K1,L2,X. ❨K1.ⓑ[I]X,↑g1❩ ⫃𝐅+ ❨L2,f2❩ →
102       ∨∨ ∃∃g2,K2. ❨K1,g1❩ ⫃𝐅+ ❨K2,g2❩ & f2 = ↑g2 & L2 = K2.ⓑ[I]X
103        | ∃∃g,g0,g2,K2,W,V. ❨K1,g0❩ ⫃𝐅+ ❨K2,g2❩ &
104            K1 ⊢ 𝐅+❨V❩ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2 &
105            I = Abbr & X = ⓝW.V & L2 = K2.ⓛW
106        | ∃∃g,g0,g2,J,K2. ❨K1,g0❩ ⫃𝐅+ ❨K2,g2❩ &
107            K1 ⊢ 𝐅+❨X❩ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2 & L2 = K2.ⓤ[J].
108 /2 width=5 by lsubf_inv_pair1_aux/ qed-.
109
110 fact lsubf_inv_unit1_aux:
111      ∀f1,f2,L1,L2. ❨L1,f1❩ ⫃𝐅+ ❨L2,f2❩ →
112      ∀g1,I,K1. f1 = ↑g1 → L1 = K1.ⓤ[I] →
113      ∃∃g2,K2. ❨K1,g1❩ ⫃𝐅+ ❨K2,g2❩ & f2 = ↑g2 & L2 = K2.ⓤ[I].
114 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
115 [ #f1 #f2 #_ #g1 #J #K1 #_ #H destruct
116 | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J #K1 #H elim (eq_inv_pr_push_next … H)
117 | #f1 #f2 #I #L1 #L2 #H12 #g1 #J #K1 #H1 #H2 destruct
118   <(eq_inv_pr_next_bi … H1) -g1 /2 width=5 by ex3_2_intro/
119 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g1 #J #K1 #_ #H destruct
120 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g1 #J #K1 #_ #H destruct
121 ]
122 qed-.
123
124 lemma lsubf_inv_unit1:
125       ∀g1,f2,I,K1,L2. ❨K1.ⓤ[I],↑g1❩ ⫃𝐅+ ❨L2,f2❩ →
126       ∃∃g2,K2. ❨K1,g1❩ ⫃𝐅+ ❨K2,g2❩ & f2 = ↑g2 & L2 = K2.ⓤ[I].
127 /2 width=5 by lsubf_inv_unit1_aux/ qed-.
128
129 fact lsubf_inv_atom2_aux:
130      ∀f1,f2,L1,L2. ❨L1,f1❩ ⫃𝐅+ ❨L2,f2❩ → L2 = ⋆ →
131      ∧∧ f1 ≡ f2 & L1 = ⋆.
132 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
133 [ /2 width=1 by conj/
134 | #f1 #f2 #I1 #I2 #L1 #L2 #_ #H destruct
135 | #f1 #f2 #I #L1 #L2 #_ #H destruct
136 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct
137 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #H destruct
138 ]
139 qed-.
140
141 lemma lsubf_inv_atom2: ∀f1,f2,L1. ❨L1,f1❩ ⫃𝐅+ ❨⋆,f2❩ → ∧∧f1 ≡ f2 & L1 = ⋆.
142 /2 width=3 by lsubf_inv_atom2_aux/ qed-.
143
144 fact lsubf_inv_push2_aux:
145      ∀f1,f2,L1,L2. ❨L1,f1❩ ⫃𝐅+ ❨L2,f2❩ →
146      ∀g2,I2,K2. f2 = ⫯g2 → L2 = K2.ⓘ[I2] →
147      ∃∃g1,I1,K1. ❨K1,g1❩ ⫃𝐅+ ❨K2,g2❩ & f1 = ⫯g1 & L1 = K1.ⓘ[I1].
148 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
149 [ #f1 #f2 #_ #g2 #J2 #K2 #_ #H destruct
150 | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J2 #K2 #H1 #H2 destruct
151   <(eq_inv_pr_push_bi … H1) -g2 /2 width=6 by ex3_3_intro/
152 | #f1 #f2 #I #L1 #L2 #_ #g2 #J2 #K2 #H elim (eq_inv_pr_next_push … H)
153 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g2 #J2 #K2 #H elim (eq_inv_pr_next_push … H)
154 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g2 #J2 #K2 #H elim (eq_inv_pr_next_push … H)
155 ]
156 qed-.
157
158 lemma lsubf_inv_push2:
159       ∀f1,g2,I2,L1,K2. ❨L1,f1❩ ⫃𝐅+ ❨K2.ⓘ[I2],⫯g2❩ →
160       ∃∃g1,I1,K1. ❨K1,g1❩ ⫃𝐅+ ❨K2,g2❩ & f1 = ⫯g1 & L1 = K1.ⓘ[I1].
161 /2 width=6 by lsubf_inv_push2_aux/ qed-.
162
163 fact lsubf_inv_pair2_aux:
164      ∀f1,f2,L1,L2. ❨L1,f1❩ ⫃𝐅+ ❨L2,f2❩ →
165      ∀g2,I,K2,W. f2 = ↑g2 → L2 = K2.ⓑ[I]W →
166      ∨∨ ∃∃g1,K1. ❨K1,g1❩ ⫃𝐅+ ❨K2,g2❩ & f1 = ↑g1 & L1 = K1.ⓑ[I]W
167       | ∃∃g,g0,g1,K1,V. ❨K1,g0❩ ⫃𝐅+ ❨K2,g2❩ &
168           K1 ⊢ 𝐅+❨V❩ ≘ g & g0 ⋓ g ≘ g1 & f1 = ↑g1 &
169           I = Abst & L1 = K1.ⓓⓝW.V.
170 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
171 [ #f1 #f2 #_ #g2 #J #K2 #X #_ #H destruct
172 | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J #K2 #X #H elim (eq_inv_pr_push_next … H)
173 | #f1 #f2 #I #L1 #L2 #H12 #g2 #J #K2 #X #H1 #H2 destruct
174   <(eq_inv_pr_next_bi … H1) -g2 /3 width=5 by ex3_2_intro, or_introl/
175 | #f #f0 #f1 #f2 #L1 #L2 #W #V #Hf #Hf1 #H12 #g2 #J #K2 #X #H1 #H2 destruct
176   <(eq_inv_pr_next_bi … H1) -g2 /3 width=10 by ex6_5_intro, or_intror/
177 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g2 #J #K2 #X #_ #H destruct
178 ]
179 qed-.
180
181 lemma lsubf_inv_pair2:
182       ∀f1,g2,I,L1,K2,W. ❨L1,f1❩ ⫃𝐅+ ❨K2.ⓑ[I]W,↑g2❩ →
183       ∨∨ ∃∃g1,K1. ❨K1,g1❩ ⫃𝐅+ ❨K2,g2❩ & f1 = ↑g1 & L1 = K1.ⓑ[I]W
184        | ∃∃g,g0,g1,K1,V. ❨K1,g0❩ ⫃𝐅+ ❨K2,g2❩ &
185            K1 ⊢ 𝐅+❨V❩ ≘ g & g0 ⋓ g ≘ g1 & f1 = ↑g1 &
186            I = Abst & L1 = K1.ⓓⓝW.V.
187 /2 width=5 by lsubf_inv_pair2_aux/ qed-.
188
189 fact lsubf_inv_unit2_aux:
190      ∀f1,f2,L1,L2. ❨L1,f1❩ ⫃𝐅+ ❨L2,f2❩ →
191      ∀g2,I,K2. f2 = ↑g2 → L2 = K2.ⓤ[I] →
192      ∨∨ ∃∃g1,K1. ❨K1,g1❩ ⫃𝐅+ ❨K2,g2❩ & f1 = ↑g1 & L1 = K1.ⓤ[I]
193       | ∃∃g,g0,g1,J,K1,V. ❨K1,g0❩ ⫃𝐅+ ❨K2,g2❩ &
194           K1 ⊢ 𝐅+❨V❩ ≘ g & g0 ⋓ g ≘ g1 & f1 = ↑g1 & L1 = K1.ⓑ[J]V.
195 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
196 [ #f1 #f2 #_ #g2 #J #K2 #_ #H destruct
197 | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J #K2 #H elim (eq_inv_pr_push_next … H)
198 | #f1 #f2 #I #L1 #L2 #H12 #g2 #J #K2 #H1 #H2 destruct
199   <(eq_inv_pr_next_bi … H1) -g2 /3 width=5 by ex3_2_intro, or_introl/
200 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g2 #J #K2 #_ #H destruct
201 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #Hf #Hf1 #H12 #g2 #J #K2 #H1 #H2 destruct
202   <(eq_inv_pr_next_bi … H1) -g2 /3 width=11 by ex5_6_intro, or_intror/
203 ]
204 qed-.
205
206 lemma lsubf_inv_unit2:
207       ∀f1,g2,I,L1,K2. ❨L1,f1❩ ⫃𝐅+ ❨K2.ⓤ[I],↑g2❩ →
208       ∨∨ ∃∃g1,K1. ❨K1,g1❩ ⫃𝐅+ ❨K2,g2❩ & f1 = ↑g1 & L1 = K1.ⓤ[I]
209        | ∃∃g,g0,g1,J,K1,V. ❨K1,g0❩ ⫃𝐅+ ❨K2,g2❩ &
210            K1 ⊢ 𝐅+❨V❩ ≘ g & g0 ⋓ g ≘ g1 & f1 = ↑g1 & L1 = K1.ⓑ[J]V.
211 /2 width=5 by lsubf_inv_unit2_aux/ qed-.
212
213 (* Advanced inversion lemmas ************************************************)
214
215 lemma lsubf_inv_atom: ∀f1,f2. ❨⋆,f1❩ ⫃𝐅+ ❨⋆,f2❩ → f1 ≡ f2.
216 #f1 #f2 #H elim (lsubf_inv_atom1 … H) -H //
217 qed-.
218
219 lemma lsubf_inv_push_sn:
220       ∀g1,f2,I1,I2,K1,K2. ❨K1.ⓘ[I1],⫯g1❩ ⫃𝐅+ ❨K2.ⓘ[I2],f2❩ →
221       ∃∃g2. ❨K1,g1❩ ⫃𝐅+ ❨K2,g2❩ & f2 = ⫯g2.
222 #g1 #f2 #I #K1 #K2 #X #H elim (lsubf_inv_push1 … H) -H
223 #g2 #I #Y #H0 #H2 #H destruct /2 width=3 by ex2_intro/
224 qed-.
225
226 lemma lsubf_inv_bind_sn:
227       ∀g1,f2,I,K1,K2. ❨K1.ⓘ[I],↑g1❩ ⫃𝐅+ ❨K2.ⓘ[I],f2❩ →
228       ∃∃g2. ❨K1,g1❩ ⫃𝐅+ ❨K2,g2❩ & f2 = ↑g2.
229 #g1 #f2 * #I [2: #X ] #K1 #K2 #H
230 [ elim (lsubf_inv_pair1 … H) -H *
231   [ #z2 #Y2 #H2 #H #H0 destruct /2 width=3 by ex2_intro/
232   | #z #z0 #z2 #Y2 #W #V #_ #_ #_ #_ #H0 #_ #H destruct
233   | #z #z0 #z2 #Z2 #Y2 #_ #_ #_ #_ #H destruct
234   ]
235 | elim (lsubf_inv_unit1 … H) -H
236   #z2 #Y2 #H2 #H #H0 destruct /2 width=3 by ex2_intro/
237 ]
238 qed-.
239
240 lemma lsubf_inv_beta_sn:
241       ∀g1,f2,K1,K2,V,W. ❨K1.ⓓⓝW.V,↑g1❩ ⫃𝐅+ ❨K2.ⓛW,f2❩ →
242       ∃∃g,g0,g2. ❨K1,g0❩ ⫃𝐅+ ❨K2,g2❩ & K1 ⊢ 𝐅+❨V❩ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2.
243 #g1 #f2 #K1 #K2 #V #W #H elim (lsubf_inv_pair1 … H) -H *
244 [ #z2 #Y2 #_ #_ #H destruct
245 | #z #z0 #z2 #Y2 #X0 #X #H02 #Hz #Hg1 #H #_ #H0 #H1 destruct
246   /2 width=7 by ex4_3_intro/
247 | #z #z0 #z2 #Z2 #Y2 #_ #_ #_ #_ #H destruct
248 ]
249 qed-.
250
251 lemma lsubf_inv_unit_sn:
252       ∀g1,f2,I,J,K1,K2,V. ❨K1.ⓑ[I]V,↑g1❩ ⫃𝐅+ ❨K2.ⓤ[J],f2❩ →
253       ∃∃g,g0,g2. ❨K1,g0❩ ⫃𝐅+ ❨K2,g2❩ & K1 ⊢ 𝐅+❨V❩ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2.
254 #g1 #f2 #I #J #K1 #K2 #V #H elim (lsubf_inv_pair1 … H) -H *
255 [ #z2 #Y2 #_ #_ #H destruct
256 | #z #z0 #z2 #Y2 #X0 #X #_ #_ #_ #_ #_ #_ #H destruct
257 | #z #z0 #z2 #Z2 #Y2 #H02 #Hz #Hg1 #H0 #H1 destruct
258   /2 width=7 by ex4_3_intro/
259 ]
260 qed-.
261
262 lemma lsubf_inv_refl: ∀L,f1,f2. ❨L,f1❩ ⫃𝐅+ ❨L,f2❩ → f1 ≡ f2.
263 #L elim L -L /2 width=1 by lsubf_inv_atom/
264 #L #I #IH #f1 #f2 #H12
265 elim (pr_map_split_tl f1) * #g1 #H destruct
266 [ elim (lsubf_inv_push_sn … H12) | elim (lsubf_inv_bind_sn … H12) ] -H12
267 #g2 #H12 #H destruct /3 width=5 by pr_eq_next, pr_eq_push/
268 qed-.
269
270 (* Basic forward lemmas *****************************************************)
271
272 lemma lsubf_fwd_bind_tl:
273       ∀f1,f2,I,L1,L2. ❨L1.ⓘ[I],f1❩ ⫃𝐅+ ❨L2.ⓘ[I],f2❩ → ❨L1,⫰f1❩ ⫃𝐅+ ❨L2,⫰f2❩.
274 #f1 #f2 #I #L1 #L2 #H
275 elim (pr_map_split_tl f1) * #g1 #H0 destruct
276 [ elim (lsubf_inv_push_sn … H) | elim (lsubf_inv_bind_sn … H) ] -H
277 #g2 #H12 #H destruct //
278 qed-.
279
280 lemma lsubf_fwd_isid_dx: ∀f1,f2,L1,L2. ❨L1,f1❩ ⫃𝐅+ ❨L2,f2❩ → 𝐈❨f2❩ → 𝐈❨f1❩.
281 #f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2
282 [ /2 width=3 by pr_isi_eq_repl_fwd/
283 | /4 width=3 by pr_isi_inv_push, pr_isi_push/
284 | #f1 #f2 #I #L1 #L2 #_ #_ #H elim (pr_isi_inv_next … H) -H //
285 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H elim (pr_isi_inv_next … H) -H //
286 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #_ #H elim (pr_isi_inv_next … H) -H //
287 ]
288 qed-.
289
290 lemma lsubf_fwd_isid_sn: ∀f1,f2,L1,L2. ❨L1,f1❩ ⫃𝐅+ ❨L2,f2❩ → 𝐈❨f1❩ → 𝐈❨f2❩.
291 #f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2
292 [ /2 width=3 by pr_isi_eq_repl_back/
293 | /4 width=3 by pr_isi_inv_push, pr_isi_push/
294 | #f1 #f2 #I #L1 #L2 #_ #_ #H elim (pr_isi_inv_next … H) -H //
295 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H elim (pr_isi_inv_next … H) -H //
296 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #_ #H elim (pr_isi_inv_next … H) -H //
297 ]
298 qed-.
299
300 lemma lsubf_fwd_sle: ∀f1,f2,L1,L2. ❨L1,f1❩ ⫃𝐅+ ❨L2,f2❩ → f2 ⊆ f1.
301 #f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2
302 /3 width=5 by pr_sor_inv_sle_sn_trans, pr_sle_next, pr_sle_push, pr_sle_refl_eq, pr_eq_sym/
303 qed-.
304
305 (* Basic properties *********************************************************)
306
307 lemma lsubf_eq_repl_back1: ∀f2,L1,L2. pr_eq_repl_back … (λf1. ❨L1,f1❩ ⫃𝐅+ ❨L2,f2❩).
308 #f2 #L1 #L2 #f #H elim H -f -f2 -L1 -L2
309 [ #f1 #f2 #Hf12 #g1 #Hfg1
310   /3 width=3 by lsubf_atom, pr_eq_canc_sn/
311 | #f1 #f2 #I1 #I2 #K1 #K2 #_ #IH #g #H
312   elim (eq_inv_px … H) -H [|*: // ] #g1 #Hfg1 #H destruct
313   /3 width=1 by lsubf_push/
314 | #f1 #f2 #I #K1 #K2 #_ #IH #g #H
315   elim (eq_inv_nx … H) -H [|*: // ] #g1 #Hfg1 #H destruct
316   /3 width=1 by lsubf_bind/
317 | #f #f0 #f1 #f2 #K1 #L2 #W #V #Hf #Hf1 #_ #IH #g #H
318   elim (eq_inv_nx … H) -H [|*: // ] #g1 #Hfg1 #H destruct
319   /3 width=5 by lsubf_beta, pr_sor_eq_repl_back/
320 | #f #f0 #f1 #f2 #I1 #I2 #K1 #K2 #V #Hf #Hf1 #_ #IH #g #H
321   elim (eq_inv_nx … H) -H [|*: // ] #g1 #Hfg1 #H destruct
322   /3 width=5 by lsubf_unit, pr_sor_eq_repl_back/
323 ]
324 qed-.
325
326 lemma lsubf_eq_repl_fwd1: ∀f2,L1,L2. pr_eq_repl_fwd … (λf1. ❨L1,f1❩ ⫃𝐅+ ❨L2,f2❩).
327 #f2 #L1 #L2 @pr_eq_repl_sym /2 width=3 by lsubf_eq_repl_back1/
328 qed-.
329
330 lemma lsubf_eq_repl_back2: ∀f1,L1,L2. pr_eq_repl_back … (λf2. ❨L1,f1❩ ⫃𝐅+ ❨L2,f2❩).
331 #f1 #L1 #L2 #f #H elim H -f1 -f -L1 -L2
332 [ #f1 #f2 #Hf12 #g2 #Hfg2
333   /3 width=3 by lsubf_atom, pr_eq_trans/
334 | #f1 #f2 #I1 #I2 #K1 #K2 #_ #IH #g #H
335   elim (eq_inv_px … H) -H [|*: // ] #g2 #Hfg2 #H destruct
336   /3 width=1 by lsubf_push/
337 | #f1 #f2 #I #K1 #K2 #_ #IH #g #H
338   elim (eq_inv_nx … H) -H [|*: // ] #g2 #Hfg2 #H destruct
339   /3 width=1 by lsubf_bind/
340 | #f #f0 #f1 #f2 #K1 #L2 #W #V #Hf #Hf1 #_ #IH #g #H
341   elim (eq_inv_nx … H) -H [|*: // ] #g2 #Hfg2 #H destruct
342   /3 width=5 by lsubf_beta/
343 | #f #f0 #f1 #f2 #I1 #I2 #K1 #K2 #V #Hf #Hf1 #_ #IH #g #H
344   elim (eq_inv_nx … H) -H [|*: // ] #g2 #Hfg2 #H destruct
345   /3 width=5 by lsubf_unit/
346 ]
347 qed-.
348
349 lemma lsubf_eq_repl_fwd2: ∀f1,L1,L2. pr_eq_repl_fwd … (λf2. ❨L1,f1❩ ⫃𝐅+ ❨L2,f2❩).
350 #f1 #L1 #L2 @pr_eq_repl_sym /2 width=3 by lsubf_eq_repl_back2/
351 qed-.
352
353 lemma lsubf_refl: bi_reflexive … lsubf.
354 #L elim L -L /2 width=1 by lsubf_atom, pr_eq_refl/
355 #L #I #IH #f elim (pr_map_split_tl f) * #g #H destruct
356 /2 width=1 by lsubf_push, lsubf_bind/
357 qed.
358
359 lemma lsubf_refl_eq: ∀f1,f2,L. f1 ≡ f2 → ❨L,f1❩ ⫃𝐅+ ❨L,f2❩.
360 /2 width=3 by lsubf_eq_repl_back2/ qed.
361
362 lemma lsubf_bind_tl_dx:
363       ∀g1,f2,I,L1,L2. ❨L1,g1❩ ⫃𝐅+ ❨L2,⫰f2❩ →
364       ∃∃f1. ❨L1.ⓘ[I],f1❩ ⫃𝐅+ ❨L2.ⓘ[I],f2❩ & g1 = ⫰f1.
365 #g1 #f2 #I #L1 #L2 #H
366 elim (pr_map_split_tl f2) * #g2 #H2 destruct
367 @ex2_intro [1,2,4,5: /2 width=2 by lsubf_push, lsubf_bind/ ] // (**) (* constructor needed *)
368 qed-.
369
370 lemma lsubf_beta_tl_dx:
371       ∀f,f0,g1,L1,V. L1 ⊢ 𝐅+❨V❩ ≘ f → f0 ⋓ f ≘ g1 →
372       ∀f2,L2,W. ❨L1,f0❩ ⫃𝐅+ ❨L2,⫰f2❩ →
373       ∃∃f1. ❨L1.ⓓⓝW.V,f1❩ ⫃𝐅+ ❨L2.ⓛW,f2❩ & ⫰f1 ⊆ g1.
374 #f #f0 #g1 #L1 #V #Hf #Hg1 #f2
375 elim (pr_map_split_tl f2) * #x2 #H2 #L2 #W #HL12 destruct
376 [ /3 width=4 by lsubf_push, pr_sor_inv_sle_sn, ex2_intro/
377 | @(ex2_intro … (↑g1)) /2 width=5 by lsubf_beta/ (**) (* full auto fails *)
378 ]
379 qed-.
380
381 (* Note: this might be moved *)
382 lemma lsubf_inv_sor_dx:
383       ∀f1,f2,L1,L2. ❨L1,f1❩ ⫃𝐅+ ❨L2,f2❩ →
384       ∀f2l,f2r. f2l⋓f2r ≘ f2 →
385       ∃∃f1l,f1r. ❨L1,f1l❩ ⫃𝐅+ ❨L2,f2l❩ & ❨L1,f1r❩ ⫃𝐅+ ❨L2,f2r❩ & f1l⋓f1r ≘ f1.
386 #f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2
387 [ /3 width=7 by pr_sor_eq_repl_fwd, ex3_2_intro/
388 | #g1 #g2 #I1 #I2 #L1 #L2 #_ #IH #f2l #f2r #H
389   elim (pr_sor_inv_push … H) -H [|*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
390   elim (IH … Hg2) -g2 /3 width=11 by lsubf_push, pr_sor_push_bi, ex3_2_intro/
391 | #g1 #g2 #I #L1 #L2 #_ #IH #f2l #f2r #H
392   elim (pr_sor_inv_next … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
393   elim (IH … Hg2) -g2 /3 width=11 by lsubf_push, lsubf_bind, pr_sor_next_push, pr_sor_push_next, pr_sor_next_bi, ex3_2_intro/
394 | #g #g0 #g1 #g2 #L1 #L2 #W #V #Hg #Hg1 #_ #IH #f2l #f2r #H
395   elim (pr_sor_inv_next … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
396   elim (IH … Hg2) -g2 #g1l #g1r #Hl #Hr #Hg0
397   [ lapply (pr_sor_comm_23 … Hg0 Hg1 ?) -g0 [3: |*: // ] #Hg1
398     /3 width=11 by lsubf_push, lsubf_beta, pr_sor_next_push, ex3_2_intro/
399   | lapply (pr_sor_assoc_dx … Hg1 … Hg0 ??) -g0 [3: |*: // ] #Hg1
400     /3 width=11 by lsubf_push, lsubf_beta, pr_sor_push_next, ex3_2_intro/
401   | lapply (pr_sor_distr_dx … Hg0 … Hg1) -g0 [5: |*: // ] #Hg1
402     /3 width=11 by lsubf_beta, pr_sor_next_bi, ex3_2_intro/
403   ]
404 | #g #g0 #g1 #g2 #I1 #I2 #L1 #L2 #V #Hg #Hg1 #_ #IH #f2l #f2r #H
405   elim (pr_sor_inv_next … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
406   elim (IH … Hg2) -g2 #g1l #g1r #Hl #Hr #Hg0
407   [ lapply (pr_sor_comm_23 … Hg0 Hg1 ?) -g0 [3: |*: // ] #Hg1
408     /3 width=11 by lsubf_push, lsubf_unit, pr_sor_next_push, ex3_2_intro/
409   | lapply (pr_sor_assoc_dx … Hg1 … Hg0 ??) -g0 [3: |*: // ] #Hg1
410     /3 width=11 by lsubf_push, lsubf_unit, pr_sor_push_next, ex3_2_intro/
411   | lapply (pr_sor_distr_dx … Hg0 … Hg1) -g0 [5: |*: // ] #Hg1
412     /3 width=11 by lsubf_unit, pr_sor_next_bi, ex3_2_intro/
413   ]
414 ]
415 qed-.