From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 31 Mar 2016 14:44:31 +0000 (+0000)
Subject: - uniform relocations
X-Git-Tag: make_still_working~618
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9a023f554e56d6edbbb2eeaf17ce61e31857ef4a;p=helm.git

- uniform relocations
- more results on at and after
---

diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/uniform_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/uniform_1.ma
new file mode 100644
index 000000000..896665d02
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/uniform_1.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( 𝐔 ❴ break term 46 a ❵ )"
+  non associative with precedence 90
+  for @{ 'Uniform $a }.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
index fdfefbba5..80401a3d1 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
@@ -14,7 +14,7 @@
 
 include "ground_2/notation/relations/rafter_3.ma".
 include "ground_2/relocation/rtmap_istot.ma".
-include "ground_2/relocation/rtmap_isuni.ma".
+include "ground_2/relocation/rtmap_uni.ma".
 
 (* RELOCATION MAP ***********************************************************)
 
@@ -251,7 +251,7 @@ corec theorem after_trans2: ∀f1,f0,f4. f1 ⊚ f0 ≡ f4 →
 ]
 qed-.
 
-(* Main inversion lemmas on after *******************************************)
+(* Main inversion lemmas ****************************************************)
 
 corec theorem after_mono: ∀f1,f2,x,y. f1 ⊚ f2 ≡ x → f1 ⊚ f2 ≡ y → x ≗ y.
 #f1 #f2 #x #y * -f1 -f2 -x
@@ -382,6 +382,43 @@ lemma after_fwd_at1: ∀i,i2,i1,f,f2. @⦃i1, f⦄ ≡ i → @⦃i2, f2⦄ ≡ i
 ]
 qed-.
 
+(* Properties with at *******************************************************)
+
+lemma after_isuni_dx: ∀i2,i1,f2. @⦃i1, f2⦄ ≡ i2 →
+                      ∀f. f2 ⊚ 𝐔❴i1❵ ≡ f → 𝐔❴i2❵ ⊚ ⫱*[i2] f2 ≡ f.
+#i2 elim i2 -i2
+[ #i1 #f2 #Hf2 #f #Hf
+  elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
+  lapply (after_isid_inv_dx … Hf ?) -Hf
+  /3 width=3 by isid_after_sn, after_eq_repl_back_0/
+| #i2 #IH #i1 #f2 #Hf2 #f #Hf
+  elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
+  [ #g2 #j1 #Hg2 #H1 #H2 destruct
+    elim (after_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
+    /3 width=5 by after_next/
+  | #g2 #Hg2 #H2 destruct
+    elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
+    /3 width=5 by after_next/
+  ]
+]
+qed.
+
+lemma after_isuni_sn: ∀i2,i1,f2. @⦃i1, f2⦄ ≡ i2 →
+                      ∀f. 𝐔❴i2❵ ⊚ ⫱*[i2] f2 ≡ f → f2 ⊚ 𝐔❴i1❵ ≡ f.
+#i2 elim i2 -i2
+[ #i1 #f2 #Hf2 #f #Hf
+  elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
+  lapply (after_isid_inv_sn … Hf ?) -Hf
+  /3 width=3 by isid_after_dx, after_eq_repl_back_0/
+| #i2 #IH #i1 #f2 #Hf2 #f #Hf
+  elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
+  elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
+  [ #g2 #j1 #Hg2 #H1 #H2 destruct /3 width=7 by after_push/
+  | #g2 #Hg2 #H2 destruct /3 width=5 by after_next/
+  ]
+]
+qed-.
+
 (* Forward lemmas on istot **************************************************)
 
 lemma after_istot_fwd: ∀f2,f1,f. f2 ⊚ f1 ≡ f → 𝐓⦃f2⦄ → 𝐓⦃f1⦄ → 𝐓⦃f⦄.
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 e60a2affc..06223bc53 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma
@@ -274,6 +274,25 @@ lemma at_pxx_tls: ∀n,f. @⦃0, f⦄ ≡ n → @⦃0, ⫱*[n]f⦄ ≡ 0.
 #n #IH #f #Hf cases (at_inv_pxn … Hf) -Hf /2 width=3 by/
 qed.
 
+lemma at_tls: ∀i2,f. ↑⫱*[⫯i2]f ≗ ⫱*[i2]f → ∃i1. @⦃i1, f⦄ ≡ i2.
+#i2 elim i2 -i2
+[ /4 width=4 by at_eq_repl_back, at_refl, ex_intro/
+| #i2 #IH #f <tls_xn <tls_xn in ⊢ (??%→?); #H
+  elim (IH … H) -IH -H #i1 #Hf
+  elim (pn_split f) * #g #Hg destruct /3 width=8 by at_push, at_next, ex_intro/  
+]
+qed-.
+
+(* Inversion lemmas with tls ************************************************)
+
+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/
+]
+qed-.
+
 (* Advanced inversion lemmas on isid ****************************************)
 
 lemma isid_inv_at: ∀i,f. 𝐈⦃f⦄ → @⦃i, f⦄ ≡ i.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isuni.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isuni.ma
index efde1a120..273793d93 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isuni.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isuni.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "ground_2/notation/relations/isuniform_1.ma".
-include "ground_2/relocation/rtmap_isid.ma".
+include "ground_2/relocation/rtmap_isfin.ma".
 
 (* RELOCATION MAP ***********************************************************)
 
@@ -39,7 +39,18 @@ lemma isuni_inv_next: ∀g. 𝐔⦃g⦄ → ∀f. ⫯f = g → 𝐔⦃f⦄.
 ]
 qed-.
 
+lemma isuni_split: ∀g. 𝐔⦃g⦄ → (∃∃f. 𝐈⦃f⦄ & ↑f = g) ∨ (∃∃f.𝐔⦃f⦄ & ⫯f = g).
+#g #H elim (pn_split g) * #f #Hf
+/4 width=3 by isuni_inv_next, isuni_inv_push, or_introl, or_intror, ex2_intro/
+qed-.
+
 (* basic forward lemmas *****************************************************)
 
 lemma isuni_fwd_push: ∀g. 𝐔⦃g⦄ → ∀f. ↑f = g → 𝐔⦃f⦄.
 /3 width=3 by isuni_inv_push, isuni_isid/ qed-.
+
+(* Forward lemmas with test for finite colength *****************************)
+
+lemma isuni_fwd_isfin: ∀f. 𝐔⦃f⦄ → 𝐅⦃f⦄.
+#f #H elim H -f /3 width=1 by isfin_next, isfin_isid/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_uni.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_uni.ma
new file mode 100644
index 000000000..5f45b1f28
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_uni.ma
@@ -0,0 +1,101 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "ground_2/notation/functions/uniform_1.ma".
+include "ground_2/relocation/rtmap_id.ma".
+include "ground_2/relocation/rtmap_isuni.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+rec definition uni (n:nat) on n: rtmap  ≝ match n with
+[ O   ⇒ 𝐈𝐝
+| S n ⇒ ⫯(uni n)
+].
+
+interpretation "uniform relocation (rtmap)"
+   'Uniform n = (uni n).
+
+(* Basic properties *********************************************************)
+
+lemma uni_zero: 𝐈𝐝 = 𝐔❴0❵.
+// qed.
+
+lemma uni_succ: ∀n. ⫯𝐔❴n❵ = 𝐔❴⫯n❵.
+// qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma uni_inv_push_dx: ∀f,n. 𝐔❴n❵ ≗ ↑f → 0 = n ∧ 𝐈𝐝 ≗ f.
+#f * /3 width=5 by eq_inv_pp, conj/
+#n <uni_succ #H elim (eq_inv_np … H) -H //
+qed-.
+
+lemma uni_inv_push_sn: ∀f,n. ↑f ≗ 𝐔❴n❵ → 0 = n ∧ 𝐈𝐝 ≗ f.
+/3 width=1 by uni_inv_push_dx, eq_sym/ qed-.
+
+lemma uni_inv_id_dx: ∀n. 𝐔❴n❵ ≗ 𝐈𝐝 → 0 = n.
+#n <id_rew #H elim (uni_inv_push_dx … H) -H //
+qed-.
+
+lemma uni_inv_id_sn: ∀n.  𝐈𝐝 ≗ 𝐔❴n❵ → 0 = n.
+/3 width=1 by uni_inv_id_dx, eq_sym/ qed-.
+
+lemma uni_inv_next_dx: ∀f,n. 𝐔❴n❵ ≗ ⫯f → ∃∃m. 𝐔❴m❵ ≗ f & ⫯m = n.
+#f *
+[ <uni_zero <id_rew #H elim (eq_inv_pn … H) -H //
+| #n <uni_succ /3 width=5 by eq_inv_nn, ex2_intro/
+]
+qed-.
+
+lemma uni_inv_next_sn: ∀f,n. ⫯f ≗ 𝐔❴n❵ → ∃∃m. 𝐔❴m❵ ≗ f & ⫯m = n.
+/3 width=1 by uni_inv_next_dx, eq_sym/ qed-.
+
+(* Properties with test for identity ****************************************)
+
+lemma uni_isid: ∀f. 𝐈⦃f⦄ → 𝐔❴0❵ ≗ f.
+/2 width=1 by eq_id_inv_isid/ qed-.
+
+(* Inversion lemmas with test for identity **********************************)
+
+lemma uni_inv_isid: ∀f. 𝐔❴0❵ ≗ f → 𝐈⦃f⦄.
+/2 width=1 by eq_id_isid/ qed-.
+
+(* Properties with finite colength assignment ***************************)
+
+lemma fcla_uni: ∀n. 𝐂⦃𝐔❴n❵⦄ ≡ n.
+#n elim n -n /2 width=1 by fcla_isid, fcla_next/
+qed.
+
+(* Properties with test for finite colength ***************************)
+
+lemma isfin_uni: ∀n. 𝐅⦃𝐔❴n❵⦄.
+/3 width=2 by ex_intro/ qed.
+
+(* Properties with test for uniformity **************************************)
+
+lemma isuni_uni: ∀n. 𝐔⦃𝐔❴n❵⦄.
+#n elim n -n /3 width=3 by isuni_isid, isuni_next/
+qed.
+
+lemma uni_isuni: ∀f. 𝐔⦃f⦄ → ∃n. 𝐔❴n❵ ≗ f.
+#f #H elim H -f /3 width=2 by uni_isid, ex_intro/
+#f #_ #g #H * /3 width=6 by eq_next, ex_intro/
+qed-.
+
+(* Inversion lemmas with test for uniformity ********************************)
+
+lemma uni_inv_isuni: ∀n,f. 𝐔❴n❵ ≗ f →  𝐔⦃f⦄.
+#n elim n -n /3 width=1 by uni_inv_isid, isuni_isid/
+#n #IH #x <uni_succ #H elim (eq_inv_nx … H) -H /3 width=3 by isuni_next/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
index a41b50b2d..9016bbd4f 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
@@ -23,8 +23,8 @@ table {
    class "grass"
    [ { "multiple relocation" * } {
         [ { "" * } {
-             [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )" "rtmap_isfin ( 𝐅⦃?⦄ )" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_sor ( ? ⋓ ? ≡ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" * ]
-             [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" "" "" "" "nstream_sand" "" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" * ]
+             [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )" "rtmap_isfin ( 𝐅⦃?⦄ )" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_uni ( 𝐔❴?❵ )" "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_sor ( ? ⋓ ? ≡ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" * ]
+             [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" "" "" "" "" "nstream_sand" "" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" * ]
 (*
              [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )"
                "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ]