X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_at.ma;h=de668c52c654a1c2abe41b9c2bae8c88f692f272;hb=528f8ea107f689d07d060e1d31ba32bf65b4e6ba;hp=a1f191a2586e98896ca9db07831e3d2793136645;hpb=93bba1c94779e83184d111cd077d4167e42a74aa;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma
index a1f191a25..de668c52c 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma
@@ -26,6 +26,10 @@ coinductive at: rtmap → relation nat ≝
 interpretation "relational application (rtmap)"
    'RAt i1 f i2 = (at f i1 i2).
 
+definition H_at_div: relation4 rtmap rtmap rtmap rtmap ≝ λf2,g2,f1,g1.
+                     ∀jf,jg,j. @⦃jf, f2⦄ ≡ j → @⦃jg, g2⦄ ≡ j →
+                     ∃∃j0. @⦃j0, f1⦄ ≡ jf & @⦃j0, g1⦄ ≡ jg.
+
 (* Basic inversion lemmas ***************************************************)
 
 lemma at_inv_ppx: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. 0 = i1 → ↑g = f → 0 = i2.
@@ -267,11 +271,52 @@ theorem at_inj: ∀f,i1,i. @⦃i1, f⦄ ≡ i → ∀i2. @⦃i2, f⦄ ≡ i →
 #Hi elim (lt_le_false i i) /3 width=6 by at_monotonic, eq_sym/
 qed-.
 
