- exclusion binder in local environments:

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / lsubf.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
index 72e63576ecfdc41ce1ff019f9e779065e32cb5b4..62b114915f9097c3447d12bae64ec9c7179bfef4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/lrsubeqf_4.ma".
+include "ground_2/relocation/nstream_sor.ma".
 include "basic_2/static/frees.ma".
 
 (* RESTRICTED REFINEMENT FOR CONTEXT-SENSITIVE FREE VARIABLES ***************)
@@ -304,10 +305,54 @@ qed.
 lemma lsubf_refl_eq: ∀f1,f2,L. f1 ≗ f2 → ⦃L, f1⦄ ⫃𝐅* ⦃L, f2⦄.
 /2 width=3 by lsubf_eq_repl_back2/ qed.
 
-lemma lsubf_tl_dx: ∀g1,f2,I,L1,L2. ⦃L1, g1⦄ ⫃𝐅* ⦃L2, ⫱f2⦄ →
-                   ∃∃f1. ⦃L1.ⓘ{I}, f1⦄ ⫃𝐅* ⦃L2.ⓘ{I}, f2⦄ & g1 = ⫱f1.
+lemma lsubf_bind_tl_dx: ∀g1,f2,I,L1,L2. ⦃L1, g1⦄ ⫃𝐅* ⦃L2, ⫱f2⦄ →
+                        ∃∃f1. ⦃L1.ⓘ{I}, f1⦄ ⫃𝐅* ⦃L2.ⓘ{I}, f2⦄ & g1 = ⫱f1.
 #g1 #f2 #I #L1 #L2 #H
 elim (pn_split f2) * #g2 #H2 destruct
 @ex2_intro [1,2,4,5: /2 width=2 by lsubf_push, lsubf_bind/ ] // (**) (* constructor needed *)
 qed-.
 
+lemma lsubf_beta_tl_dx: ∀f,f0,g1,L1,V. L1 ⊢ 𝐅*⦃V⦄ ≡ f → f0 ⋓ f ≡ g1 →
+                        ∀f2,L2,W. ⦃L1, f0⦄ ⫃𝐅* ⦃L2, ⫱f2⦄ →
+                        ∃∃f1. ⦃L1.ⓓⓝW.V, f1⦄ ⫃𝐅* ⦃L2.ⓛW, f2⦄ & ⫱f1 ⊆ g1.
+#f #f0 #g1 #L1 #V #Hf #Hg1 #f2
+elim (pn_split f2) * #x2 #H2 #L2 #W #HL12 destruct
+[ /3 width=4 by lsubf_push, sor_inv_sle_sn, ex2_intro/
+| @(ex2_intro … (⫯g1)) /2 width=5 by lsubf_beta/ (**) (* full auto fails *) 
+]
+qed-.
+
+(* Note: this might be moved *)
+lemma lsubf_inv_sor_dx: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
+                        ∀f2l,f2r. f2l⋓f2r ≡ f2 →
+                        ∃∃f1l,f1r. ⦃L1, f1l⦄ ⫃𝐅* ⦃L2, f2l⦄ & ⦃L1, f1r⦄ ⫃𝐅* ⦃L2, f2r⦄ & f1l⋓f1r ≡ f1.
+#f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2
+[ /3 width=7 by sor_eq_repl_fwd3, ex3_2_intro/
+| #g1 #g2 #I1 #I2 #L1 #L2 #_ #IH #f2l #f2r #H
+  elim (sor_inv_xxp … H) -H [|*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
+  elim (IH … Hg2) -g2 /3 width=11 by lsubf_push, sor_pp, ex3_2_intro/
+| #g1 #g2 #I #L1 #L2 #_ #IH #f2l #f2r #H
+  elim (sor_inv_xxn … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
+  elim (IH … Hg2) -g2 /3 width=11 by lsubf_push, lsubf_bind, sor_np, sor_pn, sor_nn, ex3_2_intro/
+| #g #g0 #g1 #g2 #L1 #L2 #W #V #Hg #Hg1 #_ #IH #f2l #f2r #H
+  elim (sor_inv_xxn … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
+  elim (IH … Hg2) -g2 #g1l #g1r #Hl #Hr #Hg0
+  [ lapply (sor_comm_23 … Hg0 Hg1 ?) -g0 [3: |*: // ] #Hg1
+    /3 width=11 by lsubf_push, lsubf_beta, sor_np, ex3_2_intro/
+  | lapply (sor_assoc_dx … Hg1 … Hg0 ??) -g0 [3: |*: // ] #Hg1
+    /3 width=11 by lsubf_push, lsubf_beta, sor_pn, ex3_2_intro/
+  | lapply (sor_distr_dx … Hg0 … Hg1) -g0 [5: |*: // ] #Hg1
+    /3 width=11 by lsubf_beta, sor_nn, ex3_2_intro/
+  ]
+| #g #g0 #g1 #g2 #I1 #I2 #L1 #L2 #V #Hg #Hg1 #_ #IH #f2l #f2r #H
+  elim (sor_inv_xxn … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
+  elim (IH … Hg2) -g2 #g1l #g1r #Hl #Hr #Hg0
+  [ lapply (sor_comm_23 … Hg0 Hg1 ?) -g0 [3: |*: // ] #Hg1
+    /3 width=11 by lsubf_push, lsubf_unit, sor_np, ex3_2_intro/
+  | lapply (sor_assoc_dx … Hg1 … Hg0 ??) -g0 [3: |*: // ] #Hg1
+    /3 width=11 by lsubf_push, lsubf_unit, sor_pn, ex3_2_intro/
+  | lapply (sor_distr_dx … Hg0 … Hg1) -g0 [5: |*: // ] #Hg1
+    /3 width=11 by lsubf_unit, sor_nn, ex3_2_intro/
+  ]
+]
+qed-.