From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 17 Jan 2017 12:17:51 +0000 (+0000)
Subject: improved lsubf allowes to prove lsubf_frees_trans.
X-Git-Tag: make_still_working~524
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=a78df6200d61b34a67cb1cba9edf984aae470530

improved lsubf allowes to prove lsubf_frees_trans.
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma
index 7e184e1a4..c786518ee 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma
@@ -131,8 +131,8 @@ lemma cpx_frees_conf_lfpx: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
     elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21
     elim (sor_isfin_ex gV2 (⫱gT2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #gVT2 #HgVT2 #_
     elim (lsubf_frees_trans … HgT2 (⫯gVT2) … (L2.ⓓⓝW2.V2))
-    [2: /4 width=3 by lsubf_refl, lsubf_beta, sor_inv_sle_dx, sle_inv_tl_sn/ ] -HgT2
-    #gT0 #HgT0 #HgT20
+    [2: /4 width=4 by lsubf_refl, lsubf_beta, sor_inv_sle_dx, sor_inv_sle_sn, sle_inv_tl_sn/ ]
+    -HgT2 #gT0 #HgT0 #HgT20
     elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #gV0 #HgV0 #H
     elim (sor_isfin_ex gV0 (⫱gT0)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_
     @(ex2_intro … g2)
@@ -159,8 +159,8 @@ lemma cpx_frees_conf_lfpx: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
     elim (sor_isfin_ex gW2 (⫱gV0)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_
     elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #g #Hg #_
     lapply (sor_trans2 … Hg2 … (⫱gT2) … Hg) /2 width=1 by sor_tl/ #Hg2
-    lapply (frees_lifts (Ⓣ) … HgV2 … (L2.ⓓW2) … HV2 ??) [4: |*: /3 width=3 by drops_refl, drops_drop/ ] -V2 #HgV
-    lapply (sor_sym … Hg) -Hg #Hg
+    lapply (frees_lifts (Ⓣ) … HgV2 … (L2.ⓓW2) … HV2 ??)
+    [4: lapply (sor_sym … Hg) |*: /3 width=3 by drops_refl, drops_drop/ ] -V2 (**) (* full auto too slow *)
     /4 width=10 by frees_flat, frees_bind, monotonic_sle_sor, sle_tl, ex2_intro/
   ]
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
index 3e6e63b07..148596308 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
@@ -19,9 +19,9 @@ include "basic_2/static/frees.ma".
 
 inductive lsubf: relation4 lenv rtmap lenv rtmap ≝
 | lsubf_atom: ∀f1,f2. f2 ⊆ f1 → lsubf (⋆) f1 (⋆) f2
-| lsubf_pair: ∀f1,f2,I,L1,L2,V. lsubf L1 (⫱f1) L2 (⫱f2) → f2 ⊆ f1 →
+| lsubf_pair: ∀f1,f2,I,L1,L2,V. f2 ⊆ f1 → lsubf L1 (⫱f1) L2 (⫱f2) →
               lsubf (L1.ⓑ{I}V) f1 (L2.ⓑ{I}V) f2
-| lsubf_beta: ∀f,f1,f2,L1,L2,W,V. L1 ⊢ 𝐅*⦃V⦄ ≡ f → f ⋓ ⫱f2 ≡ ⫱f1 → f2 ⊆ f1 →
+| lsubf_beta: ∀f,f1,f2,L1,L2,W,V. L1 ⊢ 𝐅*⦃V⦄ ≡ f → f ⊆ ⫱f1 → f2 ⊆ f1 →
               lsubf L1 (⫱f1) L2 (⫱f2) → lsubf (L1.ⓓⓝW.V) f1 (L2.ⓛW) f2
 .
 
@@ -46,11 +46,11 @@ lemma lsubf_inv_atom1: ∀f1,f2,L2. ⦃⋆, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L2 =
 fact lsubf_inv_pair1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
                           ∀I,K1,X. L1 = K1.ⓑ{I}X →
                           (∃∃K2. f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & L2 = K2.ⓑ{I}X) ∨
-                          ∃∃f,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ f & f ⋓ ⫱f2 ≡ ⫱f1 &
+                          ∃∃f,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ f & f ⊆ ⫱f1 &
                                       f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 [ #f1 #f2 #_ #J #K1 #X #H destruct
-| #f1 #f2 #I #L1 #L2 #V #HL12 #H21 #J #K1 #X #H destruct
+| #f1 #f2 #I #L1 #L2 #V #H21 #HL12 #J #K1 #X #H destruct
   /3 width=3 by ex3_intro, or_introl/
 | #f #f1 #f2 #L1 #L2 #W #V #Hf #Hf1 #H21 #HL12 #J #K1 #X #H destruct
   /3 width=11 by ex7_4_intro, or_intror/
@@ -59,7 +59,7 @@ qed-.
 
 lemma lsubf_inv_pair1: ∀f1,f2,I,K1,L2,X. ⦃K1.ⓑ{I}X, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
                        (∃∃K2. f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & L2 = K2.ⓑ{I}X) ∨
-                       ∃∃f,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ f & f ⋓ ⫱f2 ≡ ⫱f1 &
+                       ∃∃f,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ f & f ⊆ ⫱f1 &
                                    f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
 /2 width=3 by lsubf_inv_pair1_aux/ qed-.
 
@@ -78,11 +78,11 @@ lemma lsubf_inv_atom2: ∀f1,f2,L1. ⦃L1, f1⦄ ⫃𝐅* ⦃⋆, f2⦄ → L1 =
 fact lsubf_inv_pair2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
                           ∀I,K2,W. L2 = K2.ⓑ{I}W →
                           (∃∃K1.f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & L1 = K1.ⓑ{I}W) ∨
-                          ∃∃f,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ f & f ⋓ ⫱f2 ≡ ⫱f1 &
+                          ∃∃f,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ f & f ⊆ ⫱f1 &
                                     f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & I = Abst & L1 = K1.ⓓⓝW.V.
 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 [ #f1 #f2 #_ #J #K2 #X #H destruct
-| #f1 #f2 #I #L1 #L2 #V #HL12 #H21 #J #K2 #X #H destruct
+| #f1 #f2 #I #L1 #L2 #V #H21 #HL12 #J #K2 #X #H destruct
   /3 width=3 by ex3_intro, or_introl/
 | #f #f1 #f2 #L1 #L2 #W #V #Hf #Hf1 #H21 #HL12 #J #K2 #X #H destruct
   /3 width=7 by ex6_3_intro, or_intror/
@@ -91,7 +91,7 @@ qed-.
 
 lemma lsubf_inv_pair2: ∀f1,f2,I,L1,K2,W. ⦃L1, f1⦄ ⫃𝐅* ⦃K2.ⓑ{I}W, f2⦄ →
                        (∃∃K1.f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & L1 = K1.ⓑ{I}W) ∨
-                       ∃∃f,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ f & f ⋓ ⫱f2 ≡ ⫱f1 &
+                       ∃∃f,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ f & f ⊆ ⫱f1 &
                                  f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & I = Abst & L1 = K1.ⓓⓝW.V.
 /2 width=5 by lsubf_inv_pair2_aux/ qed-.
 
@@ -103,6 +103,16 @@ qed-.
 
 (* Basic properties *********************************************************)
 
+lemma lsubf_pair_nn: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
+                     ∀I,V. ⦃L1.ⓑ{I}V, ⫯f1⦄ ⫃𝐅* ⦃L2.ⓑ{I}V, ⫯f2⦄.
+/4 width=5 by lsubf_fwd_sle, lsubf_pair, sle_next/ qed.
+
 lemma lsubf_refl: ∀L,f1,f2. f2 ⊆ f1 → ⦃L, f1⦄ ⫃𝐅* ⦃L, f2⦄.
 #L elim L -L /4 width=1 by lsubf_atom, lsubf_pair, sle_tl/
 qed.
+
+lemma lsubf_sle_div: ∀f,f2,L1,L2. ⦃L1, f⦄ ⫃ 𝐅* ⦃L2, f2⦄ →
+                     ∀f1. f1 ⊆ f2 → ⦃L1, f⦄ ⫃ 𝐅* ⦃L2, f1⦄.
+#f #f2 #L1 #L2 #H elim H -f -f2 -L1 -L2
+/4 width=3 by lsubf_beta, lsubf_pair, lsubf_atom, sle_tl, sle_trans/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma
index 47fc2f75e..884d940bc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma
@@ -18,9 +18,8 @@ include "basic_2/static/lsubf.ma".
 
 (* Properties with context-sensitive free variables *************************)
 
-axiom lsubf_frees_trans: ∀f2,L2,T. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 → ∀f,L1. ⦃L1, f⦄ ⫃𝐅* ⦃L2, f2⦄ →
+lemma lsubf_frees_trans: ∀f2,L2,T. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 → ∀f,L1. ⦃L1, f⦄ ⫃𝐅* ⦃L2, f2⦄ →
                          ∃∃f1. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 & f1 ⊆ f.
-(*
 #f2 #L2 #T #H elim H -f2 -L2 -T
 [ #f2 #I #Hf2 #f #L1 #H elim (lsubf_inv_atom2 … H) -H
   #H #_ destruct /3 width=3 by frees_atom, sle_isid_sn, ex2_intro/
@@ -32,11 +31,10 @@ axiom lsubf_frees_trans: ∀f2,L2,T. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 → ∀f,L1. ⦃
   [ #K1 #H elim (sle_inv_nx … H ??) -H [ <tl_next_rew |*: // ]
     #g2 #_ #H1 #H12 #H2 destruct elim (IH … H12) -K2
     /3 width=7 by frees_zero, sle_next, ex2_intro/
-  | #g #K1 #V #Hg <tl_next_rew #Hf lapply (sor_sym … Hf) -Hf
-    #Hf #H elim (sle_inv_nx … H ??) -H [|*: // ]
+  | #g #K1 #V #Hg #Hf #H elim (sle_inv_nx … H ??) -H [ <tl_next_rew |*: // ]
     #g2 #_ #H1 #H12 #H2 #H3 destruct elim (IH … H12) -K2
     #f1 #Hf1 elim (sor_isfin_ex … f1 g ??)
-    /5 width=10 by frees_fwd_isfin, frees_flat, frees_zero, monotonic_sle_sor, sor_inv_sle_dx, sor_sym, sor_sle_sn, sle_next, ex2_intro/
+    /4 width=7 by frees_fwd_isfin, frees_flat, frees_zero, sor_inv_sle, sle_next, ex2_intro/
   ]
 | #f2 #I #K2 #W #i #_ #IH #f #L1 #H elim (lsubf_inv_pair2 … H) -H *
   [ #K1 #_ #H12 #H | #g #K1 #V #Hg #Hf #_ #H12 #H1 #H2 ]
@@ -47,5 +45,14 @@ axiom lsubf_frees_trans: ∀f2,L2,T. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 → ∀f,L1. ⦃
   destruct elim (IH … H12) -K2
   /3 width=3 by frees_gref, sle_inv_tl_dx, ex2_intro/
 | #f2V #f2T #f2 #p #I #L2 #V #T #_ #_ #Hf2 #IHV #IHT #f #L1 #H12
+  elim (IHV f L1) -IHV [2: /3 width=4 by lsubf_sle_div, sor_inv_sle_sn/ ]
+  elim (IHT (⫯f) (L1.ⓑ{I}V)) -IHT [2: /4 width=4 by lsubf_sle_div, lsubf_pair_nn, sor_inv_sle_dx, sor_inv_tl_dx/ ]
+  -f2V -f2T -f2 -L2 #f1T #HT #Hf1T #f1V #HV #Hf1V elim (sor_isfin_ex … f1V (⫱f1T) ??)
+  /4 width=9 by frees_fwd_isfin, frees_bind, sor_inv_sle, sle_xn_tl, isfin_tl, ex2_intro/
 | #f2V #f2T #f2 #I #L2 #V #T #_ #_ #Hf2 #IHV #IHT #f #L1 #H12
-*)
+  elim (IHV f L1) -IHV [2: /3 width=4 by lsubf_sle_div, sor_inv_sle_sn/ ]
+  elim (IHT f L1) -IHT [2: /3 width=4 by lsubf_sle_div, sor_inv_sle_dx/ ]
+  -f2V -f2T -f2 -L2 #f1T #HT #Hf1T #f1V #HV #Hf1V elim (sor_isfin_ex … f1V f1T ??)
+  /3 width=7 by frees_fwd_isfin, frees_flat, sor_inv_sle, ex2_intro/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
index efa6b54d9..bc2a7dda6 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
@@ -323,6 +323,18 @@ qed.
 lemma sor_isid: ∀f1,f2,f. 𝐈⦃f1⦄ → 𝐈⦃f2⦄ → 𝐈⦃f⦄ → f1 ⋓ f2 ≡ f.
 /4 width=3 by sor_eq_repl_back2, sor_eq_repl_back1, isid_inv_eq_repl/ qed.
 
+(* Inversion lemmas with tail ***********************************************)
+
+lemma sor_inv_tl_sn: ∀f1,f2,f. ⫱f1 ⋓ f2 ≡ f → f1 ⋓ ⫯f2 ≡ ⫯f.
+#f1 #f2 #f elim (pn_split f1) *
+#g1 #H destruct /2 width=7 by sor_pn, sor_nn/
+qed-.
+
+lemma sor_inv_tl_dx: ∀f1,f2,f. f1 ⋓ ⫱f2 ≡ f → ⫯f1 ⋓ f2 ≡ ⫯f.
+#f1 #f2 #f elim (pn_split f2) *
+#g2 #H destruct /2 width=7 by sor_np, sor_nn/
+qed-.
+
 (* Inversion lemmas with test for identity **********************************)
 
 lemma sor_isid_inv_sn: ∀f1,f2,f. f1 ⋓ f2 ≡ f → 𝐈⦃f1⦄ → f2 ≗ f.