more on lfpx_frees.ma ...

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
index d0dbc756838768eaac6d596985ab1b287ad7dee3..9587c2659096f70d55dffa66440463219951e36a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
@@ -32,7 +32,7 @@ inductive lexs (RN,RP:relation3 lenv term term): rtmap → relation lenv ≝
 interpretation "generic entrywise extension (local environment)"
    'RelationStar RN RP f L1 L2 = (lexs RN RP f L1 L2).
 
-definition lexs_pw_confluent2_R: relation3 lenv term term → relation3 lenv term term →
+definition R_pw_confluent2_lexs: relation3 lenv term term → relation3 lenv term term →
                                  relation3 lenv term term → relation3 lenv term term →
                                  relation3 lenv term term → relation3 lenv term term →
                                  relation3 rtmap lenv term ≝

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma
index 13ec6ca81e30e81104aaa626d0bdb5b862b0f6d2..cd7e64c518c77d0416011643f5df03bc026d77a7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma
@@ -45,8 +45,8 @@ theorem lexs_trans (RN) (RP) (f): lexs_transitive RN RN RN RN RP →
 (* Basic_2A1: includes: lpx_sn_conf *)
 theorem lexs_conf (RN1) (RP1) (RN2) (RP2):
                   ∀L,f.
-                  (∀g,I,K,V,n. ⬇*[n] L ≡ K.ⓑ{I}V → ⫯g = ⫱*[n] f → lexs_pw_confluent2_R RN1 RN2 RN1 RP1 RN2 RP2 g K V) →
-                  (∀g,I,K,V,n. ⬇*[n] L ≡ K.ⓑ{I}V → ↑g = ⫱*[n] f → lexs_pw_confluent2_R RP1 RP2 RN1 RP1 RN2 RP2 g K V) →
+                  (∀g,I,K,V,n. ⬇*[n] L ≡ K.ⓑ{I}V → ⫯g = ⫱*[n] f → R_pw_confluent2_lexs RN1 RN2 RN1 RP1 RN2 RP2 g K V) →
+                  (∀g,I,K,V,n. ⬇*[n] L ≡ K.ⓑ{I}V → ↑g = ⫱*[n] f → R_pw_confluent2_lexs RP1 RP2 RN1 RP1 RN2 RP2 g K V) →
                   pw_confluent2 … (lexs RN1 RP1 f) (lexs RN2 RP2 f) L.
 #RN1 #RP1 #RN2 #RP2 #L elim L -L
 [ #f #_ #_ #L1 #H1 #L2 #H2 >(lexs_inv_atom1 … H1) >(lexs_inv_atom1 … H2) -H2 -H1

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 47d35f2e56453600da7de42fadc44a36627fe43a..935109f903b0756bc42e613679da1b3df17201dc 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma
@@ -11,10 +11,7 @@
 (*        v         GNU General Public License Version 2                  *)
 (*                                                                        *)
 (**************************************************************************)
-(*
-include "basic_2/multiple/frees_lreq.ma".
-include "basic_2/multiple/frees_lift.ma".
-*)
+
 include "basic_2/relocation/drops_lexs.ma".
 include "basic_2/s_computation/fqup_weight.ma".
 include "basic_2/static/frees_drops.ma".
@@ -32,23 +29,16 @@ axiom pippo: ∀RN,RP,L1,i. ⬇*[Ⓕ, 𝐔❴i❵] L1 ≡ ⋆ →
 lapply (lexs_co_dropable_sn … H1 … H2) // -HL1 -H2
 *)
 
-lemma coafter_uni_sn: ∀i,f. 𝐔❴i❵ ~⊚ f ≡ ↑*[i] f.
-#i elim i -i /2 width=5 by coafter_isid_sn, coafter_next/
-qed.
-
-lemma sle_pushs: ∀f1,f2. f1 ⊆ f2 → ∀i. ↑*[i] f1 ⊆ ↑*[i] f2.
-#f1 #f2 #Hf12 #i elim i -i /2 width=5 by sle_push/
-qed.
-
-axiom monotonic_sle_sor: ∀f1,g1. f1 ⊆ g1 → ∀f2,g2. f2 ⊆ g2 →
-                         ∀f. f1 ⋓ f2 ≡ f → ∀g. g1 ⋓ g2 ≡ g → f ⊆ g.
-
-axiom sle_tl: ∀f1,f2. f1 ⊆ f2 → ⫱f1 ⊆ ⫱f2.
 
 axiom frees_inv_lifts_SO: ∀b,f,L,U. L ⊢ 𝐅*⦃U⦄ ≡ f →
                           ∀K. ⬇*[b, 𝐔❴1❵] L ≡ K → ∀T. ⬆*[1] T ≡ U →
                           K ⊢ 𝐅*⦃T⦄ ≡ ⫱f.
 
