From 5ac2dc4e01aca542ddd13c02b304c646d8df9799 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 30 May 2012 21:10:44 +0000 Subject: [PATCH] - nDestructTac: Sys.break handled in two places - lambda_delta: a major property of native type assignment some properties of context sensitive equivalence some notational changes some annotations --- matita/components/ng_tactics/nDestructTac.ml | 8 +- .../contribs/lambda_delta/basic_2/basic_1.txt | 17 +-- .../basic_2/computation/acp_cr.ma | 2 +- .../lambda_delta/basic_2/computation/cpe.ma | 4 +- .../basic_2/computation/cpe_cpe.ma | 2 +- .../lambda_delta/basic_2/computation/cprs.ma | 2 +- .../basic_2/computation/cprs_tstc.ma | 2 +- .../basic_2/computation/cprs_tstc_vector.ma | 2 +- .../lambda_delta/basic_2/computation/csn.ma | 2 +- .../basic_2/computation/csn_lcpr.ma | 2 +- .../basic_2/computation/csn_lift.ma | 2 +- .../basic_2/computation/csn_tstc_vector.ma | 2 +- .../lambda_delta/basic_2/computation/lsubc.ma | 4 +- .../lambda_delta/basic_2/dynamic/nta.ma | 4 +- .../lambda_delta/basic_2/dynamic/nta_ltpss.ma | 121 ++++++++++++++++++ .../lambda_delta/basic_2/equivalence/cpcs.ma | 6 +- .../basic_2/equivalence/cpcs_cpcs.ma | 3 + .../basic_2/equivalence/cpcs_ltpr.ma | 43 +++++++ .../basic_2/equivalence/cpcs_ltpss.ma | 43 +++++++ .../basic_2/grammar/term_simple.ma | 6 +- .../basic_2/grammar/term_vector.ma | 2 +- .../lambda_delta/basic_2/grammar/tshf.ma | 10 +- .../lambda_delta/basic_2/grammar/tstc.ma | 4 +- .../basic_2/grammar/tstc_vector.ma | 2 +- .../contribs/lambda_delta/basic_2/notation.ma | 28 ++-- .../lambda_delta/basic_2/reducibility/cnf.ma | 4 +- .../basic_2/reducibility/cnf_lift.ma | 10 +- .../basic_2/reducibility/cpr_lift.ma | 2 +- .../basic_2/reducibility/lcpr_cpr.ma | 4 + .../lambda_delta/basic_2/reducibility/tif.ma | 16 +-- .../lambda_delta/basic_2/reducibility/tnf.ma | 8 +- .../basic_2/reducibility/tnf_tif.ma | 12 +- .../lambda_delta/basic_2/reducibility/tpr.ma | 2 +- .../lambda_delta/basic_2/reducibility/trf.ma | 14 +- .../basic_2/reducibility/twhnf.ma | 4 +- .../lambda_delta/basic_2/substitution/lift.ma | 4 +- .../lambda_delta/basic_2/unfold/lifts.ma | 4 +- .../lambda_delta/basic_2/unfold/ltpss.ma | 4 +- 38 files changed, 313 insertions(+), 98 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpss.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpr.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpss.ma diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml index be9914840..990cc672b 100644 --- a/matita/components/ng_tactics/nDestructTac.ml +++ b/matita/components/ng_tactics/nDestructTac.ml @@ -712,7 +712,9 @@ let rec destruct_tac0 tags acc domain skip status goal = let has_cleared = try let _ = NTactics.find_in_context eq_name (get_ctx status' newgoal) in false - with _ -> true in + with + | Sys.Break as e -> raise e + |_ -> true in let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in let acc = rm_eq has_cleared acc in let skip = rm_eq has_cleared skip in @@ -728,7 +730,9 @@ let rec destruct_tac0 tags acc domain skip status goal = let has_cleared = try let _ = NTactics.find_in_context eq_name (get_ctx status' newgoal) in false - with _ -> true in + with + | Sys.Break as e -> raise e + | _ -> true in let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in let acc = rm_eq has_cleared acc in let skip = rm_eq has_cleared skip in 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 0c6fcb34a..87bf34936 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt +++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt @@ -47,6 +47,7 @@ asucc/fwd asucc_gen_head cnt/props cnt_lift C/props clt_wf__q_ind C/props clt_wf_ind + csuba/arity csuba_arity csuba/arity csuba_arity_rev csuba/arity arity_appls_appl @@ -71,11 +72,12 @@ csuba/getl csuba_getl_abst csuba/getl csuba_getl_abst_rev csuba/getl csuba_getl_abbr_rev csuba/props csuba_refl + csubc/arity csubc_arity_conf csubc/arity csubc_arity_trans -csubc/csuba csubc_csuba csubc/drop1 drop1_csubc_trans csubc/drop drop_csubc_trans + csubt/clear csubt_clear_conf csubt/csuba csubt_csuba csubt/drop csubt_drop_flat @@ -110,7 +112,6 @@ ex1/props ex1_arity ex1/props ex1_ty3 ex2/props ex2_nf2 ex2/props ex2_arity -fsubst0/fwd fsubst0_gen_base leq/asucc asucc_repl leq/asucc asucc_inj leq/asucc leq_asucc @@ -167,22 +168,15 @@ pc1/props pc1_head pc3/dec pc3_dec pc3/dec pc3_abst_dec -pc3/fsubst0 pc3_pr2_fsubst0 -pc3/fsubst0 pc3_pr2_fsubst0_back -pc3/fsubst0 pc3_fsubst0 pc3/fwd pc3_gen_not_abst pc3/fwd pc3_gen_lift_abst pc3/nf2 pc3_nf2 pc3/nf2 pc3_nf2_unfold pc3/pc1 pc3_pc1 -pc3/props pc3_pr0_pr2_t pc3/props pc3_pr2_pr2_t pc3/props pc3_pr2_pr3_t pc3/props pc3_pr3_pc3_t pc3/props pc3_eta -pc3/wcpr0 pc3_wcpr0__pc3_wcpr0_t_aux -pc3/wcpr0 pc3_wcpr0_t -pc3/wcpr0 pc3_wcpr0 pr0/fwd pr0_gen_void pr0/dec nf0_dec @@ -229,9 +223,6 @@ ty3/arity_props ty3_repellent ty3/arity_props ty3_acyclic ty3/arity_props ty3_sn3 ty3/dec ty3_inference -ty3/fsubst0 ty3_fsubst0 -ty3/fsubst0 ty3_csubst0 -ty3/fsubst0 ty3_subst0 ty3/fwd ty3_gen_appl ty3/fwd tys3_gen_nil ty3/fwd tys3_gen_cons @@ -259,8 +250,8 @@ ty3/pr3_props ty3_sred_back ty3/pr3_props ty3_sconv ty3/props ty3_gen_abst_abst ty3/sty0 ty3_sty0 -ty3/subst1 ty3_gen_cabbr ty3/subst1 ty3_gen_cvoid + wf3/clear wf3_clear_conf wf3/clear clear_wf3_trans wf3/fwd wf3_gen_sort1 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 dff92c950..1805953b9 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 @@ -27,7 +27,7 @@ definition S1 ≝ λRP,C:lenv→predicate term. (* Note: this is Tait's iii, or Girard's CR4 *) definition S2 ≝ λRR:lenv→relation term. λRS:relation term. λRP,C:lenv→predicate term. ∀L,Vs. all … (RP L) Vs → - ∀T. 𝐒[T] → NF … (RR L) RS T → C L (ⒶVs.T). + ∀T. 𝐒⦃T⦄ → NF … (RR L) RS T → C L (ⒶVs.T). (* Note: this is Tait's ii *) definition S3 ≝ λRP,C:lenv→predicate term. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma index 22d7ea92a..8877fa44f 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma @@ -18,7 +18,7 @@ include "basic_2/computation/csn.ma". (* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************) definition cpe: lenv → relation term ≝ - λL,T1,T2. L ⊢ T1 ➡* T2 ∧ L ⊢ 𝐍[T2]. + λL,T1,T2. L ⊢ T1 ➡* T2 ∧ L ⊢ 𝐍⦃T2⦄. interpretation "context-sensitive parallel evaluation (term)" 'PEval L T1 T2 = (cpe L T1 T2). @@ -26,7 +26,7 @@ interpretation "context-sensitive parallel evaluation (term)" (* Basic_properties *********************************************************) (* Basic_1: was: nf2_sn3 *) -lemma cpe_csn: ∀L,T1. L ⊢ ⬇* T1 → ∃T2. L ⊢ T1 ➡* 𝐍[T2]. +lemma cpe_csn: ∀L,T1. L ⊢ ⬇* T1 → ∃T2. L ⊢ T1 ➡* 𝐍⦃T2⦄. #L #T1 #H @(csn_ind … H) -T1 #T1 #_ #IHT1 elim (cnf_dec L T1) /3 width=3/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cpe_cpe.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cpe_cpe.ma index 2c3b8b841..ec770787b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cpe_cpe.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cpe_cpe.ma @@ -20,7 +20,7 @@ include "basic_2/computation/cpe.ma". (* Main properties *********************************************************) (* Basic_1: was: nf2_pr3_confluence *) -theorem cpe_mono: ∀L,T,T1. L ⊢ T ➡* 𝐍[T1] → ∀T2. L ⊢ T ➡* 𝐍[T2] → T1 = T2. +theorem cpe_mono: ∀L,T,T1. L ⊢ T ➡* 𝐍⦃T1⦄ → ∀T2. L ⊢ T ➡* 𝐍⦃T2⦄ → T1 = T2. #L #T #T1 * #H1T1 #H2T1 #T2 * #H1T2 #H2T2 elim (cprs_conf … H1T1 … H1T2) -T #T #HT1 >(cprs_inv_cnf1 … HT1 H2T1) -T1 #HT2 diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma index 7bfe24895..a25a36a3e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma @@ -88,7 +88,7 @@ elim (cpr_inv_cast1 … HU2) -HU2 /3 width=3/ * qed-. (* Basic_1: was: nf2_pr3_unfold *) -lemma cprs_inv_cnf1: ∀L,T,U. L ⊢ T ➡* U → L ⊢ 𝐍[T] → T = U. +lemma cprs_inv_cnf1: ∀L,T,U. L ⊢ T ➡* U → L ⊢ 𝐍⦃T⦄ → T = U. #L #T #U #H @(cprs_ind_dx … H) -T // #T0 #T #H1T0 #_ #IHT #H2T0 lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma index 359174503..59668d4d1 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma @@ -20,7 +20,7 @@ include "basic_2/computation/cprs_lcprs.ma". (* Forward lemmas involving same top term constructor ***********************) -lemma cprs_fwd_cnf: ∀L,T. L ⊢ 𝐍[T] → ∀U. L ⊢ T ➡* U → T ≃ U. +lemma cprs_fwd_cnf: ∀L,T. L ⊢ 𝐍⦃T⦄ → ∀U. L ⊢ T ➡* U → T ≃ U. #L #T #HT #U #H >(cprs_inv_cnf1 … H HT) -L -T // 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 index feaedbf76..a7f9b33cd 100644 --- 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 @@ -21,7 +21,7 @@ include "basic_2/computation/cprs_tstc.ma". (* Vector form of forward lemmas involving same top term constructor ********) (* Basic_1: was just: nf2_iso_appls_lref *) -lemma cprs_fwd_cnf_vector: ∀L,T. 𝐒[T] → L ⊢ 𝐍[T] → ∀Vs,U. L ⊢ ⒶVs.T ➡* U → ⒶVs.T ≃ U. +lemma cprs_fwd_cnf_vector: ∀L,T. 𝐒⦃T⦄ → L ⊢ 𝐍⦃T⦄ → ∀Vs,U. L ⊢ ⒶVs.T ➡* U → ⒶVs.T ≃ U. #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cprs_fwd_cnf … H2T) ] (**) (* /2 width=3 by cprs_fwd_cnf/ does not work *) #V #Vs #IHVs #U #H elim (cprs_inv_appl1 … H) -H * 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 903c62ea2..481683f2a 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma @@ -43,7 +43,7 @@ lemma csn_intro: ∀L,T1. /4 width=1/ qed. (* Basic_1: was: sn3_nf2 *) -lemma csn_cnf: ∀L,T. L ⊢ 𝐍[T] → L ⊢ ⬇* T. +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. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma index 33c6455dc..3cd83733e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma @@ -121,7 +121,7 @@ lemma csn_appl_theta: ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬇* V → ∀T1. L ⊢ ⬇* T1 → (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → ⊥) → L ⊢ ⬇* ⓐV. T2) → - 𝐒[T1] → L ⊢ ⬇* ⓐV. T1. + 𝐒⦃T1⦄ → L ⊢ ⬇* ⓐV. T1. #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1 @csn_intro #X #HL #H elim (cpr_inv_appl1_simple … HL ?) -HL // 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 71b4d3380..85cdef226 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 @@ -71,7 +71,7 @@ qed. lemma csn_appl_simple: ∀L,V. L ⊢ ⬇* V → ∀T1. (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬇* ⓐV. T2) → - 𝐒[T1] → L ⊢ ⬇* ⓐV. T1. + 𝐒⦃T1⦄ → L ⊢ ⬇* ⓐV. T1. #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #IHT1 #HT1 @csn_intro #X #H1 #H2 elim (cpr_inv_appl1_simple … H1 ?) // -H1 diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma index e1a641505..566084615 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma @@ -22,7 +22,7 @@ include "basic_2/computation/csn_vector.ma". (* Advanced properties ******************************************************) (* Basic_1: was only: sn3_appls_lref *) -lemma csn_applv_cnf: ∀L,T. 𝐒[T] → L ⊢ 𝐍[T] → +lemma csn_applv_cnf: ∀L,T. 𝐒⦃T⦄ → L ⊢ 𝐍⦃T⦄ → ∀Vs. L ⊢ ⬇* Vs → L ⊢ ⬇* ⒶVs.T. #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(csn_cnf … H2T) ] (**) (* /2 width=1/ does not work *) #V #Vs #IHV #H diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma index 31ac81bf5..bcf6c7714 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma @@ -101,4 +101,6 @@ lemma lsubc_refl: ∀RP,L. L ⊑[RP] L. #RP #L elim L -L // /2 width=1/ qed. -(* Basic_1: removed theorems 2: csubc_clear_conf csubc_getl_conf *) +(* Basic_1: removed theorems 3: + csubc_clear_conf csubc_getl_conf csubc_csuba +*) diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma index 9f42e7fca..7a24249f2 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma @@ -48,4 +48,6 @@ lemma nta_cast_old: ∀h,L,W,T,U. lemma nta_typecheck: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ ⓣU.T : T0. /3 width=2/ qed. -(* Basic_1: removed theorems 1: ty3_getl_subst0 *) +(* Basic_1: removed theorems 4: + ty3_getl_subst0 ty3_fsubst0 ty3_csubst0 ty3_subst0 +*) diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpss.ma new file mode 100644 index 000000000..828fd82e0 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpss.ma @@ -0,0 +1,121 @@ +(**************************************************************************) +(* ___ *) +(* ||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/equivalence/cpcs_ltpss.ma". +include "basic_2/dynamic/nta_nta.ma". + +(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) + +(* Properties about parallel unfold *****************************************) + +lemma nta_ltpss_tpss_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → ⦃h, L2⦄ ⊢ T2 : U. +#h #L1 #T1 #U #H @(nta_ind_alt … H) -L1 -T1 -U +[ #L1 #k #L2 #d #e #_ #T2 #H + >(tpss_inv_sort1 … H) -H // +| #L1 #K1 #V1 #W #U #i #HLK1 #_ #HWU #IHV1 #L2 #d #e #HL12 #T2 #H + elim (tpss_inv_lref1 … H) -H + [ #H destruct + elim (lt_or_ge i d) #Hdi + [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2 + elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ -Hdi #K2 #V2 #HK12 #HV12 #H destruct + /3 width=7/ + | elim (lt_or_ge i (d + e)) #Hide [ | -Hdi ] + [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2 + elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K2 #V2 #HK12 #HV12 #H destruct + /3 width=7/ + | lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /3 width=7/ + ] + ] + | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #HVW2 #HWT2 + elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0 + elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #HK12 #HV12 #H destruct + lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2 + lapply (tpss_trans_eq … HV12 HVW2) -V2 /3 width=9/ + ] +| #L1 #K1 #W1 #V1 #U1 #i #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #d #e #HL12 #T2 #H + elim (tpss_inv_lref1 … H) -H [ | -HWV1 -HWU1 -IHWV1 ] + [ #H destruct + elim (lift_total V1 0 (i+1)) #W #HW + elim (lt_or_ge i d) #Hdi [ -HWV1 ] + [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2 + elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ -Hdi #K2 #W2 #HK12 #HW12 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) #HLK + lapply (nta_lift h … HLK … HWU1 … HW) /2 width=4/ -HW + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (tpss_lift_ge … HW12 … HLK … HWU1 … HWU2) -HLK -HWU1 // #HU12 + lapply (cpr_tpss … HU12) -HU12 #HU12 + @(nta_conv … U2) /2 width=1/ /3 width=6/ (**) (* explicit constructor, /4 width=6/ is too slow *) + | elim (lt_or_ge i (d + e)) #Hide [ -HWV1 | -IHWV1 -HW -Hdi ] + [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2 + elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K2 #W2 #HK12 #HW12 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) #HLK + lapply (nta_lift h … HLK … HWU1 … HW) /2 width=4/ -HW + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (tpss_lift_ge … HW12 … HLK … HWU1 … HWU2) -HLK -HWU1 // #HU12 + lapply (cpr_tpss … HU12) -HU12 #HU12 + @(nta_conv … U2) /2 width=1/ /3 width=6/ (**) (* explicit constructor, /4 width=6/ is too slow *) + | lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /2 width=6/ + ] + ] + | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #_ #_ + elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0 + elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #_ #_ #H destruct + lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 -HLK2 #H destruct + ] +| #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL12 #X #H + elim (tpss_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + lapply (cpr_tpss … HV12) #HV + lapply (IHTU1 (L2.ⓑ{I}V1) (d+1) e ? T1 ?) // /2 width=1/ #H + elim (nta_fwd_correct … H) -H #U2 #HU12 + @(nta_conv … (ⓑ{I}V2.U1)) /3 width=2/ /3 width=4/ /4 width=4/ (**) (* explicit constructor, /5 width=6/ is too slow *) +| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL12 #X #H + elim (tpss_inv_flat1 … H) -H #V2 #Y #HV12 #HY #H destruct + elim (tpss_inv_bind1 … HY) -HY #W2 #T2 #HW12 #HT12 #H destruct + lapply (cpr_tpss … HV12) #HV + lapply (IHTU1 L2 d e ? (ⓛW1.T1) ?) // #H + elim (nta_fwd_correct … H) -H #X #H + elim (nta_inv_bind1 … H) -H #W #U #HW #HU #_ + @(nta_conv … (ⓐV2.ⓛW1.U1)) /3 width=2/ /3 width=4/ /4 width=5/ (**) (* explicit constructor, /5 width=5/ is too slow *) +| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H + elim (tpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + lapply (cpr_tpss … HV12) #HV + elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=4/ ] #U #HU + @(nta_conv … (ⓐV2.U1)) // /3 width=1/ /4 width=5/ (**) (* explicit constructor, /5 width=5/ is too slow *) +| #L1 #T1 #U1 #W1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H + elim (tpss_inv_flat1 … H) -H #U2 #T2 #HU12 #HT12 #H destruct + lapply (cpr_tpss … HU12) /4 width=4/ +| #L1 #T1 #U11 #U12 #U #_ #HU112 #_ #IHTU11 #IHU12 #L2 #d #e #HL12 #T2 #HT12 + @(nta_conv … U11) /2 width=5/ (**) (* explicot constructor, /3 width=7/ is too slow *) +] +qed. + +lemma nta_ltpss_tps_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∀T2. L2 ⊢ T1 ▶ [d, e] T2 → ⦃h, L2⦄ ⊢ T2 : U. +/3 width=7/ qed. + +lemma nta_ltpss_conf: ∀h,L1,T,U. ⦃h, L1⦄ ⊢ T : U → + ∀L2,d,e. L1 ▶* [d, e] L2 → ⦃h, L2⦄ ⊢ T : U. +/2 width=7/ qed. + +lemma nta_tpss_conf: ∀h,L,T1,U. ⦃h, L⦄ ⊢ T1 : U → + ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 → ⦃h, L⦄ ⊢ T2 : U. +/2 width=7/ qed. + +lemma nta_tps_conf: ∀h,L,T1,U. ⦃h, L⦄ ⊢ T1 : U → + ∀T2,d,e. L ⊢ T1 ▶ [d, e] T2 → ⦃h, L⦄ ⊢ T2 : U. +/2 width=7/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma index 5ee8d1696..346189f92 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma @@ -79,9 +79,11 @@ lemma cprs_comm: ∀L,T1,T2. L ⊢ T1 ⬌* T2 → L ⊢ T2 ⬌* T1. #L #T1 #T2 #H @(cpcs_ind … H) -T2 // /3 width=3/ qed. -(* Basic_1: removed theorems 6: +(* Basic_1: removed theorems 9: clear_pc3_trans pc3_ind_left pc3_head_1 pc3_head_2 pc3_head_12 pc3_head_21 - Basic_1: removed local theorems 5: + pc3_pr2_fsubst0 pc3_pr2_fsubst0_back pc3_fsubst0 + Basic_1: removed local theorems 6: pc3_left_pr3 pc3_left_trans pc3_left_sym pc3_left_pc3 pc3_pc3_left + pc3_wcpr0_t_aux *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma index b5ebbe8af..71fe21e80 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma @@ -108,6 +108,9 @@ lemma cpcs_abbr_sn: ∀L,V1,V2,T. L ⊢ V1 ⬌* V2 → L ⊢ ⓓV1. T ⬌* ⓓV2 elim (cpcs_inv_cprs … HV12) -HV12 /3 width=5 by cprs_div, cprs_abbr1/ (**) (* /3 width=5/ is a bit slow *) qed. +lemma cpcs_bind_sn: ∀I,L,V1,V2,T. L ⊢ V1 ⬌* V2 → L ⊢ ⓑ{I}V1. T ⬌* ⓑ{I}V2. T. +* /2 width=1/ /2 width=2/ qed. + (* Basic_1: was: pc3_lift *) lemma cpcs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 → diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpr.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpr.ma new file mode 100644 index 000000000..13713e51e --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpr.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||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_ltpr.ma". +include "basic_2/equivalence/cpcs_cpcs.ma". + +(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) + +(* Properties about context-free parallel reduction on local environments ***) + +(* Basic_1: was only: pc3_pr0_pr2_t *) +(* Basic_1: note: pc3_pr0_pr2_t should be renamed *) +lemma ltpr_cpr_conf: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡ T2 → L2 ⊢ T1 ⬌* T2. +#L1 #L2 #HL12 #T1 #T2 #HT12 +elim (cpr_ltpr_conf_eq … HT12 … HL12) -L1 #T #HT1 #HT2 +@(cprs_div … T) /2 width=1/ /3 width=1/ (**) (* /4 width=3/ is too long *) +qed. + +(* Basic_1: was: pc3_wcpr0_t *) +(* Basic_1: note: pc3_wcpr0_t should be renamed *) +lemma ltpr_cprs_conf: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡* T2 → L2 ⊢ T1 ⬌* T2. +#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 // +#T #T2 #_ #HT2 #IHT1 +@(cpcs_trans … IHT1) -T1 /2 width=3/ +qed. + +(* Basic_1: was: pc3_wcpr0 *) +lemma ltpr_cpcs_conf: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2. +#L1 #L2 #HL12 #T1 #T2 #H +elim (cpcs_inv_cprs … H) -H #T #HT1 #HT2 +@(cpcs_canc_dx … T) /2 width=3/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpss.ma new file mode 100644 index 000000000..1bec6e57d --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpss.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||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/ltpss_ltpss.ma". +include "basic_2/equivalence/cpcs_cpcs.ma". + +(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) + +(* Properties concerning partial unfold on local environments ***************) + +lemma ltpss_cpr_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → + ∀T1,T2. L1 ⊢ T1 ➡ T2 → L2 ⊢ T1 ⬌* T2. +#L1 #L2 #d #e #HL12 #T1 #T2 * +lapply (ltpss_weak_all … HL12) +>(ltpss_fwd_length … HL12) -HL12 #HL12 #T #HT1 #HT2 +elim (ltpss_tpss_conf … HT2 … HL12) -L1 #T0 #HT0 #HT20 +@(cprs_div … T0) /3 width=3/ (**) (* /4/ is too slow *) +qed. + +lemma ltpss_cprs_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → + ∀T1,T2. L1 ⊢ T1 ➡* T2 → L2 ⊢ T1 ⬌* T2. +#L1 #L2 #d #e #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 // +#T #T2 #_ #HT2 #IHT1 +@(cpcs_trans … IHT1) -T1 /2 width=5/ +qed. + +lemma ltpss_cpcs_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → + ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2. +#L1 #L2 #d #e #HL12 #T1 #T2 #H +elim (cpcs_inv_cprs … H) -H #T #HT1 #HT2 +@(cpcs_canc_dx … T) /2 width=5/ +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 f32ae0e7e..4c02d521d 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 @@ -25,17 +25,17 @@ interpretation "simple (term)" 'Simple T = (simple T). (* Basic inversion lemmas ***************************************************) -fact simple_inv_bind_aux: ∀T. 𝐒[T] → ∀J,W,U. T = ⓑ{J} W. U → ⊥. +fact simple_inv_bind_aux: ∀T. 𝐒⦃T⦄ → ∀J,W,U. T = ⓑ{J} W. U → ⊥. #T * -T [ #I #J #W #U #H destruct | #I #V #T #J #W #U #H destruct ] qed. -lemma simple_inv_bind: ∀I,V,T. 𝐒[ⓑ{I} V. T] → ⊥. +lemma simple_inv_bind: ∀I,V,T. 𝐒⦃ⓑ{I} V. T⦄ → ⊥. /2 width=6/ qed-. -lemma simple_inv_pair: ∀I,V,T. 𝐒[②{I}V.T] → ∃J. I = Flat2 J. +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/term_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma index 7b4923bbe..3be7a3839 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma @@ -28,6 +28,6 @@ interpretation "application o vevtor (term)" (* properties concerning simple terms ***************************************) -lemma applv_simple: ∀T,Vs. 𝐒[T] -> 𝐒[ⒶVs.T]. +lemma applv_simple: ∀T,Vs. 𝐒⦃T⦄ -> 𝐒⦃ⒶVs.T⦄. #T * // qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/tshf.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/tshf.ma index bb32a5365..34561ebf6 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/tshf.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/tshf.ma @@ -19,7 +19,7 @@ include "basic_2/grammar/term_simple.ma". inductive tshf: relation term ≝ | tshf_atom: ∀I. tshf (⓪{I}) (⓪{I}) | tshf_abst: ∀V1,V2,T1,T2. tshf (ⓛV1. T1) (ⓛV2. T2) - | tshf_appl: ∀V1,V2,T1,T2. tshf T1 T2 → 𝐒[T1] → 𝐒[T2] → + | tshf_appl: ∀V1,V2,T1,T2. tshf T1 T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄ → tshf (ⓐV1. T1) (ⓐV2. T2) . @@ -38,13 +38,13 @@ qed. lemma tshf_refl1: ∀T1,T2. T1 ≈ T2 → T1 ≈ T1. /3 width=2/ qed. -lemma simple_tshf_repl_dx: ∀T1,T2. T1 ≈ T2 → 𝐒[T1] → 𝐒[T2]. +lemma simple_tshf_repl_dx: ∀T1,T2. T1 ≈ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. #T1 #T2 #H elim H -T1 -T2 // #V1 #V2 #T1 #T2 #H elim (simple_inv_bind … H) qed. (**) (* remove from index *) -lemma simple_tshf_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝐒[T2] → 𝐒[T1]. +lemma simple_tshf_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. /3 width=3/ qed-. (* Basic inversion lemmas ***************************************************) @@ -63,7 +63,7 @@ lemma tshf_inv_bind1: ∀I,W1,U1,T2. ⓑ{I}W1.U1 ≈ T2 → /2 width=5/ qed-. fact tshf_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 → - ∃∃W2,U2. U1 ≈ U2 & 𝐒[U1] & 𝐒[U2] & + ∃∃W2,U2. U1 ≈ U2 & 𝐒⦃U1⦄ & 𝐒⦃U2⦄ & I = Appl & T2 = ⓐW2. U2. #T1 #T2 * -T1 -T2 [ #J #I #W1 #U1 #H destruct @@ -73,6 +73,6 @@ fact tshf_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 qed. lemma tshf_inv_flat1: ∀I,W1,U1,T2. ⓕ{I}W1.U1 ≈ T2 → - ∃∃W2,U2. U1 ≈ U2 & 𝐒[U1] & 𝐒[U2] & + ∃∃W2,U2. U1 ≈ U2 & 𝐒⦃U1⦄ & 𝐒⦃U2⦄ & I = Appl & T2 = ⓐW2. U2. /2 width=4/ 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 a4117b596..78a9b4987 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc.ma @@ -97,11 +97,11 @@ lemma tstc_dec: ∀T1,T2. Decidable (T1 ≃ T2). ] qed. -lemma simple_tstc_repl_dx: ∀T1,T2. T1 ≃ T2 → 𝐒[T1] → 𝐒[T2]. +lemma simple_tstc_repl_dx: ∀T1,T2. T1 ≃ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. #T1 #T2 * -T1 -T2 // #I #V1 #V2 #T1 #T2 #H elim (simple_inv_pair … H) -H #J #H destruct // qed. (**) (* remove from index *) -lemma simple_tstc_repl_sn: ∀T1,T2. T1 ≃ T2 → 𝐒[T2] → 𝐒[T1]. +lemma simple_tstc_repl_sn: ∀T1,T2. T1 ≃ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. /3 width=3/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma index 1ded6dd5d..bd4f877d4 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma @@ -21,7 +21,7 @@ include "basic_2/grammar/tstc.ma". (* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *) lemma tstc_inv_bind_appls_simple: ∀I,Vs,V2,T1,T2. ⒶVs.T1 ≃ ⓑ{I} V2. T2 → - 𝐒[T1] → ⊥. + 𝐒⦃T1⦄ → ⊥. #I #Vs #V2 #T1 #T2 #H elim (tstc_inv_pair2 … H) -H #V0 #T0 elim Vs -Vs normalize diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index 398ca7df4..ba7e981ca 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -104,7 +104,7 @@ notation "hvbox( # [ x , break y ] )" non associative with precedence 90 for @{ 'Weight $x $y }. -notation "hvbox( 𝐒 [ T ] )" +notation "hvbox( 𝐒 ⦃ T ⦄ )" non associative with precedence 45 for @{ 'Simple $T }. @@ -234,51 +234,51 @@ notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 •* break term 46 T2 (* Reducibility *************************************************************) -notation "hvbox( 𝐑 [ T ] )" +notation "hvbox( 𝐑 ⦃ T ⦄ )" non associative with precedence 45 for @{ 'Reducible $T }. -notation "hvbox( L ⊢ break 𝐑 [ T ] )" +notation "hvbox( L ⊢ break 𝐑 ⦃ T ⦄ )" non associative with precedence 45 for @{ 'Reducible $L $T }. -notation "hvbox( 𝐈 [ T ] )" +notation "hvbox( 𝐈 ⦃ T ⦄ )" non associative with precedence 45 for @{ 'NotReducible $T }. -notation "hvbox( L ⊢ break 𝐈 [ T ] )" +notation "hvbox( L ⊢ break 𝐈 ⦃ T ⦄ )" non associative with precedence 45 for @{ 'NotReducible $L $T }. -notation "hvbox( 𝐍 [ T ] )" +notation "hvbox( 𝐍 ⦃ T ⦄ )" non associative with precedence 45 for @{ 'Normal $T }. -notation "hvbox( L ⊢ break 𝐍 [ T ] )" +notation "hvbox( L ⊢ break 𝐍 ⦃ T ⦄ )" non associative with precedence 45 for @{ 'Normal $L $T }. -notation "hvbox( 𝐖𝐇𝐑 [ T ] )" +notation "hvbox( 𝐖𝐇𝐑 ⦃ T ⦄ )" non associative with precedence 45 for @{ 'WHdReducible $T }. -notation "hvbox( L ⊢ break 𝐖𝐇𝐑 [ T ] )" +notation "hvbox( L ⊢ break 𝐖𝐇𝐑 ⦃ T ⦄ )" non associative with precedence 45 for @{ 'WHdReducible $L $T }. -notation "hvbox( 𝐖𝐇𝐈 [ T ] )" +notation "hvbox( 𝐖𝐇𝐈 ⦃ T ⦄ )" non associative with precedence 45 for @{ 'NotWHdReducible $T }. -notation "hvbox( L ⊢ break 𝐖𝐇𝐈 [ T ] )" +notation "hvbox( L ⊢ break 𝐖𝐇𝐈 ⦃ T ⦄ )" non associative with precedence 45 for @{ 'NotWHdReducible $L $T }. -notation "hvbox( 𝐖𝐇𝐍 [ T ] )" +notation "hvbox( 𝐖𝐇𝐍 ⦃ T ⦄ )" non associative with precedence 45 for @{ 'WHdNormal $T }. -notation "hvbox( L ⊢ break 𝐖𝐇𝐍 [ T ] )" +notation "hvbox( L ⊢ break 𝐖𝐇𝐍 ⦃ T ⦄ )" non associative with precedence 45 for @{ 'WHdNormal $L $T }. @@ -308,7 +308,7 @@ notation "hvbox( L1 ⊢ ➡* break term 46 L2 )" non associative with precedence 45 for @{ 'CPRedStar $L1 $L2 }. -notation "hvbox( L ⊢ break term 46 T1 ➡* break 𝐍 [ T2 ] )" +notation "hvbox( L ⊢ break term 46 T1 ➡* break 𝐍 ⦃ T2 ⦄ )" non associative with precedence 45 for @{ 'PEval $L $T1 $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 index 1156dcf68..41f363368 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma @@ -25,13 +25,13 @@ interpretation (* Basic properties *********************************************************) (* Basic_1: was: nf2_sort *) -lemma cnf_sort: ∀L,k. L ⊢ 𝐍[⋆k]. +lemma cnf_sort: ∀L,k. L ⊢ 𝐍⦃⋆k⦄. #L #k #X #H >(cpr_inv_sort1 … H) // qed. (* Basic_1: was: nf2_dec *) -axiom cnf_dec: ∀L,T1. L ⊢ 𝐍[T1] ∨ +axiom cnf_dec: ∀L,T1. L ⊢ 𝐍⦃T1⦄ ∨ ∃∃T2. L ⊢ T1 ➡ T2 & (T1 = T2 → ⊥). (* 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 index e0d8d57bb..3aefb3643 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma @@ -20,7 +20,7 @@ include "basic_2/reducibility/cnf.ma". (* Advanced inversion lemmas ************************************************) (* Basic_1: was only: nf2_csort_lref *) -lemma cnf_lref_atom: ∀L,i. ⇩[0, i] L ≡ ⋆ → L ⊢ 𝐍[#i]. +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 #_ #_ #_ @@ -28,7 +28,7 @@ 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]. +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 #_ #_ #_ @@ -36,14 +36,14 @@ 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]. +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) -W0 >(HT … HT0) -T0 // qed. (* Basic_1: was only: nf2_appl_lref *) -lemma cnf_appl_simple: ∀L,V,T. L ⊢ 𝐍[V] → L ⊢ 𝐍[T] → 𝐒[T] → L ⊢ 𝐍[ⓐV.T]. +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) -V0 >(HT … HT0) -T0 // @@ -53,7 +53,7 @@ qed. (* 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]. + 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 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 120946cb1..dedb174e6 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 @@ -88,7 +88,7 @@ elim (tpr_inv_appl1 … H1) -H1 * qed-. (* Note: the main property of simple terms *) -lemma cpr_inv_appl1_simple: ∀L,V1,T1,U. L ⊢ ⓐV1. T1 ➡ U → 𝐒[T1] → +lemma cpr_inv_appl1_simple: ∀L,V1,T1,U. L ⊢ ⓐV1. T1 ➡ U → 𝐒⦃T1⦄ → ∃∃V2,T2. L ⊢ V1 ➡ V2 & L ⊢ T1 ➡ T2 & U = ⓐV2. T2. #L #V1 #T1 #U #H #HT1 diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma index 08f63e87f..69edad2aa 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma @@ -25,3 +25,7 @@ lemma lcpr_pair: ∀L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. L2 ⊢ V1 ➡ V2 → #L1 #L2 * #L #HL1 #HL2 #V1 #V2 * <(ltpss_fwd_length … HL2) /4 width=5/ qed. + +lemma ltpss_lcpr: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → L1 ⊢ ➡ L2. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // /3 width=3/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma index 653ed4700..a745dd844 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma @@ -16,39 +16,39 @@ include "basic_2/reducibility/trf.ma". (* CONTEXT-FREE IRREDUCIBLE TERMS *******************************************) -definition tif: predicate term ≝ λT. 𝐑[T] → ⊥. +definition tif: predicate term ≝ λT. 𝐑⦃T⦄ → ⊥. interpretation "context-free irreducibility (term)" 'NotReducible T = (tif T). (* Basic inversion lemmas ***************************************************) -lemma tif_inv_abbr: ∀V,T. 𝐈[ⓓV.T] → ⊥. +lemma tif_inv_abbr: ∀V,T. 𝐈⦃ⓓV.T⦄ → ⊥. /2 width=1/ qed-. -lemma tif_inv_abst: ∀V,T. 𝐈[ⓛV.T] → 𝐈[V] ∧ 𝐈[T]. +lemma tif_inv_abst: ∀V,T. 𝐈⦃ⓛV.T⦄ → 𝐈⦃V⦄ ∧ 𝐈⦃T⦄. /4 width=1/ qed-. -lemma tif_inv_appl: ∀V,T. 𝐈[ⓐV.T] → ∧∧ 𝐈[V] & 𝐈[T] & 𝐒[T]. +lemma tif_inv_appl: ∀V,T. 𝐈⦃ⓐV.T⦄ → ∧∧ 𝐈⦃V⦄ & 𝐈⦃T⦄ & 𝐒⦃T⦄. #V #T #HVT @and3_intro /3 width=1/ generalize in match HVT; -HVT elim T -T // * // * #U #T #_ #_ #H elim (H ?) -H /2 width=1/ qed-. -lemma tif_inv_cast: ∀V,T. 𝐈[ⓣV.T] → ⊥. +lemma tif_inv_cast: ∀V,T. 𝐈⦃ⓣV.T⦄ → ⊥. /2 width=1/ qed-. (* Basic properties *********************************************************) -lemma tif_atom: ∀I. 𝐈[⓪{I}]. +lemma tif_atom: ∀I. 𝐈⦃⓪{I}⦄. /2 width=4/ qed. -lemma tif_abst: ∀V,T. 𝐈[V] → 𝐈[T] → 𝐈[ⓛV.T]. +lemma tif_abst: ∀V,T. 𝐈⦃V⦄ → 𝐈⦃T⦄ → 𝐈⦃ⓛV.T⦄. #V #T #HV #HT #H elim (trf_inv_abst … H) -H /2 width=1/ qed. -lemma tif_appl: ∀V,T. 𝐈[V] → 𝐈[T] → 𝐒[T] → 𝐈[ⓐV.T]. +lemma tif_appl: ∀V,T. 𝐈⦃V⦄ → 𝐈⦃T⦄ → 𝐒⦃T⦄ → 𝐈⦃ⓐV.T⦄. #V #T #HV #HT #S #H elim (trf_inv_appl … H) -H /2 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma index 6f6d99096..294546af9 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma @@ -24,14 +24,14 @@ interpretation (* Basic inversion lemmas ***************************************************) -lemma tnf_inv_abst: ∀V,T. 𝐍[ⓛV.T] → 𝐍[V] ∧ 𝐍[T]. +lemma tnf_inv_abst: ∀V,T. 𝐍⦃ⓛV.T⦄ → 𝐍⦃V⦄ ∧ 𝐍⦃T⦄. #V1 #T1 #HVT1 @conj [ #V2 #HV2 lapply (HVT1 (ⓛV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct // | #T2 #HT2 lapply (HVT1 (ⓛV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct // ] qed-. -lemma tnf_inv_appl: ∀V,T. 𝐍[ⓐV.T] → ∧∧ 𝐍[V] & 𝐍[T] & 𝐒[T]. +lemma tnf_inv_appl: ∀V,T. 𝐍⦃ⓐV.T⦄ → ∧∧ 𝐍⦃V⦄ & 𝐍⦃T⦄ & 𝐒⦃T⦄. #V1 #T1 #HVT1 @and3_intro [ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct // | #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct // @@ -42,7 +42,7 @@ lemma tnf_inv_appl: ∀V,T. 𝐍[ⓐV.T] → ∧∧ 𝐍[V] & 𝐍[T] & 𝐒[T]. ] qed-. -lemma tnf_inv_abbr: ∀V,T. 𝐍[ⓓV.T] → ⊥. +lemma tnf_inv_abbr: ∀V,T. 𝐍⦃ⓓV.T⦄ → ⊥. #V #T #H elim (is_lift_dec T 0 1) [ * #U #HTU lapply (H U ?) -H /2 width=3/ #H destruct @@ -53,7 +53,7 @@ lemma tnf_inv_abbr: ∀V,T. 𝐍[ⓓV.T] → ⊥. ] qed. -lemma tnf_inv_cast: ∀V,T. 𝐍[ⓣV.T] → ⊥. +lemma tnf_inv_cast: ∀V,T. 𝐍⦃ⓣV.T⦄ → ⊥. #V #T #H lapply (H T ?) -H /2 width=1/ #H @discr_tpair_xy_y // qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma index ecfc2f160..2a8ea3c49 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma @@ -20,7 +20,7 @@ include "basic_2/reducibility/tnf.ma". (* Main properties properties ***********************************************) -lemma tpr_tif_eq: ∀T1,T2. T1 ➡ T2 → 𝐈[T1] → T1 = T2. +lemma tpr_tif_eq: ∀T1,T2. T1 ➡ T2 → 𝐈⦃T1⦄ → T1 = T2. #T1 #T2 #H elim H -T1 -T2 [ // | * #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H @@ -47,11 +47,11 @@ lemma tpr_tif_eq: ∀T1,T2. T1 ➡ T2 → 𝐈[T1] → T1 = T2. ] qed. -theorem tif_tnf: ∀T1. 𝐈[T1] → 𝐍[T1]. +theorem tif_tnf: ∀T1. 𝐈⦃T1⦄ → 𝐍⦃T1⦄. /3 width=1/ qed. (* Note: this property is unusual *) -lemma tnf_trf_false: ∀T1. 𝐑[T1] → 𝐍[T1] → ⊥. +lemma tnf_trf_false: ∀T1. 𝐑⦃T1⦄ → 𝐍⦃T1⦄ → ⊥. #T1 #H elim H -T1 [ #V #T #_ #IHV #H elim (tnf_inv_abst … H) -H /2 width=1/ | #V #T #_ #IHT #H elim (tnf_inv_abst … H) -H /2 width=1/ @@ -64,11 +64,11 @@ lemma tnf_trf_false: ∀T1. 𝐑[T1] → 𝐍[T1] → ⊥. ] qed. -theorem tnf_tif: ∀T1. 𝐍[T1] → 𝐈[T1]. +theorem tnf_tif: ∀T1. 𝐍⦃T1⦄ → 𝐈⦃T1⦄. /2 width=3/ qed. -lemma tnf_abst: ∀V,T. 𝐍[V] → 𝐍[T] → 𝐍[ⓛV.T]. +lemma tnf_abst: ∀V,T. 𝐍⦃V⦄ → 𝐍⦃T⦄ → 𝐍⦃ⓛV.T⦄. /4 width=1/ qed. -lemma tnf_appl: ∀V,T. 𝐍[V] → 𝐍[T] → 𝐒[T] → 𝐍[ⓐV.T]. +lemma tnf_appl: ∀V,T. 𝐍⦃V⦄ → 𝐍⦃T⦄ → 𝐒⦃T⦄ → 𝐍⦃ⓐV.T⦄. /4 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma index 3bab61adf..8cb87ef2c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma @@ -155,7 +155,7 @@ elim (tpr_inv_flat1 … H) -H * /3 width=12/ #_ #H destruct qed-. (* Note: the main property of simple terms *) -lemma tpr_inv_appl1_simple: ∀V1,T1,U. ⓐV1. T1 ➡ U → 𝐒[T1] → +lemma tpr_inv_appl1_simple: ∀V1,T1,U. ⓐV1. T1 ➡ U → 𝐒⦃T1⦄ → ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U = ⓐV2. T2. #V1 #T1 #U #H #HT1 diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma index 84b640831..eb3576d84 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma @@ -33,7 +33,7 @@ interpretation (* Basic inversion lemmas ***************************************************) -fact trf_inv_atom_aux: ∀I,T. 𝐑[T] → T = ⓪{I} → ⊥. +fact trf_inv_atom_aux: ∀I,T. 𝐑⦃T⦄ → T = ⓪{I} → ⊥. #I #T * -T [ #V #T #_ #H destruct | #V #T #_ #H destruct @@ -45,10 +45,10 @@ fact trf_inv_atom_aux: ∀I,T. 𝐑[T] → T = ⓪{I} → ⊥. ] qed. -lemma trf_inv_atom: ∀I. 𝐑[⓪{I}] → ⊥. +lemma trf_inv_atom: ∀I. 𝐑⦃⓪{I}⦄ → ⊥. /2 width=4/ qed-. -fact trf_inv_abst_aux: ∀W,U,T. 𝐑[T] → T = ⓛW. U → 𝐑[W] ∨ 𝐑[U]. +fact trf_inv_abst_aux: ∀W,U,T. 𝐑⦃T⦄ → T = ⓛW. U → 𝐑⦃W⦄ ∨ 𝐑⦃U⦄. #W #U #T * -T [ #V #T #HV #H destruct /2 width=1/ | #V #T #HT #H destruct /2 width=1/ @@ -60,11 +60,11 @@ fact trf_inv_abst_aux: ∀W,U,T. 𝐑[T] → T = ⓛW. U → 𝐑[W] ∨ 𝐑[U ] qed. -lemma trf_inv_abst: ∀V,T. 𝐑[ⓛV.T] → 𝐑[V] ∨ 𝐑[T]. +lemma trf_inv_abst: ∀V,T. 𝐑⦃ⓛV.T⦄ → 𝐑⦃V⦄ ∨ 𝐑⦃T⦄. /2 width=3/ qed-. -fact trf_inv_appl_aux: ∀W,U,T. 𝐑[T] → T = ⓐW. U → - ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → ⊥). +fact trf_inv_appl_aux: ∀W,U,T. 𝐑⦃T⦄ → T = ⓐW. U → + ∨∨ 𝐑⦃W⦄ | 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥). #W #U #T * -T [ #V #T #_ #H destruct | #V #T #_ #H destruct @@ -77,5 +77,5 @@ fact trf_inv_appl_aux: ∀W,U,T. 𝐑[T] → T = ⓐW. U → ] qed. -lemma trf_inv_appl: ∀W,U. 𝐑[ⓐW.U] → ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → ⊥). +lemma trf_inv_appl: ∀W,U. 𝐑⦃ⓐW.U⦄ → ∨∨ 𝐑⦃W⦄ | 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥). /2 width=3/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma index 2a5e62f34..5125fbb0e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma @@ -25,7 +25,7 @@ interpretation (* Basic inversion lemmas ***************************************************) -lemma twhnf_inv_tshf: ∀T. 𝐖𝐇𝐍[T] → T ≈ T. +lemma twhnf_inv_tshf: ∀T. 𝐖𝐇𝐍⦃T⦄ → T ≈ T. normalize /2 width=1/ qed-. @@ -52,5 +52,5 @@ lemma tpr_tshf: ∀T1,T2. T1 ➡ T2 → T1 ≈ T1 → T1 ≈ T2. ] qed. -lemma twhnf_tshf: ∀T. T ≈ T → 𝐖𝐇𝐍[T]. +lemma twhnf_tshf: ∀T. T ≈ T → 𝐖𝐇𝐍⦃T⦄. /3 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma index 643da9c05..622f4ef53 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma @@ -271,13 +271,13 @@ lemma tw_lift: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → #[T1] = #[T2]. #d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize // qed-. -lemma lift_simple_dx: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → 𝐒[T1] → 𝐒[T2]. +lemma lift_simple_dx: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. #d #e #T1 #T2 #H elim H -d -e -T1 -T2 // #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #H elim (simple_inv_bind … H) qed-. -lemma lift_simple_sn: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → 𝐒[T2] → 𝐒[T1]. +lemma lift_simple_sn: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. #d #e #T1 #T2 #H elim H -d -e -T1 -T2 // #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #H elim (simple_inv_bind … H) 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 3f26426e3..8846eec0b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma @@ -112,11 +112,11 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma lifts_simple_dx: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒[T1] → 𝐒[T2]. +lemma lifts_simple_dx: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. #T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_dx/ qed-. -lemma lifts_simple_sn: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒[T2] → 𝐒[T1]. +lemma lifts_simple_sn: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. #T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_sn/ qed-. 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 169f0e276..89b19ea45 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma @@ -219,7 +219,7 @@ lemma ltpss_inv_tpss12: ∀L1,K2,I,V2,d,e. L1 ▶* [d, e] K2. ⓑ{I} V2 → 0 < L1 = K1. ⓑ{I} V1. /2 width=3/ qed-. -(* Basic_1: removed theorems 27: +(* Basic_1: removed theorems 28: csubst0_clear_O csubst0_drop_lt csubst0_drop_gt csubst0_drop_eq csubst0_clear_O_back csubst0_clear_S csubst0_clear_trans csubst0_drop_gt_back csubst0_drop_eq_back csubst0_drop_lt_back @@ -228,5 +228,5 @@ lemma ltpss_inv_tpss12: ∀L1,K2,I,V2,d,e. L1 ▶* [d, e] K2. ⓑ{I} V2 → 0 < csubst0_snd_bind csubst0_fst_bind csubst0_both_bind csubst1_head csubst1_flat csubst1_gen_head csubst1_getl_ge csubst1_getl_lt csubst1_getl_ge_back getl_csubst1 - + fsubst0_gen_base *) -- 2.39.2