From b5db76fe31ab35bae0257cb6684c511bcc531e45 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 9 Feb 2012 19:30:41 +0000 Subject: [PATCH] - first properties of strongly normalizing terms - contex-sensitive normal forms - context-sensitive parallel computation of terms --- .../contribs/lambda_delta/Basic_2/Basic_1.txt | 50 ++----------- .../lambda_delta/Basic_2/computation/acp.ma | 3 +- .../Basic_2/computation/acp_aaa.ma | 2 + .../Basic_2/computation/acp_cr.ma | 14 +++- .../lambda_delta/Basic_2/computation/cprs.ma | 55 ++++++++++++++ .../Basic_2/computation/cprs_cprs.ma | 38 ++++++++++ .../Basic_2/computation/cprs_lcpr.ma | 46 ++++++++++++ .../lambda_delta/Basic_2/computation/csn.ma | 73 ++++++++++++++++++- .../Basic_2/computation/csn_cr.ma | 2 +- .../Basic_2/computation/csn_lift.ma | 64 ++++++++++++++++ .../Basic_2/computation/lsubc_ldrop.ma | 2 +- .../lambda_delta/Basic_2/grammar/term.ma | 16 +++- .../contribs/lambda_delta/Basic_2/notation.ma | 4 + .../lambda_delta/Basic_2/reducibility/cnf.ma | 33 +++++++++ .../Basic_2/reducibility/cnf_lift.ma | 61 ++++++++++++++++ .../Basic_2/reducibility/cpr_lift.ma | 10 ++- .../{cpr_tpss.ma => cpr_ltpss.ma} | 9 +++ .../Basic_2/reducibility/ltpr_ldrop.ma | 20 ++++- .../Basic_2/reducibility/ltpr_tps.ma | 37 ++++++++++ .../lambda_delta/Basic_2/substitution/ltps.ma | 12 +++ .../lambda_delta/Basic_2/unfold/ltpss.ma | 14 ++++ matita/matita/predefined_virtuals.ml | 2 + 22 files changed, 508 insertions(+), 59 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/computation/cprs.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_lcpr.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/reducibility/cnf.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/reducibility/cnf_lift.ma rename matita/matita/contribs/lambda_delta/Basic_2/reducibility/{cpr_tpss.ma => cpr_ltpss.ma} (87%) create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_tps.ma 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 8f3a63204..0570c48b3 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt +++ b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt @@ -157,6 +157,7 @@ next_plus/props next_plus_next next_plus/props next_plus_lt nf2/arity arity_nf2_inv_all nf2/dec nf2_dec + nf2/fwd nf2_gen_lref nf2/fwd nf2_gen_abst nf2/fwd nf2_gen_cast @@ -164,20 +165,15 @@ nf2/fwd nf2_gen_beta nf2/fwd nf2_gen_flat nf2/fwd nf2_gen__nf2_gen_aux nf2/fwd nf2_gen_abbr + nf2/fwd nf2_gen_void nf2/iso nf2_iso_appls_lref -nf2/lift1 nf2_lift1 nf2/pr3 nf2_pr3_unfold nf2/pr3 nf2_pr3_confluence -nf2/props nf2_sort -nf2/props nf2_csort_lref -nf2/props nf2_abst -nf2/props nf2_abst_shift + nf2/props nfs2_tapp nf2/props nf2_appls_lref -nf2/props nf2_appl_lref -nf2/props nf2_lref_abst -nf2/props nf2_lift + pc1/props pc1_pr0_r pc1/props pc1_pr0_x pc1/props pc1_refl @@ -255,6 +251,7 @@ pr2/clen pr2_gen_ctail pr2/fwd pr2_gen_void pr2/props pr2_ctail pr2/subst1 pr2_gen_cabbr + pr3/fwd pr3_gen_sort pr3/fwd pr3_gen_abst pr3/fwd pr3_gen_cast @@ -273,57 +270,26 @@ pr3/iso pr3_iso_beta pr3/iso pr3_iso_appls_beta pr3/pr1 pr3_pr1 pr3/pr3 pr3_strip -pr3/pr3 pr3_confluence -pr3/props clear_pr3_trans -pr3/props pr3_pr2 -pr3/props pr3_t pr3/props pr3_thin_dx pr3/props pr3_head_1 pr3/props pr3_head_2 pr3/props pr3_head_21 pr3/props pr3_head_12 -pr3/props pr3_cflat pr3/props pr3_flat -pr3/props pr3_pr0_pr2_t -pr3/props pr3_pr2_pr2_t -pr3/props pr3_pr2_pr3_t pr3/props pr3_pr3_pr3_t pr3/props pr3_lift pr3/props pr3_eta pr3/subst1 pr3_subst1 pr3/subst1 pr3_gen_cabbr pr3/wcpr0 pr3_wcpr0_t -sc3/arity sc3_arity_csubc -sc3/arity sc3_arity -sc3/props sc3_arity_gen -sc3/props sc3_repl -sc3/props sc3_lift -sc3/props sc3_lift1 -sc3/props sc3_abbr -sc3/props sc3_cast -sc3/props sc3_props__sc3_sn3_abst -sc3/props sc3_sn3 -sc3/props sc3_abst -sc3/props sc3_bind -sc3/props sc3_appl -sn3/fwd sn3_gen_bind -sn3/fwd sn3_gen_flat -sn3/fwd sn3_gen_head -sn3/fwd sn3_gen_cflat -sn3/fwd sn3_gen_lift -sn3/lift1 sns3_lifts1 -sn3/nf2 sn3_nf2 sn3/nf2 nf2_sn3 sn3/props sn3_pr3_trans -sn3/props sn3_pr2_intro -sn3/props sn3_cast -sn3/props sn3_cflat +sn3/props sn3_cpr3_trans + sn3/props sn3_shift sn3/props sn3_change sn3/props sn3_gen_def sn3/props sn3_cdelta -sn3/props sn3_cpr3_trans -sn3/props sn3_bind sn3/props sn3_beta sn3/props sn3_appl_lref sn3/props sn3_appl_abbr @@ -336,10 +302,10 @@ sn3/props sn3_appls_lref sn3/props sn3_appls_cast sn3/props sn3_appls_bind sn3/props sn3_appls_beta -sn3/props sn3_lift sn3/props sn3_abbr sn3/props sn3_appls_abbr sn3/props sns3_lifts + sty0/fwd sty0_gen_sort sty0/fwd sty0_gen_lref sty0/fwd sty0_gen_bind diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp.ma index ca1ba4686..8be75a31f 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp.ma @@ -27,7 +27,7 @@ definition CP3 ≝ λRR:lenv→relation term. λRP:lenv→predicate term. definition CP4 ≝ λRR:lenv→relation term. λRS:relation term. ∀L0,L,T,T0,d,e. NF … (RR L) RS T → - ⇩[d,e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR L0) RS T0. + ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR L0) RS T0. definition CP4s ≝ λRR:lenv→relation term. λRS:relation term. ∀L0,L,des. ⇩*[des] L0 ≡ L → @@ -44,6 +44,7 @@ record acp (RR:lenv->relation term) (RS:relation term) (RP:lenv→predicate term (* Basic properties *********************************************************) +(* Basic_1: was: nf2_lift1 *) lemma acp_lifts: ∀RR,RS. CP4 RR RS → CP4s RR RS. #RR #RS #HRR #L1 #L2 #des #H elim H -L1 -L2 -des [ #L #T1 #T2 #H #HT1 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 a65a8b81d..1cab5d4b8 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 @@ -22,6 +22,7 @@ include "Basic_2/computation/lsubc_ldrops.ma". (* Main propertis ***********************************************************) +(* Basic_1: was: sc3_arity_csubc *) theorem 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 → @@ -87,6 +88,7 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. ] qed. +(* Basic_1: was: sc3_arity *) lemma aacr_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → ∀L,T,A. L ⊢ T ÷ A → ⦃L, T⦄ [RP] ϵ 〚A〛. /2 width=8/ qed. 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 fef5e4c92..6eb71054b 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 @@ -44,8 +44,8 @@ definition S5 ≝ λRP,C:lenv→predicate term. definition S6 ≝ λRP,C:lenv→predicate term. ∀L,Vs,T,W. C L (ⒶVs. T) → RP L W → C L (ⒶVs. ⓣW. T). -definition S7 ≝ λC:lenv→predicate term. ∀L1,L2,T1,T2,d,e. - C L1 T1 → ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C L2 T2. +definition S7 ≝ λC:lenv→predicate term. ∀L2,L1,T1,d,e. + C L1 T1 → ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C L2 T2. definition S7s ≝ λC:lenv→predicate term. ∀L1,L2,des. ⇩*[des] L2 ≡ L1 → @@ -76,6 +76,7 @@ interpretation (* Basic properties *********************************************************) +(* Basic_1: was: sc3_lift1 *) lemma acr_lifts: ∀C. S7 C → S7s C. #C #HC #L1 #L2 #des #H elim H -L1 -L2 -des [ #L #T1 #T2 #H #HT1 @@ -93,14 +94,18 @@ lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP (λL,T. RP L T) → @(s7 … HRP) qed. +(* Basic_1: was only: sns3_lifts1 *) lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP (λL,T. RP L T) → - ∀des,L0,L,Vs,V0s. ⇧*[des] Vs ≡ V0s → ⇩*[des] L0 ≡ L → + ∀des,L0,L,Vs,V0s. ⇧*[des] Vs ≡ V0s → ⇩*[des] L0 ≡ L → all … (RP L) Vs → all … (RP L0) V0s. #RR #RS #RP #HRP #des #L0 #L #Vs #V0s #H elim H -Vs -V0s normalize // #T1s #T2s #T1 #T2 #HT12 #_ #IHT2s #HL0 * #HT1 #HT1s @conj /2 width=1/ /2 width=6 by rp_lifts/ qed. +(* Basic_1: was: + sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast sc3_lift +*) 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 // @@ -164,3 +169,6 @@ lapply (s1 … HCB) -HCB #HCB @(s3 … HCA … ◊) /2 width=6 by rp_lifts/ @(s5 … HCA … ◊ ◊) // /2 width=1/ /2 width=3/ qed. + +(* Basic_1: removed theorems 2: sc3_arity_gen sc3_repl *) +(* Basic_1: removed local theorems 1: sc3_sn3_abst *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs.ma new file mode 100644 index 000000000..276abd468 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs.ma @@ -0,0 +1,55 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/cpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) + +(* Basic_1: includes: pr3_pr2 *) +definition cprs: lenv → relation term ≝ + λL. TC … (cpr L). + +interpretation "context-sensitive parallel computation (term)" + 'PRedStar L T1 T2 = (cprs L T1 T2). + +(* Basic eliminators ********************************************************) + +lemma cprs_ind: ∀L,T1. ∀R:predicate term. R T1 → + (∀T,T2. L ⊢ T1 ➡* T → L ⊢ T ➡ T2 → R T → R T2) → + ∀T2. L ⊢ T1 ➡* T2 → R T2. +#L #T1 #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) // +qed-. + +(* Basic properties *********************************************************) + +(* Basic_1: was: pr3_refl *) +lemma cprs_refl: ∀L,T. L ⊢ T ➡* T. +/2 width=1/ qed. + +lemma cprs_strap1: ∀L,T1,T,T2. + L ⊢ T1 ➡* T → L ⊢ T ➡ T2 → L ⊢ T1 ➡* T2. +/2 width=3/ qed. + +(* Basic_1: was: pr3_step *) +lemma cprs_strap2: ∀L,T1,T,T2. + L ⊢ T1 ➡ T → L ⊢ T ➡* T2 → L ⊢ T1 ➡* T2. +/2 width=3/ qed. + +(* Note: it does not hold replacing |L1| with |L2| *) +lemma cprs_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 → + ∀L2. L1 [0, |L1|] ≼ L2 → L2 ⊢ T1 ➡* T2. +/3 width=3/ +qed. + +(* Basic_1: removed theorems 2: clear_pr3_trans pr3_cflat *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma new file mode 100644 index 000000000..20bf4ebe5 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/cpr_cpr.ma". +include "Basic_2/computation/cprs_lcpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) + +(* Main propertis ***********************************************************) + +(* Basic_1: was: pr3_t *) +theorem cprs_trans: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ➡* T2. +/2 width=3/ qed. + +(* Basic_1: was: pr3_confluence *) +theorem cprs_conf: ∀L,T1,T. L ⊢ T ➡* T1 → ∀T2. L ⊢ T ➡* T2 → + ∃∃T0. L ⊢ T1 ➡* T0 & L ⊢ T2 ➡* T0. +/3 width=3/ qed. + +(* Advanced properties ******************************************************) + +(* Basic_1: was only: pr3_pr2_pr3_t *) +lemma lcpr_cprs_trans: ∀L1,L2. L1 ⊢ ➡ L2 → + ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. +#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 // +#T #T2 #_ #HT2 #IHT2 /3 width=5/ +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_lcpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_lcpr.ma new file mode 100644 index 000000000..7816989a7 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_lcpr.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/ltpr_tps.ma". +include "Basic_2/reducibility/cpr_ltpss.ma". +include "Basic_2/reducibility/lcpr.ma". +include "Basic_2/computation/cprs.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) + +(* Properties concerning context-sensitive parallel reduction on lenv's *****) + +lemma ltpr_tpss_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2,d,e. L2 ⊢ T1 [d, e] ▶* T2 → + ∃∃T. L1 ⊢ T1 [d, e] ▶* T & L1 ⊢ T ➡* T2. +#L1 #L2 #HL12 #T1 #T2 #d #e #H @(tpss_ind … H) -T2 +[ /2 width=3/ +| #T #T2 #_ #HT2 * #T0 #HT10 #HT0 + elim (ltpr_tps_trans … HT2 … HL12) -L2 #T3 #HT3 #HT32 + @(ex2_1_intro … HT10) -T1 (**) (* explicit constructors *) + @(cprs_strap1 … T3 …) /2 width=1/ -HT32 + @(cprs_strap1 … HT0) -HT0 /3 width=3/ +] +qed. + +(* Basic_1: was just: pr3_pr0_pr2_t *) +lemma ltpr_cpr_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2. +#L1 #L2 #HL12 #T1 #T2 * #T #HT1 +<(ltpr_fwd_length … HL12) #HT2 +elim (ltpr_tpss_trans … HL12 … HT2) -L2 /3 width=3/ +qed. + +(* Basic_1: was just: pr3_pr2_pr2_t *) +lemma lcpr_cpr_trans: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2. +#L1 #L2 * /3 width=7/ +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma index b6ebc547f..2df67c9c2 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "Basic_2/reducibility/cpr.ma". -include "Basic_2/computation/acp.ma". +include "Basic_2/reducibility/cnf.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) @@ -21,8 +21,75 @@ definition csn: lenv → predicate term ≝ λL. SN … (cpr L) (eq …). interpretation "context-sensitive strong normalization (term)" - 'SN L T = (csn L T). + 'SN L T = (csn L T). + +(* Basic eliminators ********************************************************) + +lemma csn_ind: ∀L. ∀R:predicate term. + (∀T1. L ⊢ ⬇* T1 → + (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → R T2) → + R T1 + ) → + ∀T. L ⊢ ⬇* T → R T. +#L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1 +@H0 -H0 /3 width=1/ -IHT1 /4 width=1/ +qed-. (* Basic properties *********************************************************) -axiom csn_acp: acp cpr (eq …) (csn …). +(* Basic_1: was: sn3_pr2_intro *) +lemma csn_intro: ∀L,T1. + (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → L ⊢ ⬇* T2) → L ⊢ ⬇* T1. +#L #T1 #H +@(SN_intro … H) +qed. + +(* Basic_1: was: sn3_nf2 *) +lemma csn_cnf: ∀L,T. L ⊢ 𝐍[T] → L ⊢ ⬇* T. +/2 width=1/ qed. + +lemma csn_cpr_trans: ∀L,T1. L ⊢ ⬇* T1 → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ ⬇* T2. +#L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12 +@csn_intro #T #HLT2 #HT2 +elim (term_eq_dec T1 T2) #HT12 +[ -IHT1 -HLT12 destruct /3 width=1/ +| -HT1 -HT2 /3 width=4/ +qed. + +axiom tpss_csn_trans: ∀L,T2. L ⊢ ⬇* T2 → ∀T1,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ ⬇* T1. +(* +#L #T2 #H @(csn_ind … H) -T2 #T2 #HT2 #IHT2 #T1 #d #e #HT12 +@csn_intro #T #HLT1 #HT1 +*) +(* Basic_1: was: sn3_cast *) +lemma csn_cast: ∀L,W. L ⊢ ⬇* W → ∀T. L ⊢ ⬇* T → L ⊢ ⬇* ⓣW. T. +#L #W #HW elim HW -W #W #_ #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT +@csn_intro #X #H1 #H2 +elim (cpr_inv_cast1 … H1) -H1 +[ * #W0 #T0 #HLW0 #HLT0 #H destruct + elim (eq_false_inv_tpair … H2) -H2 + [ /3 width=3/ + | -HLW0 * #H destruct /3 width=1/ + ] +| /3 width=3/ +] +qed. + +(* Basic forward lemmas *****************************************************) + +fact csn_fwd_flat2_aux: ∀L,U. L ⊢ ⬇* U → ∀I,V,T. U = ⓕ{I} V. T → L ⊢ ⬇* T. +#L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct +@csn_intro #T2 #HLT2 #HT2 +@(IH (ⓕ{I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/ +qed. + +(* Basic_1: was: sn3_gen_flat *) +lemma csn_fwd_flat2: ∀I,L,V,T. L ⊢ ⬇* ⓕ{I} V. T → L ⊢ ⬇* T. +/2 width=5/ qed-. + +(* +sn3/fwd sn3_gen_bind +sn3/fwd sn3_gen_head +*) + +(* Basic_1: removed theorems 3: sn3_gen_cflat sn3_cflat sn3_bind *) 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 index 98a8db1de..bbdfd773e 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "Basic_2/computation/acp_cr.ma". -include "Basic_2/computation/csn.ma". +include "Basic_2/computation/csn_lift.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) 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 new file mode 100644 index 000000000..605e78db1 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma @@ -0,0 +1,64 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/cnf_lift.ma". +include "Basic_2/computation/acp.ma". +include "Basic_2/computation/csn.ma". + +(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) + +(* Advanced properties ******************************************************) + +lemma csn_acp: acp cpr (eq …) (csn …). +@mk_acp +[ /2 width=1/ +| /2 width=3/ +| /2 width=5/ +| @cnf_lift +] +qed. + +lemma csn_abst: ∀L,W. L ⊢ ⬇* W → ∀I,V,T. L. ⓑ{I} V ⊢ ⬇* T → L ⊢ ⬇* ⓛW. T. +#L #W #HW elim HW -W #W #_ #IHW #I #V #T #HT @(csn_ind … HT) -T #T #HT #IHT +@csn_intro #X #H1 #H2 +elim (cpr_inv_abst1 … H1 I V) -H1 +#W0 #T0 #HLW0 #HLT0 #H destruct +elim (eq_false_inv_tpair … H2) -H2 +[ /3 width=5/ +| -HLW0 * #H destruct /3 width=1/ +] +qed. + +(* Relocation properties ****************************************************) + +(* Basic_1: was: sn3_lift *) +lemma csn_lift: ∀L2,L1,T1,d,e. L1 ⊢ ⬇* T1 → + ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → L2 ⊢ ⬇* T2. +#L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL21 #HT12 +@csn_intro #T #HLT2 #HT2 +elim (cpr_inv_lift … HL21 … HT12 … HLT2) -HLT2 #T0 #HT0 #HLT10 +@(IHT1 … HLT10) // -L1 -L2 #H destruct +>(lift_mono … HT0 … HT12) in HT2; -T0 /2 width=1/ +qed. + +(* Basic_1: was: sn3_gen_lift *) +lemma csn_inv_lift: ∀L2,L1,T1,d,e. L1 ⊢ ⬇* T1 → + ∀T2. ⇩[d, e] L1 ≡ L2 → ⇧[d, e] T2 ≡ T1 → L2 ⊢ ⬇* T2. +#L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL12 #HT21 +@csn_intro #T #HLT2 #HT2 +elim (lift_total T d e) #T0 #HT0 +lapply (cpr_lift … HL12 … HT21 … HT0 HLT2) -HLT2 #HLT10 +@(IHT1 … HLT10) // -L1 -L2 #H destruct +>(lift_inj … HT0 … HT21) in HT2; -T0 /2 width=1/ +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_ldrop.ma index fcc7f683d..03ea7b628 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_ldrop.ma @@ -61,7 +61,7 @@ lemma ldrop_lsubc_trans: ∀RR,RS,RP. | #K2 #W2 #A #HV2 #HW2 #HK12 #H1 #H2 destruct elim (IHLK1 … HK12) #K #HL1K #HK2 lapply (aacr_acr … Hacp Hacr A) -Hacp -Hacr #HA - lapply (s7 … HA … HV2 HLK1 HV21) -HV2 + lapply (s7 … HA … HV2 … HLK1 HV21) -HV2 elim (lift_total W2 d e) /4 width=9/ ] ] diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma index d66a9c520..7a5a9d91d 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma @@ -55,6 +55,11 @@ interpretation "application (term)" interpretation "native type annotation (term)" 'SnCast T1 T2 = (TPair (Flat2 Cast) T1 T2). +(* Basic properties *********************************************************) + +(* Basic_1: was: term_dec *) +axiom term_eq_dec: ∀T1,T2:term. Decidable (T1 = T2). + (* Basic inversion lemmas ***************************************************) lemma discr_tpair_xy_x: ∀I,T,V. ②{I} V. T = V → False. @@ -76,10 +81,13 @@ lemma discr_tpair_xy_y: ∀I,V,T. ②{I} V. T = T → False. ] qed-. -(* Basic properties *********************************************************) - -(* Basic_1: was: term_dec *) -axiom term_eq_dec: ∀T1,T2:term. Decidable (T1 = T2). +lemma eq_false_inv_tpair: ∀I,V1,T1,V2,T2. + (②{I} V1. T1 = ②{I} V2. T2 → False) → + (V1 = V2 → False) ∨ (V1 = V2 ∧ (T1 = T2 → False)). +#I #V1 #T1 #V2 #T2 #H +elim (term_eq_dec V1 V2) /3 width=1/ #HV12 destruct +@or_intror @conj // #HT12 destruct /2 width=1/ +qed-. (* Basic_1: removed theorems 3: not_void_abst not_abbr_void not_abst_void diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma index c25341f63..9f2d54df0 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma @@ -108,6 +108,10 @@ notation "hvbox( 𝐒 [ T ] )" non associative with precedence 45 for @{ 'Simple $T }. +notation "hvbox( L ⊢ break term 90 T1 ≈ break T2 )" + non associative with precedence 45 + for @{ 'Hom $L $T1 $T2 }. + notation "hvbox( T1 break [ d , break e ] ≼ break T2 )" non associative with precedence 45 for @{ 'SubEq $T1 $d $e $T2 }. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cnf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cnf.ma new file mode 100644 index 000000000..50ff04603 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cnf.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/cpr.ma". + +(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************) + +definition cnf: lenv → predicate term ≝ λL. NF … (cpr L) (eq …). + +interpretation + "context-sensitive normality (term)" + 'Normal L T = (cnf L T). + +(* Basic properties *********************************************************) + +(* Basic_1: was: nf2_sort *) +lemma cnf_sort: ∀L,k. L ⊢ 𝐍[⋆k]. +#L #k #X #H +>(cpr_inv_sort1 … H) // +qed. + +(* Basic_1: removed theorems 1: nf2_abst_shift *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cnf_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cnf_lift.ma new file mode 100644 index 000000000..b492eb9af --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cnf_lift.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 "Basic_2/reducibility/cpr_lift.ma". +include "Basic_2/reducibility/cnf.ma". + +(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************) + +(* Advanced inversion lemmas ************************************************) + +(* Basic_1: was only: nf2_csort_lref *) +lemma cnf_lref_atom: ∀L,i. ⇩[0, i] L ≡ ⋆ → L ⊢ 𝐍[#i]. +#L #i #HLK #X #H +elim (cpr_inv_lref1 … H) // * +#K0 #V0 #V1 #HLK0 #_ #_ #_ +lapply (ldrop_mono … HLK … HLK0) -L #H destruct +qed. + +(* Basic_1: was: nf2_lref_abst *) +lemma cnf_lref_abst: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓛV → L ⊢ 𝐍[#i]. +#L #K #V #i #HLK #X #H +elim (cpr_inv_lref1 … H) // * +#K0 #V0 #V1 #HLK0 #_ #_ #_ +lapply (ldrop_mono … HLK … HLK0) -L #H destruct +qed. + +(* Basic_1: was: nf2_abst *) +lemma cnf_abst: ∀I,L,V,W,T. L ⊢ 𝐍[W] → L. ⓑ{I} V ⊢ 𝐍[T] → L ⊢ 𝐍[ⓛW.T]. +#I #L #V #W #T #HW #HT #X #H +elim (cpr_inv_abst1 … H I V) -H #W0 #T0 #HW0 #HT0 #H destruct +>(HW … HW0) -W >(HT … HT0) -T // +qed. + +(* Basic_1: was only: nf2_appl_lref *) +lemma cnf_appl_simple: ∀L,V,T. L ⊢ 𝐍[V] → L ⊢ 𝐍[T] → 𝐒[T] → L ⊢ 𝐍[ⓐV.T]. +#L #V #T #HV #HT #HS #X #H +elim (cpr_inv_appl1_simple … H ?) -H // #V0 #T0 #HV0 #HT0 #H destruct +>(HV … HV0) -V >(HT … HT0) -T // +qed. + +(* Relocation properties ****************************************************) + +(* Basic_1: was: nf2_lift *) +lemma cnf_lift: ∀L0,L,T,T0,d,e. + L ⊢ 𝐍[T] → ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → L0 ⊢ 𝐍[T0]. +#L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H +elim (cpr_inv_lift … HL0 … HT0 … H) -L0 #T1 #HT10 #HT1 +>(HLT … HT1) in HT0; -L #HT0 +>(lift_mono … HT10 … HT0) -T1 -X // +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma index 4c77444d4..032ff4638 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma @@ -44,9 +44,13 @@ elim (tpss_inv_lref1 … H) -H /2 width=1/ qed-. (* Basic_1: was: pr2_gen_abst *) -lemma cpr_inv_abst1: ∀V1,T1,U2. ⓛV1. T1 ➡ U2 → - ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓛV2. T2. -/2 width=3/ qed-. +lemma cpr_inv_abst1: ∀L,V1,T1,U2. L ⊢ ⓛV1. T1 ➡ U2 → ∀I,W. + ∃∃V2,T2. L ⊢ V1 ➡ V2 & L. ⓑ{I} W ⊢ T1 ➡ T2 & U2 = ⓛV2. T2. +#L #V1 #T1 #Y * #X #H1 #H2 #I #W +elim (tpr_inv_abst1 … H1) -H1 #V #T #HV1 #HT1 #H destruct +elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct +lapply (tpss_lsubs_conf … HT2 (L. ⓑ{I} W) ?) -HT2 /2 width=1/ /4 width=5/ +qed-. (* Basic_1: was pr2_gen_appl *) lemma cpr_inv_appl1: ∀L,V1,U0,U2. L ⊢ ⓐV1. U0 ➡ U2 → diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpss.ma similarity index 87% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_tpss.ma rename to matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpss.ma index 2add29208..d925d19c5 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_tpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpss.ma @@ -40,3 +40,12 @@ elim (tpr_inv_abbr1 … H1) -H1 * | /4 width=5/ ] qed-. + +(* Properties concerning partial unfold on local environments ***************) + +lemma ltpss_cpr_trans: ∀L1,L2,d,e. L1 [d, e] ▶* L2 → + ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2. +#L1 #L2 #d #e #HL12 #T1 #T2 * +lapply (ltpss_weak_all … HL12) +<(ltpss_fwd_length … HL12) -HL12 /3 width=5/ +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma index 9dd48e062..5c725a948 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma @@ -35,7 +35,7 @@ lemma ltpr_ldrop_conf: ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀L2. L1 ➡ L2 qed. (* Basic_1: was: wcpr0_ldrop_back *) -lemma ltpr_ldrop_trans: ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. K1 ➡ K2 → +lemma ldrop_ltpr_trans: ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. K1 ➡ K2 → ∃∃L2. ⇩[d, e] L2 ≡ K2 & L1 ➡ L2. #L1 #K1 #d #e #H elim H -L1 -K1 -d -e [ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2 width=3/ @@ -50,3 +50,21 @@ lemma ltpr_ldrop_trans: ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. K1 ➡ K2 elim (IHLK1 … HK12) -K1 /3 width=5/ ] qed. + +fact ltpr_ldrop_trans_O1_aux: ∀L2,K2,d,e. ⇩[d, e] L2 ≡ K2 → ∀L1. L1 ➡ L2 → + d = 0 → ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 ➡ K2. +#L2 #K2 #d #e #H elim H -L2 -K2 -d -e +[ #d #e #X #H >(ltpr_inv_atom2 … H) -H /2 width=3/ +| #K2 #I #V2 #X #H + elim (ltpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct /3 width=5/ +| #L2 #K2 #I #V2 #e #_ #IHLK2 #X #H #_ + elim (ltpr_inv_pair2 … H) -H #L1 #V1 #HL12 #HV12 #H destruct + elim (IHLK2 … HL12 ?) -L2 // /3 width=3/ +| #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_ + >commutative_plus normalize #H destruct +] +qed. + +lemma ltpr_ldrop_trans_O1: ∀L1,L2. L1 ➡ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 → + ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 ➡ K2. +/2 width=5/ qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_tps.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_tps.ma new file mode 100644 index 000000000..32ddb3a1f --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_tps.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/reducibility/ltpr_ldrop.ma". + +(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) + +(* Properties concerning parallel substitution on terms *********************) + +lemma ltpr_tps_trans: ∀L2,T1,T2,d,e. L2 ⊢ T1 [d, e] ▶ T2 → ∀L1. L1 ➡ L2 → + ∃∃T. L1 ⊢ T1 [d, e] ▶ T & T ➡ T2. +#L2 #T1 #T2 #d #e #H elim H -L2 -T1 -T2 -d -e +[ /2 width=3/ +| #L2 #K2 #V2 #W2 #i #d #e #Hdi #Hide #HLK2 #HVW2 #L1 #HL12 + elim (ltpr_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H + elim (ltpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct -K2 + elim (lift_total V1 0 (i+1)) #W1 #HVW1 + lapply (tpr_lift … HV12 … HVW1 … HVW2) -V2 /3 width=4/ +| #L2 #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L1 #HL12 + elim (IHV12 … HL12) -IHV12 #V #HV1 #HV2 + elim (IHT12 (L1.ⓑ{I}V) ?) /2 width=1/ -L2 /3 width=5/ +| #L2 #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L1 #HL12 + elim (IHV12 … HL12) -IHV12 + elim (IHT12 … HL12) -L2 /3 width=5/ +] +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma index 9f5547ed0..c4b6c87f0 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma @@ -53,6 +53,18 @@ lemma ltps_refl: ∀L,d,e. L [d, e] ▶ L. #L #I #V #IHL * /2 width=1/ * /2 width=1/ qed. +lemma ltps_weak_all: ∀L1,L2,d,e. L1 [d, e] ▶ L2 → L1 [0, |L2|] ▶ L2. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e +// /3 width=2/ /3 width=3/ +qed. + +(* Basic forward lemmas *****************************************************) + +lemma ltps_fwd_length: ∀L1,L2,d,e. L1 [d, e] ▶ L2 → |L1| = |L2|. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e +normalize // +qed-. + (* Basic inversion lemmas ***************************************************) fact ltps_inv_refl_O2_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → e = 0 → L1 = L2. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma index 28e9608e1..207bfc60f 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma @@ -40,6 +40,20 @@ lemma ltpss_strap: ∀L1,L,L2,d,e. lemma ltpss_refl: ∀L,d,e. L [d, e] ▶* L. /2 width=1/ qed. +lemma ltpss_weak_all: ∀L1,L2,d,e. L1 [d, e] ▶* L2 → L1 [0, |L2|] ▶* L2. +#L1 #L2 #d #e #H @(ltpss_ind … H) -L2 // +#L #L2 #_ #HL2 +>(ltps_fwd_length … HL2) /3 width=5/ +qed. + +(* Basic forward lemmas *****************************************************) + +lemma ltpss_fwd_length: ∀L1,L2,d,e. L1 [d, e] ▶* L2 → |L1| = |L2|. +#L1 #L2 #d #e #H @(ltpss_ind … H) -L2 // +#L #L2 #_ #HL2 #IHL12 >IHL12 -IHL12 +/2 width=3 by ltps_fwd_length/ +qed-. + (* Basic inversion lemmas ***************************************************) lemma ltpss_inv_refl_O2: ∀d,L1,L2. L1 [d, 0] ▶* L2 → L1 = L2. diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 72fca431c..cbedfcbf6 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1503,6 +1503,8 @@ let load_predefined_virtuals () = ;; let predefined_classes = [ + ["-"; "÷"; "⊢"; ]; + ["="; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; ]; ["→"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; ["⇒"; "➾"; "⇨"; "➡"; "⇉"; "⥤"; "⥰"; ] ; ["⇑"; "⇧"; "⬆"; ] ; -- 2.39.2