From: Ferruccio Guidi Date: Tue, 15 Jan 2013 20:08:08 +0000 (+0000) Subject: - some additions and renaming ... X-Git-Tag: make_still_working~1342 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=81fc94f4f091ec35d41e2711207218d255b75273;p=helm.git - some additions and renaming ... --- diff --git a/matita/matita/contribs/lambda/paths/alternative_standard_order.ma b/matita/matita/contribs/lambda/paths/alternative_standard_order.ma index 144c1dabf..e8eca4f11 100644 --- a/matita/matita/contribs/lambda/paths/alternative_standard_order.ma +++ b/matita/matita/contribs/lambda/paths/alternative_standard_order.ma @@ -26,7 +26,7 @@ lemma slt_step_rc: ∀p,q. p ≺ q → p < q. /2 width=1/ qed. -lemma slt_nil: ∀c,p. ◊ < c::p. +lemma slt_nil: ∀o,p. ◊ < o::p. /2 width=1/ qed. @@ -34,8 +34,8 @@ lemma slt_skip: dx::◊ < ◊. /2 width=1/ qed. -lemma slt_comp: ∀c,p,q. p < q → c::p < c::q. -#c #p #q #H elim H -q /3 width=1/ /3 width=3/ +lemma slt_comp: ∀o,p,q. p < q → o::p < o::q. +#o #p #q #H elim H -q /3 width=1/ /3 width=3/ qed. theorem slt_trans: transitive … slt. diff --git a/matita/matita/contribs/lambda/paths/labeled_st_computation.ma b/matita/matita/contribs/lambda/paths/labeled_st_computation.ma new file mode 100644 index 000000000..8ee4d304f --- /dev/null +++ b/matita/matita/contribs/lambda/paths/labeled_st_computation.ma @@ -0,0 +1,113 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "paths/standard_trace.ma". +include "paths/labeled_sequential_computation.ma". +include "paths/labeled_st_reduction.ma". + +(* PATH-LABELED STANDARD COMPUTATION (MULTISTEP) ****************************) + +(* Note: lstar shuld be replaced by l_sreds *) +definition pl_sts: trace → relation subterms ≝ lstar … pl_st. + +interpretation "path-labeled standard reduction" + 'StdStar F p G = (pl_sts p F G). + +notation "hvbox( F break Ⓡ ↦* [ term 46 p ] break term 46 G )" + non associative with precedence 45 + for @{ 'StdStar $F $p $G }. + +lemma pl_sts_fwd_pl_sreds: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → ⇓F1 ↦*[s] ⇓F2. +#s #F1 #F2 #H @(lstar_ind_r ????????? H) -s -F2 // +#p #s #F #F2 #_ #HF2 #IHF1 +lapply (pl_st_fwd_pl_sred … HF2) -HF2 /2 width=3/ +qed-. + +lemma pl_sts_refl: reflexive … (pl_sts (◊)). +// +qed. + +lemma pl_sts_step_sn: ∀p,F1,F. F1 Ⓡ↦[p] F → ∀s,F2. F Ⓡ↦*[s] F2 → F1 Ⓡ↦*[p::s] F2. +/2 width=3/ +qed-. + +lemma pl_sts_step_dx: ∀s,F1,F. F1 Ⓡ↦*[s] F → ∀p,F2. F Ⓡ↦[p] F2 → F1 Ⓡ↦*[s@p::◊] F2. +/2 width=3/ +qed-. + +lemma pl_sts_step_rc: ∀p,F1,F2. F1 Ⓡ↦[p] F2 → F1 Ⓡ↦*[p::◊] F2. +/2 width=1/ +qed. + +lemma pl_sts_inv_nil: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → ◊ = s → F1 = F2. +/2 width=5 by lstar_inv_nil/ +qed-. + +lemma pl_sts_inv_cons: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → ∀q,r. q::r = s → + ∃∃F. F1 Ⓡ↦[q] F & F Ⓡ↦*[r] F2. +/2 width=3 by lstar_inv_cons/ +qed-. + +lemma pl_sts_inv_step_rc: ∀p,F1,F2. F1 Ⓡ↦*[p::◊] F2 → F1 Ⓡ↦[p] F2. +/2 width=1 by lstar_inv_step/ +qed-. + +lemma pl_sts_inv_pos: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → 0 < |s| → + ∃∃p,r,F. p::r = s & F1 Ⓡ↦[p] F & F Ⓡ↦*[r] F2. +/2 width=1 by lstar_inv_pos/ +qed-. + +lemma pl_sts_lift: ∀s. sliftable (pl_sts s). +/2 width=1/ +qed. + +lemma pl_sts_inv_lift: ∀s. sdeliftable_sn (pl_sts s). +/3 width=3 by lstar_sdeliftable_sn, pl_st_inv_lift/ +qed-. + +lemma pl_sts_dsubst: ∀s. sdsubstable_f_dx … (booleanized ⊥) (pl_sts s). +/2 width=1/ +qed. + +theorem pl_sts_mono: ∀s. singlevalued … (pl_sts s). +/3 width=7 by lstar_singlevalued, pl_st_mono/ +qed-. + +theorem pl_sts_trans: ltransitive … pl_sts. +/2 width=3 by lstar_ltransitive/ +qed-. + +theorem pl_sts_fwd_is_standard: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → is_standard s. +#s elim s -s // #p1 * // +#p2 #s #IHs #F1 #F2 #H +elim (pl_sts_inv_cons … H ???) -H [4: // |2,3: skip ] #F3 #HF13 #H (**) (* simplify line *) +elim (pl_sts_inv_cons … H ???) [2: // |3,4: skip ] #F4 #HF34 #_ (**) (* simplify line *) +lapply (pl_st_fwd_sle … HF13 … HF34) -F1 -F4 /3 width=3/ +qed-. + +axiom pl_sred_is_standard_pl_st: ∀p,M,M2. M ↦[p] M2 → ∀F. ⇓F = M → + ∀s,M1.{⊤}⇑ M1 Ⓡ↦*[s] F → + is_standard (s@(p::◊)) → + ∃∃F2. F Ⓡ↦[p] F2 & ⇓F2 = M2. + +theorem pl_sreds_is_standard_pl_sts: ∀s,M1,M2. M1 ↦*[s] M2 → is_standard s → + ∃∃F2. {⊤}⇑ M1 Ⓡ↦*[s] F2 & ⇓F2 = M2. +#s #M1 #M2 #H @(lstar_ind_r ????????? H) -s -M2 /2 width=3/ +#p #s #M #M2 #_ #HM2 #IHM1 #Hsp +lapply (is_standard_fwd_append_sn … Hsp) #Hs +elim (IHM1 Hs) -IHM1 -Hs #F #HM1 #H +elim (pl_sred_is_standard_pl_st … HM2 … HM1 ?) -HM2 // -M -Hsp #F2 #HF2 #HFM2 +lapply (pl_sts_step_dx … HM1 … HF2) -F +#H @(ex2_intro … F2) // (**) (* auto needs some help here *) +qed-. diff --git a/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma b/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma index f6f93d6fb..101954e59 100644 --- a/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma +++ b/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma @@ -12,7 +12,8 @@ (* *) (**************************************************************************) -include "subterms/booleanize.ma". +include "subterms/booleanized.ma". +include "paths/labeled_sequential_reduction.ma". include "paths/standard_order.ma". (* PATH-LABELED STANDARD REDUCTION ON SUBTERMS (SINGLE STEP) ****************) @@ -33,44 +34,47 @@ interpretation "path-labeled standard reduction" notation "hvbox( F break Ⓡ ↦ [ term 46 p ] break term 46 G )" non associative with precedence 45 for @{ 'Std $F $p $G }. -(* -lemma pl_st_inv_pl_sred: ∀p,F,G. F Ⓡ↦[p] G → ⇓F ↦[p] ⇓G. -#p #F #G #H elim H -p -F -G // /2 width=1/ + +lemma pl_st_fwd_pl_sred: ∀p,F1,F2. F1 Ⓡ↦[p] F2 → ⇓F1 ↦[p] ⇓F2. +#p #F1 #F2 #H elim H -p -F1 -F2 normalize /2 width=1/ qed-. lemma pl_st_inv_vref: ∀p,F,G. F Ⓡ↦[p] G → ∀b,i. {b}#i = F → ⊥. -/3 width=5 by pl_st_inv_st, st_inv_vref/ +#p #F #G #HFG #b #i #H +lapply (pl_st_fwd_pl_sred … HFG) -HFG #HFG +lapply (eq_f … carrier … H) -H normalize #H +/2 width=6 by pl_sred_inv_vref/ qed-. -*) -lemma pl_st_inv_abst: ∀p,F,G. F Ⓡ↦[p] G → ∀b0,U1. {b0}𝛌.U1 = F → + +lemma pl_st_inv_abst: ∀p,F,G. F Ⓡ↦[p] G → ∀c,U1. {c}𝛌.U1 = F → ∃∃q,U2. U1 Ⓡ↦[q] U2 & rc::q = p & {⊥}𝛌.U2 = G. #p #F #G * -p -F -G -[ #V #T #b0 #U1 #H destruct -| #b #p #T1 #T2 #HT12 #b0 #U1 #H destruct /2 width=5/ -| #b #p #V1 #V2 #T #_ #b0 #U1 #H destruct -| #b #p #V #T1 #T2 #_ #b0 #U1 #H destruct +[ #V #T #c #U1 #H destruct +| #b #p #T1 #T2 #HT12 #c #U1 #H destruct /2 width=5/ +| #b #p #V1 #V2 #T #_ #c #U1 #H destruct +| #b #p #V #T1 #T2 #_ #c #U1 #H destruct ] qed-. -lemma pl_st_inv_appl: ∀p,F,G. F Ⓡ↦[p] G → ∀b0,W,U. {b0}@W.U = F → - ∨∨ (∃∃U0. ⊤ = b0 & ◊ = p & {⊤}𝛌.U0 = U & [↙W] U0 = G) +lemma pl_st_inv_appl: ∀p,F,G. F Ⓡ↦[p] G → ∀c,W,U. {c}@W.U = F → + ∨∨ (∃∃U0. ⊤ = c & ◊ = p & {⊤}𝛌.U0 = U & [↙W] U0 = G) | (∃∃q,W0. sn::q = p & W Ⓡ↦[q] W0 & {⊥}@W0.{⊥}⇕U = G) - | (∃∃q,U0. dx::q = p & U Ⓡ↦[q] U0 & {b0}@W.U0 = G). + | (∃∃q,U0. dx::q = p & U Ⓡ↦[q] U0 & {c}@W.U0 = G). #p #F #G * -p -F -G -[ #V #T #b0 #W #U #H destruct /3 width=3/ -| #b #p #T1 #T2 #_ #b0 #W #U #H destruct -| #b #p #V1 #V2 #T #HV12 #b0 #W #U #H destruct /3 width=5/ -| #b #p #V #T1 #T2 #HT12 #b0 #W #U #H destruct /3 width=5/ +[ #V #T #c #W #U #H destruct /3 width=3/ +| #b #p #T1 #T2 #_ #c #W #U #H destruct +| #b #p #V1 #V2 #T #HV12 #c #W #U #H destruct /3 width=5/ +| #b #p #V #T1 #T2 #HT12 #c #W #U #H destruct /3 width=5/ ] qed-. -lemma pl_st_fwd_abst: ∀p,F,G. F Ⓡ↦[p] G → ∀b0,U2. {b0}𝛌.U2 = G → +lemma pl_st_fwd_abst: ∀p,F,G. F Ⓡ↦[p] G → ∀c,U2. {c}𝛌.U2 = G → ◊ = p ∨ ∃q. rc::q = p. #p #F #G * -p -F -G [ /2 width=1/ | /3 width=2/ -| #b #p #V1 #V2 #T #_ #b0 #U2 #H destruct -| #b #p #V #T1 #T2 #_ #b0 #U2 #H destruct +| #b #p #V1 #V2 #T #_ #c #U2 #H destruct +| #b #p #V #T1 #T2 #_ #c #U2 #H destruct ] qed-. @@ -114,51 +118,53 @@ lemma pl_st_inv_dx: ∀p,F,G. F Ⓡ↦[p] G → ∀q. dx::q = p → ] qed-. - - -(* lemma pl_st_lift: ∀p. sliftable (pl_st p). -#p #h #F1 #F2 #H elim H -p -F1 -F2 normalize /2 width=1/ -[ #V #T #d dsubst_dsubst_ge // +lemma pl_st_dsubst: ∀p. sdsubstable_f_dx … (booleanized ⊥) (pl_st p). +#p #W1 #F1 #F2 #H elim H -p -F1 -F2 /2 width=1/ +[ #W2 #T #d normalize >sdsubst_sdsubst_ge // +| #b #p #V1 #V2 #T #_ #IHV12 #d + whd in ⊢ (??%%); <(booleanized_booleanized ⊥) in ⊢ (???(???%)); (sdsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) // ] qed. + +lemma carrier_boolean: ∀b,M. ⇓ {b}⇑ M = M. +#b #M elim M -M normalize // +qed. diff --git a/matita/matita/contribs/lambda/subterms/booleanize.ma b/matita/matita/contribs/lambda/subterms/booleanize.ma deleted file mode 100644 index f49a95335..000000000 --- a/matita/matita/contribs/lambda/subterms/booleanize.ma +++ /dev/null @@ -1,57 +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 "subterms/carrier.ma". -include "subterms/boolean.ma". - -(* BOOLEANIZE (EMPTY OR FILL) **********************************************) - -definition booleanize: bool → subterms → subterms ≝ - λb,F. {b}⇑⇓F. - -interpretation "make boolean (subterms)" - 'ProjectSame b F = (booleanize b F). - -notation "hvbox( { term 46 b } ⇕ break term 46 F)" - non associative with precedence 46 - for @{ 'ProjectSame $b $F }. - -lemma booleanize_inv_vref: ∀j,b0,b,F. {b}⇕ F = {b0}#j → - ∃∃b1. b = b0 & F = {b1}#j. -#j #b0 #b #F #H -elim (boolean_inv_vref … H) -H #H0 #H -elim (carrier_inv_vref … H) -H /2 width=2/ -qed-. - -lemma booleanize_inv_abst: ∀U,b0,b,F. {b}⇕ F = {b0}𝛌.U → - ∃∃b1,T. b = b0 & {b}⇕T = U & F = {b1}𝛌.T. -#U #b0 #b #F #H -elim (boolean_inv_abst … H) -H #C #H0 #H1 #H -elim (carrier_inv_abst … H) -H #b1 #U1 #H3 destruct /2 width=4/ -qed-. - -lemma booleanize_inv_appl: ∀W,U,b0,b,F. {b}⇕ F = {b0}@W.U → - ∃∃b1,V,T. b = b0 & {b}⇕V = W & {b}⇕T = U & F = {b1}@V.T. -#W #U #b0 #b #F #H -elim (boolean_inv_appl … H) -H #D #C #H0 #H1 #H2 #H -elim (carrier_inv_appl … H) -H #b1 #W1 #U1 #H3 #H4 destruct /2 width=6/ -qed-. -(* -lemma booleanize_lift: ∀b,h,F,d. {b}⇕ ↑[d, h] F = ↑[d, h] {b}⇕ F. -#b #h #M elim M -M normalize // -qed. - -lemma booleanize_dsubst: ∀b,G,F,d. {b}⇕ [d ↙ G] F = [d ↙ {b}⇕ G] {b}⇕ F. -#b #N #M elim M -M [2,3: normalize // ] -*) diff --git a/matita/matita/contribs/lambda/subterms/booleanized.ma b/matita/matita/contribs/lambda/subterms/booleanized.ma new file mode 100644 index 000000000..87b84b26b --- /dev/null +++ b/matita/matita/contribs/lambda/subterms/booleanized.ma @@ -0,0 +1,61 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "subterms/carrier.ma". +include "subterms/boolean.ma". + +(* BOOLEANIZED SUBSET (EMPTY OR FULL) **************************************) + +definition booleanized: bool → subterms → subterms ≝ + λb,F. {b}⇑⇓F. + +interpretation "make boolean (subterms)" + 'ProjectSame b F = (booleanized b F). + +notation "hvbox( { term 46 b } ⇕ break term 46 F)" + non associative with precedence 46 + for @{ 'ProjectSame $b $F }. + +lemma booleanized_inv_vref: ∀j,c,b,F. {b}⇕ F = {c}#j → + ∃∃b1. b = c & F = {b1}#j. +#j #c #b #F #H +elim (boolean_inv_vref … H) -H #H0 #H +elim (carrier_inv_vref … H) -H /2 width=2/ +qed-. + +lemma booleanized_inv_abst: ∀U,c,b,F. {b}⇕ F = {c}𝛌.U → + ∃∃b1,T. b = c & {b}⇕T = U & F = {b1}𝛌.T. +#U #c #b #F #H +elim (boolean_inv_abst … H) -H #C #H0 #H1 #H +elim (carrier_inv_abst … H) -H #b1 #U1 #H3 destruct /2 width=4/ +qed-. + +lemma booleanized_inv_appl: ∀W,U,c,b,F. {b}⇕ F = {c}@W.U → + ∃∃b1,V,T. b = c & {b}⇕V = W & {b}⇕T = U & F = {b1}@V.T. +#W #U #c #b #F #H +elim (boolean_inv_appl … H) -H #D #C #H0 #H1 #H2 #H +elim (carrier_inv_appl … H) -H #b1 #W1 #U1 #H3 #H4 destruct /2 width=6/ +qed-. + +lemma booleanized_booleanized: ∀c,b,F. {b}⇕ {c}⇕ F = {b}⇕ F. +normalize // +qed. + +lemma booleanized_lift: ∀b,h,F,d. {b}⇕ ↑[d, h] F = ↑[d, h] {b}⇕ F. +normalize // +qed. + +lemma booleanized_dsubst: ∀b,G,F,d. {b}⇕ [d ↙ G] F = [d ↙ {b}⇕ G] {b}⇕ F. +normalize // +qed. diff --git a/matita/matita/contribs/lambda/subterms/relocating_substitution.ma b/matita/matita/contribs/lambda/subterms/relocating_substitution.ma index 43702a703..f49a7191d 100644 --- a/matita/matita/contribs/lambda/subterms/relocating_substitution.ma +++ b/matita/matita/contribs/lambda/subterms/relocating_substitution.ma @@ -132,22 +132,31 @@ lapply (ltn_to_ltO … Hd21) #Hd1 >sdsubst_sdsubst_ge in ⊢ (???%); /2 width=1/ (tri_lt ???? … Hid) -Hid -Hjd // | #H destruct >tri_eq in Hjd; #H @@ -56,9 +56,9 @@ lemma slift_inv_vref_lt: ∀b0,j,d. j < d → ∀h,E. ↑[d, h] E = {b0}#j → E ] qed. -lemma slift_inv_vref_ge: ∀b0,j,d. d ≤ j → ∀h,E. ↑[d, h] E = {b0}#j → - d + h ≤ j ∧ E = {b0}#(j-h). -#b0 #j #d #Hdj #h * normalize +lemma slift_inv_vref_ge: ∀c,j,d. d ≤ j → ∀h,E. ↑[d, h] E = {c}#j → + d + h ≤ j ∧ E = {c}#(j-h). +#c #j #d #Hdj #h * normalize [ #b #i elim (lt_or_eq_or_gt i d) #Hid [ >(tri_lt ???? … Hid) #H destruct lapply (le_to_lt_to_lt … Hdj Hid) -Hdj -Hid #H @@ -71,29 +71,29 @@ lemma slift_inv_vref_ge: ∀b0,j,d. d ≤ j → ∀h,E. ↑[d, h] E = {b0}#j → ] qed-. -lemma slift_inv_vref_be: ∀b0,j,d,h. d ≤ j → j < d + h → ∀E. ↑[d, h] E = {b0}#j → ⊥. -#b0 #j #d #h #Hdj #Hjdh #E #H elim (slift_inv_vref_ge … H) -H // -Hdj #Hdhj #_ -E +lemma slift_inv_vref_be: ∀c,j,d,h. d ≤ j → j < d + h → ∀E. ↑[d, h] E = {c}#j → ⊥. +#c #j #d #h #Hdj #Hjdh #E #H elim (slift_inv_vref_ge … H) -H // -Hdj #Hdhj #_ -E lapply (lt_to_le_to_lt … Hjdh Hdhj) -d -h #H elim (lt_refl_false … H) qed-. -lemma slift_inv_vref_ge_plus: ∀b0,j,d,h. d + h ≤ j → - ∀E. ↑[d, h] E = {b0}#j → E = {b0}#(j-h). -#b0 #j #d #h #Hdhj #E #H elim (slift_inv_vref_ge … H) -H // -E /2 width=2/ +lemma slift_inv_vref_ge_plus: ∀c,j,d,h. d + h ≤ j → + ∀E. ↑[d, h] E = {c}#j → E = {c}#(j-h). +#c #j #d #h #Hdhj #E #H elim (slift_inv_vref_ge … H) -H // -E /2 width=2/ qed. -lemma slift_inv_abst: ∀b0,U,d,h,E. ↑[d, h] E = {b0}𝛌.U → - ∃∃T. ↑[d+1, h] T = U & E = {b0}𝛌.T. -#b0 #U #d #h * normalize +lemma slift_inv_abst: ∀c,U,d,h,E. ↑[d, h] E = {c}𝛌.U → + ∃∃T. ↑[d+1, h] T = U & E = {c}𝛌.T. +#c #U #d #h * normalize [ #b #i #H destruct | #b #T #H destruct /2 width=3/ | #b #V #T #H destruct ] qed-. -lemma slift_inv_appl: ∀b0,W,U,d,h,E. ↑[d, h] E = {b0}@W.U → - ∃∃V,T. ↑[d, h] V = W & ↑[d, h] T = U & E = {b0}@V.T. -#b0 #W #U #d #h * normalize +lemma slift_inv_appl: ∀c,W,U,d,h,E. ↑[d, h] E = {c}@W.U → + ∃∃V,T. ↑[d, h] V = W & ↑[d, h] T = U & E = {c}@V.T. +#c #W #U #d #h * normalize [ #b #i #H destruct | #b #T #H destruct | #b #V #T #H destruct /2 width=5/ diff --git a/matita/matita/contribs/lambda/subterms/subterms.ma b/matita/matita/contribs/lambda/subterms/subterms.ma index 909515122..6c75a3f4c 100644 --- a/matita/matita/contribs/lambda/subterms/subterms.ma +++ b/matita/matita/contribs/lambda/subterms/subterms.ma @@ -16,7 +16,7 @@ include "background/preamble.ma". (* SUBSETS OF SUBTERMS ******************************************************) -(* Policy: boolean marks metavariables: b +(* Policy: boolean marks metavariables: b,c subterms metavariables: F,G,T,U,V,W *) (* Note: each subterm is marked with true if it belongs to the subset *) diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma index a34ac3c9c..a51998ae4 100644 --- a/matita/matita/lib/basics/lists/list.ma +++ b/matita/matita/lib/basics/lists/list.ma @@ -445,12 +445,18 @@ lemma All_nth : ∀A,P,n,l. ] ] qed. +(**************************** Allr ******************************) + let rec Allr (A:Type[0]) (R:relation A) (l:list A) on l : Prop ≝ match l with [ nil ⇒ True | cons a1 l ⇒ match l with [ nil ⇒ True | cons a2 _ ⇒ R a1 a2 ∧ Allr A R l ] ]. +lemma Allr_fwd_append_sn: ∀A,R,l1,l2. Allr A R (l1@l2) → Allr A R l1. +#A #R #l1 elim l1 -l1 // #a1 * // #a2 #l1 #IHl1 #l2 * /3 width=2/ +qed-. + (**************************** Exists *******************************) let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