+theorem at_div_comm: ∀f2,g2,f1,g1.
+                     H_at_div f2 g2 f1 g1 → H_at_div g2 f2 g1 f1.
+#f2 #g2 #f1 #g1 #IH #jg #jf #j #Hg #Hf
+elim (IH … Hf Hg) -IH -j /2 width=3 by ex2_intro/
+qed-.
+
+theorem at_div_pp: ∀f2,g2,f1,g1.
+                   H_at_div f2 g2 f1 g1 → H_at_div (↑f2) (↑g2) (↑f1) (↑g1).
+#f2 #g2 #f1 #g1 #IH #jf #jg #j #Hf #Hg
+elim (at_inv_xpx … Hf) -Hf [1,2: * |*: // ]
+[ #H1 #H2 destruct -IH
+  lapply (at_inv_xpp … Hg ???) -Hg [4: |*: // ] #H destruct
+  /3 width=3 by at_refl, ex2_intro/
+| #xf #i #Hf2 #H1 #H2 destruct
+  lapply (at_inv_xpn … Hg ????) -Hg [5: * |*: // ] #xg #Hg2 #H destruct
+  elim (IH … Hf2 Hg2) -IH -i /3 width=9 by at_push, ex2_intro/
+]
+qed-.
+
+theorem at_div_nn: ∀f2,g2,f1,g1.
+                   H_at_div f2 g2 f1 g1 → H_at_div (⫯f2) (⫯g2) (f1) (g1).
+#f2 #g2 #f1 #g1 #IH #jf #jg #j #Hf #Hg
+elim (at_inv_xnx … Hf) -Hf [ |*: // ] #i #Hf2 #H destruct
+lapply (at_inv_xnn … Hg ????) -Hg [5: |*: // ] #Hg2
+elim (IH … Hf2 Hg2) -IH -i /2 width=3 by ex2_intro/
+qed-.
+
+theorem at_div_np: ∀f2,g2,f1,g1.
+                   H_at_div f2 g2 f1 g1 → H_at_div (⫯f2) (↑g2) (f1) (⫯g1).
+#f2 #g2 #f1 #g1 #IH #jf #jg #j #Hf #Hg
+elim (at_inv_xnx … Hf) -Hf [ |*: // ] #i #Hf2 #H destruct
+lapply (at_inv_xpn … Hg ????) -Hg [5: * |*: // ] #xg #Hg2 #H destruct
+elim (IH … Hf2 Hg2) -IH -i /3 width=7 by at_next, ex2_intro/
+qed-.
+
+theorem at_div_pn: ∀f2,g2,f1,g1.
+                   H_at_div f2 g2 f1 g1 → H_at_div (↑f2) (⫯g2) (⫯f1) (g1).
+/4 width=6 by at_div_np, at_div_comm/ qed-.
+
 (* Properties on tls ********************************************************)
 
 lemma at_pxx_tls: ∀n,f. @⦃0, f⦄ ≡ n → @⦃0, ⫱*[n]f⦄ ≡ 0.
 #n elim n -n //
-#n #IH #f #Hf cases (at_inv_pxn … Hf) -Hf /2 width=3 by/
+#n #IH #f #Hf
+cases (at_inv_pxn … Hf) -Hf [ |*: // ] #g #Hg #H0 destruct
+<tls_xn /2 width=1 by/
 qed.
 
 lemma at_tls: ∀i2,f. ↑⫱*[⫯i2]f ≗ ⫱*[i2]f → ∃i1. @⦃i1, f⦄ ≡ i2.
@@ -285,11 +330,29 @@ qed-.
 
 (* Inversion lemmas with tls ************************************************)
 
+lemma at_inv_nxx: ∀n,g,i1,j2. @⦃⫯i1, g⦄ ≡ j2 → @⦃0, g⦄ ≡ n →
+                  ∃∃i2. @⦃i1, ⫱*[⫯n]g⦄ ≡ i2 & ⫯(n+i2) = j2.
+#n elim n -n
+[ #g #i1 #j2 #Hg #H
+  elim (at_inv_pxp … H) -H [ |*: // ] #f #H0
+  elim (at_inv_npx … Hg … H0) -Hg [ |*: // ] #x2 #Hf #H2 destruct
+  /2 width=3 by ex2_intro/
+| #n #IH #g #i1 #j2 #Hg #H
+  elim (at_inv_pxn … H) -H [ |*: // ] #f #Hf2 #H0
+  elim (at_inv_xnx … Hg … H0) -Hg #x2 #Hf1 #H2 destruct
+  elim (IH … Hf1 Hf2) -IH -Hf1 -Hf2 #i2 #Hf #H2 destruct
+  /2 width=3 by ex2_intro/
+]
+qed-.
+
 lemma at_inv_tls: ∀i2,i1,f. @⦃i1, f⦄ ≡ i2 → ↑⫱*[⫯i2]f ≗ ⫱*[i2]f.
 #i2 elim i2 -i2
 [ #i1 #f #Hf elim (at_inv_xxp … Hf) -Hf // #g #H1 #H destruct
   /2 width=1 by eq_refl/
-| #i2 #IH #i1 #f #Hf elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ] /2 width=2 by/
+| #i2 #IH #i1 #f #Hf
+  elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ]
+  [ #g #j1 #Hg #H1 #H2 | #g #Hg #Ho ] destruct
+  <tls_xn /2 width=2 by/
 ]
 qed-.
 
@@ -321,8 +384,29 @@ lemma id_inv_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → 𝐈𝐝 ≗ f.
 lemma id_at: ∀i. @⦃i, 𝐈𝐝⦄ ≡ i.
 /2 width=1 by isid_inv_at/ qed.
 
+(* Advanced forward lemmas on id ********************************************)
+
+lemma at_id_fwd: ∀i1,i2. @⦃i1, 𝐈𝐝⦄ ≡ i2 → i1 = i2.
+/2 width=4 by at_mono/ qed.
+
+(* Main properties on id ****************************************************)
+
+theorem at_div_id_dx: ∀f. H_at_div f 𝐈𝐝 𝐈𝐝 f.
+#f #jf #j0 #j #Hf #H0
+lapply (at_id_fwd … H0) -H0 #H destruct
+/2 width=3 by ex2_intro/
+qed-.
+
+theorem at_div_id_sn: ∀f. H_at_div 𝐈𝐝 f f 𝐈𝐝.
+/3 width=6 by at_div_id_dx, at_div_comm/ qed-.
+
 (* Properties with uniform relocations **************************************)
 
 lemma at_uni: ∀n,i. @⦃i,𝐔❴n❵⦄ ≡ n+i.
 #n elim n -n /2 width=5 by at_next/
 qed.
+
+(* Inversion lemmas with uniform relocations ********************************)
+
+lemma at_inv_uni: ∀n,i,j. @⦃i,𝐔❴n❵⦄ ≡ j → j = n+i.
+/2 width=4 by at_mono/ qed-.