update in ground_2

+ basic relocation swap
+ one name fixed
+ bugs emerging in cpr fixed

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma
index 091282ef316e06447346846c3f54e05b9a14f480..a3cfa2c8c505c93ddc185e68a520e22ab9044802 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma
@@ -42,13 +42,15 @@ lemma cpr_inv_atom1: ∀h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[h] T2 →
                       | ∃∃I,K,T,i. ⦃G, K⦄ ⊢ #i ➡[h] T & ⬆*[1] T ≘ T2 &
                                    L = K.ⓘ{I} & J = LRef (↑i).
 #h #J #G #L #T2 #H elim (cpm_inv_atom1 … H) -H *
-/3 width=8 by tri_lt, or3_intro0, or3_intro1, or3_intro2, ex4_4_intro, ex4_3_intro/
-#n #_ #_ #H destruct
+[2,4:|*: /3 width=8 by or3_intro0, or3_intro1, or3_intro2, ex4_4_intro, ex4_3_intro/ ]
+[ #n #_ #_ #H destruct
+| #n #K #V1 #V2 #_ #_ #_ #_ #H destruct
+]  
 qed-.
 
 (* Basic_1: includes: pr0_gen_sort pr2_gen_sort *)
 lemma cpr_inv_sort1: ∀h,G,L,T2,s. ⦃G, L⦄ ⊢ ⋆s ➡[h] T2 → T2 = ⋆s.
-#h #G #L #T2 #s #H elim (cpm_inv_sort1 … H) -H * // #_ #H destruct
+#h #G #L #T2 #s #H elim (cpm_inv_sort1 … H) -H * [ // ] #_ #H destruct
 qed-.
 
 lemma cpr_inv_zero1: ∀h,G,L,T2. ⦃G, L⦄ ⊢ #0 ➡[h] T2 →
@@ -125,7 +127,7 @@ lemma cpr_ind (h): ∀Q:relation4 genv lenv term term.
                    ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → Q G L T1 T2.
 #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T1 #T2
 @(insert_eq_0 … 0) #n #H