+axiom frees_pair_flat: ∀L,T,f1,I1,V1. L.ⓑ{I1}V1 ⊢ 𝐅*⦃T⦄ ≡ f1 →
+                       ∀f2,I2,V2. L.ⓑ{I2}V2 ⊢ 𝐅*⦃T⦄ ≡ f2 →
+                       ∀f0. f1 ⋓ f2 ≡ f0 →
+                       ∀I0,I. L.ⓑ{I0}ⓕ{I}V1.V2 ⊢ 𝐅*⦃T⦄ ≡ f0.
+
 (* Basic_2A1: was: lpx_cpx_frees_trans *)
 lemma cpx_frees_trans_lexs: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
                             ∀L2. L1 ⦻*[cpx h G, cfull, f1] L2 →
@@ -102,8 +92,63 @@ lemma cpx_frees_trans_lexs: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
   | #T2 #HT12 #HUT2 #H0 #H1 destruct -HgV1
     lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
     lapply (lexs_inv_tl … Abbr … V1 V1 HL12T ??) // -HL12T #HL12T
+    elim (IH … HgT1 … HL12T … HT12) // -L1 -T1 #gT2 #HgT2 #HgT21
+    lapply (frees_inv_lifts_SO (Ⓣ) … HgT2 … L2 … HUT2) [ /3 width=1 by drops_refl, drops_drop/ ] -V1 -T2
+    /5 width=6 by sor_inv_sle_dx, sle_trans, sle_tl, ex2_intro/
+  ]
+| #I #V1 #T0 #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct
+  elim (frees_inv_flat … H1) -H1 #gV1 #gT0 #HgV1 #HgT0 #Hg1
+  elim (cpx_inv_flat1 … H0) -H0 *
+  [ #V2 #T2 #HV12 #HT12 #H destruct
+    lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V
+    lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
+    elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21
+    elim (IH … HgT0 … HL12T … HT12) // -IH -HgT0 -HL12T -HT12 #gT2 #HgT2 #HgT21
+    elim (sor_isfin_ex gV2 gT2) /2 width=3 by frees_fwd_isfin/
+    /3 width=10 by frees_flat, monotonic_sle_sor, ex2_intro/
+  | #HU2 #H destruct -HgV1
+    lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
+    elim (IH … HgT0 … HL12T … HU2) // -L1 -T0 -V1
+    /4 width=6 by sor_inv_sle_dx, sle_trans, ex2_intro/
+  | #HU2 #H destruct -HgT0
+    lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ -H2 #HL12V
+    elim (IH … HgV1 … HL12V … HU2) // -L1 -T0 -V1
+    /4 width=6 by sor_inv_sle_sn, sle_trans, ex2_intro/
+  | #p #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #H0 #H1 #H destruct
+    elim (frees_inv_bind … HgT0) -HgT0 #gW1 #gT1 #HgW1 #HgT1 #HgT0
+    lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V
+    lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #H2
+    lapply (sle_lexs_trans … H2 gW1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12W
+    lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
+    lapply (lexs_inv_tl … Abst … HL12T … HW12 ?) // -HL12T #HL12T
+    elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21
+    elim (IH … HgW1 … HL12W … HW12) // -HgW1 -HL12W -HW12 #gW2 #HgW2 #HgW21
     elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21
-    lapply (frees_inv_lifts_SO (Ⓣ) … HgT2 … L2 … HUT2) [ /3 width=1 by drops_refl, drops_drop/ ]
+    elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #gV0 #HgV0 #H
+    elim (sor_isfin_ex gV0 (⫱gT2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_
+    @(ex2_intro … g2)
+    [ @(frees_bind … Hg2) /2 width=5 by frees_flat/ ]
+  | #p #V2 #V #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #H0 #H1 #H destruct
+    elim (frees_inv_bind … HgT0) -HgT0 #gW1 #gT1 #HgW1 #HgT1 #HgT0
+    lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V
+    lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #H2
+    lapply (sle_lexs_trans … H2 gW1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12W
+    lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
+    lapply (lexs_inv_tl … Abbr … HL12T … HW12 ?) // -HL12T #HL12T
+    elim (sor_isfin_ex gV1 gW1) /2 width=3 by frees_fwd_isfin/ #g0 #Hg0 #_
+    lapply (sor_trans2 … Hg1 … HgT0 … Hg0) -Hg1 -HgT0 #Hg1
+    elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21
+    elim (IH … HgW1 … HL12W … HW12) // -HgW1 -HL12W -HW12 #gW2 #HgW2 #HgW21
+    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_push/ #gV0 #HgV0 #H
+    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
+    /4 width=10 by frees_flat, frees_bind, monotonic_sle_sor, sle_tl, ex2_intro/
+  ]
+]
 
 lemma cpx_frees_trans: ∀h,o,G. frees_trans (cpx h o G).
 /2 width=8 by lpx_cpx_frees_trans/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
index 5c3a07a2a0de2eb1b741a642947d8231beb1be88..605af05cea8ced70374ffc829f217816f0c716e8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
@@ -26,12 +26,12 @@ definition lfxs (R) (T): relation lenv ≝
 interpretation "generic extension on referred entries (local environment)"
    'RelationStar R T L1 L2 = (lfxs R T L1 L2).
 
-definition R_confluent_lfxs: relation4 (relation3 lenv term term)
-                                       (relation3 lenv term term) … ≝
-                             λR1,R2,RP1,RP2.
-                             ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 →
-                             ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 →
-                             ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
+definition R_confluent2_lfxs: relation4 (relation3 lenv term term)
+                                        (relation3 lenv term term) … ≝
+                              λR1,R2,RP1,RP2.
+                              ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 →
+                              ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 →
+                              ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
 
 (* Basic properties ***********************************************************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_main.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_main.ma
index 3d6a2658e038b91b2f6eedc35a330705d4f428dc..444d413ef4230f151039777d22a60aa2bd10f6a6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_main.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_main.ma
@@ -22,7 +22,7 @@ axiom frees_lexs_conf_sle: ∀RN,RP,f1,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 →
                            ∀L2. L1 ⦻*[RN, RP, f1] L2 →
                            ∃∃f2. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 & f2 ⊆ f1.
 
-theorem lfxs_conf: ∀R. R_confluent_lfxs R R R R →
+theorem lfxs_conf: ∀R. R_confluent2_lfxs R R R R →
                    ∀T. confluent … (lfxs R T).
 #R #H1R #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02
 lapply (frees_mono … Hf1 … Hf) -Hf1 #Hf12
@@ -47,4 +47,4 @@ lemma pippo: ∀R1,R2,RP1,RP2. R_confluent_lfxs R1 R2 RP1 RP2 →
              lexs_confluent R1 R2 RP1 cfull RP2 cfull.
 #R1 #R2 #RP1 #RP2 #HR #f #L0 #T0 #T1 #HT01 #T2 #HT02 #L1 #HL01 #L2
 #HL02
-*)
\ No newline at end of file
+*)

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma
index cb5ede22b61de36de2ab149c6d9711148486000a..56449d8385412e88314dc4f7add69c3cc2986a86 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma
@@ -257,7 +257,7 @@ lemma coafter_inv_tl0: ∀g2,g1,g. g2 ~⊚ g1 ≡ ⫱g →
 ]
 qed-.
 
-(* Properties on tls ********************************************************)
+(* Properties with iterated tail ********************************************)
 
 lemma coafter_tls: ∀n,f1,f2,f. @⦃0, f1⦄ ≡ n →
                    f1 ~⊚ f2 ≡ f → ⫱*[n]f1 ~⊚ f2 ≡ ⫱*[n]f.
@@ -304,7 +304,7 @@ elim (coafter_inv_pxx … Hf … H2) -Hf -H2 * #f1 #g #_ #H1 #H0 destruct
 ] 
 qed-.
 
-(* Properties on isid *******************************************************)
+(* Properties with test for identity ****************************************)
 
 corec lemma coafter_isid_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ~⊚ f2 ≡ f2.
 #f1 * -f1 #f1 #g1 #Hf1 #H1 #f2 cases (pn_split f2) * #g2 #H2
@@ -318,13 +318,19 @@ corec lemma coafter_isid_dx: ∀f2,f. 𝐈⦃f2⦄ → 𝐈⦃f⦄ → ∀f1. f1
 ]
 qed.
 
-(* Inversion lemmas on isid *************************************************)
+(* Inversion lemmas with test for identity **********************************)
 
 lemma coafter_isid_inv_sn: ∀f1,f2,f. f1 ~⊚ f2 ≡ f → 𝐈⦃f1⦄ → f2 ≗ f.
 /3 width=6 by coafter_isid_sn, coafter_mono/ qed-.
 
 lemma coafter_isid_inv_dx: ∀f1,f2,f. f1 ~⊚ f2 ≡ f → 𝐈⦃f2⦄ → 𝐈⦃f⦄.
 /4 width=4 by eq_id_isid, coafter_isid_dx, coafter_mono/ qed-.
+
+(* Properties with uniform relocations **************************************)
+
+lemma coafter_uni_sn: ∀i,f. 𝐔❴i❵ ~⊚ f ≡ ↑*[i] f.
+#i elim i -i /2 width=5 by coafter_isid_sn, coafter_next/
+qed.
 (*
 (* Properties on isuni ******************************************************)
 

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma
index 29614b3dc5c0a09a86a75e73f85f59fc3d5426ee..2fc90abd113e3dbecbac60066707a03fc983a0b0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma
@@ -88,12 +88,25 @@ corec theorem sle_trans: Transitive … sle.
 /3 width=5 by sle_push, sle_next, sle_weak/
 qed-.
 
+(* Properties with iteraded push ********************************************)
+
+lemma sle_pushs: ∀f1,f2. f1 ⊆ f2 → ∀i. ↑*[i] f1 ⊆ ↑*[i] f2.
+#f1 #f2 #Hf12 #i elim i -i /2 width=5 by sle_push/
+qed.
+
 (* Properties with tail *****************************************************)
 
 lemma sle_px_tl: ∀g1,g2. g1 ⊆ g2 → ∀f1. ↑f1 = g1 → f1 ⊆ ⫱g2.
 #g1 #g2 #H #f1 #H1 elim (sle_inv_px … H … H1) -H -H1 * //
 qed.
 
+lemma sle_tl: ∀f1,f2. f1 ⊆ f2 → ⫱f1 ⊆ ⫱f2.
+#f1 elim (pn_split f1) * #g1 #H1 #f2 #H
+[ lapply (sle_px_tl … H … H1) -H //
+| elim (sle_inv_nx … H … H1) -H //
+]
+qed.
+
 (* Inversion lemmas with tail ***********************************************)
 
 lemma sle_inv_tl_sn: ∀f1,f2. ⫱f1 ⊆ f2 → f1 ⊆ ⫯f2.

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 839426b9acb8ede8d994f16e6a6dff43338631d6..f86e7f8092784bb8e8ddd8e07c07dc9134aba43e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
@@ -266,6 +266,19 @@ corec lemma sor_sym: ∀f1,f2,f. f1 ⋓ f2 ≡ f → f2 ⋓ f1 ≡ f.
 [ @sor_pp | @sor_pn | @sor_np | @sor_nn ] /2 width=7 by/
 qed-.
 
+(* Main properties **********************************************************)
+
+axiom monotonic_sle_sor: ∀f1,g1. f1 ⊆ g1 → ∀f2,g2. f2 ⊆ g2 →
+                         ∀f. f1 ⋓ f2 ≡ f → ∀g. g1 ⋓ g2 ≡ g → f ⊆ g.
+
+axiom sor_trans1: ∀f0,f3,f4. f0 ⋓ f3 ≡ f4 →
+                  ∀f1,f2. f1 ⋓ f2 ≡ f0 →
+                  ∀f. f2 ⋓ f3 ≡ f → f1 ⋓ f ≡ f4.
+
+axiom sor_trans2: ∀f1,f0,f4. f1 ⋓ f0 ≡ f4 →
+                  ∀f2, f3. f2 ⋓ f3 ≡ f0 →
+                  ∀f. f1 ⋓ f2 ≡ f → f ⋓ f3 ≡ f4.
+
 (* Properties with tail *****************************************************)
 
 lemma sor_tl: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ⫱f1 ⋓ ⫱f2 ≡ ⫱f.