From: Ferruccio Guidi Date: Fri, 13 Jan 2012 15:27:13 +0000 (+0000) Subject: - the development of abstract reducibility candidates continues ... X-Git-Tag: make_still_working~1978 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=720637242f8c46adef24da44f29129faa09469de;p=helm.git - the development of abstract reducibility candidates continues ... - some annotations added --- 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 b7fa79e70..da672ace3 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt +++ b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt @@ -154,9 +154,6 @@ lift1/fwd lift1_cons_tail lift1/fwd lifts1_flat lift1/fwd lifts1_nil lift1/fwd lifts1_cons -lift1/props lift1_lift1 -lift1/props lift1_xhg -lift1/props lifts1_xhg lift1/props lift1_free lift/props thead_x_lift_y_y lift/props lifts_tapp 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 03526d8f1..a2c5045e0 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 @@ -21,9 +21,6 @@ axiom lsubc_ldrops_trans: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀K2,des. ⇩[des] L2 axiom ldrops_lsubc_trans: ∀RP,L1,K1,des. ⇩*[des] L1 ≡ K1 → ∀K2. K1 [RP] ⊑ K2 → ∃∃L2. L1 [RP] ⊑ L2 & ⇩*[des] L2 ≡ K2. -axiom lifts_trans: ∀T1,T,des1. ⇧*[des1] T1 ≡ T → ∀T2:term. ∀des2. ⇧*[des2] T ≡ T2 → - ⇧*[des1 @ des2] T1 ≡ T2. - axiom ldrops_trans: ∀L1,L,des1. ⇩*[des1] L1 ≡ L → ∀L2,des2. ⇩*[des2] L ≡ L2 → ⇩*[des2 @ des1] L1 ≡ L2. 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 fc0b87b17..77f782298 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_vector.ma". +include "Basic_2/unfold/lifts_lifts_vector.ma". include "Basic_2/computation/acp.ma". (* ABSTRACT COMPUTATION PROPERTIES ******************************************) @@ -94,13 +94,12 @@ lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP (λL,T. RP L T) → @conj /2 width=1/ /2 width=6 by rp_lifts/ qed. -axiom aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → +lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → ∀A. acr RR RS RP (aacr RP A). -(* #RR #RS #RP #H1RP #H2RP #A elim A -A normalize // #B #A #IHB #IHA @mk_acr normalize [ #L #T #H - lapply (H ? (⋆0) ? ⟠ ? ? ?) -H + lapply (H ? (⋆0) ? ⟠ ? ? ?) -H [1,3: // |2,4: skip | @(s2 … IHB … ◊) // /2 width=2/ | #H @(cp3 … H1RP … 0) @(s1 … IHA) // @@ -123,26 +122,28 @@ axiom aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → @(HA … (ss des)) /2 width=1/ [ @(s7 … IHB … HB … HV120) /2 width=1/ | @liftsv_applv // + elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s + >(liftv_mono … HV12s … HV10s) -V1s // ] | #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct - @(s6 … IHA … (V0 :: V0s)) /2 width=6 by rp_lifts/ /3 width=4/ + @(s6 … IHA … (V0 :: V0s)) /2 width=6 by rp_lifts/ /3 width=4/ | /3 width=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⦄ [RP] ϵ 〚B〛→ ⦃L0. 𝕓{Abbr} V0, T0⦄ [RP] ϵ 〚A〛 + ⦃L0, V0⦄ [RP] ϵ 〚B〛 → ⦃L0. 𝕓{Abbr} V0, T0⦄ [RP] ϵ 〚A〛 ) → ⦃L, 𝕓{Abst} W. T⦄ [RP] ϵ 〚𝕔 B. A〛. #RR #RS #RP #H1RP #H2RP #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HB #HL0 #H lapply (aacr_acr … H1RP H2RP A) #HCA lapply (aacr_acr … H1RP H2RP B) #HCB elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct -lapply (s1 … HCB) -HCB #HCB +lapply (s1 … HCB) -HCB #HCB @(s3 … HCA … ◊) /2 width=6 by rp_lifts/ @(s5 … HCA … ◊ ◊) // /2 width=1/ /2 width=3/ qed. 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 235c4233d..d207ebf23 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 @@ -19,7 +19,7 @@ include "Basic_2/substitution/lift.ma". (* Main properies ***********************************************************) (* Basic_1: was: lift_inj *) -theorem lift_inj: ∀d,e,T1,U. ⇧[d,e] T1 ≡ U → ∀T2. ⇧[d,e] T2 ≡ U → T1 = T2. +theorem lift_inj: ∀d,e,T1,U. ⇧[d,e] T1 ≡ U → ∀T2. ⇧[d,e] T2 ≡ U → T1 = T2. #d #e #T1 #U #H elim H -d -e -T1 -U [ #k #d #e #X #HX lapply (lift_inv_sort2 … HX) -HX // 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 new file mode 100644 index 000000000..7513a5abe --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift_vector.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/substitution/lift_lift.ma". +include "Basic_2/substitution/lift_vector.ma". + +(* RELOCATION ***************************************************************) + +(* Main properies ***********************************************************) + +theorem liftv_mono: ∀Ts,U1s,d,e. ⇧[d,e] Ts ≡ U1s → + ∀U2s:list term. ⇧[d,e] Ts ≡ U2s → U1s = U2s. +#Ts #U1s #d #e #H elim H -Ts -U1s +[ #U2s #H >(liftv_inv_nil1 … H) -H // +| #Ts #U1s #T #U1 #HTU1 #_ #IHTU1s #X #H destruct + elim (liftv_inv_cons1 … H) -H #U2 #U2s #HTU2 #HTU2s #H destruct + >(lift_mono … HTU1 … HTU2) -T /3 width=1/ +] +qed. 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 ef422bdd4..710ab34cd 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 @@ -26,6 +26,31 @@ inductive liftv (d,e:nat) : relation (list term) ≝ interpretation "relocation (vector)" 'RLift d e T1s T2s = (liftv d e T1s T2s). +(* Basic inversion lemmas ***************************************************) + +fact liftv_inv_nil1_aux: ∀T1s,T2s,d,e. ⇧[d, e] T1s ≡ T2s → T1s = ◊ → T2s = ◊. +#T1s #T2s #d #e * -T1s -T2s // +#T1s #T2s #T1 #T2 #_ #_ #H destruct +qed. + +lemma liftv_inv_nil1: ∀T2s,d,e. ⇧[d, e] ◊ ≡ T2s → T2s = ◊. +/2 width=5/ qed-. + +fact liftv_inv_cons1_aux: ∀T1s,T2s,d,e. ⇧[d, e] T1s ≡ T2s → + ∀U1,U1s. T1s = U1 :: U1s → + ∃∃U2,U2s. ⇧[d, e] U1 ≡ U2 & ⇧[d, e] U1s ≡ U2s & + T2s = U2 :: U2s. +#T1s #T2s #d #e * -T1s -T2s +[ #U1 #U1s #H destruct +| #T1s #T2s #T1 #T2 #HT12 #HT12s #U1 #U1s #H destruct /2 width=5/ +] +qed. + +lemma liftv_inv_cons1: ∀U1,U1s,T2s,d,e. ⇧[d, e] U1 :: U1s ≡ T2s → + ∃∃U2,U2s. ⇧[d, e] U1 ≡ U2 & ⇧[d, e] U1s ≡ U2s & + T2s = U2 :: U2s. +/2 width=3/ qed-. + (* Basic properties *********************************************************) lemma liftv_total: ∀d,e. ∀T1s:list term. ∃T2s. ⇧[d, e] T1s ≡ T2s. 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 new file mode 100644 index 000000000..3cbd346ca --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lifts.ma @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||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 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. +#T1 #T #des1 #H elim H -T1 -T -des1 // /3 width=3/ +qed. 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 new file mode 100644 index 000000000..6f0eeca70 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lifts_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_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/Ground_2/list.ma b/matita/matita/contribs/lambda_delta/Ground_2/list.ma index 883a8a8ba..0a6e69bbe 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/list.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/list.ma @@ -34,7 +34,7 @@ inductive list2 (A1,A2:Type[0]) : Type[0] := | nil2 : list2 A1 A2 | cons2: A1 → A2 → list2 A1 A2 → list2 A1 A2. -interpretation "nil (list of pairs)" 'Nil2 = (nil2 ? ?). (**) (* 'Nil causes unification error in aacr_abst *) +interpretation "nil (list of pairs)" 'Nil2 = (nil2 ? ?). interpretation "cons (list of pairs)" 'Cons hd1 hd2 tl = (cons2 ? ? hd1 hd2 tl).