From fb5c93c9812ea39fb78f1470da2095c80822e158 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 14 Oct 2015 19:42:43 +0000 Subject: [PATCH] colength and identity relocation --- .../contribs/lambdadelta/ground_2/lib/bool.ma | 6 + .../contribs/lambdadelta/ground_2/lib/list.ma | 41 ++-- .../lambdadelta/ground_2/lib/list2.ma | 44 ++++ .../ground_2/notation/functions/norm_1.ma | 19 ++ .../ground_2/notation/relations/isid_1.ma | 19 ++ .../lambdadelta/ground_2/relocation/mr2.ma | 2 +- .../lambdadelta/ground_2/relocation/trace.ma | 30 +++ .../ground_2/relocation/trace_after.ma | 27 ++- .../ground_2/relocation/trace_at.ma | 216 +++++++++++------- .../ground_2/relocation/trace_isid.ma | 81 +++++++ .../ground_2/relocation/trace_sor.ma | 31 ++- .../lambdadelta/ground_2/web/ground_2_src.tbl | 4 +- 12 files changed, 411 insertions(+), 109 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/lib/list2.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/functions/norm_1.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/relations/isid_1.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/trace_isid.ma diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma index d2acdb2bc..680cc4ac2 100644 --- 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 e72b54531..9e8d1ff41 100644 --- 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 index 000000000..f73099445 --- /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 index 000000000..d0f0719f1 --- /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 index 000000000..eb11c1545 --- /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 072b07f6c..3bd8fa3f9 100644 --- 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 680e89dbb..699942e05 100644 --- 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 06c914a9b..72c5d1612 100644 --- 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 f4b6f8d3a..b40b1c87b 100644 --- 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 index 000000000..0aa9a4c03 --- /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 f4e79a6ce..65aba02ac 100644 --- 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 2c23eacc1..f23379992 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 @@ -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 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )" * ] } ] -- 2.39.2