From: Ferruccio Guidi Date: Fri, 27 Jan 2012 21:01:01 +0000 (+0000) Subject: support for abstract candidates of reducibility closed! ... X-Git-Tag: make_still_working~1964 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ca9cf24217384150ed1474dacba7b7dbb8836dbf;p=helm.git support for abstract candidates of reducibility closed! ... --- 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 0f70ef703..a65a8b81d 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 @@ -44,7 +44,7 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. [ #K2 #HK20 #H destruct generalize in match HLK2; generalize in match I; -HLK2 -I * #HLK2 [ elim (lift_total V0 0 (i0 +1)) #V #HV0 - elim (lifts_lift_trans … HV10 … HV0 … Hi0 Hdes0) -HV10 #V2 #HV12 #HV2 + elim (lifts_lift_trans … Hi0 … Hdes0 … HV10 … HV0) -HV10 #V2 #HV12 #HV2 @(s4 … HB … ◊ … HV0 HLK2) /3 width=7/ (* uses IHB HL20 V2 HV0 *) | @(s2 … HB … ◊) // /2 width=3/ ] 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 9f94d8969..46f864522 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 @@ -127,7 +127,7 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → >(at_mono … Hi1 … Hi0) in HL02; -i1 #HL02 elim (ldrops_inv_skip2 … Hdes0 … H) -H -des0 #L2 #W1 #des0 #Hdes0 #HLK #HVW1 #H destruct elim (lift_total W1 0 (i0 + 1)) #W2 #HW12 - elim (lifts_lift_trans … HVW1 … HW12 … Hdes0) // -Hdes0 -Hi0 #V3 #HV13 #HVW2 + elim (lifts_lift_trans … Hdes0 … HVW1 … HW12) // -Hdes0 -Hi0 #V3 #HV13 #HVW2 >(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2 @(s4 … IHA … (V0 :: V0s) … HW12 HL02) /3 width=4/ | #L #V1s #V2s #HV12s #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma index 61a9666b5..15418582b 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma @@ -13,6 +13,7 @@ (**************************************************************************) (* THE FORMAL SYSTEM λδ - MATITA SOURCE FILES + * Support for abstract candidates of reducibility closed: 2012 January 27 * Confluence of context-sensitive parallel reduction closed: 2011 September 21 * Confluence of context-free parallel reduction closed: 2011 September 6 * Specification started: 2011 April 17 diff --git a/matita/matita/contribs/lambda_delta/Basic_2/names.txt b/matita/matita/contribs/lambda_delta/Basic_2/names.txt index cc9bb6936..dfa83ebdd 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/names.txt +++ b/matita/matita/contribs/lambda_delta/Basic_2/names.txt @@ -23,6 +23,7 @@ i,j : local reference position index (de Bruijn's) k : sort index p,q : global reference position t,u : local reference position level (de Bruijn's) +x,y,z : reserved: transient objet denoted by a small letter NAMING CONVENTIONS FOR CONSTRUCTORS diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_aaa.ma b/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_aaa.ma new file mode 100644 index 000000000..4f9bb7dc3 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_aaa.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/aaa.ma". + +(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) + +(* Main properties **********************************************************) + +theorem aaa_mono: ∀L,T,A1. L ⊢ T ÷ A1 → ∀A2. L ⊢ T ÷ A2 → A1 = A2. +#L #T #A1 #H elim H -L -T -A1 +[ #L #k #A2 #H + >(aaa_inv_sort … H) -H // +| #I1 #L #K1 #V1 #B #i #HLK1 #_ #IHA1 #A2 #H + elim (aaa_inv_lref … H) -H #I2 #K2 #V2 #HLK2 #HA2 + lapply (ldrop_mono … HLK1 … HLK2) -L #H destruct /2 width=1/ +| #L #V #T #B1 #A1 #_ #_ #_ #IHA1 #A2 #H + elim (aaa_inv_abbr … H) -H /2 width=1/ +| #L #V1 #T1 #B1 #A1 #_ #_ #IHB1 #IHA1 #X #H + elim (aaa_inv_abst … H) -H #B2 #A2 #HB2 #HA2 #H destruct /3 width=1/ +| #L #V1 #T1 #B1 #A1 #_ #_ #_ #IHA1 #A2 #H + elim (aaa_inv_appl … H) -H #B2 #_ #HA2 + lapply (IHA1 … HA2) -L #H destruct // +| #L #V #T #A1 #_ #_ #_ #IHA1 #A2 #H + elim (aaa_inv_cast … H) -H /2 width=1/ +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_lift.ma new file mode 100644 index 000000000..edf08147e --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_lift.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/substitution/ldrop_ldrop.ma". +include "Basic_2/static/aaa.ma". + +(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) + +(* Properties concerning basic relocation ***********************************) + +lemma aaa_lift: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 → + ∀T2. ⇧[d, e] T1 ≡ T2 → L2 ⊢ T2 ÷ A. +#L1 #T1 #A #H elim H -L1 -T1 -A +[ #L1 #k #L2 #d #e #_ #T2 #H + >(lift_inv_sort1 … H) -H // +| #I #L1 #K1 #V1 #B #i #HLK1 #_ #IHB #L2 #d #e #HL21 #T2 #H + elim (lift_inv_lref1 … H) -H * #Hid #H destruct + [ elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H + elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct + /3 width=8/ + | lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/ + ] +| #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H + elim (lift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + /4 width=4/ +| #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H + elim (lift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + /4 width=4/ +| #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H + elim (lift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + /3 width=4/ +| #L1 #V1 #T1 #A #_ #_ #IH1 #IH2 #L2 #d #e #HL21 #X #H + elim (lift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + /3 width=4/ +] +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_lifts.ma b/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_lifts.ma new file mode 100644 index 000000000..156e75c9d --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_lifts.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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.ma". +include "Basic_2/static/aaa_lift.ma". + +(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) + +(* Properties concerning generic relocation *********************************) + +lemma aaa_lifts: ∀L1,L2,T2,A,des. ⇩*[des] L2 ≡ L1 → ∀T1. ⇧*[des] T1 ≡ T2 → + L1 ⊢ T1 ÷ A → L2 ⊢ T2 ÷ A. +#L1 #L2 #T2 #A #des #H elim H -L1 -L2 -des +[ #L #T1 #H #HT1 + <(lifts_inv_nil … H) -H // +| #L1 #L #L2 #des #d #e #_ #HL2 #IHL1 #T1 #H #HT1 + elim (lifts_inv_cons … H) -H /3 width=9/ +] +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2.ma index a33f018c2..0896b6ba3 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2.ma @@ -16,14 +16,6 @@ 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 → @@ -35,13 +27,47 @@ inductive at: list2 nat nat → relation nat ≝ 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 -. +(* Basic inversion lemmas ***************************************************) + +fact at_inv_nil_aux: ∀des,i1,i2. @[i1] des ≡ i2 → des = ⟠ → i1 = i2. +#des #i1 #i2 * -des -i1 -i2 +[ // +| #des #d #e #i1 #i2 #_ #_ #H destruct +| #des #d #e #i1 #i2 #_ #_ #H destruct +] +qed. + +lemma at_inv_nil: ∀i1,i2. @[i1] ⟠ ≡ i2 → i1 = i2. +/2 width=3/ qed-. + +fact at_inv_cons_aux: ∀des,i1,i2. @[i1] des ≡ i2 → + ∀d,e,des0. des = {d, e} :: des0 → + i1 < d ∧ @[i1] des0 ≡ i2 ∨ + d ≤ i1 ∧ @[i1 + e] des0 ≡ i2. +#des #i1 #i2 * -des -i1 -i2 +[ #i #d #e #des #H destruct +| #des1 #d1 #e1 #i1 #i2 #Hid1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1/ +| #des1 #d1 #e1 #i1 #i2 #Hdi1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1/ +] +qed. + +lemma at_inv_cons: ∀des,d,e,i1,i2. @[i1] {d, e} :: des ≡ i2 → + i1 < d ∧ @[i1] des ≡ i2 ∨ + d ≤ i1 ∧ @[i1 + e] des ≡ i2. +/2 width=3/ qed-. + +lemma at_inv_cons_lt: ∀des,d,e,i1,i2. @[i1] {d, e} :: des ≡ i2 → + i1 < d → @[i1] des ≡ i2. +#des #d #e #i1 #e2 #H +elim (at_inv_cons … H) -H * // #Hdi1 #_ #Hi1d +lapply (le_to_lt_to_lt … Hdi1 Hi1d) -Hdi1 -Hi1d #Hd +elim (lt_refl_false … Hd) +qed-. -interpretation "minus (generic relocation with pairs)" - 'RMinus des1 i des2 = (minuss i des1 des2). +lemma at_inv_cons_ge: ∀des,d,e,i1,i2. @[i1] {d, e} :: des ≡ i2 → + d ≤ i1 → @[i1 + e] des ≡ i2. +#des #d #e #i1 #e2 #H +elim (at_inv_cons … H) -H * // #Hi1d #_ #Hdi1 +lapply (le_to_lt_to_lt … Hdi1 Hi1d) -Hdi1 -Hi1d #Hd +elim (lt_refl_false … Hd) +qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_gr2.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_gr2.ma index dd2d34d07..438605e85 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_gr2.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_gr2.ma @@ -18,4 +18,12 @@ include "Basic_2/unfold/gr2.ma". (* Main properties **********************************************************) -axiom at_mono: ∀des,i,i1. @[i] des ≡ i1 → ∀i2. @[i] des ≡ i2 → i1 = i2. +theorem at_mono: ∀des,i,i1. @[i] des ≡ i1 → ∀i2. @[i] des ≡ i2 → i1 = i2. +#des #i #i1 #H elim H -des -i -i1 +[ #i #x #H <(at_inv_nil … H) -x // +| #des #d #e #i #i1 #Hid #_ #IHi1 #x #H + lapply (at_inv_cons_lt … H Hid) -H -Hid /2 width=1/ +| #des #d #e #i #i1 #Hdi #_ #IHi1 #x #H + lapply (at_inv_cons_ge … H Hdi) -H -Hdi /2 width=1/ +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_minus.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_minus.ma new file mode 100644 index 000000000..5e3144c93 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_minus.ma @@ -0,0 +1,76 @@ +(**************************************************************************) +(* ___ *) +(* ||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/gr2.ma". + +(* GENERIC RELOCATION WITH PAIRS ********************************************) + +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). + +(* Basic inversion lemmas ***************************************************) + +fact minuss_inv_nil1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → des1 = ⟠ → des2 = ⟠. +#des1 #des2 #i * -des1 -des2 -i +[ // +| #des1 #des2 #d #e #i #_ #_ #H destruct +| #des1 #des2 #d #e #i #_ #_ #H destruct +] +qed. + +lemma minuss_inv_nil1: ∀des2,i. ⟠ ▭ i ≡ des2 → des2 = ⟠. +/2 width=4/ qed-. + +fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → + ∀d,e,des. des1 = {d, e} :: des → + d ≤ i ∧ des ▭ e + i ≡ des2 ∨ + ∃∃des0. i < d & des ▭ i ≡ des0 & + des2 = {d - i, e} :: des0. +#des1 #des2 #i * -des1 -des2 -i +[ #i #d #e #des #H destruct +| #des1 #des #d1 #e1 #i1 #Hid1 #Hdes #d2 #e2 #des2 #H destruct /3 width=3/ +| #des1 #des #d1 #e1 #i1 #Hdi1 #Hdes #d2 #e2 #des2 #H destruct /3 width=1/ +] +qed. + +lemma minuss_inv_cons1: ∀des1,des2,d,e,i. {d, e} :: des1 ▭ i ≡ des2 → + d ≤ i ∧ des1 ▭ e + i ≡ des2 ∨ + ∃∃des. i < d & des1 ▭ i ≡ des & + des2 = {d - i, e} :: des. +/2 width=3/ qed-. + +lemma minuss_inv_cons1_ge: ∀des1,des2,d,e,i. {d, e} :: des1 ▭ i ≡ des2 → + d ≤ i → des1 ▭ e + i ≡ des2. +#des1 #des2 #d #e #i #H +elim (minuss_inv_cons1 … H) -H * // #des #Hid #_ #_ #Hdi +lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi +elim (lt_refl_false … Hi) +qed-. + +lemma minuss_inv_cons1_lt: ∀des1,des2,d,e,i. {d, e} :: des1 ▭ i ≡ des2 → + i < d → + ∃∃des. des1 ▭ i ≡ des & des2 = {d - i, e} :: des. +#des1 #des2 #d #e #i #H +elim (minuss_inv_cons1 … H) -H * /2 width=3/ #Hdi #_ #Hid +lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi +elim (lt_refl_false … Hi) +qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_plus.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_plus.ma new file mode 100644 index 000000000..938f955b9 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_plus.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 "Basic_2/unfold/gr2.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). + +(* Basic inversion lemmas ***************************************************) + +lemma pluss_inv_nil2: ∀i,des. des + i = ⟠ → des = ⟠. +#i * // normalize +#d #e #des #H destruct +qed. + +lemma pluss_inv_cons2: ∀i,d,e,des2,des. des + i = {d, e} :: des2 → + ∃∃des1. des1 + i = des2 & des = {d - i, e} :: des1. +#i #d #e #des2 * normalize +[ #H destruct +| #d1 #e1 #des1 #H destruct /2 width=3/ +] +qed-. 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 78f4dd6af..d271fe2c6 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "Basic_2/substitution/ldrop.ma". +include "Basic_2/unfold/gr2_minus.ma". include "Basic_2/unfold/lifts.ma". (* GENERIC LOCAL ENVIRONMENT SLICING ****************************************) 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 40f4325b1..57405868f 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "Basic_2/substitution/lift.ma". -include "Basic_2/unfold/gr2.ma". +include "Basic_2/unfold/gr2_plus.ma". (* GENERIC TERM RELOCATION **************************************************) 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 index 8bec02119..b10b3c17b 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "Basic_2/substitution/lift_lift.ma". +include "Basic_2/unfold/gr2_minus.ma". include "Basic_2/unfold/lifts.ma". (* GENERIC TERM RELOCATION **************************************************) @@ -31,7 +32,28 @@ lemma lifts_lift_trans_le: ∀T1,T,des. ⇧*[des] T1 ≡ T → ∀T2. ⇧[0, 1] qed-. (* Basic_1: was: lift1_free (right to left) *) -axiom lifts_lift_trans: ∀T1,T0,des0. ⇧*[des0] T1 ≡ T0 → - ∀T2,i0. ⇧[O, i0 + 1] T0 ≡ T2 → - ∀des,i. @[i] des ≡ i0 → des + 1 ▭ i + 1 ≡ des0 + 1 → +lemma lifts_lift_trans: ∀des,i,i0. @[i] des ≡ i0 → + ∀des0. des + 1 ▭ i + 1 ≡ des0 + 1 → + ∀T1,T0. ⇧*[des0] T1 ≡ T0 → + ∀T2. ⇧[O, i0 + 1] T0 ≡ T2 → ∃∃T. ⇧[0, i + 1] T1 ≡ T & ⇧*[des] T ≡ T2. +#des elim des -des normalize +[ #i #x #H1 #des0 #H2 #T1 #T0 #HT10 #T2 + <(at_inv_nil … H1) -x #HT02 + lapply (minuss_inv_nil1 … H2) -H2 #H + >(pluss_inv_nil2 … H) in HT10; -des0 #H + >(lifts_inv_nil … H) -T1 /2 width=3/ +| #d #e #des #IHdes #i #i0 #H1 #des0 #H2 #T1 #T0 #HT10 #T2 #HT02 + elim (at_inv_cons … H1) -H1 * #Hid #Hi0 + [ elim (minuss_inv_cons1_lt … H2 ?) -H2 [2: /2 width=1/ ] #des1 #Hdes1 minus_plus #HT1 #HT0 + elim (IHdes … Hi0 … Hdes1 … HT0 … HT02) -IHdes -Hi0 -Hdes1 -T0 #T0 #HT0 #HT02 + elim (lift_trans_le … HT1 … HT0 ?) -T /2 width=1/ #T #HT1 commutative_plus in Hi0; #Hi0 + lapply (minuss_inv_cons1_ge … H2 ?) -H2 [ /2 width=1/ ]