From: Ferruccio Guidi Date: Mon, 16 Jan 2012 12:09:42 +0000 (+0000) Subject: the support for candidates of reducibility continues ... X-Git-Tag: make_still_working~1975 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5c213ad3e00d815eca11b65ee50d71af82873d6e;p=helm.git the support for candidates of reducibility continues ... --- diff --git a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt index da672ace3..0d06d98b5 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt +++ b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt @@ -74,6 +74,9 @@ csuba/getl csuba_getl_abst csuba/getl csuba_getl_abst_rev csuba/getl csuba_getl_abbr_rev csuba/props csuba_refl + +# check ############################################################# + csubc/arity csubc_arity_conf csubc/arity csubc_arity_trans csubc/clear csubc_clear_conf @@ -89,6 +92,9 @@ csubc/fwd csubc_gen_sort_r csubc/fwd csubc_gen_head_r csubc/getl csubc_getl_conf csubc/props csubc_refl + +# waiting #################################################################### + csubt/clear csubt_clear_conf csubt/csuba csubt_csuba csubt/drop csubt_drop_flat @@ -114,10 +120,8 @@ csubv/props csubv_bind_same csubv/props csubv_refl drop1/fwd drop1_gen_pnil drop1/fwd drop1_gen_pcons -drop1/getl drop1_getl_trans drop1/props drop1_skip_bind drop1/props drop1_cons_tail -drop1/props drop1_trans drop/props drop_ctail ex0/props aplus_gz_le ex0/props aplus_gz_ge @@ -146,10 +150,6 @@ leq/props leq_sym leq/props leq_trans leq/props leq_ahead_false_1 leq/props leq_ahead_false_2 -lift1/fwd lift1_sort -lift1/fwd lift1_lref -lift1/fwd lift1_bind -lift1/fwd lift1_flat lift1/fwd lift1_cons_tail lift1/fwd lifts1_flat lift1/fwd lifts1_nil diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma index a2c5045e0..002fe0171 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma @@ -12,43 +12,50 @@ (* *) (**************************************************************************) +include "Basic_2/unfold/lifts_lifts.ma". +include "Basic_2/unfold/ldrops_ldrops.ma". include "Basic_2/static/aaa.ma". include "Basic_2/computation/lsubc.ma". -(* -axiom lsubc_ldrops_trans: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀K2,des. ⇩[des] L2 ≡ K2 → - ∃∃K1. ⇩[des] L1 ≡ K1 & K1 [RP] ⊑ K2. -*) + +(* NOTE: The constant (0) can not be generalized *) +axiom lsubc_ldrop_trans: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 → + ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 [RP] ⊑ K2. + axiom ldrops_lsubc_trans: ∀RP,L1,K1,des. ⇩*[des] L1 ≡ K1 → ∀K2. K1 [RP] ⊑ K2 → ∃∃L2. L1 [RP] ⊑ L2 & ⇩*[des] L2 ≡ K2. -axiom ldrops_trans: ∀L1,L,des1. ⇩*[des1] L1 ≡ L → ∀L2,des2. ⇩*[des2] L ≡ L2 → - ⇩*[des2 @ des1] L1 ≡ L2. - (* ABSTRACT COMPUTATION PROPERTIES ******************************************) (* Main propertis ***********************************************************) -axiom aacr_aaa_csubc_lifts: ∀RR,RS,RP. +axiom aacr_aaa_csubc_lifts: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → ∀L1,T,A. L1 ⊢ T ÷ A → ∀L0,des. ⇩*[des] L0 ≡ L1 → ∀T0. ⇧*[des] T ≡ T0 → ∀L2. L2 [RP] ⊑ L0 → ⦃L2, T0⦄ [RP] ϵ 〚A〛. (* #RR #RS #RP #H1RP #H2RP #L1 #T #A #H elim H -L1 -T -A -[ (*#L #k #L2 #HL2 +[ #L #k #L0 #des #HL0 #X #H #L2 #HL20 + >(lifts_inv_sort1 … H) -H lapply (aacr_acr … H1RP H2RP 𝕒) #HAtom - @(s2 … HAtom … ◊) // /2 width=2/ *) -| (* * #L #K #V #B #i #HLK #_ #IHB #L2 #HL2 + @(s2 … HAtom … ◊) // /2 width=2/ +| * #L #K #V #B #i #HLK #_ #IHB #L0 #des #HL0 #X #H #L2 #HL20 + elim (lifts_inv_lref1 … H) -H #i0 #Hi0 #H destruct + elim (ldrops_ldrop_trans … HL0 … HLK) -L #L #des1 #i1 #HL0 #HLK #Hi1 #Hdes1 + + elim (lsubc_ldrop_trans … HL20 … HL0) -L0 #L0 #HL20 #HL0 [ | lapply (aacr_acr … H1RP H2RP B) #HB @(s2 … HB … ◊) // -(* @(cp2 … H1RP) *) - ] *) -| (* #L #V #T #B #A #_ #_ #IHB #IHA #L2 #HL2 + @(cp2 … H1RP) + ] + +| #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20 + elim (lifts_inv_bind1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct lapply (aacr_acr … H1RP H2RP A) #HA lapply (aacr_acr … H1RP H2RP B) #HB lapply (s1 … HB) -HB #HB - @(s5 … HA … ◊ ◊) // /3 width=1/ *) + @(s5 … HA … ◊ ◊) // /3 width=5/ | #L #W #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02 elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct @(aacr_abst … H1RP H2RP) @@ -60,11 +67,14 @@ axiom aacr_aaa_csubc_lifts: ∀RR,RS,RP. @(IHA (L2. 𝕓{Abst} W2) … (ss des @ ss des3)) /2 width=3/ /3 width=5/ /4 width=6/ ] -| /3 width=1/ -| #L #V #T #A #_ #_ #IH1A #IH2A #L2 #HL2 +| #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20 + elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct + /3 width=10/ +| #L #V #T #A #_ #_ #IH1A #IH2A #L0 #des #HL0 #X #H #L2 #HL20 + elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct lapply (aacr_acr … H1RP H2RP A) #HA lapply (s1 … HA) #H - @(s6 … HA … ◊) /2 width=1/ /3 width=1/ + @(s6 … HA … ◊) /2 width=5/ /3 width=5/ ] *) lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma index 77f782298..cad6aba67 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "Basic_2/grammar/aarity.ma". -include "Basic_2/unfold/lifts_lifts_vector.ma". +include "Basic_2/unfold/lifts_lift_vector.ma". include "Basic_2/computation/acp.ma". (* ABSTRACT COMPUTATION PROPERTIES ******************************************) @@ -119,7 +119,7 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → elim (lift_total V10 0 1) #V20 #HV120 elim (liftv_total 0 1 V10s) #V20s #HV120s @(s5 … IHA … (V10 :: V10s) (V20 :: V20s)) /2 width=1/ /2 width=6 by rp_lifts/ - @(HA … (ss des)) /2 width=1/ + @(HA … (des + 1)) /2 width=1/ [ @(s7 … IHB … HB … HV120) /2 width=1/ | @liftsv_applv // elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s @@ -135,7 +135,7 @@ qed. lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → ∀L,W,T,A,B. RP L W → ( - ∀L0,V0,T0,des. ⇩*[des] L0 ≡ L → ⇧*[ss des] T ≡ T0 → + ∀L0,V0,T0,des. ⇩*[des] L0 ≡ L → ⇧*[des + 1] T ≡ T0 → ⦃L0, V0⦄ [RP] ϵ 〚B〛 → ⦃L0. 𝕓{Abbr} V0, T0⦄ [RP] ϵ 〚A〛 ) → ⦃L, 𝕓{Abst} W. T⦄ [RP] ϵ 〚𝕔 B. A〛. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma index a801fae21..813630dae 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma @@ -112,6 +112,14 @@ notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ▶ break T2 )" (* Unfold *******************************************************************) +notation "hvbox( @ [ T1 ] break f ≡ break T2 )" + non associative with precedence 45 + for @{ 'RAt $T1 $f $T2 }. + +notation "hvbox( T1 ▭ break T2 ≡ break T )" + non associative with precedence 45 + for @{ 'RMinus $T1 $T2 $T }. + notation "hvbox( ⇧ * [ e ] break T1 ≡ break T2 )" non associative with precedence 45 for @{ 'RLiftStar $e $T1 $T2 }. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma index 5c7a28bd2..b588b29b7 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma @@ -15,7 +15,7 @@ include "Basic_2/grammar/term_weight.ma". include "Basic_2/grammar/term_simple.ma". -(* RELOCATION ***************************************************************) +(* BASIC TERM RELOCATION ****************************************************) (* Basic_1: includes: lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma index d207ebf23..30bf8886e 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma @@ -14,7 +14,7 @@ include "Basic_2/substitution/lift.ma". -(* RELOCATION ***************************************************************) +(* BASIC TERM RELOCATION ****************************************************) (* Main properies ***********************************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift_vector.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift_vector.ma index 7513a5abe..cfb7b9250 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift_vector.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift_vector.ma @@ -15,7 +15,7 @@ include "Basic_2/substitution/lift_lift.ma". include "Basic_2/substitution/lift_vector.ma". -(* RELOCATION ***************************************************************) +(* BASIC TERM VECTOR RELOCATION *********************************************) (* Main properies ***********************************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_vector.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_vector.ma index 710ab34cd..aa0a30f95 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_vector.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_vector.ma @@ -15,7 +15,7 @@ include "Basic_2/grammar/term_vector.ma". include "Basic_2/substitution/lift.ma". -(* RELOCATION ***************************************************************) +(* BASIC TERM VECTOR RELOCATION *********************************************) inductive liftv (d,e:nat) : relation (list term) ≝ | liftv_nil : liftv d e ◊ ◊ diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2.ma new file mode 100644 index 000000000..a33f018c2 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2.ma @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "Basic_2/grammar/term_vector.ma". + +(* GENERIC RELOCATION WITH PAIRS ********************************************) + +let rec pluss (des:list2 nat nat) (i:nat) on des ≝ match des with +[ nil2 ⇒ ⟠ +| cons2 d e des ⇒ {d + i, e} :: pluss des i +]. + +interpretation "plus (generic relocation with pairs)" + 'plus x y = (pluss x y). + +inductive at: list2 nat nat → relation nat ≝ +| at_nil: ∀i. at ⟠ i i +| at_lt : ∀des,d,e,i1,i2. i1 < d → + at des i1 i2 → at ({d, e} :: des) i1 i2 +| at_ge : ∀des,d,e,i1,i2. d ≤ i1 → + at des (i1 + e) i2 → at ({d, e} :: des) i1 i2 +. + +interpretation "application (generic relocation with pairs)" + 'RAt i1 des i2 = (at des i1 i2). + +inductive minuss: nat → relation (list2 nat nat) ≝ +| minuss_nil: ∀i. minuss i ⟠ ⟠ +| minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 → + minuss i ({d, e} :: des1) ({d - i, e} :: des2) +| minuss_ge : ∀des1,des2,d,e,i. d ≤ i → minuss (e + i) des1 des2 → + minuss i ({d, e} :: des1) des2 +. + +interpretation "minus (generic relocation with pairs)" + 'RMinus des1 i des2 = (minuss i des1 des2). diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma index 077bee168..1bf80b5be 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma @@ -29,7 +29,7 @@ interpretation "generic local environment slicing" (* Basic properties *********************************************************) lemma ldrops_skip: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → ∀V1,V2. ⇧*[des] V2 ≡ V1 → - ∀I. ⇩*[ss des] L1. 𝕓{I} V1 ≡ L2. 𝕓{I} V2. + ∀I. ⇩*[des + 1] L1. 𝕓{I} V1 ≡ L2. 𝕓{I} V2. #L1 #L2 #des #H elim H -L1 -L2 -des [ #L #V1 #V2 #HV12 #I >(lifts_inv_nil … HV12) -HV12 // @@ -37,3 +37,14 @@ lemma ldrops_skip: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → ∀V1,V2. ⇧*[des] V2 elim (lifts_inv_cons … H) -H /3 width=5/ ]. qed. + +(* Basic_1: removed theorems 1: drop1_getl_trans +*) +(* +lemma ldrops_inv_skip2: ∀des2,L1,I,K2,V2. ⇩*[des2] L1 ≡ K2. 𝕓{I} V2 → + ∀des,i. des ▭ i ≡ des2 → + ∃∃K1,V1,des1. des ▭ (i + 1) ≡ des1 & + ⇩*[des1] K1 ≡ K2 & + ⇧*[des1] V2 ≡ V1 & + L1 = K1. 𝕓{I} V1. +*) \ No newline at end of file diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops_ldrop.ma new file mode 100644 index 000000000..de8a1fef6 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops_ldrop.ma @@ -0,0 +1,35 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "Basic_2/substitution/ldrop_ldrop.ma". +include "Basic_2/unfold/ldrops.ma". + +(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************) + +(* Properties concerning basic local environment slicing ********************) + +lemma ldrops_ldrop_trans: ∀L1,L,des. ⇩*[des] L1 ≡ L → ∀L2,i. ⇩[0, i] L ≡ L2 → + ∃∃L0,des0,i0. ⇩[0, i0] L1 ≡ L0 & ⇩*[des0] L0 ≡ L2 & + @[i] des ≡ i0 & des ▭ i ≡ des0. +#L1 #L #des #H elim H -L1 -L -des +[ /2 width=7/ +| #L1 #L3 #L #des3 #d #e #_ #HL3 #IHL13 #L2 #i #HL2 + elim (lt_or_ge i d) #Hid + [ elim (ldrop_trans_le … HL3 … HL2 ?) -L /2 width=2/ #L #HL3 #HL2 + elim (IHL13 … HL3) -L3 /3 width=7/ + | lapply (ldrop_trans_ge … HL3 … HL2 ?) -L // #HL32 + elim (IHL13 … HL32) -L3 /3 width=7/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops_ldrops.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops_ldrops.ma new file mode 100644 index 000000000..1bb40cb5d --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops_ldrops.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "Basic_2/unfold/ldrops_ldrop.ma". + +(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************) + +(* Main properties **********************************************************) + +(* Basic_1: was: drop1_trans *) +theorem ldrops_trans: ∀L,L2,des2. ⇩*[des2] L ≡ L2 → ∀L1,des1. ⇩*[des1] L1 ≡ L → + ⇩*[des2 @ des1] L1 ≡ L2. +#L #L2 #des2 #H elim H -L -L2 -des2 // /3 width=3/ +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma index 4e005842b..27ddc5174 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma @@ -12,15 +12,10 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/term_vector.ma". include "Basic_2/substitution/lift.ma". +include "Basic_2/unfold/gr2.ma". -(* GENERIC RELOCATION *******************************************************) - -let rec ss (des:list2 nat nat) ≝ match des with -[ nil2 ⇒ ⟠ -| cons2 d e des ⇒ {d + 1, e} :: ss des -]. +(* GENERIC TERM RELOCATION **************************************************) inductive lifts: list2 nat nat → relation term ≝ | lifts_nil : ∀T. lifts ⟠ T T @@ -28,7 +23,7 @@ inductive lifts: list2 nat nat → relation term ≝ ⇧[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} :: des) T1 T2 . -interpretation "generic relocation" +interpretation "generic relocation (term)" 'RLiftStar des T1 T2 = (lifts des T1 T2). (* Basic inversion lemmas ***************************************************) @@ -54,8 +49,40 @@ lemma lifts_inv_cons: ∀T1,T2,d,e,des. ⇧*[{d, e} :: des] T1 ≡ T2 → ∃∃T. ⇧[d, e] T1 ≡ T & ⇧*[des] T ≡ T2. /2 width=3/ qed-. +(* Basic_1: was: lift1_sort *) +lemma lifts_inv_sort1: ∀T2,k,des. ⇧*[des] ⋆k ≡ T2 → T2 = ⋆k. +#T2 #k #des elim des -des +[ #H <(lifts_inv_nil … H) -H // +| #d #e #des #IH #H + elim (lifts_inv_cons … H) -H #X #H + >(lift_inv_sort1 … H) -H /2 width=1/ +] +qed-. + +(* Basic_1: was: lift1_lref *) +lemma lifts_inv_lref1: ∀T2,des,i1. ⇧*[des] #i1 ≡ T2 → + ∃∃i2. @[i1] des ≡ i2 & T2 = #i2. +#T2 #des elim des -des +[ #i1 #H <(lifts_inv_nil … H) -H /2 width=3/ +| #d #e #des #IH #i1 #H + elim (lifts_inv_cons … H) -H #X #H1 #H2 + elim (lift_inv_lref1 … H1) -H1 * #Hdi1 #H destruct + elim (IH … H2) -IH -H2 /3 width=3/ +] +qed-. + +lemma lifts_inv_gref1: ∀T2,p,des. ⇧*[des] §p ≡ T2 → T2 = §p. +#T2 #p #des elim des -des +[ #H <(lifts_inv_nil … H) -H // +| #d #e #des #IH #H + elim (lifts_inv_cons … H) -H #X #H + >(lift_inv_gref1 … H) -H /2 width=1/ +] +qed-. + +(* Basic_1: was: lift1_bind *) lemma lifts_inv_bind1: ∀I,T2,des,V1,U1. ⇧*[des] 𝕓{I} V1. U1 ≡ T2 → - ∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[ss des] U1 ≡ U2 & + ∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[des + 1] U1 ≡ U2 & T2 = 𝕓{I} V2. U2. #I #T2 #des elim des -des [ #V1 #U1 #H @@ -68,6 +95,7 @@ lemma lifts_inv_bind1: ∀I,T2,des,V1,U1. ⇧*[des] 𝕓{I} V1. U1 ≡ T2 → ] qed-. +(* Basic_1: was: lift1_flat *) lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⇧*[des] 𝕗{I} V1. U1 ≡ T2 → ∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[des] U1 ≡ U2 & T2 = 𝕗{I} V2. U2. @@ -95,7 +123,7 @@ qed-. (* Basic properties *********************************************************) lemma lifts_bind: ∀I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 → - ∀T1. ⇧*[ss des] T1 ≡ T2 → + ∀T1. ⇧*[des + 1] T1 ≡ T2 → ⇧*[des] 𝕓{I} V1. T1 ≡ 𝕓{I} V2. T2. #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des [ #V #T1 #H >(lifts_inv_nil … H) -H // diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift.ma new file mode 100644 index 000000000..c10f25a30 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "Basic_2/substitution/lift_lift.ma". +include "Basic_2/unfold/lifts.ma". + +(* GENERIC TERM RELOCATION **************************************************) + +(* Properties concerning basic term relocation ******************************) + +(* Basic_1: was: lift1_xhg *) +lemma lifts_lift_trans_le: ∀T1,T,des. ⇧*[des] T1 ≡ T → ∀T2. ⇧[0, 1] T ≡ T2 → + ∃∃T0. ⇧[0, 1] T1 ≡ T0 & ⇧*[des + 1] T0 ≡ T2. +#T1 #T #des #H elim H -T1 -T -des +[ /2 width=3/ +| #T1 #T3 #T #des #d #e #HT13 #_ #IHT13 #T2 #HT2 + elim (IHT13 … HT2) -T #T #HT3 #HT2 + elim (lift_trans_le … HT13 … HT3 ?) -T3 // /3 width=5/ +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift_vector.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift_vector.ma new file mode 100644 index 000000000..727a93f54 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift_vector.ma @@ -0,0 +1,35 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "Basic_2/substitution/lift_lift_vector.ma". +include "Basic_2/unfold/lifts_lift.ma". +include "Basic_2/unfold/lifts_vector.ma". + +(* GENERIC RELOCATION *******************************************************) + +(* Main properties **********************************************************) + +(* Basic_1: was: lifts1_xhg *) +lemma liftsv_liftv_trans_le: ∀T1s,Ts,des. ⇧*[des] T1s ≡ Ts → + ∀T2s:list term. ⇧[0, 1] Ts ≡ T2s → + ∃∃T0s. ⇧[0, 1] T1s ≡ T0s & ⇧*[des + 1] T0s ≡ T2s. +#T1s #Ts #des #H elim H -T1s -Ts +[ #T1s #H + >(liftv_inv_nil1 … H) -T1s /2 width=3/ +| #T1s #Ts #T1 #T #HT1 #_ #IHT1s #X #H + elim (liftv_inv_cons1 … H) -H #T2 #T2s #HT2 #HT2s #H destruct + elim (IHT1s … HT2s) -Ts #Ts #HT1s #HT2s + elim (lifts_lift_trans_le … HT1 … HT2) -T /3 width=5/ +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lifts.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lifts.ma index 3cbd346ca..331de05df 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lifts.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lifts.ma @@ -12,24 +12,12 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/lift_lift.ma". -include "Basic_2/unfold/lifts.ma". +include "Basic_2/unfold/lifts_lift.ma". (* GENERIC RELOCATION *******************************************************) (* Main properties **********************************************************) -(* Basic_1: was: lift1_xhg *) -lemma lifts_lift_trans_le: ∀T1,T,des. ⇧*[des] T1 ≡ T → ∀T2. ⇧[0, 1] T ≡ T2 → - ∃∃T0. ⇧[0, 1] T1 ≡ T0 & ⇧*[ss des] T0 ≡ T2. -#T1 #T #des #H elim H -T1 -T -des -[ /2 width=3/ -| #T1 #T3 #T #des #d #e #HT13 #_ #IHT13 #T2 #HT2 - elim (IHT13 … HT2) -T #T #HT3 #HT2 - elim (lift_trans_le … HT13 … HT3 ?) -T3 // /3 width=5/ -] -qed-. - (* Basic_1: was: lift1_lift1 *) theorem lifts_trans: ∀T1,T,des1. ⇧*[des1] T1 ≡ T → ∀T2:term. ∀des2. ⇧*[des2] T ≡ T2 → ⇧*[des1 @ des2] T1 ≡ T2. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lifts_vector.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lifts_vector.ma deleted file mode 100644 index 6f0eeca70..000000000 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lifts_vector.ma +++ /dev/null @@ -1,35 +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 "Basic_2/substitution/lift_lift_vector.ma". -include "Basic_2/unfold/lifts_lifts.ma". -include "Basic_2/unfold/lifts_vector.ma". - -(* GENERIC RELOCATION *******************************************************) - -(* Main properties **********************************************************) - -(* Basic_1: was: lifts1_xhg *) -lemma liftsv_liftv_trans_le: ∀T1s,Ts,des. ⇧*[des] T1s ≡ Ts → - ∀T2s:list term. ⇧[0, 1] Ts ≡ T2s → - ∃∃T0s. ⇧[0, 1] T1s ≡ T0s & ⇧*[ss des] T0s ≡ T2s. -#T1s #Ts #des #H elim H -T1s -Ts -[ #T1s #H - >(liftv_inv_nil1 … H) -T1s /2 width=3/ -| #T1s #Ts #T1 #T #HT1 #_ #IHT1s #X #H - elim (liftv_inv_cons1 … H) -H #T2 #T2s #HT2 #HT2s #H destruct - elim (IHT1s … HT2s) -Ts #Ts #HT1s #HT2s - elim (lifts_lift_trans_le … HT1 … HT2) -T /3 width=5/ -] -qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_vector.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_vector.ma index 3032bc476..7c3c7640f 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_vector.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_vector.ma @@ -15,7 +15,7 @@ include "Basic_2/substitution/lift_vector.ma". include "Basic_2/unfold/lifts.ma". -(* GENERIC RELOCATION *******************************************************) +(* GENERIC TERM VECTOR RELOCATION *******************************************) inductive liftsv (des:list2 nat nat) : relation (list term) ≝ | liftsv_nil : liftsv des ◊ ◊ diff --git a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma index 418a176d5..39d28c959 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma @@ -17,7 +17,7 @@ include "Ground_2/star.ma". (* ARITHMETICAL PROPERTIES **************************************************) -(* equations ****************************************************************) +(* Equations ****************************************************************) lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p). /2 by plus_minus/ qed. @@ -69,4 +69,8 @@ qed-. (* lemma pippo: ∀x,y,z. x < z → y < z - x → x + y < z. /3 width=2/ + +lemma le_or_ge: ∀m,n. m ≤ n ∨ n ≤ m. +#m #n elim (lt_or_ge m n) /2 width=1/ /3 width=2/ +qed-. *)