colength and identity relocation

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma
index d2acdb2bc79c4ad3e2862072d9567056407650d7..680cc4ac2afde0c61169bd9da1c0c78b7923bec5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma
@@ -32,6 +32,12 @@ qed-.
 lemma commutative_orb: commutative … orb.
 * * // qed.
 
+lemma orb_true_dx: ∀b. (b ∨ Ⓣ) = Ⓣ.
+* // qed.
+
+lemma orb_true_sn: ∀b. (Ⓣ ∨ b) = Ⓣ.
+// qed.
+
 lemma eq_bool_dec: ∀b1,b2:bool. Decidable (b1 = b2).
 * * /2 width=1 by or_introl/
 @or_intror #H destruct

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma
index e72b54531a68816777ebcab50614b146f8c87bbe..9e8d1ff4136e27778c44778e6e44b27bc2586562 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma
@@ -14,8 +14,6 @@
 
 include "ground_2/notation/constructors/nil_0.ma".
 include "ground_2/notation/constructors/cons_2.ma".
-include "ground_2/notation/constructors/cons_3.ma".
-include "ground_2/notation/functions/append_2.ma".
 include "ground_2/lib/arith.ma".
 
 (* LISTS ********************************************************************)
@@ -30,7 +28,7 @@ interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl).
 
 let rec length (A:Type[0]) (l:list A) on l ≝ match l with
 [ nil      ⇒ 0
-| cons _ l ⇒ length A l + 1
+| cons _ l ⇒ ⫯(length A l)
 ].
 
 interpretation "length (list)"
@@ -42,26 +40,29 @@ let rec all A (R:predicate A) (l:list A) on l ≝
   | cons hd tl ⇒ R hd ∧ all A R tl
   ].
 
-inductive list2 (A1,A2:Type[0]) : Type[0] :=
-  | nil2 : list2 A1 A2
-  | cons2: A1 → A2 → list2 A1 A2 → list2 A1 A2.
+(* Basic properties on length ***********************************************)
 
-interpretation "nil (list of pairs)" 'Nil = (nil2 ? ?).
+lemma length_nil (A:Type[0]): |nil A| = 0.
+// qed.
 
-interpretation "cons (list of pairs)" 'Cons hd1 hd2 tl = (cons2 ? ? hd1 hd2 tl).
+lemma length_cons (A:Type[0]) (l:list A) (a:A): |a@l| = ⫯|l|.
+// qed.
 
-let rec append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with
-[ nil2           ⇒ l2
-| cons2 a1 a2 tl ⇒ {a1, a2} @ append2 A1 A2 tl l2
-].
+(* Basic inversion lemmas on length *****************************************)
 
-interpretation "append (list of pairs)"
-   'Append l1 l2 = (append2 ? ? l1 l2).
+lemma length_inv_zero_dx (A:Type[0]) (l:list A): |l| = 0 → l = ◊.
+#A * // #a #l >length_cons #H destruct
+qed-.
 
-let rec length2 (A1,A2:Type[0]) (l:list2 A1 A2) on l ≝ match l with
-[ nil2        ⇒ 0
-| cons2 _ _ l ⇒ length2 A1 A2 l + 1
-].
+lemma length_inv_zero_sn (A:Type[0]) (l:list A): 0 = |l| → l = ◊.
+/2 width=1 by length_inv_zero_dx/ qed-.
+
+lemma length_inv_succ_dx (A:Type[0]) (l:list A) (x): |l| = ⫯x →
+                         ∃∃tl,a. x = |tl| & l = a @ tl.
+#A * /2 width=4 by ex2_2_intro/
+>length_nil #x #H destruct
+qed-.
 
-interpretation "length (list of pairs)"
-   'card l = (length2 ? ? l).
+lemma length_inv_succ_sn (A:Type[0]) (l:list A) (x): ⫯x = |l| →
+                         ∃∃tl,a. x = |tl| & l = a @ tl.
+/2 width=1 by length_inv_succ_dx/ qed.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/list2.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/list2.ma
new file mode 100644 (file)
index 0000000..f730994
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/list2.ma
@@ -0,0 +1,44 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/constructors/nil_0.ma".
+include "ground_2/notation/constructors/cons_3.ma".
+include "ground_2/notation/functions/append_2.ma".
+include "ground_2/lib/arith.ma".
+
+(* LISTS OF PAIRS ***********************************************************)
+
+inductive list2 (A1,A2:Type[0]) : Type[0] :=
+  | nil2 : list2 A1 A2
+  | cons2: A1 → A2 → list2 A1 A2 → list2 A1 A2.
+
+interpretation "nil (list of pairs)" 'Nil = (nil2 ? ?).
+
+interpretation "cons (list of pairs)" 'Cons hd1 hd2 tl = (cons2 ? ? hd1 hd2 tl).
+
+let rec append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with
+[ nil2           ⇒ l2
+| cons2 a1 a2 tl ⇒ {a1, a2} @ append2 A1 A2 tl l2
+].
+
+interpretation "append (list of pairs)"
+   'Append l1 l2 = (append2 ? ? l1 l2).
+
+let rec length2 (A1,A2:Type[0]) (l:list2 A1 A2) on l ≝ match l with
+[ nil2        ⇒ 0
+| cons2 _ _ l ⇒ ⫯(length2 A1 A2 l)
+].
+
+interpretation "length (list of pairs)"
+   'card l = (length2 ? ? l).

diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/norm_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/norm_1.ma
new file mode 100644 (file)
index 0000000..d0f0719
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/norm_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 ( ∥ term 19 C ∥ )"
+  with precedence 70
+  for @{ 'Norm $C }.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isid_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isid_1.ma
new file mode 100644 (file)
index 0000000..eb11c15
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isid_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( 𝐈 ⦃ term 46 f ⦄ )"
+   non associative with precedence 45
+   for @{ 'IsId $f }.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2.ma
index 072b07f6cdc7fcc1245193fd1a860fe26d884678..3bd8fa3f9f3548ecc9f8d2d1b905e02faea36d6d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/lib/list.ma".
+include "ground_2/lib/list2.ma".
 
 (* MULTIPLE RELOCATION WITH PAIRS *******************************************)
 

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace.ma
index 680e89dbb3a1891f8dd8f14a8f3d3571cc74fd4c..699942e056864b7196cb729e6982f1f87c497ac1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace.ma
@@ -12,9 +12,39 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/notation/functions/norm_1.ma".
 include "ground_2/lib/bool.ma".
 include "ground_2/lib/list.ma".
 
 (* RELOCATION TRACE *********************************************************)
 
 definition trace: Type[0] ≝ list bool.
+
+let rec colength (cs:trace) on cs ≝ match cs with
+[ nil       ⇒ 0
+| cons b tl ⇒ match b with [ true ⇒  ⫯(colength tl) | false ⇒ colength tl ] 
+].
+
+interpretation "colength (trace)"
+   'Norm cs = (colength cs).
+
+(* basic properties *********************************************************)
+
+lemma colength_empty: ∥◊∥ = 0.
+// qed.
+
+lemma colength_true: ∀cs. ∥Ⓣ@cs∥ = ⫯∥cs∥.
+// qed.
+
+lemma colength_false: ∀cs. ∥Ⓕ@cs∥ = ∥cs∥.
+// qed.
+
+lemma colength_cons: ∀cs1,cs2. ∥cs1∥ = ∥cs2∥ →
+                     ∀b. ∥b@cs1∥ = ∥b@cs2∥.
+#cs1 #cs2 #H * /2 width=1 by/
+qed.
+
+lemma colength_le: ∀cs. ∥cs∥ ≤ |cs|.
+#cs elim cs -cs //
+* /2 width=1 by le_S_S, le_S/
+qed.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_after.ma
index 06c914a9b5aa9a3ec8425bf2860865a7635e1be3..72c5d161223487b4e204a2eb4c59cf620fefbe6e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_after.ma
@@ -27,6 +27,21 @@ inductive after: relation3 trace trace trace ≝
 interpretation "composition (trace)"
    'RAfter cs1 cs2 cs = (after cs1 cs2 cs).
 
+(* Basic properties *********************************************************)
+
+lemma after_length: ∀cs1,cs2. ∥cs1∥ = |cs2| →
+                    ∃∃cs. cs1 ⊚ cs2 ≡ cs & |cs| = |cs1| & ∥cs∥ = ∥cs2∥.
+#cs1 elim cs1 -cs1
+[ #cs2 #H >(length_inv_zero_sn … H) -cs2 /2 width=4 by after_empty, ex3_intro/
+| * #cs1 #IH #cs2 #Hcs
+  [ elim (length_inv_succ_sn … Hcs) -Hcs
+    #tl #b #Hcs #H destruct
+  ]
+  elim (IH … Hcs) -IH -Hcs
+  #cs #Hcs #H1 #H2 [ @(ex3_intro … (b@cs)) | @(ex3_intro … (Ⓕ@cs)) ] /2 width=1 by after_true, after_false, colength_cons/
+]  
+qed-.
+
 (* Basic inversion lemmas ***************************************************)
 
 fact after_inv_empty1_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → cs1 = ◊ →
@@ -98,12 +113,19 @@ lemma after_inv_inh3: ∀cs1,cs2,tl,b. cs1 ⊚ cs2 ≡ b @ tl →
                       ∃∃tl1.  cs1 = Ⓕ @ tl1 & b = Ⓕ & tl1 ⊚ cs2 ≡ tl.
 /2 width=3 by after_inv_inh3_aux/ qed-.
 
+lemma after_inv_length: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs →
+                        ∧∧ ∥cs1∥ = |cs2| & |cs| = |cs1| & ∥cs∥ = ∥cs2∥.
+#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs /2 width=1 by and3_intro/
+#cs1 #cs2 #cs #_ [ * ] * /2 width=1 by and3_intro/
+qed-.
+
 (* Basic forward lemmas *****************************************************)
 
 lemma after_at_fwd: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → ∀i1,i. @⦃i1, cs⦄ ≡ i →
                     ∃∃i2. @⦃i1, cs1⦄ ≡ i2 & @⦃i2, cs2⦄ ≡ i.
 #cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs
-[ #i1 #i #H elim (at_inv_empty … H)
+[ #i1 #i #H elim (at_inv_empty … H) -H
+  #H1 #H2 destruct /2 width=3 by at_empty, ex2_intro/  
 | #cs1 #cs2 #cs #_ * #IH #i1 #i #H
   [ elim (at_inv_true … H) -H *
     [ -IH #H1 #H2 destruct /2 width=3 by at_zero, ex2_intro/
@@ -123,7 +145,8 @@ qed-.
 lemma after_fwd_at: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → ∀i1,i2. @⦃i1, cs1⦄ ≡ i2 →
                     ∃∃i. @⦃i2, cs2⦄ ≡ i & @⦃i1, cs⦄ ≡ i.
 #cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs
-[ #i1 #i2 #H elim (at_inv_empty … H)
+[ #i1 #i2 #H elim (at_inv_empty … H) -H
+  #H1 #H2 destruct /2 width=3 by at_empty, ex2_intro/
 | #cs1 #cs2 #cs #_ * #IH #i1 #i2 #H
   [ elim (at_inv_true … H) -H *
     [ -IH #H1 #H2 destruct /2 width=3 by at_zero, ex2_intro/

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma
index f4b6f8d3ad033753006b53d8247855b8bb261ef8..b40b1c87b3be088ea46e2c08fea38a329e561cc9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma
@@ -18,132 +18,184 @@ include "ground_2/relocation/trace.ma".
 (* RELOCATION TRACE *********************************************************)
 
 inductive at: trace → relation nat ≝
+   | at_empty: at (◊) 0 0
    | at_zero : ∀cs. at (Ⓣ @ cs) 0 0
-   | at_succ : ∀cs,i,j. at cs i j → at (Ⓣ @ cs) (⫯i) (⫯j)
-   | at_false: ∀cs,i,j. at cs i j → at (Ⓕ @ cs) i (⫯j).
+   | at_succ : ∀cs,i1,i2. at cs i1 i2 → at (Ⓣ @ cs) (⫯i1) (⫯i2)
+   | at_false: ∀cs,i1,i2. at cs i1 i2 → at (Ⓕ @ cs) i1 (⫯i2).
 
 interpretation "relocation (trace)"
    'RAt i1 cs i2 = (at cs i1 i2).
 
 (* Basic inversion lemmas ***************************************************)
 
-fact at_inv_empty_aux: ∀cs,i,j. @⦃i, cs⦄ ≡ j → cs = ◊ → ⊥.
-#cs #i #j * -cs -i -j
-#cs [2,3: #i #j #_ ] #H destruct
+fact at_inv_empty_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → cs = ◊ → i1 = 0 ∧ i2 = 0.
+#cs #i1 #i2 * -cs -i1 -i2 /2 width=1 by conj/
+#cs #i1 #i2 #_ #H destruct
 qed-.
 
-lemma at_inv_empty: ∀i,j. @⦃i, ◊⦄ ≡ j → ⊥.
+lemma at_inv_empty: ∀i1,i2. @⦃i1, ◊⦄ ≡ i2 → i1 = 0 ∧ i2 = 0.
 /2 width=5 by at_inv_empty_aux/ qed-.
 
-fact at_inv_true_aux: ∀cs,i,j. @⦃i, cs⦄ ≡ j → ∀tl. cs = Ⓣ @ tl →
-                      (i = 0 ∧ j = 0) ∨
-                      ∃∃i0,j0. i = ⫯i0 & j = ⫯j0 & @⦃i0, tl⦄ ≡ j0.
-#cs #i #j * -cs -i -j
-#cs [2,3: #i #j #Hij ] #tl #H destruct
+lemma at_inv_empty_zero_sn: ∀i. @⦃0, ◊⦄ ≡ i → i = 0.
+#i #H elim (at_inv_empty … H) -H //
+qed-.
+
+lemma at_inv_empty_zero_dx: ∀i. @⦃i, ◊⦄ ≡ 0 → i = 0.
+#i #H elim (at_inv_empty … H) -H //
+qed-.
+
+lemma at_inv_empty_succ_sn: ∀i1,i2. @⦃⫯i1, ◊⦄ ≡ i2 → ⊥.
+#i1 #i2 #H elim (at_inv_empty … H) -H #H1 #H2 destruct
+qed-.
+
+lemma at_inv_empty_succ_dx: ∀i1,i2. @⦃i1, ◊⦄ ≡ ⫯i2 → ⊥.
+#i1 #i2 #H elim (at_inv_empty … H) -H #H1 #H2 destruct
+qed-.
+
+fact at_inv_true_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∀tl. cs = Ⓣ @ tl →
+                      (i1 = 0 ∧ i2 = 0) ∨
+                      ∃∃j1,j2. i1 = ⫯j1 & i2 = ⫯j2 & @⦃j1, tl⦄ ≡ j2.
+#cs #i1 #i2 * -cs -i1 -i2
+[2,3,4: #cs [2,3: #i1 #i2 #Hij ] ] #tl #H destruct
 /3 width=5 by ex3_2_intro, or_introl, or_intror, conj/
 qed-.
 
-lemma at_inv_true: ∀cs,i,j. @⦃i, Ⓣ @ cs⦄ ≡ j →
-                   (i = 0 ∧ j = 0) ∨
-                   ∃∃i0,j0. i = ⫯i0 & j = ⫯j0 & @⦃i0, cs⦄ ≡ j0.
+lemma at_inv_true: ∀cs,i1,i2. @⦃i1, Ⓣ @ cs⦄ ≡ i2 →
+                   (i1 = 0 ∧ i2 = 0) ∨
+                   ∃∃j1,j2. i1 = ⫯j1 & i2 = ⫯j2 & @⦃j1, cs⦄ ≡ j2.
 /2 width=3 by at_inv_true_aux/ qed-.
 
-lemma at_inv_true_zero_sn: ∀cs,j. @⦃0, Ⓣ @ cs⦄ ≡ j → j = 0.
-#cs #j #H elim (at_inv_true … H) -H * //
-#i0 #j0 #H destruct
+lemma at_inv_true_zero_sn: ∀cs,i. @⦃0, Ⓣ @ cs⦄ ≡ i → i = 0.
+#cs #i #H elim (at_inv_true … H) -H * //
+#j1 #j2 #H destruct
 qed-.
 
 lemma at_inv_true_zero_dx: ∀cs,i. @⦃i, Ⓣ @ cs⦄ ≡ 0 → i = 0.
 #cs #i #H elim (at_inv_true … H) -H * //
-#i0 #j0 #_ #H destruct
+#j1 #j2 #_ #H destruct
 qed-.
 
-lemma at_inv_true_succ_sn: ∀cs,i,j. @⦃⫯i, Ⓣ @ cs⦄ ≡ j →
-                           ∃∃j0. j = ⫯j0 & @⦃i, cs⦄ ≡ j0.
-#cs #i #j #H elim (at_inv_true … H) -H *
+lemma at_inv_true_succ_sn: ∀cs,i1,i2. @⦃⫯i1, Ⓣ @ cs⦄ ≡ i2 →
+                           ∃∃j2. i2 = ⫯j2 & @⦃i1, cs⦄ ≡ j2.
+#cs #i1 #i2 #H elim (at_inv_true … H) -H *
 [ #H destruct
-| #i0 #j0 #H1 #H2 destruct /2 width=3 by ex2_intro/
+| #j1 #j2 #H1 #H2 destruct /2 width=3 by ex2_intro/
 ]
 qed-.
 
-lemma at_inv_true_succ_dx: ∀cs,i,j. @⦃i, Ⓣ @ cs⦄ ≡ ⫯j →
-                           ∃∃i0. i = ⫯i0 & @⦃i0, cs⦄ ≡ j.
-#cs #i #j #H elim (at_inv_true … H) -H *
+lemma at_inv_true_succ_dx: ∀cs,i1,i2. @⦃i1, Ⓣ @ cs⦄ ≡ ⫯i2 →
+                           ∃∃j1. i1 = ⫯j1 & @⦃j1, cs⦄ ≡ i2.
+#cs #i1 #i2 #H elim (at_inv_true … H) -H *
 [ #_ #H destruct
-| #i0 #j0 #H1 #H2 destruct /2 width=3 by ex2_intro/
+| #j1 #j2 #H1 #H2 destruct /2 width=3 by ex2_intro/
 ]
 qed-.
 
-lemma at_inv_true_succ: ∀cs,i,j. @⦃⫯i, Ⓣ @ cs⦄ ≡ ⫯j →
-                        @⦃i, cs⦄ ≡ j.
-#cs #i #j #H elim (at_inv_true … H) -H *
+lemma at_inv_true_succ: ∀cs,i1,i2. @⦃⫯i1, Ⓣ @ cs⦄ ≡ ⫯i2 →
+                        @⦃i1, cs⦄ ≡ i2.
+#cs #i1 #i2 #H elim (at_inv_true … H) -H *
 [ #H destruct
-| #i0 #j0 #H1 #H2 destruct //
+| #j1 #j2 #H1 #H2 destruct //
 ]
 qed-.
 
-lemma at_inv_true_O_S: ∀cs,j. @⦃0, Ⓣ @ cs⦄ ≡ ⫯j → ⊥.
-#cs #j #H elim (at_inv_true … H) -H *
+lemma at_inv_true_O_S: ∀cs,i. @⦃0, Ⓣ @ cs⦄ ≡ ⫯i → ⊥.
+#cs #i #H elim (at_inv_true … H) -H *
 [ #_ #H destruct
-| #i0 #j0 #H1 destruct
+| #j1 #j2 #H destruct
 ]
 qed-.
 
 lemma at_inv_true_S_O: ∀cs,i. @⦃⫯i, Ⓣ @ cs⦄ ≡ 0 → ⊥.
 #cs #i #H elim (at_inv_true … H) -H *
 [ #H destruct
-| #i0 #j0 #_ #H1 destruct
+| #j1 #j2 #_ #H destruct
 ]
 qed-.
 
-fact at_inv_false_aux: ∀cs,i,j. @⦃i, cs⦄ ≡ j → ∀tl. cs = Ⓕ @ tl →
-                       ∃∃j0. j = ⫯j0 & @⦃i, tl⦄ ≡ j0.
-#cs #i #j * -cs -i -j
-#cs [2,3: #i #j #Hij ] #tl #H destruct
+fact at_inv_false_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∀tl. cs = Ⓕ @ tl →
+                       ∃∃j2. i2 = ⫯j2 & @⦃i1, tl⦄ ≡ j2.
+#cs #i1 #i2 * -cs -i1 -i2
+[2,3,4: #cs [2,3: #i1 #i2 #Hij ] ] #tl #H destruct
 /2 width=3 by ex2_intro/
 qed-.
 
-lemma at_inv_false: ∀cs,i,j. @⦃i, Ⓕ @ cs⦄ ≡ j →
-                    ∃∃j0. j = ⫯j0 & @⦃i, cs⦄ ≡ j0.
+lemma at_inv_false: ∀cs,i1,i2. @⦃i1, Ⓕ @ cs⦄ ≡ i2 →
+                    ∃∃j2. i2 = ⫯j2 & @⦃i1, cs⦄ ≡ j2.
 /2 width=3 by at_inv_false_aux/ qed-.
 
-lemma at_inv_false_S: ∀cs,i,j. @⦃i, Ⓕ @ cs⦄ ≡ ⫯j → @⦃i, cs⦄ ≡ j.
-#cs #i #j #H elim (at_inv_false … H) -H
-#j0 #H destruct //
+lemma at_inv_false_S: ∀cs,i1,i2. @⦃i1, Ⓕ @ cs⦄ ≡ ⫯i2 → @⦃i1, cs⦄ ≡ i2.
+#cs #i1 #i2 #H elim (at_inv_false … H) -H
+#j2 #H destruct //
 qed-.
 
 lemma at_inv_false_O: ∀cs,i. @⦃i, Ⓕ @ cs⦄ ≡ 0 → ⊥.
 #cs #i #H elim (at_inv_false … H) -H
-#j0 #H destruct
+#j2 #H destruct
+qed-.
+
+lemma at_inv_le: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → i1 ≤ ∥cs∥ ∧ i2 ≤ |cs|.
+#cs #i1 #i2 #H elim H -cs -i1 -i2 /2 width=1 by conj/
+#cs #i1 #i2 #_ * /3 width=1 by le_S_S, conj/ 
+qed-.
+
+lemma at_inv_gt1: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∥cs∥  < i1 → ⊥.
+#cs #i1 #i2 #H elim (at_inv_le … H) -H /2 width=4 by lt_le_false/
+qed-.
+
+lemma at_inv_gt2: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → |cs| < i2 → ⊥.
+#cs #i1 #i2 #H elim (at_inv_le … H) -H /2 width=4 by lt_le_false/
 qed-.
 
 (* Basic properties *********************************************************)
 
-lemma at_monotonic: ∀cs,i2,j2. @⦃i2, cs⦄ ≡ j2 → ∀i1. i1 < i2 →
-                    ∃∃j1. @⦃i1, cs⦄ ≡ j1 & j1 < j2.
-#cs #i2 #j2 #H elim H -cs -i2 -j2
-[ #cs #i1 #H elim (lt_zero_false … H)
-| #cs #i #j #Hij #IH * /2 width=3 by ex2_intro, at_zero/
-  #i1 #H lapply (lt_S_S_to_lt … H) -H
-  #H elim (IH … H) -i
-  #j1 #Hij1 #H /3 width=3 by le_S_S, ex2_intro, at_succ/
-| #cs #i #j #_ #IH #i1 #H elim (IH … H) -i
+(* Note: lemma 250 *)
+lemma at_le: ∀cs,i1. i1 ≤ ∥cs∥ →
+             ∃∃i2. @⦃i1, cs⦄ ≡ i2 & i2 ≤ |cs|.
+#cs elim cs -cs
+[ #i1 #H <(le_n_O_to_eq … H) -i1 /2 width=3 by at_empty, ex2_intro/
+| * #cs #IH
+  [ * /2 width=3 by at_zero, ex2_intro/
+    #i1 #H lapply (le_S_S_to_le … H) -H
+    #H elim (IH … H) -IH -H /3 width=3 by at_succ, le_S_S, ex2_intro/
+  | #i1 #H elim (IH … H) -IH -H /3 width=3 by at_false, le_S_S, ex2_intro/
+  ]
+]
+qed-.
+
+lemma at_top: ∀cs. @⦃∥cs∥, cs⦄ ≡ |cs|.
+#cs elim cs -cs // * /2 width=1 by at_succ, at_false/
+qed. 
+
+lemma at_monotonic: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∀j1. j1 < i1 →
+                    ∃∃j2. @⦃j1, cs⦄ ≡ j2 & j2 < i2.
+#cs #i1 #i2 #H elim H -cs -i1 -i2
+[ #j1 #H elim (lt_zero_false … H)
+| #cs #j1 #H elim (lt_zero_false … H)
+| #cs #i1 #i2 #Hij #IH * /2 width=3 by ex2_intro, at_zero/
+  #j1 #H lapply (lt_S_S_to_lt … H) -H
+  #H elim (IH … H) -i1
+  #j2 #Hj12 #H /3 width=3 by le_S_S, ex2_intro, at_succ/
+| #cs #i1 #i2 #_ #IH #j1 #H elim (IH … H) -i1
   /3 width=3 by le_S_S, ex2_intro, at_false/
 ]
 qed-.
 
-lemma at_at_dec: ∀cs,i,j. Decidable (@⦃i, cs⦄ ≡ j).
+lemma at_at_dec: ∀cs,i1,i2. Decidable (@⦃i1, cs⦄ ≡ i2).
 #cs elim cs -cs [ | * #cs #IH ]
-[ /3 width=3 by at_inv_empty, or_intror/
-| * [2: #i ] * [2,4: #j ]
-  [ elim (IH i j) -IH
+[ * [2: #i1 ] * [2,4: #i2 ]
+  [4: /2 width=1 by at_empty, or_introl/
+  |*: @or_intror #H elim (at_inv_empty … H) #H1 #H2 destruct  
+  ]
+| * [2: #i1 ] * [2,4: #i2 ]
+  [ elim (IH i1 i2) -IH
     /4 width=1 by at_inv_true_succ, at_succ, or_introl, or_intror/
   | -IH /3 width=3 by at_inv_true_O_S, or_intror/
   | -IH /3 width=3 by at_inv_true_S_O, or_intror/
   | -IH /2 width=1 by or_introl, at_zero/
   ]
-| #i * [2: #j ]
-  [ elim (IH i j) -IH
+| #i1 * [2: #i2 ]
+  [ elim (IH i1 i2) -IH
     /4 width=1 by at_inv_false_S, at_false, or_introl, or_intror/
   | -IH /3 width=3 by at_inv_false_O, or_intror/
   ]
@@ -152,42 +204,40 @@ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma at_increasing: ∀cs,i,j. @⦃i, cs⦄ ≡ j → i ≤ j.
-#cs #i elim i -i //
-#i0 #IHi #j #H elim (at_monotonic … H i0) -H
+lemma at_increasing: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → i1 ≤ i2.
+#cs #i1 elim i1 -i1 //
+#j1 #IHi #i2 #H elim (at_monotonic … H j1) -H
 /3 width=3 by le_to_lt_to_lt/
 qed-.
 
-lemma at_length_lt: ∀cs,i,j. @⦃i, cs⦄ ≡ j → j < |cs|.
-#cs elim cs -cs [ | * #cs #IH ] #i #j #H normalize
-[ elim (at_inv_empty … H)
-| elim (at_inv_true … H) * -H //
-  #i0 #j0 #H1 #H2 #Hij0 destruct /3 width=2 by le_S_S/
-| elim (at_inv_false … H) -H
-  #j0 #H #H0 destruct /3 width=2 by le_S_S/
-]
+lemma at_increasing_strict: ∀cs,i1,i2. @⦃i1, Ⓕ @ cs⦄ ≡ i2 →
+                            i1 < i2 ∧ @⦃i1, cs⦄ ≡ ⫰i2.
+#cs #i1 #i2 #H elim (at_inv_false … H) -H
+#j2 #H #Hj2 destruct /4 width=2 by conj, at_increasing, le_S_S/
 qed-.
 
 (* Main properties **********************************************************)
 
-theorem at_mono: ∀cs,i,j1. @⦃i, cs⦄ ≡ j1 → ∀j2. @⦃i, cs⦄ ≡ j2 → j1 = j2.
-#cs #i #j1 #H elim H -cs -i -j1
-#cs [ |2,3: #i #j1 #_ #IH ] #j2 #H
-[ lapply (at_inv_true_zero_sn … H) -H //
-| elim (at_inv_true_succ_sn … H) -H
-  #j0 #H destruct #H >(IH … H) -cs -i -j1 //
+theorem at_mono: ∀cs,i,i1. @⦃i, cs⦄ ≡ i1 → ∀i2. @⦃i, cs⦄ ≡ i2 → i1 = i2.
+#cs #i #i1 #H elim H -cs -i -i1
+[2,3,4: #cs [2,3: #i #i1 #_ #IH ] ] #i2 #H
+[ elim (at_inv_true_succ_sn … H) -H
+  #j2 #H destruct #H >(IH … H) -cs -i -i1 //
 | elim (at_inv_false … H) -H
-  #j0 #H destruct #H >(IH … H) -cs -i -j1 //
+  #j2 #H destruct #H >(IH … H) -cs -i -i1 //
+| /2 width=2 by at_inv_true_zero_sn/
+| /2 width=1 by at_inv_empty_zero_sn/
 ]
 qed-.
 
-theorem at_inj: ∀cs,i1,j. @⦃i1, cs⦄ ≡ j → ∀i2. @⦃i2, cs⦄ ≡ j → i1 = i2.
-#cs #i1 #j #H elim H -cs -i1 -j
-#cs [ |2,3: #i1 #j #_ #IH ] #i2 #H
-[ lapply (at_inv_true_zero_dx … H) -H //
+theorem at_inj: ∀cs,i1,i. @⦃i1, cs⦄ ≡ i → ∀i2. @⦃i2, cs⦄ ≡ i → i1 = i2.
+#cs #i1 #i #H elim H -cs -i1 -i
+[2,3,4: #cs [ |2,3: #i1 #i #_ #IH ] ] #i2 #H
+[ /2 width=2 by at_inv_true_zero_dx/
 | elim (at_inv_true_succ_dx … H) -H
-  #i0 #H destruct #H >(IH … H) -cs -i1 -j //
+  #j2 #H destruct #H >(IH … H) -cs -i1 -i //
 | elim (at_inv_false … H) -H
-  #j0 #H destruct #H >(IH … H) -cs -i1 -j0 //
+  #j #H destruct #H >(IH … H) -cs -i1 -j //
+| /2 width=1 by at_inv_empty_zero_dx/
 ]
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_isid.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_isid.ma
new file mode 100644 (file)
index 0000000..0aa9a4c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_isid.ma
@@ -0,0 +1,81 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/relations/isid_1.ma".
+include "ground_2/relocation/trace_after.ma".
+
+(* RELOCATION TRACE *********************************************************)
+
+definition isid: predicate trace ≝ λcs. ∥cs∥ = |cs|.
+
+interpretation "test for identity (trace)"
+   'IsId cs = (isid cs).
+
+(* Basic properties *********************************************************)
+
+lemma isid_empty: 𝐈⦃◊⦄.
+// qed.
+
+lemma isid_true: ∀cs. 𝐈⦃cs⦄ → 𝐈⦃Ⓣ @ cs⦄.
+// qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma isid_inv_true: ∀cs. 𝐈⦃Ⓣ @ cs⦄ → 𝐈⦃cs⦄.
+/2 width=1 by injective_S/ qed-.
+
+lemma isid_inv_false: ∀cs. 𝐈⦃Ⓕ @ cs⦄ → ⊥.
+/3 width=4 by colength_le, lt_le_false/ qed-.
+
+lemma isid_inv_cons: ∀cs,b.  𝐈⦃b @ cs⦄ → 𝐈⦃cs⦄ ∧ b = Ⓣ.
+#cs * #H /3 width=1 by isid_inv_true, conj/
+elim (isid_inv_false … H)
+qed-.
+
+(* Properties on application ************************************************)
+
+lemma isid_at: ∀cs. (∀i1,i2. @⦃i1, cs⦄ ≡ i2 → i1 = i2) → 𝐈⦃cs⦄.
+#cs elim cs -cs // * /2 width=1 by/
+qed.
+
+(* Inversion lemmas on application ******************************************)
+
+lemma isid_inv_at: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → 𝐈⦃cs⦄ → i1 = i2.
+#cs #i1 #i2 #H elim H -cs -i1 -i2 /4 width=1 by isid_inv_true, eq_f/
+#cs #i1 #i2 #_ #IH #H elim (isid_inv_false … H)
+qed-.
+
+(* Properties on composition ************************************************)
+
+lemma isid_after_sn: ∀cs1,cs2. cs1 ⊚ cs2 ≡ cs2 →  𝐈⦃cs1⦄ .
+#cs1 #cs2 #H elim (after_inv_length … H) -H //
+qed.
+
+lemma isid_after_dx: ∀cs1,cs2. cs1 ⊚ cs2 ≡ cs1 →  𝐈⦃cs2⦄ .
+#cs1 #cs2 #H elim (after_inv_length … H) -H //
+qed.
+
+(* Inversion lemmas on composition ******************************************)
+
+lemma isid_inv_after_sn: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs →  𝐈⦃cs1⦄ → cs = cs2.
+#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs //
+#cs1 #cs2 #cs #_ [ #b ] #IH #H
+[ >IH -IH // | elim (isid_inv_false … H) ]
+qed-.
+
+lemma isid_inv_after_dx: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs →  𝐈⦃cs2⦄ → cs = cs1.
+#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs //
+#cs1 #cs2 #cs #_ [ #b ] #IH #H
+[ elim (isid_inv_cons … H) -H #H >IH -IH // | >IH -IH // ]
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sor.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sor.ma
index f4e79a6ce25f44ea770e2c07784f33b91c684aeb..65aba02ac4da17fa88f8b24b11aa8e701c892653 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sor.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sor.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "ground_2/notation/relations/runion_3.ma".
-include "ground_2/relocation/trace.ma".
+include "ground_2/relocation/trace_isid.ma".
 
 (* RELOCATION TRACE *********************************************************)
 
@@ -28,6 +28,35 @@ interpretation
 
 (* Basic properties *********************************************************)
 
+lemma sor_length: ∀cs1,cs2. |cs1| = |cs2| →
+                  ∃∃cs. cs2 ⋓ cs1 ≡ cs & |cs| = |cs1| & |cs| = |cs2|.
+#cs1 elim cs1 -cs1
+[ #cs2 #H >(length_inv_zero_sn … H) -H /2 width=4 by sor_empty, ex3_intro/
+| #b1 #cs1 #IH #x #H elim (length_inv_succ_sn … H) -H
+  #cs2 #b2 #H12 #H destruct elim (IH … H12) -IH -H12
+  #cs #H12 #H1 #H2 @(ex3_intro … ((b1 ∨ b2) @ cs)) /2 width=1 by sor_inh/ (**) (* explicit constructor *)
+]
+qed-.
+
 lemma sor_sym: ∀cs1,cs2,cs. cs1 ⋓ cs2 ≡ cs → cs2 ⋓ cs1 ≡ cs.
 #cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs /2 width=1 by sor_inh/
 qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma sor_inv_length: ∀cs1,cs2,cs. cs2 ⋓ cs1 ≡ cs →
+                      ∧∧ |cs1| = |cs2| & |cs| = |cs1| & |cs| = |cs2|.
+#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs /2 width=1 by and3_intro/
+#cs1 #cs2 #cs #_ #b1 #b2 * /2 width=1 by and3_intro/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma sor_fwd_isid_sn: ∀cs1,cs2,cs. cs1 ⋓ cs2 ≡ cs → 𝐈⦃cs1⦄ → 𝐈⦃cs⦄.
+#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs //
+#cs1 #cs2 #cs #_ #b1 #b2 #IH #H elim (isid_inv_cons … H) -H
+/3 width=1 by isid_true/
+qed-.
+
+lemma sor_fwd_isid_dx: ∀cs1,cs2,cs. cs1 ⋓ cs2 ≡ cs → 𝐈⦃cs2⦄ → 𝐈⦃cs⦄.
+/3 width=4 by sor_fwd_isid_sn, sor_sym/ 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 2c23eacc1b039bb93c0604e0e6a7a51723d1c1ce..f2337999239d64f51519104a734f78c9e4973c33 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
@@ -12,7 +12,7 @@ table {
    class "green"
    [ { "multiple relocation" * } {
         [ { "" * } {
-             [ "trace" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" * ]
+             [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_sor ( ? ⋓ ? ≡ ? )" * ]
              [ "mr2" "mr2_at ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" * ]
           }
         ]
@@ -33,7 +33,7 @@ table {
    [ { "extensions to the library" * } {
         [ { "" * } {
              [ "star" "lstar" "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ⫯? ) ( ⫰? )"
-               "list ( ◊ ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )" *
+               "list ( ◊ ) ( ? @ ? ) ( |?| )" "list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )" *
              ]
           }
         ]