-@(cpm_ind … H) -G -L -T1 -T2 -n /3 width=4 by/
+@(cpm_ind … H) -G -L -T1 -T2 -n [2,4,11:|*: /3 width=4 by/ ]
 [ #G #L #s #H destruct
 | #n #G #K #V1 #V2 #W2 #_ #_ #_ #H destruct
 | #n #G #L #U1 #U2 #T #_ #_ #H destruct

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
index 0f21ba6c3774da6595e4df07715653c882f7f8d9..6ce6fa476a68bc4e2ed4587653a9f4e0d25b2677 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
@@ -151,3 +151,8 @@ qed-.
 lemma after_inv_apply: ∀f2,f1,f,n2,n1,n. n2⨮f2 ⊚ n1⨮f1 ≘ n⨮f →
                        (n2⨮f2)@❴n1❵ = n ∧ (⫰*[n1]f2) ⊚ f1 ≘ f.
 /3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.
+
+(* Properties on apply ******************************************************)
+
+lemma compose_apply (f2) (f1) (i): f2@❴f1@❴i❵❵ = (f2∘f1)@❴i❵.
+/4 width=6 by after_fwd_at, at_inv_total, sym_eq/ qed.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_basic.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_basic.ma
new file mode 100644 (file)
index 0000000..613f279
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_basic.ma
@@ -0,0 +1,48 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/relocation/rtmap_basic.ma".
+include "ground_2/relocation/nstream_after.ma".
+
+(* RELOCATION N-STREAM ******************************************************)
+
+(* Specific properties on basic relocation **********************************)
+
+lemma apply_basic_lt: ∀m,n,i. i < m → 𝐁❴m,n❵@❴i❵ = i.
+/3 width=1 by at_inv_total, at_basic_lt/ qed-.
+
+lemma apply_basic_ge: ∀m,n,i. m ≤ i → 𝐁❴m,n❵@❴i❵ = n+i.
+/3 width=1 by at_inv_total, at_basic_ge/ qed-.
+
+(* Specific main properties on basic relocation *****************************)
+
+theorem basic_swap: ∀d1,d2. d2 ≤ d1 →
+                    ∀h1,h2. 𝐁❴d2,h2❵∘𝐁❴d1,h1❵ ≡ 𝐁❴h2+d1,h1❵∘𝐁❴d2,h2❵.
+#d1 #d2 #Hd21 #h1 #h2
+@nstream_inv_eq
+@nstream_eq_inv_ext #i
+<compose_apply <compose_apply
+elim (lt_or_ge i d2) #Hd2
+[ lapply (lt_to_le_to_lt … Hd2 Hd21) -Hd21 #Hd1
+  >(apply_basic_lt … Hd1) >(apply_basic_lt … Hd2) >apply_basic_lt
+  /2 width=1 by le_plus_a/
+| elim (lt_or_ge i d1) -Hd21 #Hd1
+  [ >(apply_basic_lt … Hd1) >(apply_basic_ge … Hd2) >apply_basic_lt
+    /2 width=1 by monotonic_lt_plus_r/
+  | >(apply_basic_ge … Hd1) >(apply_basic_ge … Hd2)
+    >apply_basic_ge [2: /2 width=1 by le_plus_a/ ]
+    >apply_basic_ge /2 width=1 by monotonic_le_plus_r/
+  ]
+]
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
index 5ceef8a1be9738cc02d84ab3c2aa3073044ede81..9d2f3cd2b0e74dd8dabf2c7788b3281a57d01845 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
@@ -88,13 +88,19 @@ qed-.
 
 (* Basic properties *********************************************************)
 
+lemma apply_O1: ∀n,f. (n⨮f)@❴0❵ = n.
+// qed.
+
+lemma apply_S1: ∀n,f,i. (n⨮f)@❴↑i❵ = ↑(n+f@❴i❵).
+// qed.
+
 lemma apply_eq_repl (i): eq_repl … (λf1,f2. f1@❴i❵ = f2@❴i❵).
 #i elim i -i [2: #i #IH ] * #n1 #f1 * #n2 #f2 #H
 elim (eq_inv_seq_aux … H) -H normalize //
 #Hn #Hf /4 width=1 by eq_f2, eq_f/
 qed.
 
-lemma apply_S1: ∀f,i. (↑f)@❴i❵ = ↑(f@❴i❵).
+lemma apply_S2: ∀f,i. (↑f)@❴i❵ = ↑(f@❴i❵).
 * #n #f * //
 qed.
 
@@ -102,3 +108,13 @@ qed.
 
 theorem apply_inj: ∀f,i1,i2,j. f@❴i1❵ = j → f@❴i2❵ = j → i1 = i2.
 /2 width=4 by at_inj/ qed-.
+
+corec theorem nstream_eq_inv_ext: ∀f1,f2. (∀i. f1@❴i❵ = f2@❴i❵) → f1 ≗ f2.
+* #n1 #f1 * #n2 #f2 #Hf @eq_seq
+[ @(Hf 0)
+| @nstream_eq_inv_ext -nstream_eq_inv_ext #i
+  lapply (Hf 0) >apply_O1 >apply_O1 #H destruct
+  lapply (Hf (↑i)) >apply_S1 >apply_S1 #H
+  /3 width=2 by injective_plus_r, injective_S/
+]
+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 baad25fc2a5a05ac84a893b30364a6b9dd54f24e..310871c3de71fd98ebfbaf3c8295fe0cf8fb5ca0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
@@ -27,8 +27,12 @@ table {
                "rtmap_at ( @⦃?,?⦄ ≘ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≘ ? )" "rtmap_coafter ( ? ~⊚ ? ≘ ? )"
                "rtmap_basic ( 𝐁❴?,?❵ )"
              * ]
-             [ "nstream ( ⫯? ) ( ↑? )" "nstream_eq" "" "" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" ""
-               "" "" "" "" "" "" "" "nstream_sor" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )"
+             [ "nstream ( ⫯? ) ( ↑? )" "nstream_eq" "" ""
+               "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" ""
+               "" "" "" ""
+               "" "" "" "nstream_sor"
+               "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )"
+               "nstream_basic"
              * ]
 (*
              [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≘ ? )" "trace_after ( ? ⊚ ? ≘ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )"