- first prroperties on lfsx proved

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / lexs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
index 9587c2659096f70d55dffa66440463219951e36a..b002e073af1af7be489b4f845d88376be49088cf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
@@ -14,7 +14,7 @@
 
 include "ground_2/relocation/rtmap_sle.ma".
 include "basic_2/notation/relations/relationstar_5.ma".
-include "basic_2/grammar/lenv.ma".
+include "basic_2/syntax/lenv.ma".
 
 (* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
 
@@ -173,16 +173,23 @@ lemma lexs_eq_repl_fwd: ∀RN,RP,L1,L2. eq_repl_fwd … (λf. L1 ⦻*[RN, RP, f]
 #RN #RP #L1 #L2 @eq_repl_sym /2 width=3 by lexs_eq_repl_back/ (**) (* full auto fails *)
 qed-.
 
-(* Note: fexs_sym and fexs_trans hold, but lexs_sym and lexs_trans do not  *)
 (* Basic_2A1: includes: lpx_sn_refl *)
-lemma lexs_refl: ∀RN,RP,f.
+lemma lexs_refl: ∀RN,RP.
                  (∀L. reflexive … (RN L)) →
                  (∀L. reflexive … (RP L)) →
-                 reflexive … (lexs RN RP f).
-#RN #RP #f #HRN #HRP #L generalize in match f; -f elim L -L //
+                 ∀f.reflexive … (lexs RN RP f).
+#RN #RP #HRN #HRP #f #L generalize in match f; -f elim L -L //
 #L #I #V #IH * * /2 width=1 by lexs_next, lexs_push/
 qed.
 
+lemma lexs_sym: ∀RN,RP.
+                (∀L1,L2,T1,T2. RN L1 T1 T2 → RN L2 T2 T1) →
+                (∀L1,L2,T1,T2. RP L1 T1 T2 → RP L2 T2 T1) →
+                ∀f. symmetric … (lexs RN RP f).
+#RN #RP #HRN #HRP #f #L1 #L2 #H elim H -L1 -L2 -f
+/3 width=2 by lexs_next, lexs_push/
+qed-.
+
 lemma lexs_pair_repl: ∀RN,RP,f,I,L1,L2,V1,V2.
                       L1.ⓑ{I}V1 ⦻*[RN, RP, f] L2.ⓑ{I}V2 →
                       ∀W1,W2. RN L1 W1 W2 → RP L1 W1 W2 →
@@ -199,6 +206,17 @@ lemma lexs_co: ∀RN1,RP1,RN2,RP2.
 /3 width=1 by lexs_atom, lexs_next, lexs_push/
 qed-.
 
+lemma lexs_co_isid: ∀RN1,RP1,RN2,RP2.
+                    (∀L1,T1,T2. RP1 L1 T1 T2 → RP2 L1 T1 T2) →
+                    ∀f,L1,L2. L1 ⦻*[RN1, RP1, f] L2 → 𝐈⦃f⦄ →
+                    L1 ⦻*[RN2, RP2, f] L2.
+#RN1 #RP1 #RN2 #RP2 #HR #f #L1 #L2 #H elim H -f -L1 -L2 //
+#f #I #K1 #K2 #V1 #V2 #_ #HV12 #IH #H
+[ elim (isid_inv_next … H) -H //
+| /4 width=3 by lexs_push, isid_inv_push/
+] 
+qed-.
+
 lemma sle_lexs_trans: ∀RN,RP. (∀L,T1,T2. RN L T1 T2 → RP L T1 T2) →
                       ∀f2,L1,L2. L1 ⦻*[RN, RP, f2] L2 →
                       ∀f1. f1 ⊆ f2 → L1 ⦻*[RN, RP, f1] L2.
@@ -224,3 +242,16 @@ lemma sle_lexs_conf: ∀RN,RP. (∀L,T1,T2. RP L T1 T2 → RN L T1 T2) →
   #g2 #H #H2 destruct /3 width=5 by lexs_next/
 ]
 qed-.
+
+lemma lexs_sle_split: ∀R1,R2,RP. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
+                      ∀f,L1,L2. L1 ⦻*[R1, RP, f] L2 → ∀g. f ⊆ g →
+                      ∃∃L. L1 ⦻*[R1, RP, g] L & L ⦻*[R2, cfull, f] L2.
+#R1 #R2 #RP #HR1 #HR2 #f #L1 #L2 #H elim H -f -L1 -L2
+[ /2 width=3 by lexs_atom, ex2_intro/ ]
+#f #I #L1 #L2 #V1 #V2 #_ #HV12 #IH #y #H
+[ elim (sle_inv_nx … H ??) -H [ |*: // ] #g #Hfg #H destruct
+  elim (IH … Hfg) -IH -Hfg /3 width=5 by lexs_next, ex2_intro/
+| elim (sle_inv_px … H ??) -H [1,3: * |*: // ] #g #Hfg #H destruct
+  elim (IH … Hfg) -IH -Hfg /3 width=5 by lexs_next, lexs_push, ex2_intro/
+]
+qed-.