From: Ferruccio Guidi Date: Wed, 2 Mar 2016 21:32:00 +0000 (+0000) Subject: - second precommit for rtmap X-Git-Tag: make_still_working~640 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=b9526dac808d40bf89dc378cf9c5ea0c121526a4;p=helm.git - second precommit for rtmap - we park relocation by streams of booleans --- diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/rtmap_le.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/rtmap_le.etc new file mode 100644 index 000000000..6fe63a523 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/rtmap_le.etc @@ -0,0 +1,59 @@ +(**************************************************************************) +(* ___ *) +(* ||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_tl.ma". + +(* RELOCATION MAP ***********************************************************) + +inductive le (f1): predicate rtmap ≝ +| le_eq: ∀f2. f1 ≗ f2 → le f1 f2 +| le_tl: ∀f2,g2. le f1 f2 → ↓g2 = f2 → le f1 g2 +. + +interpretation "less or equal to (rtmap)" 'leq x y = (le x y). + +(* Basic properties *********************************************************) + +lemma le_refl: reflexive … le. +/2 width=1 by eq_refl, le_eq/ qed. + +lemma le_eq_repl_back_dx: ∀f1. eq_repl_back (λf2. f1 ≤ f2). +#f #f1 #Hf1 elim Hf1 -f1 +/4 width=3 by le_tl, le_eq, tl_eq_repl, eq_trans/ +qed-. + +lemma le_eq_repl_fwd_dx: ∀f1. eq_repl_fwd (λf2. f1 ≤ f2). +#f1 @eq_repl_sym /2 width=3 by le_eq_repl_back_dx/ +qed-. + +lemma le_eq_repl_back_sn: ∀f2. eq_repl_back (λf1. f1 ≤ f2). +#f #f1 #Hf1 elim Hf1 -f +/4 width=3 by le_tl, le_eq, tl_eq_repl, eq_canc_sn/ +qed-. + +lemma le_eq_repl_fwd_sn: ∀f2. eq_repl_fwd (λf1. f1 ≤ f2). +#f2 @eq_repl_sym /2 width=3 by le_eq_repl_back_sn/ +qed-. + +lemma le_tl_comp: ∀f1,f2. f1 ≤ f2 → ∀g1,g2. ↓f1 = g1 → ↓f2 = g2 → g1 ≤ g2. +#f1 #f2 #H elim H -f2 +/3 width=3 by le_tl, le_eq, tl_eq_repl/ +qed. + +(* Main properties **********************************************************) + +theorem le_trans: Transitive … le. +#f1 #f #H elim H -f +/4 width=5 by le_tl_comp, le_eq_repl_fwd_sn, le_tl/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace.etc new file mode 100644 index 000000000..699942e05 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace.etc @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||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/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/etc/relocation/trace_after.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_after.etc new file mode 100644 index 000000000..78dd6fb9a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_after.etc @@ -0,0 +1,271 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rafter_3.ma". +include "ground_2/relocation/trace_at.ma". + +(* RELOCATION TRACE *********************************************************) + +inductive after: relation3 trace trace trace ≝ + | after_empty: after (◊) (◊) (◊) + | after_true : ∀cs1,cs2,cs. after cs1 cs2 cs → + ∀b. after (Ⓣ @ cs1) (b @ cs2) (b @ cs) + | after_false: ∀cs1,cs2,cs. after cs1 cs2 cs → + after (Ⓕ @ cs1) cs2 (Ⓕ @ cs). + +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 = ◊ → + cs2 = ◊ ∧ cs = ◊. +#cs1 #cs2 #cs * -cs1 -cs2 -cs +[ /2 width=1 by conj/ +| #cs1 #cs2 #cs #_ #b #H destruct +| #cs1 #cs2 #cs #_ #H destruct +] +qed-. + +lemma after_inv_empty1: ∀cs2,cs. ◊ ⊚ cs2 ≡ cs → cs2 = ◊ ∧ cs = ◊. +/2 width=3 by after_inv_empty1_aux/ qed-. + +fact after_inv_true1_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl1. cs1 = Ⓣ @ tl1 → + ∃∃tl2,tl,b. cs2 = b @ tl2 & cs = b @ tl & tl1 ⊚ tl2 ≡ tl. +#cs1 #cs2 #cs * -cs1 -cs2 -cs +[ #tl1 #H destruct +| #cs1 #cs2 #cs #H12 #b #tl1 #H destruct + /2 width=6 by ex3_3_intro/ +| #cs1 #cs2 #cs #_ #tl1 #H destruct +] +qed-. + +lemma after_inv_true1: ∀tl1,cs2,cs. (Ⓣ @ tl1) ⊚ cs2 ≡ cs → + ∃∃tl2,tl,b. cs2 = b @ tl2 & cs = b @ tl & tl1 ⊚ tl2 ≡ tl. +/2 width=3 by after_inv_true1_aux/ qed-. + +fact after_inv_false1_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl1. cs1 = Ⓕ @ tl1 → + ∃∃tl. cs = Ⓕ @ tl & tl1 ⊚ cs2 ≡ tl. +#cs1 #cs2 #cs * -cs1 -cs2 -cs +[ #tl1 #H destruct +| #cs1 #cs2 #cs #_ #b #tl1 #H destruct +| #cs1 #cs2 #cs #H12 #tl1 #H destruct + /2 width=3 by ex2_intro/ +] +qed-. + +lemma after_inv_false1: ∀tl1,cs2,cs. (Ⓕ @ tl1) ⊚ cs2 ≡ cs → + ∃∃tl. cs = Ⓕ @ tl & tl1 ⊚ cs2 ≡ tl. +/2 width=3 by after_inv_false1_aux/ qed-. + +fact after_inv_empty3_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → cs = ◊ → + cs1 = ◊ ∧ cs2 = ◊. +#cs1 #cs2 #cs * -cs1 -cs2 -cs +[ /2 width=1 by conj/ +| #cs1 #cs2 #cs #_ #b #H destruct +| #cs1 #cs2 #cs #_ #H destruct +] +qed-. + +lemma after_inv_empty3: ∀cs1,cs2. cs1 ⊚ cs2 ≡ ◊ → cs1 = ◊ ∧ cs2 = ◊. +/2 width=3 by after_inv_empty3_aux/ qed-. + +fact after_inv_inh3_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl,b. cs = b @ tl → + (∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = b @ tl2 & tl1 ⊚ tl2 ≡ tl) ∨ + ∃∃tl1. cs1 = Ⓕ @ tl1 & b = Ⓕ & tl1 ⊚ cs2 ≡ tl. +#cs1 #cs2 #cs * -cs1 -cs2 -cs +[ #tl #b #H destruct +| #cs1 #cs2 #cs #H12 #b0 #tl #b #H destruct + /3 width=5 by ex3_2_intro, or_introl/ +| #cs1 #cs2 #cs #H12 #tl #b #H destruct + /3 width=3 by ex3_intro, or_intror/ +] +qed-. + +lemma after_inv_inh3: ∀cs1,cs2,tl,b. cs1 ⊚ cs2 ≡ b @ tl → + (∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = b @ tl2 & tl1 ⊚ tl2 ≡ tl) ∨ + ∃∃tl1. cs1 = Ⓕ @ tl1 & b = Ⓕ & tl1 ⊚ cs2 ≡ tl. +/2 width=3 by after_inv_inh3_aux/ qed-. + +lemma after_inv_true3: ∀cs1,cs2,tl. cs1 ⊚ cs2 ≡ Ⓣ @ tl → + ∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = Ⓣ @ tl2 & tl1 ⊚ tl2 ≡ tl. +#cs1 #cs2 #tl #H elim (after_inv_inh3 … H) -H // * +#tl1 #_ #H destruct +qed-. + +lemma after_inv_false3: ∀cs1,cs2,tl. cs1 ⊚ cs2 ≡ Ⓕ @ tl → + (∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = Ⓕ @ tl2 & tl1 ⊚ tl2 ≡ tl) ∨ + ∃∃tl1. cs1 = Ⓕ @ tl1 & tl1 ⊚ cs2 ≡ tl. +#cs1 #cs2 #tl #H elim (after_inv_inh3 … H) -H /2 width=1 by or_introl/ * /3 width=3 by ex2_intro, or_intror/ +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) -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/ + | #j1 #j #H1 #H2 #Hj1 destruct + elim (IH … Hj1) -IH -Hj1 /3 width=3 by at_succ, ex2_intro/ + ] + | elim (at_inv_false … H) -H + #j #H #Hj destruct + elim (IH … Hj) -IH -Hj /3 width=3 by at_succ, at_false, ex2_intro/ + ] +| #cs1 #cs2 #cs #_ #IH #i1 #i #H elim (at_inv_false … H) -H + #j #H #Hj destruct + elim (IH … Hj) -IH -Hj /3 width=3 by at_false, ex2_intro/ +] +qed-. + +lemma after_at1_fwd: ∀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) -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/ + | #j1 #j2 #H1 #H2 #Hj12 destruct + elim (IH … Hj12) -IH -Hj12 /3 width=3 by at_succ, ex2_intro/ + ] + | elim (at_inv_false … H) -H + #j2 #H #Hj2 destruct + elim (IH … Hj2) -IH -Hj2 /3 width=3 by at_succ, at_false, ex2_intro/ + ] +| #cs1 #cs2 #cs #_ #IH #i1 #i2 #H elim (IH … H) -IH -H + /3 width=3 by at_false, ex2_intro/ +] +qed-. + +lemma after_fwd_at: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → + ∀i1,i2,i. @⦃i1, cs1⦄ ≡ i2 → @⦃i2, cs2⦄ ≡ i → @⦃i1, cs⦄ ≡ i. +#cs1 #cs2 #cs #Hcs #i1 #i2 #i #Hi1 #Hi2 elim (after_at1_fwd … Hcs … Hi1) -cs1 +#j #H #Hj >(at_mono … Hi2 … H) -i2 // +qed-. + +lemma after_fwd_at1: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → + ∀i1,i2,i. @⦃i1, cs⦄ ≡ i → @⦃i2, cs2⦄ ≡ i → @⦃i1, cs1⦄ ≡ i2. +#cs1 #cs2 #cs #Hcs #i1 #i2 #i #Hi1 #Hi2 elim (after_at_fwd … Hcs … Hi1) -cs +#j1 #Hij1 #H >(at_inj … Hi2 … H) -i // +qed-. + +lemma after_fwd_at2: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → + ∀i1,i2,i. @⦃i1, cs⦄ ≡ i → @⦃i1, cs1⦄ ≡ i2 → @⦃i2, cs2⦄ ≡ i. +#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs +[ #i1 #i2 #i #Hi #Hi1 elim (at_inv_empty … Hi1) -Hi1 // +| #cs1 #cs2 #cs #_ * #IH #i1 #i2 #i #Hi #Hi1 + [ elim (at_inv_true … Hi1) -Hi1 * + [ -IH #H1 #H2 destruct >(at_inv_true_zero_sn … Hi) -i // + | #j1 #j2 #H1 #H2 #Hj12 destruct elim (at_inv_true_succ_sn … Hi) -Hi + #j #H #Hj1 destruct /3 width=3 by at_succ/ + ] + | elim (at_inv_false … Hi1) -Hi1 + #j2 #H #Hj2 destruct elim (at_inv_false … Hi) -Hi + #j #H #Hj destruct /3 width=3 by at_succ/ + ] +| #cs1 #cs2 #cs #_ #IH #i1 #i2 #i #Hi #Hi2 elim (at_inv_false … Hi) -Hi + #j #H #Hj destruct /3 width=3 by at_false/ +] +qed-. + +(* Main properties **********************************************************) + +theorem after_trans1: ∀cs1,cs2,cs0. cs1 ⊚ cs2 ≡ cs0 → + ∀cs3, cs4. cs0 ⊚ cs3 ≡ cs4 → + ∃∃cs. cs2 ⊚ cs3 ≡ cs & cs1 ⊚ cs ≡ cs4. +#cs1 #cs2 #cs0 #H elim H -cs1 -cs2 -cs0 +[ #cs3 #cs4 #H elim (after_inv_empty1 … H) -H + #H1 #H2 destruct /2 width=3 by ex2_intro, after_empty/ +| #cs1 #cs2 #cs0 #_ * #IH #cs3 #cs4 #H + [ elim (after_inv_true1 … H) -H + #tl3 #tl4 #b #H1 #H2 #Htl destruct + elim (IH … Htl) -cs0 + /3 width=3 by ex2_intro, after_true/ + | elim (after_inv_false1 … H) -H + #tl4 #H #Htl destruct + elim (IH … Htl) -cs0 + /3 width=3 by ex2_intro, after_true, after_false/ + ] +| #cs1 #cs2 #cs0 #_ #IH #cs3 #cs4 #H + elim (after_inv_false1 … H) -H + #tl4 #H #Htl destruct + elim (IH … Htl) -cs0 + /3 width=3 by ex2_intro, after_false/ +] +qed-. + +theorem after_trans2: ∀cs1,cs0,cs4. cs1 ⊚ cs0 ≡ cs4 → + ∀cs2, cs3. cs2 ⊚ cs3 ≡ cs0 → + ∃∃cs. cs1 ⊚ cs2 ≡ cs & cs ⊚ cs3 ≡ cs4. +#cs1 #cs0 #cs4 #H elim H -cs1 -cs0 -cs4 +[ #cs2 #cs3 #H elim (after_inv_empty3 … H) -H + #H1 #H2 destruct /2 width=3 by ex2_intro, after_empty/ +| #cs1 #cs0 #cs4 #_ #b #IH #cs2 #cs3 #H elim (after_inv_inh3 … H) -H * + [ #tl2 #tl3 #H1 #H2 #Htl destruct + elim (IH … Htl) -cs0 + /3 width=3 by ex2_intro, after_true/ + | #tl2 #H1 #H2 #Htl destruct + elim (IH … Htl) -cs0 + /3 width=3 by ex2_intro, after_true, after_false/ + ] +| #cs1 #cs0 #cs4 #_ #IH #cs2 #cs3 #H elim (IH … H) -cs0 + /3 width=3 by ex2_intro, after_false/ +] +qed-. + +theorem after_mono: ∀cs1,cs2,x. cs1 ⊚ cs2 ≡ x → ∀y. cs1 ⊚ cs2 ≡ y → x = y. +#cs1 #cs2 #x #H elim H -cs1 -cs2 -x +[ #y #H elim (after_inv_empty1 … H) -H // +| #cs1 #cs #x #_ #b #IH #y #H elim (after_inv_true1 … H) -H + #tl #tly #b0 #H1 #H2 #Htl destruct >(IH … Htl) -tl -cs1 -x // +| #cs1 #cs2 #x #_ #IH #y #H elim (after_inv_false1 … H) -H + #tly #H #Htl destruct >(IH … Htl) -cs1 -cs2 -x // +] +qed-. + +theorem after_inj: ∀cs1,x,cs. cs1 ⊚ x ≡ cs → ∀y. cs1 ⊚ y ≡ cs → x = y. +#cs1 #x #cs #H elim H -cs1 -x -cs +[ #y #H elim (after_inv_empty1 … H) -H // +| #cs1 #x #cs #_ #b #IH #y #H elim (after_inv_true1 … H) -H + #tly #tl #b0 #H1 #H2 #Htl destruct >(IH … Htl) -tl -cs1 -x // +| #cs1 #x #cs #_ #IH #y #H elim (after_inv_false1 … H) -H + #tl #H #Htl destruct >(IH … Htl) -tl -cs1 -x // +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_at.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_at.etc new file mode 100644 index 000000000..02d8ac1eb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_at.etc @@ -0,0 +1,264 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rat_3.ma". +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,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,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: ∀i1,i2. @⦃i1, ◊⦄ ≡ i2 → i1 = 0 ∧ i2 = 0. +/2 width=5 by at_inv_empty_aux/ qed-. + +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,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,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 * // +#j1 #j2 #_ #H destruct +qed-. + +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 +| #j1 #j2 #H1 #H2 destruct /2 width=3 by ex2_intro/ +] +qed-. + +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 +| #j1 #j2 #H1 #H2 destruct /2 width=3 by ex2_intro/ +] +qed-. + +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 +| #j1 #j2 #H1 #H2 destruct // +] +qed-. + +lemma at_inv_true_O_S: ∀cs,i. @⦃0, Ⓣ @ cs⦄ ≡ ⫯i → ⊥. +#cs #i #H elim (at_inv_true … H) -H * +[ #_ #H 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 +| #j1 #j2 #_ #H destruct +] +qed-. + +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,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,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 +#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 *********************************************************) + +(* 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_dec: ∀cs,i1,i2. Decidable (@⦃i1, cs⦄ ≡ i2). +#cs elim cs -cs [ | * #cs #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/ + ] +| #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/ + ] +] +qed-. + +lemma is_at_dec: ∀cs,i2. Decidable (∃i1. @⦃i1, cs⦄ ≡ i2). +#cs elim cs -cs +[ * /3 width=2 by ex_intro, or_introl/ + #i2 @or_intror * /2 width=3 by at_inv_empty_succ_dx/ +| * #cs #IH * [2,4: #i2 ] + [ elim (IH i2) -IH + [ * /4 width=2 by at_succ, ex_intro, or_introl/ + | #H @or_intror * #x #Hx + elim (at_inv_true_succ_dx … Hx) -Hx + /3 width=2 by ex_intro/ + ] + | elim (IH i2) -IH + [ * /4 width=2 by at_false, ex_intro, or_introl/ + | #H @or_intror * /4 width=2 by at_inv_false_S, ex_intro/ + ] + | /3 width=2 by at_zero, ex_intro, or_introl/ + | @or_intror * /2 width=3 by at_inv_false_O/ + ] +] +qed-. + +(* Basic forward lemmas *****************************************************) + +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_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,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 + #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,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 + #j2 #H destruct #H >(IH … H) -cs -i1 -i // +| elim (at_inv_false … H) -H + #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/etc/relocation/trace_isid.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_isid.etc new file mode 100644 index 000000000..6dce9e0a2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_isid.etc @@ -0,0 +1,114 @@ +(**************************************************************************) +(* ___ *) +(* ||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/isidentity_1.ma". +include "ground_2/relocation/trace_after.ma". +include "ground_2/relocation/trace_sle.ma". + +(* RELOCATION TRACE *********************************************************) + +definition isid: predicate trace ≝ λcs. ∥cs∥ = |cs|. + +interpretation "test for identity (trace)" + 'IsIdentity cs = (isid cs). + +definition t_reflexive: ∀S:Type[0]. predicate (trace → relation S) ≝ + λS,R. ∀a. ∃∃t. 𝐈⦃t⦄ & R t a a. + +(* 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: ∀cs2. ∃∃cs1. 𝐈⦃cs1⦄ & cs1 ⊚ cs2 ≡ cs2. +#cs2 elim cs2 -cs2 /2 width=3 by after_empty, ex2_intro/ +#b #cs2 * /3 width=3 by isid_true, after_true, ex2_intro/ +qed-. + +lemma isid_after_dx: ∀cs1. ∃∃cs2. 𝐈⦃cs2⦄ & cs1 ⊚ cs2 ≡ cs1. +#cs1 elim cs1 -cs1 /2 width=3 by after_empty, ex2_intro/ +* #cs1 * /3 width=3 by isid_true, after_true, after_false, ex2_intro/ +qed-. + +lemma after_isid_sn: ∀cs1,cs2. cs1 ⊚ cs2 ≡ cs2 → 𝐈⦃cs1⦄ . +#cs1 #cs2 #H elim (after_inv_length … H) -H // +qed. + +lemma after_isid_dx: ∀cs1,cs2. cs1 ⊚ cs2 ≡ cs1 → 𝐈⦃cs2⦄ . +#cs1 #cs2 #H elim (after_inv_length … H) -H // +qed. + +(* Inversion lemmas on composition ******************************************) + +lemma after_isid_inv_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 after_isid_inv_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-. + +lemma after_inv_isid3: ∀t1,t2,t. t1 ⊚ t2 ≡ t → 𝐈⦃t⦄ → 𝐈⦃t1⦄ ∧ 𝐈⦃t2⦄. +#t1 #t2 #t #H elim H -t1 -t2 -t +[ /2 width=1 by conj/ +| #t1 #t2 #t #_ #b #IHt #H elim (isid_inv_cons … H) -H + #Ht #H elim (IHt Ht) -t /2 width=1 by isid_true, conj/ +| #t1 #t2 #t #_ #_ #H elim (isid_inv_false … H) +] +qed-. + +(* Forward on inclusion *****************************************************) + +lemma sle_isid1_fwd: ∀t1,t2. t1 ⊆ t2 → 𝐈⦃t1⦄ → t1 = t2. +#t1 #t2 #H elim H -t1 -t2 // +[ #t1 #t2 #_ #IH #H lapply (isid_inv_true … H) -H + #HT1 @eq_f2 // @IH @HT1 (**) (* full auto fails *) +| #t1 #t2 #b #_ #_ #H elim (isid_inv_false … H) +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_isun.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_isun.etc new file mode 100644 index 000000000..bdcb249c5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_isun.etc @@ -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/notation/relations/isuniform_1.ma". +include "ground_2/relocation/trace_isid.ma". + +(* RELOCATION TRACE *********************************************************) + +inductive isun: predicate trace ≝ +| isun_id : ∀t. 𝐈⦃t⦄ → isun t +| isun_false: ∀t. isun t → isun (Ⓕ@t) +. + +interpretation "test for uniformity (trace)" + 'IsUniform t = (isun t). + +(* Basic inversion lennas ***************************************************) + +fact isun_inv_true_aux: ∀t. 𝐔⦃t⦄ → ∀u. t = Ⓣ@u → 𝐈⦃u⦄. +#t * -t +[ #t #Ht #u #H destruct /2 width=1 by isid_inv_true/ +| #t #_ #u #H destruct +] +qed-. + +lemma isun_inv_true: ∀t. 𝐔⦃Ⓣ@t⦄ → 𝐈⦃t⦄. +/2 width=3 by isun_inv_true_aux/ qed-. + +fact isun_inv_false_aux: ∀t. 𝐔⦃t⦄ → ∀u. t = Ⓕ@u → 𝐔⦃u⦄. +#t * -t +[ #t #Ht #u #H destruct elim (isid_inv_false … Ht) +| #t #Ht #u #H destruct // +] +qed-. + +lemma isun_inv_false: ∀t. 𝐔⦃Ⓕ@t⦄ → 𝐔⦃t⦄. +/2 width=3 by isun_inv_false_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_sle.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_sle.etc new file mode 100644 index 000000000..be738b18e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_sle.etc @@ -0,0 +1,60 @@ +(**************************************************************************) +(* ___ *) +(* ||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/trace_at.ma". + +(* RELOCATION TRACE *********************************************************) + +inductive sle: relation trace ≝ +| sle_empty: sle (◊) (◊) +| sle_true : ∀t1,t2. sle t1 t2 → sle (Ⓣ @ t1) (Ⓣ @ t2) +| sle_false: ∀t1,t2,b. sle t1 t2 → sle (Ⓕ @ t1) (b @ t2) +. + +interpretation + "inclusion (trace)" + 'subseteq t1 t2 = (sle t1 t2). + +(* Basic properties *********************************************************) + +(* Basic forward lemmas *****************************************************) + +lemma sle_fwd_length: ∀t1,t2. t1 ⊆ t2 → |t1| = |t2|. +#t1 #t2 #H elim H -t1 -t2 // +qed-. + +lemma sle_fwd_colength: ∀t1,t2. t1 ⊆ t2 → ∥t1∥ ≤ ∥t2∥. +#t1 #t2 #H elim H -t1 -t2 /2 width=1 by le_S_S/ +#t1 #t2 * /2 width=1 by le_S/ +qed-. + +(* Inversion lemmas on application ******************************************) + +lemma sle_inv_at: ∀t1,t2. t1 ⊆ t2 → + ∀i,i1,i2. @⦃i, t1⦄ ≡ i1 → @⦃i, t2⦄ ≡ i2 → i2 ≤ i1. +#t1 #t2 #H elim H -t1 -t2 +[ #i #i1 #i2 #_ #H2 elim (at_inv_empty … H2) -H2 // +| #t1 #t2 #_ #IH #i #i1 #i2 #H0 #H2 elim (at_inv_true … H2) -H2 * // + #j1 #j2 #H1 #H2 #Hj destruct elim (at_inv_true_succ_sn … H0) -H0 + /3 width=3 by le_S_S/ +| #t1 #t2 * #_ #IH #i #i1 #i2 #H0 #H2 + [ elim (at_inv_true … H2) -H2 * // + #j #j2 #H1 #H2 #Hj2 destruct elim (at_inv_false … H0) -H0 + #j1 #H #Hj1 destruct elim (at_monotonic … Hj1 j) -Hj1 // + #x #H1x #H2x @le_S_S /4 width=3 by lt_to_le, le_to_lt_to_lt/ (**) (* full auto too slow *) + | elim (at_inv_false … H2) elim (at_inv_false … H0) -H0 -H2 + /3 width=3 by le_S_S/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_snot.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_snot.etc new file mode 100644 index 000000000..d1697b9cc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_snot.etc @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||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/complement_1.ma". +include "ground_2/relocation/trace.ma". + +(* RELOCATION TRACE *********************************************************) + +let rec snot (t:trace) on t ≝ match t with +[ nil ⇒ ◊ +| cons b t ⇒ (¬ b) @ snot t +]. + +interpretation + "complement (trace)" + 'Complement t = (snot t). + +(* Basic properties *********************************************************) + +lemma snot_empty: ∁ (◊) = ◊. +// qed. + +lemma snot_inh: ∀t,b. ∁ (b@t) = (¬ b) @ ∁ t. +// qed. + +lemma snot_true: ∀t. ∁ (Ⓣ @ t) = Ⓕ @ ∁ t. +// qed. + +lemma snot_false: ∀t. ∁ (Ⓕ @ t) = Ⓣ @ ∁ t. +// qed. + +lemma snot_length: ∀t. |∁ t| = |t|. +#t elim t -t normalize // +qed. + +lemma snot_colength: ∀t. ∥∁ t∥ = |t| - ∥t∥. +#t elim t -t // +* /2 width=1 by minus_Sn_m/ +qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_sor.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_sor.etc new file mode 100644 index 000000000..65aba02ac --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/relocation/trace_sor.etc @@ -0,0 +1,62 @@ +(**************************************************************************) +(* ___ *) +(* ||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/runion_3.ma". +include "ground_2/relocation/trace_isid.ma". + +(* RELOCATION TRACE *********************************************************) + +inductive sor: relation3 trace trace trace ≝ + | sor_empty: sor (◊) (◊) (◊) + | sor_inh : ∀cs1,cs2,cs. sor cs1 cs2 cs → + ∀b1,b2. sor (b1 @ cs1) (b2 @ cs2) ((b1 ∨ b2) @ cs). + +interpretation + "union (trace)" + 'RUnion L1 L2 L = (sor L2 L1 L). + +(* 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/notation/functions/drop_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/drop_1.ma new file mode 100644 index 000000000..1cc9141bb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/drop_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 T )" + non associative with precedence 46 + for @{ 'Drop $T }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma index 7ba0d13eb..aaa1ba9b6 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma @@ -12,9 +12,79 @@ (* *) (**************************************************************************) +include "ground_2/notation/functions/lift_1.ma". include "ground_2/lib/arith.ma". include "ground_2/lib/streams.ma". (* RELOCATION N-STREAM ******************************************************) definition rtmap: Type[0] ≝ stream nat. + +definition push: rtmap → rtmap ≝ λf. 0@f. + +interpretation "push (nstream)" 'Lift f = (push f). + +definition next: rtmap → rtmap. +* #n #f @(⫯n@f) +qed. + +interpretation "next (nstream)" 'Successor f = (next f). + +(* Basic properties *********************************************************) + +lemma push_rew: ∀f. 0@f = ↑f. +// qed. + +lemma next_rew: ∀f,n. (⫯n)@f = ⫯(n@f). +// qed. + +(* Basic inversion lemmas ***************************************************) + +lemma injective_push: injective ? ? push. +#f1 #f2 normalize #H destruct // +qed-. + +lemma discr_push_next: ∀f1,f2. ↑f1 = ⫯f2 → ⊥. +#f1 * #n2 #f2 normalize #H destruct +qed-. + +lemma discr_next_push: ∀f1,f2. ⫯f1 = ↑f2 → ⊥. +* #n1 #f1 #f2 normalize #H destruct +qed-. + +lemma injective_next: injective ? ? next. +* #n1 #f1 * #n2 #f2 normalize #H destruct // +qed-. + +lemma push_inv_seq_sn: ∀f,g,n. n@g = ↑f → 0 = n ∧ g = f. +#f #g #n (injective_push … Hx1) >(injective_push … Hx2) -x2 -x1 + /2 width=3 by ex2_intro/ +| #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct + elim (discr_push_next … Hx2) +| #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct + elim (discr_push_next … Hx1) +] +qed-. + +lemma after_inv_pnx: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → + ∃∃f. f1 ⊚ f2 ≡ f & ⫯f = g. +#g1 #g2 #g * -g1 -g2 -g #f1 #f2 #f #g1 +[ #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct + elim (discr_next_push … Hx2) +| #g2 #g #Hf #H1 #H2 #H3 #x1 #x2 #Hx1 #Hx2 destruct + >(injective_push … Hx1) >(injective_next … Hx2) -x2 -x1 + /2 width=3 by ex2_intro/ +| #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct + elim (discr_push_next … Hx1) +] +qed-. + +lemma after_inv_nxx: ∀g1,f2,g. g1 ⊚ f2 ≡ g → ∀f1. ⫯f1 = g1 → + ∃∃f. f1 ⊚ f2 ≡ f & ⫯f = g. +#g1 #f2 #g * -g1 -f2 -g #f1 #f2 #f #g1 +[ #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct + elim (discr_next_push … Hx1) +| #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct + elim (discr_next_push … Hx1) +| #g #Hf #H1 #H #x1 #Hx1 destruct + >(injective_next … Hx1) -x1 + /2 width=3 by ex2_intro/ +] +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma after_inv_ppp: ∀g1,g2,g. g1 ⊚ g2 ≡ g → + ∀f1,f2,f. ↑f1 = g1 → ↑f2 = g2 → ↑f = g → f1 ⊚ f2 ≡ f. +#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_ppx … Hg … H1 H2) -g1 -g2 +#x #Hf #Hx destruct <(injective_push … Hx) -f // +qed-. + +lemma after_inv_ppn: ∀g1,g2,g. g1 ⊚ g2 ≡ g → + ∀f1,f2,f. ↑f1 = g1 → ↑f2 = g2 → ⫯f = g → ⊥. +#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_ppx … Hg … H1 H2) -g1 -g2 +#x #Hf #Hx destruct elim (discr_push_next … Hx) +qed-. + +lemma after_inv_pnn: ∀g1,g2,g. g1 ⊚ g2 ≡ g → + ∀f1,f2,f. ↑f1 = g1 → ⫯f2 = g2 → ⫯f = g → f1 ⊚ f2 ≡ f. +#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_pnx … Hg … H1 H2) -g1 -g2 +#x #Hf #Hx destruct <(injective_next … Hx) -f // +qed-. + +lemma after_inv_pnp: ∀g1,g2,g. g1 ⊚ g2 ≡ g → + ∀f1,f2,f. ↑f1 = g1 → ⫯f2 = g2 → ↑f = g → ⊥. +#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_pnx … Hg … H1 H2) -g1 -g2 +#x #Hf #Hx destruct elim (discr_next_push … Hx) +qed-. + +lemma after_inv_nxn: ∀g1,f2,g. g1 ⊚ f2 ≡ g → + ∀f1,f. ⫯f1 = g1 → ⫯f = g → f1 ⊚ f2 ≡ f. +#g1 #f2 #g #Hg #f1 #f #H1 #H elim (after_inv_nxx … Hg … H1) -g1 +#x #Hf #Hx destruct <(injective_next … Hx) -f // +qed-. + +lemma after_inv_nxp: ∀g1,f2,g. g1 ⊚ f2 ≡ g → + ∀f1,f. ⫯f1 = g1 → ↑f = g → ⊥. +#g1 #f2 #g #Hg #f1 #f #H1 #H elim (after_inv_nxx … Hg … H1) -g1 +#x #Hf #Hx destruct elim (discr_next_push … Hx) +qed-. + +lemma after_inv_pxp: ∀g1,g2,g. g1 ⊚ g2 ≡ g → + ∀f1,f. ↑f1 = g1 → ↑f = g → + ∃∃f2. f1 ⊚ f2 ≡ f & ↑f2 = g2. +#g1 * * [2: #m2] #g2 #g #Hg #f1 #f #H1 #H +[ elim (after_inv_pnp … Hg … H1 … H) -g1 -g -f1 -f // +| lapply (after_inv_ppp … Hg … H1 … H) -g1 -g /2 width=3 by ex2_intro/ +] +qed-. + +lemma after_inv_pxn: ∀g1,g2,g. g1 ⊚ g2 ≡ g → + ∀f1,f. ↑f1 = g1 → ⫯f = g → + ∃∃f2. f1 ⊚ f2 ≡ f & ⫯f2 = g2. +#g1 * * [2: #m2] #g2 #g #Hg #f1 #f #H1 #H +[ lapply (after_inv_pnn … Hg … H1 … H) -g1 -g /2 width=3 by ex2_intro/ +| elim (after_inv_ppn … Hg … H1 … H) -g1 -g -f1 -f // +] +qed-. + +lemma after_inv_xxp: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f. ↑f = g → + ∃∃f1,f2. f1 ⊚ f2 ≡ f & ↑f1 = g1 & ↑f2 = g2. +* * [2: #m1 ] #g1 #g2 #g #Hg #f #H +[ elim (after_inv_nxp … Hg … H) -g2 -g -f // +| elim (after_inv_pxp … Hg … H) -g /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma after_inv_xxn: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f. ⫯f = g → + (∃∃f1,f2. f1 ⊚ f2 ≡ f & ↑f1 = g1 & ⫯f2 = g2) ∨ + ∃∃f1. f1 ⊚ g2 ≡ f & ⫯f1 = g1. +* * [2: #m1 ] #g1 #g2 #g #Hg #f #H +[ /4 width=5 by after_inv_nxn, or_intror, ex2_intro/ +| elim (after_inv_pxn … Hg … H) -g + /3 width=5 by or_introl, ex3_2_intro/ +] +qed-. + +lemma after_inv_pxx: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1. ↑f1 = g1 → + (∃∃f2,f. f1 ⊚ f2 ≡ f & ↑f2 = g2 & ↑f = g) ∨ + (∃∃f2,f. f1 ⊚ f2 ≡ f & ⫯f2 = g2 & ⫯f = g). +#g1 * * [2: #m2 ] #g2 #g #Hg #f1 #H +[ elim (after_inv_pnx … Hg … H) -g1 + /3 width=5 by or_intror, ex3_2_intro/ +| elim (after_inv_ppx … Hg … H) -g1 + /3 width=5 by or_introl, ex3_2_intro/ +] +qed-. + +(* Main properties **********************************************************) + +let corec after_trans1: ∀f0,f3,f4. f0 ⊚ f3 ≡ f4 → + ∀f1,f2. f1 ⊚ f2 ≡ f0 → + ∀f. f2 ⊚ f3 ≡ f → f1 ⊚ f ≡ f4 ≝ ?. +#f0 #f3 #f4 * -f0 -f3 -f4 #f0 #f3 #f4 #g0 [1,2: #g3 ] #g4 +[ #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg + cases (after_inv_xxp … Hg0 … H0) -g0 + #f1 #f2 #Hf0 #H1 #H2 + cases (after_inv_ppx … Hg … H2 H3) -g2 -g3 + #f #Hf #H /3 width=7 by after_refl/ +| #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg + cases (after_inv_xxp … Hg0 … H0) -g0 + #f1 #f2 #Hf0 #H1 #H2 + cases (after_inv_pnx … Hg … H2 H3) -g2 -g3 + #f #Hf #H /3 width=7 by after_push/ +| #Hf4 #H0 #H4 #g1 #g2 #Hg0 #g #Hg + cases (after_inv_xxn … Hg0 … H0) -g0 * + [ #f1 #f2 #Hf0 #H1 #H2 + cases (after_inv_nxx … Hg … H2) -g2 + #f #Hf #H /3 width=7 by after_push/ + | #f1 #Hf0 #H1 /3 width=6 by after_next/ + ] +] +qed-. + +let corec after_trans2: ∀f1,f0,f4. f1 ⊚ f0 ≡ f4 → + ∀f2, f3. f2 ⊚ f3 ≡ f0 → + ∀f. f1 ⊚ f2 ≡ f → f ⊚ f3 ≡ f4 ≝ ?. +#f1 #f0 #f4 * -f1 -f0 -f4 #f1 #f0 #f4 #g1 [1,2: #g0 ] #g4 +[ #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg + cases (after_inv_xxp … Hg0 … H0) -g0 + #f2 #f3 #Hf0 #H2 #H3 + cases (after_inv_ppx … Hg … H1 H2) -g1 -g2 + #f #Hf #H /3 width=7 by after_refl/ +| #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg + cases (after_inv_xxn … Hg0 … H0) -g0 * + [ #f2 #f3 #Hf0 #H2 #H3 + cases (after_inv_ppx … Hg … H1 H2) -g1 -g2 + #f #Hf #H /3 width=7 by after_push/ + | #f2 #Hf0 #H2 + cases (after_inv_pnx … Hg … H1 H2) -g1 -g2 + #f #Hf #H /3 width=6 by after_next/ + ] +| #Hf4 #H1 #H4 #f2 #f3 #Hf0 #g #Hg + cases (after_inv_nxx … Hg … H1) -g1 + #f #Hg #H /3 width=6 by after_next/ +] +qed-. + +(* Main inversion lemmas on after *******************************************) + +let corec after_mono: ∀f1,f2,x,y. f1 ⊚ f2 ≡ x → f1 ⊚ f2 ≡ y → x ≗ y ≝ ?. +#f1 #f2 #x #y * -f1 -f2 -x +#f1 #f2 #x #g1 [1,2: #g2 ] #g #Hx #H1 [1,2: #H2 ] #H0x #Hy +[ cases (after_inv_ppx … Hy … H1 H2) -g1 -g2 /3 width=8 by eq_push/ +| cases (after_inv_pnx … Hy … H1 H2) -g1 -g2 /3 width=8 by eq_next/ +| cases (after_inv_nxx … Hy … H1) -g1 /3 width=8 by eq_next/ +] +qed-. + +(* Properties on minus ******************************************************) + +lemma after_minus: ∀n,f1,f2,f. @⦃0, f1⦄ ≡ n → + f1 ⊚ f2 ≡ f → f1-n ⊚ f2 ≡ f-n. +#n elim n -n // +#n #IH #f1 #f2 #f #Hf1 #Hf cases (at_inv_pxn … Hf1) -Hf1 [ |*: // ] +#g1 #Hg1 #H1 cases (after_inv_nxx … Hf … H1) -Hf /2 width=1 by/ +qed. + +(* Inversion lemmas on isid *************************************************) + +let corec isid_after_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ⊚ f2 ≡ f2 ≝ ?. +#f1 * -f1 #f1 #g1 #Hf1 #H1 #f2 cases (pn_split f2) * #g2 #H2 +/3 width=7 by after_push, after_refl/ +qed-. + +let corec isid_after_dx: ∀f2. 𝐈⦃f2⦄ → ∀f1. f1 ⊚ f2 ≡ f1 ≝ ?. +#f2 * -f2 #f2 #g2 #Hf2 #H2 #f1 cases (pn_split f1) * #g1 #H1 +[ /3 width=7 by after_refl/ +| @(after_next … H1 H1) /3 width=3 by isid_push/ +] +qed-. + +lemma after_isid_inv_sn: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f1⦄ → f2 ≗ f. +/3 width=6 by isid_after_sn, after_mono/ +qed-. + +lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f2⦄ → f1 ≗ f. +/3 width=6 by isid_after_dx, after_mono/ +qed-. + +let corec after_fwd_isid1: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄ ≝ ?. +#f1 #f2 #f * -f1 -f2 -f +#f1 #f2 #f #g1 [1,2: #g2 ] #g #Hf #H1 [1,2: #H2 ] #H0 #H +[ /4 width=6 by isid_inv_push, isid_push/ ] +cases (isid_inv_next … H … H0) +qed-. + +let corec after_fwd_isid2: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f2⦄ ≝ ?. +#f1 #f2 #f * -f1 -f2 -f +#f1 #f2 #f #g1 [1,2: #g2 ] #g #Hf #H1 [1,2: #H2 ] #H0 #H +[ /4 width=6 by isid_inv_push, isid_push/ ] +cases (isid_inv_next … H … H0) +qed-. + +lemma after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄ ∧ 𝐈⦃f2⦄. +/3 width=4 by after_fwd_isid2, after_fwd_isid1, conj/ qed-. + +(* Forward lemmas on at *****************************************************) + +lemma after_at_fwd: ∀i,i1,f. @⦃i1, f⦄ ≡ i → ∀f2,f1. f2 ⊚ f1 ≡ f → + ∃∃i2. @⦃i1, f1⦄ ≡ i2 & @⦃i2, f2⦄ ≡ i. +#i elim i -i [2: #i #IH ] #i1 #f #Hf #f2 #f1 #Hf21 +[ elim (at_inv_xxn … Hf) -Hf [1,3:* |*: // ] + [1: #g #j1 #Hg #H0 #H |2,4: #g #Hg #H ] +| elim (at_inv_xxp … Hf) -Hf // + #g #H1 #H +] +[2: elim (after_inv_xxn … Hf21 … H) -f * + [ #g2 #g1 #Hg21 #H2 #H1 | #g2 #Hg21 #H2 ] +|*: elim (after_inv_xxp … Hf21 … H) -f + #g2 #g1 #Hg21 #H2 #H1 +] +[4: -Hg21 |*: elim (IH … Hg … Hg21) -g -IH ] +/3 width=9 by at_refl, at_push, at_next, ex2_intro/ +qed-. + +lemma after_fwd_at: ∀i,i2,i1,f1,f2. @⦃i1, f1⦄ ≡ i2 → @⦃i2, f2⦄ ≡ i → + ∀f. f2 ⊚ f1 ≡ f → @⦃i1, f⦄ ≡ i. +#i elim i -i [2: #i #IH ] #i2 #i1 #f1 #f2 #Hf1 #Hf2 #f #Hf +[ elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ] + #g2 [ #j2 ] #Hg2 [ #H22 ] #H20 + [ elim (at_inv_xxn … Hf1 … H22) -i2 * + #g1 [ #j1 ] #Hg1 [ #H11 ] #H10 + [ elim (after_inv_ppx … Hf … H20 H10) -f1 -f2 /3 width=7 by at_push/ + | elim (after_inv_pnx … Hf … H20 H10) -f1 -f2 /3 width=6 by at_next/ + ] + | elim (after_inv_nxx … Hf … H20) -f2 /3 width=7 by at_next/ + ] +| elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H22 #H20 + elim (at_inv_xxp … Hf1 … H22) -i2 #g1 #H11 #H10 + elim (after_inv_ppx … Hf … H20 H10) -f1 -f2 /2 width=2 by at_refl/ +] +qed-. + +lemma after_fwd_at2: ∀f,i1,i. @⦃i1, f⦄ ≡ i → ∀f1,i2. @⦃i1, f1⦄ ≡ i2 → + ∀f2. f2 ⊚ f1 ≡ f → @⦃i2, f2⦄ ≡ i. +#f #i1 #i #Hf #f1 #i2 #Hf1 #f2 #H elim (after_at_fwd … Hf … H) -f +#j1 #H #Hf2 <(at_mono … Hf1 … H) -i1 -i2 // +qed-. + +lemma after_fwd_at1: ∀i,i2,i1,f,f2. @⦃i1, f⦄ ≡ i → @⦃i2, f2⦄ ≡ i → + ∀f1. f2 ⊚ f1 ≡ f → @⦃i1, f1⦄ ≡ i2. +#i elim i -i [2: #i #IH ] #i2 #i1 #f #f2 #Hf #Hf2 #f1 #Hf1 +[ elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ] + #g [ #j1 ] #Hg [ #H01 ] #H00 + elim (at_inv_xxn … Hf2) -Hf2 [1,3,5,7: * |*: // ] + #g2 [1,3: #j2 ] #Hg2 [1,2: #H22 ] #H20 + [ elim (after_inv_pxp … Hf1 … H20 H00) -f2 -f /3 width=7 by at_push/ + | elim (after_inv_pxn … Hf1 … H20 H00) -f2 -f /3 width=5 by at_next/ + | elim (after_inv_nxp … Hf1 … H20 H00) + | /4 width=9 by after_inv_nxn, at_next/ + ] +| elim (at_inv_xxp … Hf) -Hf // #g #H01 #H00 + elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H21 #H20 + elim (after_inv_pxp … Hf1 … H20 H00) -f2 -f /3 width=2 by at_refl/ +] +qed-. + +(* Forward lemmas on istot **************************************************) + +lemma after_istot_fwd: ∀f2,f1,f. f2 ⊚ f1 ≡ f → 𝐓⦃f2⦄ → 𝐓⦃f1⦄ → 𝐓⦃f⦄. +#f2 #f1 #f #Hf #Hf2 #Hf1 #i1 elim (Hf1 i1) -Hf1 +#i2 #Hf1 elim (Hf2 i2) -Hf2 +/3 width=7 by after_fwd_at, ex_intro/ +qed-. + +lemma after_fwd_istot_dx: ∀f2,f1,f. f2 ⊚ f1 ≡ f → 𝐓⦃f⦄ → 𝐓⦃f1⦄. +#f2 #f1 #f #H #Hf #i1 elim (Hf i1) -Hf +#i2 #Hf elim (after_at_fwd … Hf … H) -f /2 width=2 by ex_intro/ +qed-. + +lemma after_fwd_istot_sn: ∀f2,f1,f. f2 ⊚ f1 ≡ f → 𝐓⦃f⦄ → 𝐓⦃f2⦄. +#f2 #f1 #f #H #Hf #i1 elim (Hf i1) -Hf +#i #Hf elim (after_at_fwd … Hf … H) -f +#i2 #Hf1 #Hf2 lapply (at_increasing … Hf1) -f1 +#Hi12 elim (at_le_ex … Hf2 … Hi12) -i2 /2 width=2 by ex_intro/ +qed-. + +lemma after_inv_istot: ∀f2,f1,f. f2 ⊚ f1 ≡ f → 𝐓⦃f⦄ → 𝐓⦃f2⦄ ∧ 𝐓⦃f1⦄. +/3 width=4 by after_fwd_istot_sn, after_fwd_istot_dx, conj/ qed-. + +lemma after_at1_fwd: ∀f1,i1,i2. @⦃i1, f1⦄ ≡ i2 → ∀f2. 𝐓⦃f2⦄ → ∀f. f2 ⊚ f1 ≡ f → + ∃∃i. @⦃i2, f2⦄ ≡ i & @⦃i1, f⦄ ≡ i. +#f1 #i1 #i2 #Hf1 #f2 #Hf2 #f #Hf elim (Hf2 i2) -Hf2 +/3 width=8 by after_fwd_at, ex2_intro/ +qed-. + +lemma after_fwd_isid_sn: ∀f2,f1,f. 𝐓⦃f⦄ → f2 ⊚ f1 ≡ f → f1 ≗ f → 𝐈⦃f2⦄. +#f2 #f1 #f #H #Hf elim (after_inv_istot … Hf H) -H +#Hf2 #Hf1 #H @isid_at_total // -Hf2 +#i2 #i #Hf2 elim (Hf1 i2) -Hf1 +#i0 #Hf1 lapply (at_increasing … Hf1) +#Hi20 lapply (after_fwd_at2 … i0 … Hf1 … Hf) -Hf +/3 width=7 by at_eq_repl_back, at_mono, at_id_le/ +qed-. + +lemma after_fwd_isid_dx: ∀f2,f1,f. 𝐓⦃f⦄ → f2 ⊚ f1 ≡ f → f2 ≗ f → 𝐈⦃f1⦄. +#f2 #f1 #f #H #Hf elim (after_inv_istot … Hf H) -H +#Hf2 #Hf1 #H2 @isid_at_total // -Hf1 +#i1 #i2 #Hi12 elim (after_at1_fwd … Hi12 … Hf) -f1 +/3 width=8 by at_inj, at_eq_repl_back/ +qed-. + +let corec after_inj_O_aux: ∀f1. @⦃0, f1⦄ ≡ 0 → H_after_inj f1 ≝ ?. +#f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f +cases (at_inv_pxp … H1f1) -H1f1 [ |*: // ] #g1 #H1 +lapply (istot_inv_push … H2f1 … H1) -H2f1 #H2g1 +cases (H2g1 0) #n #Hn +cases (after_inv_pxx … H1f … H1) -H1f * #g21 #g #H1g #H21 #H +[ cases (after_inv_pxp … H2f … H1 H) -f1 -f #g22 #H2g #H22 + @(eq_push … H21 H22) -f21 -f22 +| cases (after_inv_pxn … H2f … H1 H) -f1 -f #g22 #H2g #H22 + @(eq_next … H21 H22) -f21 -f22 +] +@(after_inj_O_aux (g1-n) … (g-n)) -after_inj_O_aux +/2 width=1 by after_minus, istot_minus, at_pxx_minus/ +qed-. + +fact after_inj_aux: (∀f1. @⦃0, f1⦄ ≡ 0 → H_after_inj f1) → + ∀i2,f1. @⦃0, f1⦄ ≡ i2 → H_after_inj f1. +#H0 #i2 elim i2 -i2 /2 width=1 by/ -H0 +#i2 #IH #f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f +elim (at_inv_pxn … H1f1) -H1f1 [ |*: // ] #g1 #H1g1 #H1 +elim (after_inv_nxx … H1f … H1) -H1f #g #H1g #H +lapply (after_inv_nxn … H2f … H1 H) -f #H2g +/3 width=6 by istot_inv_next/ +qed-. + +theorem after_inj: ∀f1. H_after_inj f1. +#f1 #H cases (H 0) /3 width=7 by after_inj_aux, after_inj_O_aux/ +qed-. 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 f6377be85..3bc16b8ec 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma @@ -61,15 +61,21 @@ lemma at_inv_ppn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → #H destruct qed-. +lemma at_inv_npp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → + ∀g,j1. ⫯j1 = i1 → ↑g = f → 0 = i2 → ⊥. +#f #i1 #i2 #Hf #g #j1 #H1 #H elim (at_inv_npx … Hf … H1 H) -f -i1 +#x2 #Hg * -i2 #H destruct +qed-. + lemma at_inv_npn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g,j1,j2. ⫯j1 = i1 → ↑g = f → ⫯j2 = i2 → @⦃j1, g⦄ ≡ j2. #f #i1 #i2 #Hf #g #j1 #j2 #H1 #H elim (at_inv_npx … Hf … H1 H) -f -i1 #x2 #Hg * -i2 #H destruct // qed-. -lemma at_inv_npp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → - ∀g,j1. ⫯j1 = i1 → ↑g = f → 0 = i2 → ⊥. -#f #i1 #i2 #Hf #g #j1 #H1 #H elim (at_inv_npx … Hf … H1 H) -f -i1 +lemma at_inv_xnp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → + ∀g. ⫯g = f → 0 = i2 → ⊥. +#f #i1 #i2 #Hf #g #H elim (at_inv_xnx … Hf … H) -f #x2 #Hg * -i2 #H destruct qed-. @@ -79,6 +85,13 @@ lemma at_inv_xnn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → #x2 #Hg * -i2 #H destruct // qed-. +(* --------------------------------------------------------------------------*) + +lemma at_inv_pxp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → 0 = i1 → 0 = i2 → ∃g. ↑g = f. +#f elim (pn_split … f) * /2 width=2 by ex_intro/ +#g #H #i1 #i2 #Hf #H1 #H2 cases (at_inv_xnp … Hf … H H2) +qed-. + lemma at_inv_pxn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀j2. 0 = i1 → ⫯j2 = i2 → ∃∃g. @⦃i1, g⦄ ≡ j2 & ⫯g = f. #f elim (pn_split … f) * @@ -88,12 +101,6 @@ lemma at_inv_pxn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀j2. 0 = i1 → ⫯j2 = ] qed-. -lemma at_inv_xnp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → - ∀g. ⫯g = f → 0 = i2 → ⊥. -#f #i1 #i2 #Hf #g #H elim (at_inv_xnx … Hf … H) -f -#x2 #Hg * -i2 #H destruct -qed-. - lemma at_inv_nxp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀j1. ⫯j1 = i1 → 0 = i2 → ⊥. #f elim (pn_split f) * @@ -110,6 +117,8 @@ lemma at_inv_nxn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀j1,j2. ⫯j1 = i1 → /4 width=7 by at_inv_xnn, at_inv_npn, ex2_intro, or_intror, or_introl/ qed-. +(* --------------------------------------------------------------------------*) + lemma at_inv_xpx: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. ↑g = f → (0 = i1 ∧ 0 = i2) ∨ ∃∃j1,j2. @⦃j1, g⦄ ≡ j2 & ⫯j1 = i1 & ⫯j2 = i2. @@ -141,6 +150,16 @@ lemma at_inv_xxp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → 0 = i2 → ] qed-. +lemma at_inv_xxn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀j2. ⫯j2 = i2 → + (∃∃g,j1. @⦃j1, g⦄ ≡ j2 & ⫯j1 = i1 & ↑g = f) ∨ + ∃∃g. @⦃i1, g⦄ ≡ j2 & ⫯g = f. +#f elim (pn_split f) * +#g #H #i1 #i2 #Hf #j2 #H2 +[ elim (at_inv_xpn … Hf … H H2) -i2 /3 width=5 by or_introl, ex3_2_intro/ +| lapply (at_inv_xnn … Hf … H H2) -i2 /3 width=3 by or_intror, ex2_intro/ +] +qed-. + (* Basic forward lemmas *****************************************************) lemma at_increasing: ∀i2,i1,f. @⦃i1, f⦄ ≡ i2 → i1 ≤ i2. @@ -179,6 +198,24 @@ lemma at_eq_repl_fwd: ∀i1,i2. eq_repl_fwd (λf. @⦃i1, f⦄ ≡ i2). #i1 #i2 @eq_repl_sym /2 width=3 by at_eq_repl_back/ qed-. +lemma at_le_ex: ∀j2,i2,f. @⦃i2, f⦄ ≡ j2 → ∀i1. i1 ≤ i2 → + ∃∃j1. @⦃i1, f⦄ ≡ j1 & j1 ≤ j2. +#j2 elim j2 -j2 [2: #j2 #IH ] #i2 #f #Hf +[ elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ] + #g [ #x2 ] #Hg [ #H2 ] #H0 + [ * /3 width=3 by at_refl, ex2_intro/ + #i1 #Hi12 destruct lapply (le_S_S_to_le … Hi12) -Hi12 + #Hi12 elim (IH … Hg … Hi12) -x2 -IH + /3 width=7 by at_push, ex2_intro, le_S_S/ + | #i1 #Hi12 elim (IH … Hg … Hi12) -IH -i2 + /3 width=5 by at_next, ex2_intro, le_S_S/ + ] +| elim (at_inv_xxp … Hf) -Hf // + #g * -i2 #H2 #i1 #Hi12 <(le_n_O_to_eq … Hi12) + /3 width=3 by at_refl, ex2_intro/ +] +qed-. + lemma at_id_le: ∀i1,i2. i1 ≤ i2 → ∀f. @⦃i2, f⦄ ≡ i2 → @⦃i1, f⦄ ≡ i1. #i1 #i2 #H @(le_elim … H) -i1 -i2 [ #i2 | #i1 #i2 #IH ] #f #Hf elim (at_fwd_id_ex … Hf) /4 width=7 by at_inv_npn, at_push, at_refl/ @@ -186,57 +223,60 @@ qed-. (* Main properties **********************************************************) -theorem at_monotonic: ∀j2,i2,f2. @⦃i2, f2⦄ ≡ j2 → ∀j1,i1,f1. @⦃i1, f1⦄ ≡ j1 → - f1 ≗ f2 → i1 < i2 → j1 < j2. +theorem at_monotonic: ∀j2,i2,f. @⦃i2, f⦄ ≡ j2 → ∀j1,i1. @⦃i1, f⦄ ≡ j1 → + i1 < i2 → j1 < j2. #j2 elim j2 -j2 -[ #i2 #f2 #Hf2 elim (at_inv_xxp … Hf2) -Hf2 // - #g #H21 #_ #j1 #i1 #f1 #_ #_ #Hi elim (lt_le_false … Hi) -Hi // -| #j2 #IH #i2 #f2 #Hf2 * // - #j1 #i1 #f1 #Hf1 #Hf #Hi elim (lt_inv_gen … Hi) - #x2 #_ #H21 elim (at_inv_nxn … Hf2 … H21) -Hf2 [1,3: * |*: // ] - #g2 #Hg2 #H2 - [ elim (eq_inv_xp … Hf … H2) -f2 - #g1 #Hg #H1 elim (at_inv_xpn … Hf1 … H1) -f1 +[ #i2 #f #H2f elim (at_inv_xxp … H2f) -H2f // + #g #H21 #_ #j1 #i1 #_ #Hi elim (lt_le_false … Hi) -Hi // +| #j2 #IH #i2 #f #H2f * // + #j1 #i1 #H1f #Hi elim (lt_inv_gen … Hi) + #x2 #_ #H21 elim (at_inv_nxn … H2f … H21) -H2f [1,3: * |*: // ] + #g #H2g #H + [ elim (at_inv_xpn … H1f … H) -f /4 width=8 by lt_S_S_to_lt, lt_S_S/ - | elim (eq_inv_xn … Hf … H2) -f2 - /4 width=8 by at_inv_xnn, lt_S_S/ + | /4 width=8 by at_inv_xnn, lt_S_S/ ] ] qed-. -theorem at_inv_monotonic: ∀j1,i1,f1. @⦃i1, f1⦄ ≡ j1 → ∀j2,i2,f2. @⦃i2, f2⦄ ≡ j2 → - f1 ≗ f2 → j1 < j2 → i1 < i2. +theorem at_inv_monotonic: ∀j1,i1,f. @⦃i1, f⦄ ≡ j1 → ∀j2,i2. @⦃i2, f⦄ ≡ j2 → + j1 < j2 → i1 < i2. #j1 elim j1 -j1 -[ #i1 #f1 #Hf1 elim (at_inv_xxp … Hf1) -Hf1 // - #g1 * -i1 #H1 #j2 #i2 #f2 #Hf2 #Hf #Hj elim (lt_inv_O1 … Hj) -Hj - #x2 #H22 elim (eq_inv_px … Hf … H1) -f1 - #g2 #Hg #H2 elim (at_inv_xpn … Hf2 … H2 H22) -f2 // +[ #i1 #f #H1f elim (at_inv_xxp … H1f) -H1f // + #g * -i1 #H #j2 #i2 #H2f #Hj elim (lt_inv_O1 … Hj) -Hj + #x2 #H22 elim (at_inv_xpn … H2f … H H22) -f // | #j1 #IH * - [ #f1 #Hf1 elim (at_inv_pxn … Hf1) -Hf1 [ |*: // ] - #g1 #Hg1 #H1 #j2 #i2 #f2 #Hf2 #Hf #Hj elim (lt_inv_S1 … Hj) -Hj - elim (eq_inv_nx … Hf … H1) -f1 /3 width=7 by at_inv_xnn/ - | #i1 #f1 #Hf1 #j2 #i2 #f2 #Hf2 #Hf #Hj elim (lt_inv_S1 … Hj) -Hj - #y2 #Hj #H22 elim (at_inv_nxn … Hf1) -Hf1 [1,4: * |*: // ] - #g1 #Hg1 #H1 - [ elim (eq_inv_px … Hf … H1) -f1 - #g2 #Hg #H2 elim (at_inv_xpn … Hf2 … H2 H22) -f2 -H22 + [ #f #H1f elim (at_inv_pxn … H1f) -H1f [ |*: // ] + #g #H1g #H #j2 #i2 #H2f #Hj elim (lt_inv_S1 … Hj) -Hj + /3 width=7 by at_inv_xnn/ + | #i1 #f #H1f #j2 #i2 #H2f #Hj elim (lt_inv_S1 … Hj) -Hj + #y2 #Hj #H22 elim (at_inv_nxn … H1f) -H1f [1,4: * |*: // ] + #g #Hg #H + [ elim (at_inv_xpn … H2f … H H22) -f -H22 /3 width=7 by lt_S_S/ - | elim (eq_inv_nx … Hf … H1) -f1 /3 width=7 by at_inv_xnn/ + | /3 width=7 by at_inv_xnn/ ] ] ] qed-. -theorem at_mono: ∀f1,f2. f1 ≗ f2 → ∀i,i1. @⦃i, f1⦄ ≡ i1 → ∀i2. @⦃i, f2⦄ ≡ i2 → i2 = i1. -#f1 #f2 #Ht #i #i1 #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) // -#Hi elim (lt_le_false i i) /3 width=8 by at_inv_monotonic, eq_sym/ +theorem at_mono: ∀f,i,i1. @⦃i, f⦄ ≡ i1 → ∀i2. @⦃i, f⦄ ≡ i2 → i2 = i1. +#f #i #i1 #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) // +#Hi elim (lt_le_false i i) /3 width=6 by at_inv_monotonic, eq_sym/ qed-. -theorem at_inj: ∀f1,f2. f1 ≗ f2 → ∀i1,i. @⦃i1, f1⦄ ≡ i → ∀i2. @⦃i2, f2⦄ ≡ i → i1 = i2. -#f1 #f2 #Ht #i1 #i #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) // -#Hi elim (lt_le_false i i) /3 width=8 by at_monotonic, eq_sym/ +theorem at_inj: ∀f,i1,i. @⦃i1, f⦄ ≡ i → ∀i2. @⦃i2, f⦄ ≡ i → i1 = i2. +#f #i1 #i #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) // +#Hi elim (lt_le_false i i) /3 width=6 by at_monotonic, eq_sym/ qed-. +(* Properties on minus ******************************************************) + +lemma at_pxx_minus: ∀n,f. @⦃0, f⦄ ≡ n → @⦃0, f-n⦄ ≡ 0. +#n elim n -n // +#n #IH #f #Hf cases (at_inv_pxn … Hf) -Hf /2 width=3 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_eq.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma index 44a83c7ff..4430c2f8a 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "ground_2/notation/relations/funexteq_2.ma". -include "ground_2/relocation/nstream_lift.ma". +include "ground_2/relocation/rtmap.ma". (* RELOCATION MAP ***********************************************************) @@ -136,8 +136,8 @@ let corec eq_trans: Transitive … eq ≝ ?. /3 width=5 by eq_push, eq_next/ qed-. -theorem eq_canc_sn: ∀f,f1,f2. f ≗ f1 → f ≗ f2 → f1 ≗ f2. +theorem eq_canc_sn: ∀f2. eq_repl_back (λf. f ≗ f2). /3 width=3 by eq_trans, eq_sym/ qed-. -theorem eq_canc_dx: ∀f,f1,f2. f1 ≗ f → f2 ≗ f → f1 ≗ f2. +theorem eq_canc_dx: ∀f1. eq_repl_fwd (λf. f1 ≗ f). /3 width=3 by eq_trans, eq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma index 357f0fd20..cfe2b3771 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "ground_2/notation/relations/isidentity_1.ma". -include "ground_2/relocation/rtmap_eq.ma". +include "ground_2/relocation/rtmap_minus.ma". (* RELOCATION MAP ***********************************************************) diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma index 85d70d4da..07b24f973 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma @@ -34,6 +34,19 @@ lemma istot_inv_next: ∀g. 𝐓⦃g⦄ → ∀f. ⫯f = g → 𝐓⦃f⦄. #j #Hg elim (at_inv_xnx … Hg … H) -Hg -H /2 width=2 by ex_intro/ qed-. +(* Properties on tl *********************************************************) + +lemma istot_tl: ∀f. 𝐓⦃f⦄ → 𝐓⦃↓f⦄. +#f cases (pn_split f) * +#g * -f /2 width=3 by istot_inv_next, istot_inv_push/ +qed. + +(* Properties on minus ******************************************************) + +lemma istot_minus: ∀n,f. 𝐓⦃f⦄ → 𝐓⦃f-n⦄. +#n elim n -n /3 width=1 by istot_tl/ +qed. + (* Advanced forward lemmas on at ********************************************) let corec at_ext: ∀f1,f2. 𝐓⦃f1⦄ → 𝐓⦃f2⦄ → diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_minus.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_minus.ma new file mode 100644 index 000000000..91f2c8479 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_minus.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||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_tl.ma". + +(* RELOCATION MAP ***********************************************************) + +let rec minus (f:rtmap) (n:nat) on n: rtmap ≝ match n with +[ O ⇒ f | S m ⇒ ↓(minus f m) ]. + +interpretation "minus (rtmap)" 'minus f n = (minus f n). + +(* Basic properties *********************************************************) + +lemma minus_rew_O: ∀f. f = f - 0. +// qed. + +lemma minus_rew_S: ∀f,n. ↓(f - n) = f - ⫯n. +// qed. + +lemma minus_eq_repl: ∀n. eq_repl (λf1,f2. f1 - n ≗ f2 - n). +#n elim n -n /3 width=1 by tl_eq_repl/ +qed. + +(* Advancedd properties *****************************************************) + +lemma minus_xn: ∀n,f. (↓f) - n = f - ⫯n. +#n elim n -n // +qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tl.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tl.ma new file mode 100644 index 000000000..779cc4f6f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tl.ma @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||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/drop_1.ma". +include "ground_2/relocation/rtmap_eq.ma". + +(* RELOCATION MAP ***********************************************************) + +definition tl: rtmap → rtmap. +@case_type0 #f @f +defined. + +interpretation "tail (rtmap)" 'Drop f = (tl f). + +(* Basic properties *********************************************************) + +lemma tl_rew: ∀f. case_type0 (λ_:rtmap.rtmap) (λf:rtmap.f) (λf:rtmap.f) f = ↓f. +// qed. + +lemma tl_push_rew: ∀f. f = ↓↑f. +#f (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 = ◊ → - cs2 = ◊ ∧ cs = ◊. -#cs1 #cs2 #cs * -cs1 -cs2 -cs -[ /2 width=1 by conj/ -| #cs1 #cs2 #cs #_ #b #H destruct -| #cs1 #cs2 #cs #_ #H destruct -] -qed-. - -lemma after_inv_empty1: ∀cs2,cs. ◊ ⊚ cs2 ≡ cs → cs2 = ◊ ∧ cs = ◊. -/2 width=3 by after_inv_empty1_aux/ qed-. - -fact after_inv_true1_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl1. cs1 = Ⓣ @ tl1 → - ∃∃tl2,tl,b. cs2 = b @ tl2 & cs = b @ tl & tl1 ⊚ tl2 ≡ tl. -#cs1 #cs2 #cs * -cs1 -cs2 -cs -[ #tl1 #H destruct -| #cs1 #cs2 #cs #H12 #b #tl1 #H destruct - /2 width=6 by ex3_3_intro/ -| #cs1 #cs2 #cs #_ #tl1 #H destruct -] -qed-. - -lemma after_inv_true1: ∀tl1,cs2,cs. (Ⓣ @ tl1) ⊚ cs2 ≡ cs → - ∃∃tl2,tl,b. cs2 = b @ tl2 & cs = b @ tl & tl1 ⊚ tl2 ≡ tl. -/2 width=3 by after_inv_true1_aux/ qed-. - -fact after_inv_false1_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl1. cs1 = Ⓕ @ tl1 → - ∃∃tl. cs = Ⓕ @ tl & tl1 ⊚ cs2 ≡ tl. -#cs1 #cs2 #cs * -cs1 -cs2 -cs -[ #tl1 #H destruct -| #cs1 #cs2 #cs #_ #b #tl1 #H destruct -| #cs1 #cs2 #cs #H12 #tl1 #H destruct - /2 width=3 by ex2_intro/ -] -qed-. - -lemma after_inv_false1: ∀tl1,cs2,cs. (Ⓕ @ tl1) ⊚ cs2 ≡ cs → - ∃∃tl. cs = Ⓕ @ tl & tl1 ⊚ cs2 ≡ tl. -/2 width=3 by after_inv_false1_aux/ qed-. - -fact after_inv_empty3_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → cs = ◊ → - cs1 = ◊ ∧ cs2 = ◊. -#cs1 #cs2 #cs * -cs1 -cs2 -cs -[ /2 width=1 by conj/ -| #cs1 #cs2 #cs #_ #b #H destruct -| #cs1 #cs2 #cs #_ #H destruct -] -qed-. - -lemma after_inv_empty3: ∀cs1,cs2. cs1 ⊚ cs2 ≡ ◊ → cs1 = ◊ ∧ cs2 = ◊. -/2 width=3 by after_inv_empty3_aux/ qed-. - -fact after_inv_inh3_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl,b. cs = b @ tl → - (∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = b @ tl2 & tl1 ⊚ tl2 ≡ tl) ∨ - ∃∃tl1. cs1 = Ⓕ @ tl1 & b = Ⓕ & tl1 ⊚ cs2 ≡ tl. -#cs1 #cs2 #cs * -cs1 -cs2 -cs -[ #tl #b #H destruct -| #cs1 #cs2 #cs #H12 #b0 #tl #b #H destruct - /3 width=5 by ex3_2_intro, or_introl/ -| #cs1 #cs2 #cs #H12 #tl #b #H destruct - /3 width=3 by ex3_intro, or_intror/ -] -qed-. - -lemma after_inv_inh3: ∀cs1,cs2,tl,b. cs1 ⊚ cs2 ≡ b @ tl → - (∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = b @ tl2 & tl1 ⊚ tl2 ≡ tl) ∨ - ∃∃tl1. cs1 = Ⓕ @ tl1 & b = Ⓕ & tl1 ⊚ cs2 ≡ tl. -/2 width=3 by after_inv_inh3_aux/ qed-. - -lemma after_inv_true3: ∀cs1,cs2,tl. cs1 ⊚ cs2 ≡ Ⓣ @ tl → - ∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = Ⓣ @ tl2 & tl1 ⊚ tl2 ≡ tl. -#cs1 #cs2 #tl #H elim (after_inv_inh3 … H) -H // * -#tl1 #_ #H destruct -qed-. - -lemma after_inv_false3: ∀cs1,cs2,tl. cs1 ⊚ cs2 ≡ Ⓕ @ tl → - (∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = Ⓕ @ tl2 & tl1 ⊚ tl2 ≡ tl) ∨ - ∃∃tl1. cs1 = Ⓕ @ tl1 & tl1 ⊚ cs2 ≡ tl. -#cs1 #cs2 #tl #H elim (after_inv_inh3 … H) -H /2 width=1 by or_introl/ * /3 width=3 by ex2_intro, or_intror/ -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) -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/ - | #j1 #j #H1 #H2 #Hj1 destruct - elim (IH … Hj1) -IH -Hj1 /3 width=3 by at_succ, ex2_intro/ - ] - | elim (at_inv_false … H) -H - #j #H #Hj destruct - elim (IH … Hj) -IH -Hj /3 width=3 by at_succ, at_false, ex2_intro/ - ] -| #cs1 #cs2 #cs #_ #IH #i1 #i #H elim (at_inv_false … H) -H - #j #H #Hj destruct - elim (IH … Hj) -IH -Hj /3 width=3 by at_false, ex2_intro/ -] -qed-. - -lemma after_at1_fwd: ∀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) -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/ - | #j1 #j2 #H1 #H2 #Hj12 destruct - elim (IH … Hj12) -IH -Hj12 /3 width=3 by at_succ, ex2_intro/ - ] - | elim (at_inv_false … H) -H - #j2 #H #Hj2 destruct - elim (IH … Hj2) -IH -Hj2 /3 width=3 by at_succ, at_false, ex2_intro/ - ] -| #cs1 #cs2 #cs #_ #IH #i1 #i2 #H elim (IH … H) -IH -H - /3 width=3 by at_false, ex2_intro/ -] -qed-. - -lemma after_fwd_at: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → - ∀i1,i2,i. @⦃i1, cs1⦄ ≡ i2 → @⦃i2, cs2⦄ ≡ i → @⦃i1, cs⦄ ≡ i. -#cs1 #cs2 #cs #Hcs #i1 #i2 #i #Hi1 #Hi2 elim (after_at1_fwd … Hcs … Hi1) -cs1 -#j #H #Hj >(at_mono … Hi2 … H) -i2 // -qed-. - -lemma after_fwd_at1: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → - ∀i1,i2,i. @⦃i1, cs⦄ ≡ i → @⦃i2, cs2⦄ ≡ i → @⦃i1, cs1⦄ ≡ i2. -#cs1 #cs2 #cs #Hcs #i1 #i2 #i #Hi1 #Hi2 elim (after_at_fwd … Hcs … Hi1) -cs -#j1 #Hij1 #H >(at_inj … Hi2 … H) -i // -qed-. - -lemma after_fwd_at2: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → - ∀i1,i2,i. @⦃i1, cs⦄ ≡ i → @⦃i1, cs1⦄ ≡ i2 → @⦃i2, cs2⦄ ≡ i. -#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs -[ #i1 #i2 #i #Hi #Hi1 elim (at_inv_empty … Hi1) -Hi1 // -| #cs1 #cs2 #cs #_ * #IH #i1 #i2 #i #Hi #Hi1 - [ elim (at_inv_true … Hi1) -Hi1 * - [ -IH #H1 #H2 destruct >(at_inv_true_zero_sn … Hi) -i // - | #j1 #j2 #H1 #H2 #Hj12 destruct elim (at_inv_true_succ_sn … Hi) -Hi - #j #H #Hj1 destruct /3 width=3 by at_succ/ - ] - | elim (at_inv_false … Hi1) -Hi1 - #j2 #H #Hj2 destruct elim (at_inv_false … Hi) -Hi - #j #H #Hj destruct /3 width=3 by at_succ/ - ] -| #cs1 #cs2 #cs #_ #IH #i1 #i2 #i #Hi #Hi2 elim (at_inv_false … Hi) -Hi - #j #H #Hj destruct /3 width=3 by at_false/ -] -qed-. - -(* Main properties **********************************************************) - -theorem after_trans1: ∀cs1,cs2,cs0. cs1 ⊚ cs2 ≡ cs0 → - ∀cs3, cs4. cs0 ⊚ cs3 ≡ cs4 → - ∃∃cs. cs2 ⊚ cs3 ≡ cs & cs1 ⊚ cs ≡ cs4. -#cs1 #cs2 #cs0 #H elim H -cs1 -cs2 -cs0 -[ #cs3 #cs4 #H elim (after_inv_empty1 … H) -H - #H1 #H2 destruct /2 width=3 by ex2_intro, after_empty/ -| #cs1 #cs2 #cs0 #_ * #IH #cs3 #cs4 #H - [ elim (after_inv_true1 … H) -H - #tl3 #tl4 #b #H1 #H2 #Htl destruct - elim (IH … Htl) -cs0 - /3 width=3 by ex2_intro, after_true/ - | elim (after_inv_false1 … H) -H - #tl4 #H #Htl destruct - elim (IH … Htl) -cs0 - /3 width=3 by ex2_intro, after_true, after_false/ - ] -| #cs1 #cs2 #cs0 #_ #IH #cs3 #cs4 #H - elim (after_inv_false1 … H) -H - #tl4 #H #Htl destruct - elim (IH … Htl) -cs0 - /3 width=3 by ex2_intro, after_false/ -] -qed-. - -theorem after_trans2: ∀cs1,cs0,cs4. cs1 ⊚ cs0 ≡ cs4 → - ∀cs2, cs3. cs2 ⊚ cs3 ≡ cs0 → - ∃∃cs. cs1 ⊚ cs2 ≡ cs & cs ⊚ cs3 ≡ cs4. -#cs1 #cs0 #cs4 #H elim H -cs1 -cs0 -cs4 -[ #cs2 #cs3 #H elim (after_inv_empty3 … H) -H - #H1 #H2 destruct /2 width=3 by ex2_intro, after_empty/ -| #cs1 #cs0 #cs4 #_ #b #IH #cs2 #cs3 #H elim (after_inv_inh3 … H) -H * - [ #tl2 #tl3 #H1 #H2 #Htl destruct - elim (IH … Htl) -cs0 - /3 width=3 by ex2_intro, after_true/ - | #tl2 #H1 #H2 #Htl destruct - elim (IH … Htl) -cs0 - /3 width=3 by ex2_intro, after_true, after_false/ - ] -| #cs1 #cs0 #cs4 #_ #IH #cs2 #cs3 #H elim (IH … H) -cs0 - /3 width=3 by ex2_intro, after_false/ -] -qed-. - -theorem after_mono: ∀cs1,cs2,x. cs1 ⊚ cs2 ≡ x → ∀y. cs1 ⊚ cs2 ≡ y → x = y. -#cs1 #cs2 #x #H elim H -cs1 -cs2 -x -[ #y #H elim (after_inv_empty1 … H) -H // -| #cs1 #cs #x #_ #b #IH #y #H elim (after_inv_true1 … H) -H - #tl #tly #b0 #H1 #H2 #Htl destruct >(IH … Htl) -tl -cs1 -x // -| #cs1 #cs2 #x #_ #IH #y #H elim (after_inv_false1 … H) -H - #tly #H #Htl destruct >(IH … Htl) -cs1 -cs2 -x // -] -qed-. - -theorem after_inj: ∀cs1,x,cs. cs1 ⊚ x ≡ cs → ∀y. cs1 ⊚ y ≡ cs → x = y. -#cs1 #x #cs #H elim H -cs1 -x -cs -[ #y #H elim (after_inv_empty1 … H) -H // -| #cs1 #x #cs #_ #b #IH #y #H elim (after_inv_true1 … H) -H - #tly #tl #b0 #H1 #H2 #Htl destruct >(IH … Htl) -tl -cs1 -x // -| #cs1 #x #cs #_ #IH #y #H elim (after_inv_false1 … H) -H - #tl #H #Htl destruct >(IH … Htl) -tl -cs1 -x // -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma deleted file mode 100644 index 02d8ac1eb..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma +++ /dev/null @@ -1,264 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/rat_3.ma". -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,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,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: ∀i1,i2. @⦃i1, ◊⦄ ≡ i2 → i1 = 0 ∧ i2 = 0. -/2 width=5 by at_inv_empty_aux/ qed-. - -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,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,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 * // -#j1 #j2 #_ #H destruct -qed-. - -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 -| #j1 #j2 #H1 #H2 destruct /2 width=3 by ex2_intro/ -] -qed-. - -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 -| #j1 #j2 #H1 #H2 destruct /2 width=3 by ex2_intro/ -] -qed-. - -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 -| #j1 #j2 #H1 #H2 destruct // -] -qed-. - -lemma at_inv_true_O_S: ∀cs,i. @⦃0, Ⓣ @ cs⦄ ≡ ⫯i → ⊥. -#cs #i #H elim (at_inv_true … H) -H * -[ #_ #H 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 -| #j1 #j2 #_ #H destruct -] -qed-. - -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,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,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 -#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 *********************************************************) - -(* 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_dec: ∀cs,i1,i2. Decidable (@⦃i1, cs⦄ ≡ i2). -#cs elim cs -cs [ | * #cs #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/ - ] -| #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/ - ] -] -qed-. - -lemma is_at_dec: ∀cs,i2. Decidable (∃i1. @⦃i1, cs⦄ ≡ i2). -#cs elim cs -cs -[ * /3 width=2 by ex_intro, or_introl/ - #i2 @or_intror * /2 width=3 by at_inv_empty_succ_dx/ -| * #cs #IH * [2,4: #i2 ] - [ elim (IH i2) -IH - [ * /4 width=2 by at_succ, ex_intro, or_introl/ - | #H @or_intror * #x #Hx - elim (at_inv_true_succ_dx … Hx) -Hx - /3 width=2 by ex_intro/ - ] - | elim (IH i2) -IH - [ * /4 width=2 by at_false, ex_intro, or_introl/ - | #H @or_intror * /4 width=2 by at_inv_false_S, ex_intro/ - ] - | /3 width=2 by at_zero, ex_intro, or_introl/ - | @or_intror * /2 width=3 by at_inv_false_O/ - ] -] -qed-. - -(* Basic forward lemmas *****************************************************) - -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_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,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 - #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,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 - #j2 #H destruct #H >(IH … H) -cs -i1 -i // -| elim (at_inv_false … H) -H - #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 deleted file mode 100644 index 6dce9e0a2..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_isid.ma +++ /dev/null @@ -1,114 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/isidentity_1.ma". -include "ground_2/relocation/trace_after.ma". -include "ground_2/relocation/trace_sle.ma". - -(* RELOCATION TRACE *********************************************************) - -definition isid: predicate trace ≝ λcs. ∥cs∥ = |cs|. - -interpretation "test for identity (trace)" - 'IsIdentity cs = (isid cs). - -definition t_reflexive: ∀S:Type[0]. predicate (trace → relation S) ≝ - λS,R. ∀a. ∃∃t. 𝐈⦃t⦄ & R t a a. - -(* 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: ∀cs2. ∃∃cs1. 𝐈⦃cs1⦄ & cs1 ⊚ cs2 ≡ cs2. -#cs2 elim cs2 -cs2 /2 width=3 by after_empty, ex2_intro/ -#b #cs2 * /3 width=3 by isid_true, after_true, ex2_intro/ -qed-. - -lemma isid_after_dx: ∀cs1. ∃∃cs2. 𝐈⦃cs2⦄ & cs1 ⊚ cs2 ≡ cs1. -#cs1 elim cs1 -cs1 /2 width=3 by after_empty, ex2_intro/ -* #cs1 * /3 width=3 by isid_true, after_true, after_false, ex2_intro/ -qed-. - -lemma after_isid_sn: ∀cs1,cs2. cs1 ⊚ cs2 ≡ cs2 → 𝐈⦃cs1⦄ . -#cs1 #cs2 #H elim (after_inv_length … H) -H // -qed. - -lemma after_isid_dx: ∀cs1,cs2. cs1 ⊚ cs2 ≡ cs1 → 𝐈⦃cs2⦄ . -#cs1 #cs2 #H elim (after_inv_length … H) -H // -qed. - -(* Inversion lemmas on composition ******************************************) - -lemma after_isid_inv_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 after_isid_inv_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-. - -lemma after_inv_isid3: ∀t1,t2,t. t1 ⊚ t2 ≡ t → 𝐈⦃t⦄ → 𝐈⦃t1⦄ ∧ 𝐈⦃t2⦄. -#t1 #t2 #t #H elim H -t1 -t2 -t -[ /2 width=1 by conj/ -| #t1 #t2 #t #_ #b #IHt #H elim (isid_inv_cons … H) -H - #Ht #H elim (IHt Ht) -t /2 width=1 by isid_true, conj/ -| #t1 #t2 #t #_ #_ #H elim (isid_inv_false … H) -] -qed-. - -(* Forward on inclusion *****************************************************) - -lemma sle_isid1_fwd: ∀t1,t2. t1 ⊆ t2 → 𝐈⦃t1⦄ → t1 = t2. -#t1 #t2 #H elim H -t1 -t2 // -[ #t1 #t2 #_ #IH #H lapply (isid_inv_true … H) -H - #HT1 @eq_f2 // @IH @HT1 (**) (* full auto fails *) -| #t1 #t2 #b #_ #_ #H elim (isid_inv_false … H) -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_isun.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_isun.ma deleted file mode 100644 index bdcb249c5..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_isun.ma +++ /dev/null @@ -1,48 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/isuniform_1.ma". -include "ground_2/relocation/trace_isid.ma". - -(* RELOCATION TRACE *********************************************************) - -inductive isun: predicate trace ≝ -| isun_id : ∀t. 𝐈⦃t⦄ → isun t -| isun_false: ∀t. isun t → isun (Ⓕ@t) -. - -interpretation "test for uniformity (trace)" - 'IsUniform t = (isun t). - -(* Basic inversion lennas ***************************************************) - -fact isun_inv_true_aux: ∀t. 𝐔⦃t⦄ → ∀u. t = Ⓣ@u → 𝐈⦃u⦄. -#t * -t -[ #t #Ht #u #H destruct /2 width=1 by isid_inv_true/ -| #t #_ #u #H destruct -] -qed-. - -lemma isun_inv_true: ∀t. 𝐔⦃Ⓣ@t⦄ → 𝐈⦃t⦄. -/2 width=3 by isun_inv_true_aux/ qed-. - -fact isun_inv_false_aux: ∀t. 𝐔⦃t⦄ → ∀u. t = Ⓕ@u → 𝐔⦃u⦄. -#t * -t -[ #t #Ht #u #H destruct elim (isid_inv_false … Ht) -| #t #Ht #u #H destruct // -] -qed-. - -lemma isun_inv_false: ∀t. 𝐔⦃Ⓕ@t⦄ → 𝐔⦃t⦄. -/2 width=3 by isun_inv_false_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sle.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sle.ma deleted file mode 100644 index be738b18e..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sle.ma +++ /dev/null @@ -1,60 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/trace_at.ma". - -(* RELOCATION TRACE *********************************************************) - -inductive sle: relation trace ≝ -| sle_empty: sle (◊) (◊) -| sle_true : ∀t1,t2. sle t1 t2 → sle (Ⓣ @ t1) (Ⓣ @ t2) -| sle_false: ∀t1,t2,b. sle t1 t2 → sle (Ⓕ @ t1) (b @ t2) -. - -interpretation - "inclusion (trace)" - 'subseteq t1 t2 = (sle t1 t2). - -(* Basic properties *********************************************************) - -(* Basic forward lemmas *****************************************************) - -lemma sle_fwd_length: ∀t1,t2. t1 ⊆ t2 → |t1| = |t2|. -#t1 #t2 #H elim H -t1 -t2 // -qed-. - -lemma sle_fwd_colength: ∀t1,t2. t1 ⊆ t2 → ∥t1∥ ≤ ∥t2∥. -#t1 #t2 #H elim H -t1 -t2 /2 width=1 by le_S_S/ -#t1 #t2 * /2 width=1 by le_S/ -qed-. - -(* Inversion lemmas on application ******************************************) - -lemma sle_inv_at: ∀t1,t2. t1 ⊆ t2 → - ∀i,i1,i2. @⦃i, t1⦄ ≡ i1 → @⦃i, t2⦄ ≡ i2 → i2 ≤ i1. -#t1 #t2 #H elim H -t1 -t2 -[ #i #i1 #i2 #_ #H2 elim (at_inv_empty … H2) -H2 // -| #t1 #t2 #_ #IH #i #i1 #i2 #H0 #H2 elim (at_inv_true … H2) -H2 * // - #j1 #j2 #H1 #H2 #Hj destruct elim (at_inv_true_succ_sn … H0) -H0 - /3 width=3 by le_S_S/ -| #t1 #t2 * #_ #IH #i #i1 #i2 #H0 #H2 - [ elim (at_inv_true … H2) -H2 * // - #j #j2 #H1 #H2 #Hj2 destruct elim (at_inv_false … H0) -H0 - #j1 #H #Hj1 destruct elim (at_monotonic … Hj1 j) -Hj1 // - #x #H1x #H2x @le_S_S /4 width=3 by lt_to_le, le_to_lt_to_lt/ (**) (* full auto too slow *) - | elim (at_inv_false … H2) elim (at_inv_false … H0) -H0 -H2 - /3 width=3 by le_S_S/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_snot.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_snot.ma deleted file mode 100644 index d1697b9cc..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_snot.ma +++ /dev/null @@ -1,50 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/complement_1.ma". -include "ground_2/relocation/trace.ma". - -(* RELOCATION TRACE *********************************************************) - -let rec snot (t:trace) on t ≝ match t with -[ nil ⇒ ◊ -| cons b t ⇒ (¬ b) @ snot t -]. - -interpretation - "complement (trace)" - 'Complement t = (snot t). - -(* Basic properties *********************************************************) - -lemma snot_empty: ∁ (◊) = ◊. -// qed. - -lemma snot_inh: ∀t,b. ∁ (b@t) = (¬ b) @ ∁ t. -// qed. - -lemma snot_true: ∀t. ∁ (Ⓣ @ t) = Ⓕ @ ∁ t. -// qed. - -lemma snot_false: ∀t. ∁ (Ⓕ @ t) = Ⓣ @ ∁ t. -// qed. - -lemma snot_length: ∀t. |∁ t| = |t|. -#t elim t -t normalize // -qed. - -lemma snot_colength: ∀t. ∥∁ t∥ = |t| - ∥t∥. -#t elim t -t // -* /2 width=1 by minus_Sn_m/ -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 deleted file mode 100644 index 65aba02ac..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sor.ma +++ /dev/null @@ -1,62 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/runion_3.ma". -include "ground_2/relocation/trace_isid.ma". - -(* RELOCATION TRACE *********************************************************) - -inductive sor: relation3 trace trace trace ≝ - | sor_empty: sor (◊) (◊) (◊) - | sor_inh : ∀cs1,cs2,cs. sor cs1 cs2 cs → - ∀b1,b2. sor (b1 @ cs1) (b2 @ cs2) ((b1 ∨ b2) @ cs). - -interpretation - "union (trace)" - 'RUnion L1 L2 L = (sor L2 L1 L). - -(* 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 b1b08518f..d35679f25 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_eq ( ? ≗ ? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_sle ( ? ⊆ ? )" * ] - [ "nstream" "nstream_lift ( ↑? ) ( ⫯? )" "nstream_eq" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? ) ( ? ⊚ ? ≡ ? )" * ] + [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ↓? )" "rtmap_minus ( ? - ? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_sle ( ? ⊆ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" * ] + [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" * ] [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )" "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ] [ "mr2" "mr2_at ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" * ]