From: Ferruccio Guidi Date: Fri, 24 Feb 2012 12:53:09 +0000 (+0000) Subject: - "functional" component moved to Apps_2 X-Git-Tag: make_still_working~1940 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f21509c476b20e5446335c967b1e81f87ceb4f6c;p=helm.git - "functional" component moved to Apps_2 - property S5 of the candidates of reducibility almost proved ... --- diff --git a/matita/matita/contribs/lambda_delta/Apps_2/functional/lift.ma b/matita/matita/contribs/lambda_delta/Apps_2/functional/lift.ma new file mode 100644 index 000000000..aefa1576d --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Apps_2/functional/lift.ma @@ -0,0 +1,69 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tri.ma". +include "Basic_2/substitution/lift.ma". +include "Apps_2/functional/notation.ma". + +(* RELOCATION ***************************************************************) + +let rec flift d e U on U ≝ match U with +[ TAtom I ⇒ match I with + [ Sort _ ⇒ U + | LRef i ⇒ #(tri … i d i (i + e) (i + e)) + | GRef _ ⇒ U + ] +| TPair I V T ⇒ match I with + [ Bind2 I ⇒ ⓑ{I} (flift d e V). (flift (d+1) e T) + | Flat2 I ⇒ ⓕ{I} (flift d e V). (flift d e T) + ] +]. + +interpretation "functional relocation" 'Lift d e T = (flift d e T). + +(* Main properties **********************************************************) + +theorem flift_lift: ∀T,d,e. ⇧[d, e] T ≡ ↑[d, e] T. +#T elim T -T +[ * #i #d #e // + elim (lt_or_eq_or_gt i d) #Hid normalize + [ >(tri_lt ?????? Hid) /2 width=1/ + | /2 width=1/ + | >(tri_gt ?????? Hid) /3 width=2/ + ] +| * /2/ +] +qed. + +(* Main inversion properties ************************************************) + +theorem flift_inv_lift: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → ↑[d, e] T1 = T2. +#d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize // +[ #i #d #e #Hid >(tri_lt ?????? Hid) // +| #i #d #e #Hid + elim (le_to_or_lt_eq … Hid) -Hid #Hid + [ >(tri_gt ?????? Hid) // + | destruct // + ] +] +qed-. + +(* Derived properties *******************************************************) + +lemma flift_join: ∀e1,e2,T. ⇧[e1, e2] ↑[0, e1] T ≡ ↑[0, e1 + e2] T. +#e1 #e2 #T +lapply (flift_lift T 0 (e1+e2)) #H +elim (lift_split … H e1 e1 ? ? ?) -H // #U #H +>(flift_inv_lift … H) -H // +qed. diff --git a/matita/matita/contribs/lambda_delta/Apps_2/functional/notation.ma b/matita/matita/contribs/lambda_delta/Apps_2/functional/notation.ma new file mode 100644 index 000000000..48df845c1 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Apps_2/functional/notation.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE "functional" COMPONENT ********************************) + +notation "hvbox( ↑ [ d , break e ] break T )" + non associative with precedence 55 + for @{ 'Lift $d $e $T }. + +notation "hvbox( [ d ← break V ] break T )" + non associative with precedence 55 + for @{ 'Subst $V $d $T }. + +notation "hvbox( T1 ⇨ break T2 )" + non associative with precedence 45 + for @{ 'SRed $T1 $T2 }. diff --git a/matita/matita/contribs/lambda_delta/Apps_2/functional/rtm.ma b/matita/matita/contribs/lambda_delta/Apps_2/functional/rtm.ma new file mode 100644 index 000000000..845e8a04d --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Apps_2/functional/rtm.ma @@ -0,0 +1,85 @@ +(**************************************************************************) +(* ___ *) +(* ||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". +include "Basic_2/grammar/genv.ma". + +(* REDUCTION AND TYPE MACHINE ***********************************************) + +(* machine local environment *) +inductive xenv: Type[0] ≝ +| XAtom: xenv (* empty *) +| XQuad: xenv → bind2 → nat → xenv → term → xenv (* entry *) +. + +interpretation "atom (ext. local environment)" + 'Star = XAtom. + +interpretation "environment construction (quad)" + 'DxItem4 L I u K V = (XQuad L I u K V). + +(* machine stack *) +definition stack: Type[0] ≝ list2 xenv term. + +(* machine status *) +record rtm: Type[0] ≝ +{ rg: genv; (* global environment *) + ru: nat; (* current de Bruijn's level *) + re: xenv; (* extended local environment *) + rs: stack; (* application stack *) + rt: term (* code *) +}. + +(* initial state *) +definition rtm_i: genv → term → rtm ≝ + λG,T. mk_rtm G 0 (⋆) (⟠) T. + +(* update code *) +definition rtm_t: rtm → term → rtm ≝ + λM,T. match M with + [ mk_rtm G u E _ _ ⇒ mk_rtm G u E (⟠) T + ]. + +(* update closure *) +definition rtm_u: rtm → xenv → term → rtm ≝ + λM,E,T. match M with + [ mk_rtm G u _ _ _ ⇒ mk_rtm G u E (⟠) T + ]. + +(* get global environment *) +definition rtm_g: rtm → genv ≝ + λM. match M with + [ mk_rtm G _ _ _ _ ⇒ G + ]. + +(* get local reference level *) +definition rtm_l: rtm → nat ≝ + λM. match M with + [ mk_rtm _ u E _ _ ⇒ match E with + [ XAtom ⇒ u + | XQuad _ _ u _ _ ⇒ u + ] + ]. + +(* get stack *) +definition rtm_s: rtm → stack ≝ + λM. match M with + [ mk_rtm _ _ _ S _ ⇒ S + ]. + +(* get code *) +definition rtm_c: rtm → term ≝ + λM. match M with + [ mk_rtm _ _ _ _ T ⇒ T + ]. diff --git a/matita/matita/contribs/lambda_delta/Apps_2/functional/rtm_step.ma b/matita/matita/contribs/lambda_delta/Apps_2/functional/rtm_step.ma new file mode 100644 index 000000000..5b2a4eb2c --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Apps_2/functional/rtm_step.ma @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "Apps_2/functional/rtm.ma". + +(* REDUCTION AND TYPE MACHINE ***********************************************) + +(* transitions *) +inductive rtm_step: relation rtm ≝ +| rtm_ldrop : ∀G,u,E,I,t,F,V,S,i. + rtm_step (mk_rtm G u (E. ④{I} {t, F, V}) S (#(i + 1))) + (mk_rtm G u E S (#i)) +| rtm_ldelta: ∀G,u,E,t,F,V,S. + rtm_step (mk_rtm G u (E. ④{Abbr} {t, F, V}) S (#0)) + (mk_rtm G u F S V) +| rtm_ltype : ∀G,u,E,t,F,V,S. + rtm_step (mk_rtm G u (E. ④{Abst} {t, F, V}) S (#0)) + (mk_rtm G u F S V) +| rtm_gdrop : ∀G,I,V,u,E,S,p. p < |G| → + rtm_step (mk_rtm (G. ⓑ{I} V) u E S (§p)) + (mk_rtm G u E S (§p)) +| rtm_gdelta: ∀G,V,u,E,S,p. p = |G| → + rtm_step (mk_rtm (G. ⓓV) u E S (§p)) + (mk_rtm G u E S V) +| rtm_gtype : ∀G,V,u,E,S,p. p = |G| → + rtm_step (mk_rtm (G. ⓛV) u E S (§p)) + (mk_rtm G u E S V) +| rtm_tau : ∀G,u,E,S,W,T. + rtm_step (mk_rtm G u E S (ⓣW. T)) + (mk_rtm G u E S T) +| rtm_appl : ∀G,u,E,S,V,T. + rtm_step (mk_rtm G u E S (ⓐV. T)) + (mk_rtm G u E ({E, V} :: S) T) +| rtm_beta : ∀G,u,E,F,V,S,W,T. + rtm_step (mk_rtm G u E ({F, V} :: S) (ⓛW. T)) + (mk_rtm G u (E. ④{Abbr} {u, F, V}) S T) +| rtm_push : ∀G,u,E,W,T. + rtm_step (mk_rtm G u E ⟠ (ⓛW. T)) + (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) ⟠ T) +| rtm_theta : ∀G,u,E,S,V,T. + rtm_step (mk_rtm G u E S (ⓓV. T)) + (mk_rtm G u (E. ④{Abbr} {u, E, V}) S T) +. + +interpretation "sequential reduction (RTM)" + 'SRed O1 O2 = (rtm_step O1 O2). diff --git a/matita/matita/contribs/lambda_delta/Apps_2/functional/subst.ma b/matita/matita/contribs/lambda_delta/Apps_2/functional/subst.ma new file mode 100644 index 000000000..6aa75625d --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Apps_2/functional/subst.ma @@ -0,0 +1,73 @@ +(**************************************************************************) +(* ___ *) +(* ||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/delift_lift.ma". +include "Apps_2/functional/lift.ma". + +(* CORE SUBSTITUTION ********************************************************) + +let rec fsubst W d U on U ≝ match U with +[ TAtom I ⇒ match I with + [ Sort _ ⇒ U + | LRef i ⇒ tri … i d (#i) (↑[0, i] W) (#(i-1)) + | GRef _ ⇒ U + ] +| TPair I V T ⇒ match I with + [ Bind2 I ⇒ ⓑ{I} (fsubst W d V). (fsubst W (d+1) T) + | Flat2 I ⇒ ⓕ{I} (fsubst W d V). (fsubst W d T) + ] +]. + +interpretation "functional core substitution" 'Subst V d T = (fsubst V d T). + +(* Main properties **********************************************************) + +theorem fsubst_delift: ∀K,V,T,L,d. + ⇩[0, d] L ≡ K. ⓓV → L ⊢ T [d, 1] ≡ [d ← V] T. +#K #V #T elim T -T +[ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/ + elim (lt_or_eq_or_gt i d) #Hid + [ -HLK >(tri_lt ?????? Hid) /3 width=3/ + | destruct >tri_eq /4 width=4 by tpss_strap, tps_subst, le_n, ex2_1_intro/ (**) (* too slow without trace *) + | -HLK >(tri_gt ?????? Hid) /3 width=3/ + ] +| * /3 width=1/ /4 width=1/ +] +qed. + +(* Main inversion properties ************************************************) + +theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. ⓓV → + L ⊢ T1 [d, 1] ≡ T2 → [d ← V] T1 = T2. +#K #V #T1 elim T1 -T1 +[ * #i #L #T2 #d #HLK #H + [ -HLK >(delift_fwd_sort1 … H) -H // + | elim (lt_or_eq_or_gt i d) #Hid normalize + [ -HLK >(delift_fwd_lref1_lt … H) -H // /2 width=1/ + | destruct + elim (delift_fwd_lref1_be … H ? ?) -H // #K0 #V0 #V2 #HLK0 + lapply (ldrop_mono … HLK0 … HLK) -HLK0 -HLK #H >minus_plus (delift_inv_refl_O2 … HV2) -V >(flift_inv_lift … HVT2) -V2 // + | -HLK >(delift_fwd_lref1_ge … H) -H // /2 width=1/ + ] + | -HLK >(delift_fwd_gref1 … H) -H // + ] +| * #I #V1 #T1 #IHV1 #IHT1 #L #X #d #HLK #H + [ elim (delift_fwd_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 // /2 width=1/ + | elim (delift_fwd_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 // + ] +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_tstc_vector.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_tstc_vector.ma new file mode 100644 index 000000000..d073bad24 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_tstc_vector.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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_vector.ma". +include "Basic_2/computation/cprs_tstc.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) + +(* Vector form of forward lemmas involving same top term constructor ********) + +lemma cpr_fwd_theta_vector: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → + ∀V,T,U. L ⊢ ⒶV1s. ⓓV. T ➡ U → + ⒶV1s. ⓓV. T ≃ U ∨ L ⊢ ⓓV. ⒶV2s. T ➡* U. +#L #V1s #V2s * -V1s -V2s /3 width=1/ +#V1s #V2s #V1a #V2a #HV12a * -V1s -V2s /2 width=1 by cpr_fwd_theta/ -HV12a +#V1s #V2s #V1b #V2b #_ #_ #V #U #T #H +elim (cpr_inv_appl1_simple … H ?) -H // +#V0 #T0 #_ #_ #H destruct /2 width=1/ +qed-. + +axiom cprs_fwd_theta_vector: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → + ∀V,T,U. L ⊢ ⒶV1s. ⓓV. T ➡* U → + ⒶV1s. ⓓV. T ≃ U ∨ L ⊢ ⓓV. ⒶV2s. T ➡* U. \ No newline at end of file diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_aaa.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_aaa.ma index 8bc613aa4..421a3a7f7 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_aaa.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_aaa.ma @@ -13,13 +13,13 @@ (**************************************************************************) include "Basic_2/computation/acp_aaa.ma". -include "Basic_2/computation/csn_cr.ma". +include "Basic_2/computation/csn_lcpr_vector.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) -(* Main properties **********************************************************) +(* Properties concerning atomic arity assignment ****************************) -theorem csn_aaa: ∀L,T,A. L ⊢ T ÷ A → L ⊢ ⬇* T. +lemma csn_aaa: ∀L,T,A. L ⊢ T ÷ A → L ⊢ ⬇* T. #L #T #A #H @(acp_aaa … csn_acp csn_acr … H) qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma deleted file mode 100644 index 81c179293..000000000 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma +++ /dev/null @@ -1,53 +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/computation/acp_cr.ma". -include "Basic_2/computation/csn_lcpr.ma". -include "Basic_2/computation/csn_vector.ma". - -(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) - -(* Advanced properties ******************************************************) -(* - -(* Basic_1: was only: sn3_appl_appls *) -lemma csn_appl_appls_simple_tstc: ∀L,Vs,V,T1. L ⊢ ⬇* V → L ⊢ ⬇* T1 → - (∀T2. L ⊢ ⒶVs.T1 ➡* T2 → (ⒶVs.T1 ≃ T2 → False) → L ⊢ ⬇* ⓐV. T2) → - 𝐒[T1] → L ⊢ ⬇* ⓐV. ⒶVs. T1. -#L * -[ #V #T1 #HV - @csn_appl_simple_tstc // -| #V0 #Vs #V #T1 #HV #H1T1 #H2T1 #H3T1 - @csn_appl_simple_tstc // -HV - [ @H2T1 -] -qed. - -lemma csn_applv_theta: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → - ∀V,T. L ⊢ ⬇* ⓓV. ⒶV2s. T → L ⊢ ⬇* V → L ⊢ ⬇* ⒶV1s. ⓓV. T. -#L #V1s #V2s * -V1s -V2s /2 width=1/ -#V1s #V2s #V1 #V2 #HV12 * -V1s -V2s /2 width=3/ -#V1s #V2s #W1 #W2 #HW12 #HV12s #V #T #H #HV -lapply (csn_appl_theta … HV12 … H) -H -HV12 #H -lapply (csn_fwd_pair_sn … H) #HV1 -@csn_appl_simple // #X #H1 #H2 -whd in ⊢ (? ? %); -*) -(* -lemma csn_S5: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → - ∀V,T. L. ⓓV ⊢ ⬇* ⒶV2s. T → L ⊢ ⬇* V → L ⊢ ⬇* ⒶV1s. ⓓV. T. -#L #V1s #V2s #H elim H -V1s -V2s /2 width=1/ -*) - -axiom csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬇* T). diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr_vector.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr_vector.ma new file mode 100644 index 000000000..36e44ce6d --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr_vector.ma @@ -0,0 +1,67 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/acp_cr.ma". +include "Basic_2/computation/cprs_tstc_vector.ma". +include "Basic_2/computation/csn_lcpr.ma". +include "Basic_2/computation/csn_vector.ma". + +(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************) + +(* Advanced properties ******************************************************) +(* +(* Basic_1: was only: sn3_appl_appls *) +lemma csn_appl_appls_simple_tstc: ∀L,Vs,V,T1. L ⊢ ⬇* V → L ⊢ ⬇* T1 → + (∀T2. L ⊢ ⒶVs.T1 ➡* T2 → (ⒶVs.T1 ≃ T2 → False) → L ⊢ ⬇* ⓐV. T2) → + 𝐒[T1] → L ⊢ ⬇* ⓐV. ⒶVs. T1. +#L * +[ #V #T1 #HV + @csn_appl_simple_tstc // +| #V0 #Vs #V #T1 #HV #H1T1 #H2T1 #H3T1 + @csn_appl_simple_tstc // -HV + [ @H2T1 +] +qed. +*) +lemma csn_applv_theta: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → + ∀V,T. L ⊢ ⬇* ⓓV. ⒶV2s. T → L ⊢ ⬇* V → L ⊢ ⬇* ⒶV1s. ⓓV. T. +#L #V1s #V2s * -V1s -V2s /2 width=1/ +#V1s #V2s #V1 #V2 #HV12 #H +generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1 +elim H -V1s -V2s /2 width=3/ +#V1s #V2s #V1 #V2 #HV12 #HV12s #IHV12s #W1 #W2 #HW12 #V #T #H #HV +lapply (csn_appl_theta … HW12 … H) -H -HW12 #H +lapply (csn_fwd_pair_sn … H) #HW1 +lapply (csn_fwd_flat_dx … H) #H1 +@csn_appl_simple_tstc // -HW1 /2 width=3/ -IHV12s -HV -H1 #X #H1 #H2 +elim (cprs_fwd_theta_vector … (V2::V2s) … H1) -H1 /2 width=1/ -HV12s -HV12 +[ -H #H elim (H2 ?) -H2 // +| -H2 #H1 @(csn_cprs_trans … H) -H /2 width=1/ +] +qed. +(* +theorem csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬇* T). +@mk_acr // +[ +| +| +| #L #V1 #V2 #HV12 #V #T #H #HVT + @(csn_applv_theta … HV12) -HV12 // + @(csn_abbr) // +| +| @csn_lift +] +qed. +*) +axiom csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬇* T). diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma index 1326a8bb4..01d983c0c 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma @@ -43,15 +43,6 @@ qed. (* Advanced properties ******************************************************) -lemma csn_acp: acp cpr (eq …) (csn …). -@mk_acp -[ /2 width=1/ -| /2 width=3/ -| /2 width=5/ -| @cnf_lift -] -qed. - (* Basic_1: was: sn3_abbr *) lemma csn_lref_abbr: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓓV → K ⊢ ⬇* V → L ⊢ ⬇* #i. #L #K #V #i #HLK #HV @@ -96,3 +87,14 @@ elim (eq_false_inv_tpair_dx … H2) -H2 @IHT1 -IHT1 // -HLT02 /2 width=1/ ] qed. + +(* Main properties **********************************************************) + +theorem csn_acp: acp cpr (eq …) (csn …). +@mk_acp +[ /2 width=1/ +| /2 width=3/ +| /2 width=5/ +| @cnf_lift +] +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/functional/lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/functional/lift.ma deleted file mode 100644 index 780467209..000000000 --- a/matita/matita/contribs/lambda_delta/Basic_2/functional/lift.ma +++ /dev/null @@ -1,68 +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/tri.ma". -include "Basic_2/substitution/lift.ma". - -(* RELOCATION ***************************************************************) - -let rec flift d e U on U ≝ match U with -[ TAtom I ⇒ match I with - [ Sort _ ⇒ U - | LRef i ⇒ #(tri … i d i (i + e) (i + e)) - | GRef _ ⇒ U - ] -| TPair I V T ⇒ match I with - [ Bind2 I ⇒ ⓑ{I} (flift d e V). (flift (d+1) e T) - | Flat2 I ⇒ ⓕ{I} (flift d e V). (flift d e T) - ] -]. - -interpretation "functional relocation" 'Lift d e T = (flift d e T). - -(* Main properties **********************************************************) - -theorem flift_lift: ∀T,d,e. ⇧[d, e] T ≡ ↑[d, e] T. -#T elim T -T -[ * #i #d #e // - elim (lt_or_eq_or_gt i d) #Hid normalize - [ >(tri_lt ?????? Hid) /2 width=1/ - | /2 width=1/ - | >(tri_gt ?????? Hid) /3 width=2/ - ] -| * /2/ -] -qed. - -(* Main inversion properties ************************************************) - -theorem flift_inv_lift: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → ↑[d, e] T1 = T2. -#d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize // -[ #i #d #e #Hid >(tri_lt ?????? Hid) // -| #i #d #e #Hid - elim (le_to_or_lt_eq … Hid) -Hid #Hid - [ >(tri_gt ?????? Hid) // - | destruct // - ] -] -qed-. - -(* Derived properties *******************************************************) - -lemma flift_join: ∀e1,e2,T. ⇧[e1, e2] ↑[0, e1] T ≡ ↑[0, e1 + e2] T. -#e1 #e2 #T -lapply (flift_lift T 0 (e1+e2)) #H -elim (lift_split … H e1 e1 ? ? ?) -H // #U #H ->(flift_inv_lift … H) -H // -qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm.ma b/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm.ma deleted file mode 100644 index 845e8a04d..000000000 --- a/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm.ma +++ /dev/null @@ -1,85 +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/grammar/term_vector.ma". -include "Basic_2/grammar/genv.ma". - -(* REDUCTION AND TYPE MACHINE ***********************************************) - -(* machine local environment *) -inductive xenv: Type[0] ≝ -| XAtom: xenv (* empty *) -| XQuad: xenv → bind2 → nat → xenv → term → xenv (* entry *) -. - -interpretation "atom (ext. local environment)" - 'Star = XAtom. - -interpretation "environment construction (quad)" - 'DxItem4 L I u K V = (XQuad L I u K V). - -(* machine stack *) -definition stack: Type[0] ≝ list2 xenv term. - -(* machine status *) -record rtm: Type[0] ≝ -{ rg: genv; (* global environment *) - ru: nat; (* current de Bruijn's level *) - re: xenv; (* extended local environment *) - rs: stack; (* application stack *) - rt: term (* code *) -}. - -(* initial state *) -definition rtm_i: genv → term → rtm ≝ - λG,T. mk_rtm G 0 (⋆) (⟠) T. - -(* update code *) -definition rtm_t: rtm → term → rtm ≝ - λM,T. match M with - [ mk_rtm G u E _ _ ⇒ mk_rtm G u E (⟠) T - ]. - -(* update closure *) -definition rtm_u: rtm → xenv → term → rtm ≝ - λM,E,T. match M with - [ mk_rtm G u _ _ _ ⇒ mk_rtm G u E (⟠) T - ]. - -(* get global environment *) -definition rtm_g: rtm → genv ≝ - λM. match M with - [ mk_rtm G _ _ _ _ ⇒ G - ]. - -(* get local reference level *) -definition rtm_l: rtm → nat ≝ - λM. match M with - [ mk_rtm _ u E _ _ ⇒ match E with - [ XAtom ⇒ u - | XQuad _ _ u _ _ ⇒ u - ] - ]. - -(* get stack *) -definition rtm_s: rtm → stack ≝ - λM. match M with - [ mk_rtm _ _ _ S _ ⇒ S - ]. - -(* get code *) -definition rtm_c: rtm → term ≝ - λM. match M with - [ mk_rtm _ _ _ _ T ⇒ T - ]. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm_step.ma b/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm_step.ma deleted file mode 100644 index c1dc7dcb1..000000000 --- a/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm_step.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 "Basic_2/functional/rtm.ma". - -(* REDUCTION AND TYPE MACHINE ***********************************************) - -(* transitions *) -inductive rtm_step: relation rtm ≝ -| rtm_ldrop : ∀G,u,E,I,t,F,V,S,i. - rtm_step (mk_rtm G u (E. ④{I} {t, F, V}) S (#(i + 1))) - (mk_rtm G u E S (#i)) -| rtm_ldelta: ∀G,u,E,t,F,V,S. - rtm_step (mk_rtm G u (E. ④{Abbr} {t, F, V}) S (#0)) - (mk_rtm G u F S V) -| rtm_ltype : ∀G,u,E,t,F,V,S. - rtm_step (mk_rtm G u (E. ④{Abst} {t, F, V}) S (#0)) - (mk_rtm G u F S V) -| rtm_gdrop : ∀G,I,V,u,E,S,p. p < |G| → - rtm_step (mk_rtm (G. ⓑ{I} V) u E S (§p)) - (mk_rtm G u E S (§p)) -| rtm_gdelta: ∀G,V,u,E,S,p. p = |G| → - rtm_step (mk_rtm (G. ⓓV) u E S (§p)) - (mk_rtm G u E S V) -| rtm_gtype : ∀G,V,u,E,S,p. p = |G| → - rtm_step (mk_rtm (G. ⓛV) u E S (§p)) - (mk_rtm G u E S V) -| rtm_tau : ∀G,u,E,S,W,T. - rtm_step (mk_rtm G u E S (ⓣW. T)) - (mk_rtm G u E S T) -| rtm_appl : ∀G,u,E,S,V,T. - rtm_step (mk_rtm G u E S (ⓐV. T)) - (mk_rtm G u E ({E, V} :: S) T) -| rtm_beta : ∀G,u,E,F,V,S,W,T. - rtm_step (mk_rtm G u E ({F, V} :: S) (ⓛW. T)) - (mk_rtm G u (E. ④{Abbr} {u, F, V}) S T) -| rtm_push : ∀G,u,E,W,T. - rtm_step (mk_rtm G u E ⟠ (ⓛW. T)) - (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) ⟠ T) -| rtm_theta : ∀G,u,E,S,V,T. - rtm_step (mk_rtm G u E S (ⓓV. T)) - (mk_rtm G u (E. ④{Abbr} {u, E, V}) S T) -. - -interpretation "sequential reduction (RTM)" - 'SRed O1 O2 = (rtm_step O1 O2). diff --git a/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma b/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma deleted file mode 100644 index b12e9b413..000000000 --- a/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma +++ /dev/null @@ -1,73 +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/unfold/delift_lift.ma". -include "Basic_2/functional/lift.ma". - -(* CORE SUBSTITUTION ********************************************************) - -let rec fsubst W d U on U ≝ match U with -[ TAtom I ⇒ match I with - [ Sort _ ⇒ U - | LRef i ⇒ tri … i d (#i) (↑[0, i] W) (#(i-1)) - | GRef _ ⇒ U - ] -| TPair I V T ⇒ match I with - [ Bind2 I ⇒ ⓑ{I} (fsubst W d V). (fsubst W (d+1) T) - | Flat2 I ⇒ ⓕ{I} (fsubst W d V). (fsubst W d T) - ] -]. - -interpretation "functional core substitution" 'Subst V d T = (fsubst V d T). - -(* Main properties **********************************************************) - -theorem fsubst_delift: ∀K,V,T,L,d. - ⇩[0, d] L ≡ K. ⓓV → L ⊢ T [d, 1] ≡ [d ← V] T. -#K #V #T elim T -T -[ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/ - elim (lt_or_eq_or_gt i d) #Hid - [ -HLK >(tri_lt ?????? Hid) /3 width=3/ - | destruct >tri_eq /4 width=4 by tpss_strap, tps_subst, le_n, ex2_1_intro/ (**) (* too slow without trace *) - | -HLK >(tri_gt ?????? Hid) /3 width=3/ - ] -| * /3 width=1/ /4 width=1/ -] -qed. - -(* Main inversion properties ************************************************) - -theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. ⓓV → - L ⊢ T1 [d, 1] ≡ T2 → [d ← V] T1 = T2. -#K #V #T1 elim T1 -T1 -[ * #i #L #T2 #d #HLK #H - [ -HLK >(delift_fwd_sort1 … H) -H // - | elim (lt_or_eq_or_gt i d) #Hid normalize - [ -HLK >(delift_fwd_lref1_lt … H) -H // /2 width=1/ - | destruct - elim (delift_fwd_lref1_be … H ? ?) -H // #K0 #V0 #V2 #HLK0 - lapply (ldrop_mono … HLK0 … HLK) -HLK0 -HLK #H >minus_plus (delift_inv_refl_O2 … HV2) -V >(flift_inv_lift … HVT2) -V2 // - | -HLK >(delift_fwd_lref1_ge … H) -H // /2 width=1/ - ] - | -HLK >(delift_fwd_gref1 … H) -H // - ] -| * #I #V1 #T1 #IHV1 #IHT1 #L #X #d #HLK #H - [ elim (delift_fwd_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct - <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 // /2 width=1/ - | elim (delift_fwd_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct - <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 // - ] -] -qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma index 557299afd..9b6c08270 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma @@ -34,3 +34,8 @@ qed. lemma simple_inv_bind: ∀I,V,T. 𝐒[ⓑ{I} V. T] → False. /2 width=6/ qed-. + +lemma simple_inv_pair: ∀I,V,T. 𝐒[②{I}V.T] → ∃J. I = Flat2 J. +* /2 width=2/ #I #V #T #H +elim (simple_inv_bind … H) +qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma index 9c91d59f9..75ec4c523 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma @@ -97,8 +97,6 @@ lemma tstc_dec: ∀T1,T2. Decidable (T1 ≃ T2). ] qed. -axiom simple_inv_pair: ∀I,V,T. 𝐒[②{I}V.T] → ∃J. I = Flat2 J. - lemma simple_tstc_repl_dx: ∀T1,T2. T1 ≃ T2 → 𝐒[T1] → 𝐒[T2]. #T1 #T2 * -T1 -T2 // #I #V1 #V2 #T1 #T2 #H diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma index 7d05a2f67..0aabfd481 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma @@ -294,16 +294,14 @@ notation "hvbox( T1 break [ R ] ⊑ break T2 )" non associative with precedence 45 for @{ 'CrSubEq $T1 $R $T2 }. -(* Functional ***************************************************************) +(* Conversion ***************************************************************) -notation "hvbox( ↑ [ d , break e ] break T )" - non associative with precedence 55 - for @{ 'Lift $d $e $T }. +notation "hvbox( L ⊢ break term 90 T1 ⬌ break T2 )" + non associative with precedence 45 + for @{ 'PConv $L $T1 $T2 }. -notation "hvbox( [ d ← break V ] break T )" - non associative with precedence 55 - for @{ 'Subst $V $d $T }. +(* Congruence ***************************************************************) -notation "hvbox( T1 ⇨ break T2 )" +notation "hvbox( L ⊢ break term 90 T1 ⬌* break T2 )" non associative with precedence 45 - for @{ 'SRed $T1 $T2 }. + for @{ 'PConvStar $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile index e5a20a1f3..3ce097690 100644 --- a/matita/matita/contribs/lambda_delta/Makefile +++ b/matita/matita/contribs/lambda_delta/Makefile @@ -5,7 +5,7 @@ XOA = xoa.native CONF = Ground_2/xoa.conf.xml TARGETS = Ground_2/xoa_natation.ma Ground_2/xoa.ma -PACKAGES = Ground_2 Basic_2 +PACKAGES = Ground_2 Basic_2 Apps_2 all: @@ -25,10 +25,12 @@ stats: $(PACKAGES:%=%.stats) %.stats: CHARS = $(shell cat $(MAS) | wc -c) -%.stats: C1 = $(shell grep "inductive\|record" $(MAS) | wc -l) -%.stats: C2 = $(shell grep "definition\|let rec" $(MAS) | wc -l) +%.stats: C1 = $(shell grep "inductive \|record " $(MAS) | wc -l) +%.stats: C2 = $(shell grep "definition \|let rec " $(MAS) | wc -l) +%.stats: C3 = $(shell grep "inductive \|record \|definition \|let rec " $(MAS) | wc -l) %.stats: P1 = $(shell grep "theorem " $(MAS) | wc -l) %.stats: P2 = $(shell grep "lemma " $(MAS) | wc -l) +%.stats: P3 = $(shell grep "lemma \|theorem " $(MAS) | wc -l) %.stats: TBL = ld_$*_sum @@ -65,20 +67,22 @@ stats: $(PACKAGES:%=%.stats) @printf ' %-6s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l` @printf ' %-10s' '' @printf '\x1B[0m\n' - @printf 'name "$(TBL)"\n\n' > $*/$(TBL).tbl - @printf 'table {\n' >> $*/$(TBL).tbl - @printf ' class "grey" [ "category"\n' >> $*/$(TBL).tbl - @printf ' [ "objects" * ]\n' >> $*/$(TBL).tbl - @printf ' ]\n' >> $*/$(TBL).tbl - @printf ' class "green" [ "propositions"\n' >> $*/$(TBL).tbl - @printf ' [ "theorems" "$(P1)" * ]\n' >> $*/$(TBL).tbl - @printf ' [ "lemmas" "$(P2)" * ]\n' >> $*/$(TBL).tbl - @printf ' ]\n' >> $*/$(TBL).tbl - @printf ' class "yellow" [ "concepts"\n' >> $*/$(TBL).tbl - @printf ' [ "declared" "$(C1)" * ]\n' >> $*/$(TBL).tbl - @printf ' [ "defined" "$(C2)" * ]\n' >> $*/$(TBL).tbl - @printf ' ]\n' >> $*/$(TBL).tbl - @printf '}\n\n' >> $*/$(TBL).tbl - @printf 'class "component" { 0 }\n\n' >> $*/$(TBL).tbl - @printf 'class "plane" { 1 } { 3 } \n\n' >> $*/$(TBL).tbl - @printf 'class "number" { 2 } { 4 } \n\n' >> $*/$(TBL).tbl + @printf 'name "$(TBL)"\n\n' > $*/$(TBL).tbl + @printf 'table {\n' >> $*/$(TBL).tbl + @printf ' class "grey" [ "category"\n' >> $*/$(TBL).tbl + @printf ' [ "objects" * ]\n' >> $*/$(TBL).tbl + @printf ' ]\n' >> $*/$(TBL).tbl + @printf ' class "green" [ "propositions"\n' >> $*/$(TBL).tbl + @printf ' [ "theorems" "$(P1)" * ]\n' >> $*/$(TBL).tbl + @printf ' [ "lemmas" "$(P2)" * ]\n' >> $*/$(TBL).tbl + @printf ' [ "total" "$(P3)" * ]\n' >> $*/$(TBL).tbl + @printf ' ]\n' >> $*/$(TBL).tbl + @printf ' class "yellow" [ "concepts"\n' >> $*/$(TBL).tbl + @printf ' [ "declared" "$(C1)" * ]\n' >> $*/$(TBL).tbl + @printf ' [ "defined" "$(C2)" * ]\n' >> $*/$(TBL).tbl + @printf ' [ "total" "$(C3)" * ]\n' >> $*/$(TBL).tbl + @printf ' ]\n' >> $*/$(TBL).tbl + @printf '}\n\n' >> $*/$(TBL).tbl + @printf 'class "component" { 0 }\n\n' >> $*/$(TBL).tbl + @printf 'class "plane" { 1 } { 3 } { 5 } \n\n' >> $*/$(TBL).tbl + @printf 'class "number" { 2 } { 4 } { 6 } \n\n' >> $*/$(TBL).tbl