From 439b6ec33d749ba4e6ae0938e973a85bc23e306e Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 23 Jul 2012 20:32:03 +0000 Subject: [PATCH] - lambda_delta: we updated some notation we are switching from context-free to context-sensitive reducible terms - basics/star: star constructor refl renamed to srefl to avoid name clash with id constructor refl --- .../lambda_delta/basic_2/grammar/cl_weight.ma | 17 +-- .../basic_2/grammar/lenv_append.ma | 60 +++++++++++ .../basic_2/grammar/lenv_weight.ma | 6 +- .../basic_2/grammar/term_weight.ma | 4 +- .../contribs/lambda_delta/basic_2/notation.ma | 62 ++++------- .../lambda_delta/basic_2/reducibility/crf.ma | 100 ++++++++++++++++++ .../reducibility/{twhnf.ma => thnf.ma} | 10 +- .../basic_2/reducibility/tpr_tpr.ma | 22 ++-- .../lambda_delta/basic_2/reducibility/trf.ma | 81 -------------- .../basic_2/substitution/ldrop.ma | 10 +- .../basic_2/substitution/ldrop_append.ma | 43 ++++++++ .../lambda_delta/basic_2/substitution/lift.ma | 2 +- .../lambda_delta/basic_2/substitution/tps.ma | 2 +- .../lambda_delta/basic_2/unfold/delift.ma | 2 +- .../lambda_delta/basic_2/unfold/gr2.ma | 24 ++--- .../lambda_delta/basic_2/unfold/gr2_gr2.ma | 2 +- .../basic_2/unfold/ldrops_ldrop.ma | 2 +- .../lambda_delta/basic_2/unfold/lifts.ma | 2 +- .../lambda_delta/basic_2/unfold/lifts_lift.ma | 2 +- .../basic_2/unfold/ltpss_ltpss.ma | 2 +- .../lambda_delta/basic_2/unfold/tpss.ma | 2 +- matita/matita/lib/basics/star.ma | 2 +- 22 files changed, 285 insertions(+), 174 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/crf.ma rename matita/matita/contribs/lambda_delta/basic_2/reducibility/{twhnf.ma => thnf.ma} (90%) delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_append.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma index f5f7feb7f..40a364a44 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma @@ -17,7 +17,7 @@ include "basic_2/grammar/cl_shift.ma". (* WEIGHT OF A CLOSURE ******************************************************) -definition cw: lenv → term → ? ≝ λL,T. #[L] + #[T]. +definition cw: lenv → term → ? ≝ λL,T. #{L} + #{T}. interpretation "weight (closure)" 'Weight L T = (cw L T). @@ -27,33 +27,34 @@ interpretation "weight (closure)" 'Weight L T = (cw L T). (* Basic_1: was: flt_wf_ind *) axiom cw_wf_ind: ∀R:lenv→predicate term. - (∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → R L1 T1) → R L2 T2) → + (∀L2,T2. (∀L1,T1. #{L1,T1} < #{L2,T2} → R L1 T1) → R L2 T2) → ∀L,T. R L T. (* Basic_1: was: flt_shift *) -lemma cw_shift: ∀a,K,I,V,T. #[K. ⓑ{I} V, T] < #[K, ⓑ{a,I} V. T]. +lemma cw_shift: ∀a,K,I,V,T. #{K. ⓑ{I} V, T} < #{K, ⓑ{a,I} V. T}. normalize // qed. -lemma tw_shift: ∀L,T. #[L, T] ≤ #[L @@ T]. +lemma tw_shift: ∀L,T. #{L, T} ≤ #{L @@ T}. #L elim L // #K #I #V #IHL #T @transitive_le [3: @IHL |2: /2 width=2/ | skip ] qed. -lemma cw_tpair_sn: ∀I,L,V,T. #[L, V] < #[L, ②{I}V.T]. +lemma cw_tpair_sn: ∀I,L,V,T. #{L, V} < #{L, ②{I}V.T}. #I #L #V #T normalize in ⊢ (? % %); // qed. -lemma cw_tpair_dx: ∀I,L,V,T. #[L, T] < #[L, ②{I}V.T]. +lemma cw_tpair_dx: ∀I,L,V,T. #{L, T} < #{L, ②{I}V.T}. #I #L #V #T normalize in ⊢ (? % %); // qed. -lemma cw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. #[L, V2] < #[L, ②{I1}V1.②{I2}V2.T]. +lemma cw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. #{L, V2} < #{L, ②{I1}V1.②{I2}V2.T}. #I1 #I2 #L #V1 #V2 #T normalize in ⊢ (? % %); /2 width=1/ qed. -lemma cw_tpair_dx_sn_shift: ∀a2,I1,I2,L,V1,V2,T. #[L.ⓑ{I2}V2, T] < #[L, ②{I1}V1.ⓑ{a2,I2}V2.T]. +lemma cw_tpair_dx_sn_shift: ∀a2,I1,I2,L,V1,V2,T. + #{L.ⓑ{I2}V2, T} < #{L, ②{I1}V1.ⓑ{a2,I2}V2.T}. #a2 #I1 #I2 #L #V1 #V2 #T normalize in ⊢ (? % %); /2 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma new file mode 100644 index 000000000..336cd7b2f --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma @@ -0,0 +1,60 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lenv_length.ma". + +(* LOCAL ENVIRONMENTS *******************************************************) + +let rec append L K on K ≝ match K with +[ LAtom ⇒ L +| LPair K I V ⇒ (append L K). ⓑ{I} V +]. + +interpretation "append (local environment)" 'Append L1 L2 = (append L1 L2). + +(* Basic properties *********************************************************) + +lemma append_atom_sn: ∀L. ⋆ @@ L = L. +#L elim L -L normalize // +qed. + +lemma append_length: ∀L1,L2. |L1 @@ L2| = |L1| + |L2|. +#L1 #L2 elim L2 -L2 normalize // +qed. + +(* Basic inversion lemmas ***************************************************) + +axiom discr_lpair_append_xy_x: ∀I,L,K,V. (L @@ K).ⓑ{I}V = L → ⊥. +(* +#I #L #K #V #H +lapply (refl … (|L|)) append_length -I -V #H +*) +lemma append_inv_sn: ∀L1,L2,L. L1 @@ L = L2 @@ L → L1 = L2. +#L1 #L2 #L elim L -L normalize // +#L #I #V #IHL #HL12 destruct /2 width=1/ (**) (* destruct does not simplify well *) +qed. + +lemma append_inv_dx: ∀L1,L2,L. L @@ L1 = L @@ L2 → L1 = L2. +#L1 elim L1 -L1 +[ * normalize // + #L2 #I2 #V2 #L #H + elim (discr_lpair_append_xy_x I2 L L2 V2 ?) // +| #L1 #I1 #V1 #IHL1 * normalize + [ #L #H -IHL1 elim (discr_lpair_append_xy_x … H) + | #L2 #I2 #V2 #L normalize #H destruct (**) (* destruct does not simplify well *) + -H >e0 /3 width=2/ + ] +] +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma index 48ef29453..d277ed00e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma @@ -19,20 +19,20 @@ include "basic_2/grammar/lenv.ma". let rec lw L ≝ match L with [ LAtom ⇒ 0 -| LPair L _ V ⇒ lw L + #[V] +| LPair L _ V ⇒ lw L + #{V} ]. interpretation "weight (local environment)" 'Weight L = (lw L). (* Basic properties *********************************************************) -lemma lw_pair: ∀I,L,V. #[L] < #[(L.ⓑ{I}V)]. +lemma lw_pair: ∀I,L,V. #{L} < #{(L.ⓑ{I}V)}. /3 width=1/ qed. (* Basic eliminators ********************************************************) axiom lw_wf_ind: ∀R:predicate lenv. - (∀L2. (∀L1. #[L1] < #[L2] → R L1) → R L2) → + (∀L2. (∀L1. #{L1} < #{L2} → R L1) → R L2) → ∀L. R L. (* Basic_1: removed theorems 2: clt_cong clt_head clt_thead *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma index e567df208..ce05e436e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma @@ -26,14 +26,14 @@ interpretation "weight (term)" 'Weight T = (tw T). (* Basic properties *********************************************************) (* Basic_1: was: tweight_lt *) -lemma tw_pos: ∀T. 1 ≤ #[T]. +lemma tw_pos: ∀T. 1 ≤ #{T}. #T elim T -T // qed. (* Basic eliminators ********************************************************) axiom tw_wf_ind: ∀R:predicate term. - (∀T2. (∀T1. #[T1] < #[T2] → R T1) → R T2) → + (∀T2. (∀T1. #{T1} < #{T2} → R T1) → R T2) → ∀T. R T. (* Basic_1: removed theorems 11: diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index d6d38ef61..b396acf55 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -120,11 +120,11 @@ notation "hvbox( T . break ④ { I } break { T1 , break T2 , break T3 } )" non associative with precedence 50 for @{ 'DxItem4 $T $I $T1 $T2 $T3 }. -notation "hvbox( # [ x ] )" +notation "hvbox( # { x } )" non associative with precedence 90 for @{ 'Weight $x }. -notation "hvbox( # [ x , break y ] )" +notation "hvbox( # { x , break y } )" non associative with precedence 90 for @{ 'Weight $x $y }. @@ -142,18 +142,6 @@ notation "hvbox( T1 ≃ break term 46 T2 )" (* Substitution *************************************************************) -notation "hvbox( L ⊢ break 𝐑 [ d , break e ] break ⦃ T ⦄ )" - non associative with precedence 45 - for @{ 'Reducible $L $d $e $T }. - -notation "hvbox( L ⊢ break 𝐈 [ d , break e ] break ⦃ T ⦄ )" - non associative with precedence 45 - for @{ 'NotReducible $L $d $e $T }. - -notation "hvbox( L ⊢ break 𝐍 [ d , break e ] break ⦃ T ⦄ )" - non associative with precedence 45 - for @{ 'Normal $L $d $e $T }. - notation "hvbox( ⇧ [ d , break e ] break term 46 T1 ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'RLift $d $e $T1 $T2 }. @@ -184,7 +172,7 @@ notation "hvbox( L ⊢ break term 46 T1 break ▶ [ d , break e ] break term 46 (* Unfold *******************************************************************) -notation "hvbox( @ [ T1 ] break term 46 f ≡ break term 46 T2 )" +notation "hvbox( @ ⦃ T1 , break f ⦄ ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'RAt $T1 $f $T2 }. @@ -256,59 +244,53 @@ notation "hvbox( h ⊢ break term 46 L1 • ⊑ [ g ] break term 46 L2 )" (* Unwind *******************************************************************) -notation "hvbox( L1 ⊢ ⧫* break term 46 T ≡ break term 46 L2 )" +notation "hvbox( L1 ⊢ ⧫ * break term 46 T ≡ break term 46 L2 )" non associative with precedence 45 for @{ 'Unwind $L1 $T $L2 }. (* Reducibility *************************************************************) -notation "hvbox( 𝐑 ⦃ T ⦄ )" - non associative with precedence 45 - for @{ 'Reducible $T }. - notation "hvbox( L ⊢ break 𝐑 ⦃ T ⦄ )" non associative with precedence 45 for @{ 'Reducible $L $T }. -notation "hvbox( 𝐈 ⦃ T ⦄ )" - non associative with precedence 45 - for @{ 'NotReducible $T }. - notation "hvbox( L ⊢ break 𝐈 ⦃ T ⦄ )" non associative with precedence 45 for @{ 'NotReducible $L $T }. -notation "hvbox( 𝐍 ⦃ T ⦄ )" - non associative with precedence 45 - for @{ 'Normal $T }. - notation "hvbox( L ⊢ break 𝐍 ⦃ T ⦄ )" non associative with precedence 45 for @{ 'Normal $L $T }. -notation "hvbox( 𝐖𝐇𝐑 ⦃ T ⦄ )" +(* this might be removed *) +notation "hvbox( 𝐇𝐑 ⦃ T ⦄ )" non associative with precedence 45 - for @{ 'WHdReducible $T }. + for @{ 'HdReducible $T }. -notation "hvbox( L ⊢ break 𝐖𝐇𝐑 ⦃ T ⦄ )" +(* this might be removed *) +notation "hvbox( L ⊢ break 𝐇𝐑 ⦃ T ⦄ )" non associative with precedence 45 - for @{ 'WHdReducible $L $T }. + for @{ 'HdReducible $L $T }. -notation "hvbox( 𝐖𝐇𝐈 ⦃ T ⦄ )" +(* this might be removed *) +notation "hvbox( 𝐇𝐈 ⦃ T ⦄ )" non associative with precedence 45 - for @{ 'NotWHdReducible $T }. + for @{ 'NotHdReducible $T }. -notation "hvbox( L ⊢ break 𝐖𝐇𝐈 ⦃ T ⦄ )" +(* this might be removed *) +notation "hvbox( L ⊢ break 𝐇𝐈 ⦃ T ⦄ )" non associative with precedence 45 - for @{ 'NotWHdReducible $L $T }. + for @{ 'NotHdReducible $L $T }. -notation "hvbox( 𝐖𝐇𝐍 ⦃ T ⦄ )" +(* this might be removed *) +notation "hvbox( 𝐇𝐍 ⦃ T ⦄ )" non associative with precedence 45 - for @{ 'WHdNormal $T }. + for @{ 'HdNormal $T }. -notation "hvbox( L ⊢ break 𝐖𝐇𝐍 ⦃ T ⦄ )" +(* this might be removed *) +notation "hvbox( L ⊢ break 𝐇𝐍 ⦃ T ⦄ )" non associative with precedence 45 - for @{ 'WHdNormal $L $T }. + for @{ 'HdNormal $L $T }. notation "hvbox( T1 ➡ break term 46 T2 )" non associative with precedence 45 diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/crf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/crf.ma new file mode 100644 index 000000000..cb860ef7d --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/crf.ma @@ -0,0 +1,100 @@ +(**************************************************************************) +(* ___ *) +(* ||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_simple.ma". +include "basic_2/substitution/ldrop.ma". + +(* CONTEXT-SENSITIVE REDUCIBLE TERMS ****************************************) + +(* reducible binary items *) +definition ri2: item2 → Prop ≝ + λI. I = Bind2 true Abbr ∨ I = Flat2 Cast. + +(* irreducible binary binders *) +definition ib2: bool → bind2 → Prop ≝ + λa,I. I = Abst ∨ Bind2 a I = Bind2 false Abbr. + +(* reducible terms *) +inductive crf: lenv → predicate term ≝ +| crf_delta : ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → crf L (#i) +| crf_appl_sn: ∀L,V,T. crf L V → crf L (ⓐV. T) +| crf_appl_dx: ∀L,V,T. crf L T → crf L (ⓐV. T) +| crf_ri2 : ∀I,L,V,T. ri2 I → crf L (②{I}V. T) +| crf_ib2_sn : ∀a,I,L,V,T. ib2 a I → crf L V → crf L (ⓑ{a,I}V. T) +| crf_ib2_dx : ∀a,I,L,V,T. ib2 a I → crf (L.ⓑ{I}V) T → crf L (ⓑ{a,I}V. T) +| crf_beta : ∀a,L,V,W,T. crf L (ⓐV. ⓛ{a}W. T) +| crf_theta : ∀a,L,V,W,T. crf L (ⓐV. ⓓ{a}W. T) +. + +interpretation + "context-sensitive reducibility (term)" + 'Reducible L T = (crf L T). + +(* Basic inversion lemmas ***************************************************) + +fact trf_inv_atom_aux: ∀I,L,T. L ⊢ 𝐑⦃T⦄ → L = ⋆ → T = ⓪{I} → ⊥. +#I #L #T * -L -T +[ #L #K #V #i #HLK #H1 #H2 destruct + lapply (ldrop_inv_atom1 … HLK) -HLK #H destruct +| #L #V #T #_ #_ #H destruct +| #L #V #T #_ #_ #H destruct +| #J #L #V #T #_ #_ #H destruct +| #a #J #L #V #T #_ #_ #_ #H destruct +| #a #J #L #V #T #_ #_ #_ #H destruct +| #a #L #V #W #T #_ #H destruct +| #a #L #V #W #T #_ #H destruct +] +qed. + +lemma trf_inv_atom: ∀I. ⋆ ⊢ 𝐑⦃⓪{I}⦄ → ⊥. +/2 width=6/ qed-. + +fact crf_inv_abst_aux: ∀a,L,W,U,T. L ⊢ 𝐑⦃T⦄ → T = ⓛ{a}W. U → + L ⊢ 𝐑⦃W⦄ ∨ L.ⓛW ⊢ 𝐑⦃U⦄. +#a #L #W #U #T * -T +[ #L #K #V #i #_ #H destruct +| #L #V #T #_ #H destruct +| #L #V #T #_ #H destruct +| #J #L #V #T #H1 #H2 destruct + elim H1 -H1 #H destruct +| #b #J #L #V #T #_ #HV #H destruct /2 width=1/ +| #b #J #L #V #T #_ #HT #H destruct /2 width=1/ +| #b #L #V #W #T #H destruct +| #b #L #V #W #T #H destruct +] +qed. + +lemma crf_inv_abst: ∀a,L,W,T. L ⊢ 𝐑⦃ⓛ{a}W.T⦄ → L ⊢ 𝐑⦃W⦄ ∨ L.ⓛW ⊢ 𝐑⦃T⦄. +/2 width=4/ qed-. + +fact crf_inv_appl_aux: ∀L,W,U,T. L ⊢ 𝐑⦃T⦄ → T = ⓐW. U → + ∨∨ L ⊢ 𝐑⦃W⦄ | L ⊢ 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥). +#L #W #U #T * -T +[ #L #K #V #i #_ #H destruct +| #L #V #T #HV #H destruct /2 width=1/ +| #L #V #T #HT #H destruct /2 width=1/ +| #J #L #V #T #H1 #H2 destruct + elim H1 -H1 #H destruct +| #a #I #L #V #T #_ #_ #H destruct +| #a #I #L #V #T #_ #_ #H destruct +| #a #L #V #W0 #T #H destruct + @or3_intro2 #H elim (simple_inv_bind … H) +| #a #L #V #W0 #T #H destruct + @or3_intro2 #H elim (simple_inv_bind … H) +] +qed. + +lemma crf_inv_appl: ∀L,V,T. L ⊢ 𝐑⦃ⓐV.T⦄ → ∨∨ L ⊢ 𝐑⦃V⦄ | L ⊢ 𝐑⦃T⦄ | (𝐒⦃T⦄ → ⊥). +/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/thnf.ma similarity index 90% rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/thnf.ma index 6284eaa0b..b271a112b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/thnf.ma @@ -17,15 +17,15 @@ include "basic_2/reducibility/tpr.ma". (* CONTEXT-FREE WEAK HEAD NORMAL TERMS **************************************) -definition twhnf: predicate term ≝ NF … tpr tshf. +definition thnf: predicate term ≝ NF … tpr tshf. interpretation - "context-free weak head normality (term)" - 'WHdNormal T = (twhnf T). + "context-free head normality (term)" + 'HdNormal T = (thnf T). (* 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/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma index 8c7f2819e..a50580b96 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma @@ -23,7 +23,7 @@ fact tpr_conf_atom_atom: ∀I. ∃∃X. ⓪{I} ➡ X & ⓪{I} ➡ X. fact tpr_conf_flat_flat: ∀I,V0,V1,T0,T1,V2,T2. ( - ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → + ∀X0:term. #{X0} < #{V0} + #{T0} + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -36,7 +36,7 @@ qed. fact tpr_conf_flat_beta: ∀a,V0,V1,T1,V2,W0,U0,T2. ( - ∀X0:term. #[X0] < #[V0] + (#[W0] + #[U0] + 1) + 1 → + ∀X0:term. #{X0} < #{V0} + (#{W0} + #{U0} + 1) + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -55,7 +55,7 @@ qed. *) fact tpr_conf_flat_theta: ∀a,V0,V1,T1,V2,V,W0,W2,U0,U2. ( - ∀X0:term. #[X0] < #[V0] + (#[W0] + #[U0] + 1) + 1 → + ∀X0:term. #{X0} < #{V0} + (#{W0} + #{U0} + 1) + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -87,7 +87,7 @@ qed. fact tpr_conf_flat_cast: ∀X2,V0,V1,T0,T1. ( - ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → + ∀X0:term. #{X0} < #{V0} + #{T0} + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -99,7 +99,7 @@ qed. fact tpr_conf_beta_beta: ∀a. ∀W0:term. ∀V0,V1,T0,T1,V2,T2. ( - ∀X0:term. #[X0] < #[V0] + (#[W0] + #[T0] + 1) + 1 → + ∀X0:term. #{X0} < #{V0} + (#{W0} + #{T0} + 1) + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -113,7 +113,7 @@ qed. (* Basic_1: was: pr0_cong_delta pr0_delta_delta *) fact tpr_conf_delta_delta: ∀a,I1,V0,V1,T0,T1,TT1,V2,T2,TT2. ( - ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → + ∀X0:term. #{X0} < #{V0} + #{T0} + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -132,7 +132,7 @@ qed. fact tpr_conf_delta_zeta: ∀X2,V0,V1,T0,T1,TT1,T2. ( - ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → + ∀X0:term. #{X0} < #{V0} + #{T0} + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -149,7 +149,7 @@ qed. (* Basic_1: was: pr0_upsilon_upsilon *) fact tpr_conf_theta_theta: ∀a,VV1,V0,V1,W0,W1,T0,T1,V2,VV2,W2,T2. ( - ∀X0:term. #[X0] < #[V0] + (#[W0] + #[T0] + 1) + 1 → + ∀X0:term. #{X0} < #{V0} + (#{W0} + #{T0} + 1) + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -168,7 +168,7 @@ qed. fact tpr_conf_zeta_zeta: ∀V0:term. ∀X2,TT0,T0,T1,TT2. ( - ∀X0:term. #[X0] < #[V0] + #[TT0] + 1 → + ∀X0:term. #{X0} < #{V0} + #{TT0} + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -184,7 +184,7 @@ qed. fact tpr_conf_tau_tau: ∀V0,T0:term. ∀X2,T1. ( - ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → + ∀X0:term. #{X0} < #{V0} + #{T0} + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -198,7 +198,7 @@ qed. fact tpr_conf_aux: ∀Y0:term. ( - ∀X0:term. #[X0] < #[Y0] → + ∀X0:term. #{X0} < #{Y0} → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma deleted file mode 100644 index 6d6993de3..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma +++ /dev/null @@ -1,81 +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_simple.ma". - -(* CONTEXT-FREE REDUCIBLE TERMS *********************************************) - -(* reducible terms *) -inductive trf: predicate term ≝ -| trf_abst_sn: ∀V,T. trf V → trf (ⓛV. T) -| trf_abst_dx: ∀V,T. trf T → trf (ⓛV. T) -| trf_appl_sn: ∀V,T. trf V → trf (ⓐV. T) -| trf_appl_dx: ∀V,T. trf T → trf (ⓐV. T) -| trf_abbr : ∀V,T. trf (ⓓV. T) -| trf_cast : ∀V,T. trf (ⓝV. T) -| trf_beta : ∀V,W,T. trf (ⓐV. ⓛW. T) -. - -interpretation - "context-free reducibility (term)" - 'Reducible T = (trf T). - -(* Basic inversion lemmas ***************************************************) - -fact trf_inv_atom_aux: ∀I,T. 𝐑⦃T⦄ → T = ⓪{I} → ⊥. -#I #T * -T -[ #V #T #_ #H destruct -| #V #T #_ #H destruct -| #V #T #_ #H destruct -| #V #T #_ #H destruct -| #V #T #H destruct -| #V #T #H destruct -| #V #W #T #H destruct -] -qed. - -lemma trf_inv_atom: ∀I. 𝐑⦃⓪{I}⦄ → ⊥. -/2 width=4/ qed-. - -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/ -| #V #T #_ #H destruct -| #V #T #_ #H destruct -| #V #T #H destruct -| #V #T #H destruct -| #V #W0 #T #H destruct -] -qed. - -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⦄ → ⊥). -#W #U #T * -T -[ #V #T #_ #H destruct -| #V #T #_ #H destruct -| #V #T #HV #H destruct /2 width=1/ -| #V #T #HT #H destruct /2 width=1/ -| #V #T #H destruct -| #V #T #H destruct -| #V #W0 #T #H destruct - @or3_intro2 #H elim (simple_inv_bind … H) -] -qed. - -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/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma index 29759fe08..c16669661 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma @@ -141,6 +141,12 @@ lemma ldrop_ldrop_lt: ∀L1,L2,I,V,e. #L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/ qed. +lemma ldrop_skip_lt: ∀L1,L2,I,V1,V2,d,e. + ⇩[d - 1, e] L1 ≡ L2 → ⇧[d - 1, e] V2 ≡ V1 → 0 < d → + ⇩[d, e] L1. ⓑ{I} V1 ≡ L2. ⓑ{I} V2. +#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV21 #Hd >(plus_minus_m_m d 1) // /2 width=1/ +qed. + lemma ldrop_O1: ∀L,i. i < |L| → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V. #L elim L -L [ #i #H elim (lt_zero_false … H) @@ -194,7 +200,7 @@ lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ⇩[O, e] L1 ≡ K2. ⓑ{I2} V2 → ] qed-. -lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → #[L2] ≤ #[L1]. +lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → #{L2} ≤ #{L1}. #L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize [ /2 width=3/ | #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 @@ -203,7 +209,7 @@ lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → #[L2] ≤ #[L1]. qed-. lemma ldrop_pair2_fwd_cw: ∀I,L,K,V,d,e. ⇩[d, e] L ≡ K. ⓑ{I} V → - ∀T. #[K, V] < #[L, T]. + ∀T. #{K, V} < #{L, T}. #I #L #K #V #d #e #H #T lapply (ldrop_fwd_lw … H) -H #H @(le_to_lt_to_lt … H) -H /3 width=1/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_append.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_append.ma new file mode 100644 index 000000000..ec5258552 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_append.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/grammar/lenv_append.ma". +include "basic_2/substitution/ldrop.ma". + +(* DROPPING *****************************************************************) + +(* Properties on append for local environments ******************************) + +lemma ldrop_append_O1_ge: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K → + |L2| ≤ e → ⇩[0, e - |L2|] L1 ≡ K. +#K #L1 #L2 elim L2 -L2 normalize // +#L2 #I #V #IHL2 #e #H #H1e +elim (ldrop_inv_O1 … H) -H * #H2e #HL12 destruct +[ lapply (le_n_O_to_eq … H1e) -H1e -IHL2 + >commutative_plus normalize #H destruct +| minus_minus_comm /3 width=1/ +] +qed. + +lemma ldrop_append_O1_lt: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K → e < |L2| → + ∃∃K2. ⇩[0, e] L2 ≡ K2 & K = L1 @@ K2. +#K #L1 #L2 elim L2 -L2 +[ #e #_ #H elim (lt_zero_false … H) +| #L2 #I #V #IHL2 #e normalize #HL12 #H1e + elim (ldrop_inv_O1 … HL12) -HL12 * #H2e #HL12 destruct + [ -H1e -IHL2 /3 width=3/ + | elim (IHL2 … HL12 ?) -IHL2 -HL12 /2 width=1/ -H1e #K2 #HLK2 #H destruct /3 width=3/ + ] +] +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 49a453ffa..3f3f6b0ff 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma @@ -267,7 +267,7 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma tw_lift: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → #[T1] = #[T2]. +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-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma index 88de45dd1..db116f77e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma @@ -245,7 +245,7 @@ lemma tps_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 ▶ [d, 0] T2 → T1 = T2. (* Basic forward lemmas *****************************************************) -lemma tps_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → #[T1] ≤ #[T2]. +lemma tps_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → #{T1} ≤ #{T2}. #L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e normalize /3 by monotonic_le_plus_l, le_plus/ (**) (* just /3 width=1/ is too slow *) qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma index 1af082f28..e8ac23dae 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma @@ -102,7 +102,7 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma delift_fwd_tw: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → #[T1] ≤ #[T2]. +lemma delift_fwd_tw: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → #{T1} ≤ #{T2}. #L #T1 #T2 #d #e * #T #HT1 #HT2 >(tw_lift … HT2) -T2 /2 width=4 by tpss_fwd_tw / qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2.ma index 1168e52df..562b79530 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2.ma @@ -29,7 +29,7 @@ interpretation "application (generic relocation with pairs)" (* Basic inversion lemmas ***************************************************) -fact at_inv_nil_aux: ∀des,i1,i2. @[i1] des ≡ i2 → des = ⟠ → i1 = i2. +fact at_inv_nil_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → des = ⟠ → i1 = i2. #des #i1 #i2 * -des -i1 -i2 [ // | #des #d #e #i1 #i2 #_ #_ #H destruct @@ -37,13 +37,13 @@ fact at_inv_nil_aux: ∀des,i1,i2. @[i1] des ≡ i2 → des = ⟠ → i1 = i2. ] qed. -lemma at_inv_nil: ∀i1,i2. @[i1] ⟠ ≡ i2 → i1 = i2. +lemma at_inv_nil: ∀i1,i2. @⦃i1, ⟠⦄ ≡ i2 → i1 = i2. /2 width=3/ qed-. -fact at_inv_cons_aux: ∀des,i1,i2. @[i1] des ≡ i2 → +fact at_inv_cons_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → ∀d,e,des0. des = {d, e} @ des0 → - i1 < d ∧ @[i1] des0 ≡ i2 ∨ - d ≤ i1 ∧ @[i1 + e] des0 ≡ i2. + i1 < d ∧ @⦃i1, des0⦄ ≡ i2 ∨ + d ≤ i1 ∧ @⦃i1 + e, des0⦄ ≡ i2. #des #i1 #i2 * -des -i1 -i2 [ #i #d #e #des #H destruct | #des1 #d1 #e1 #i1 #i2 #Hid1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1/ @@ -51,21 +51,21 @@ fact at_inv_cons_aux: ∀des,i1,i2. @[i1] des ≡ i2 → ] qed. -lemma at_inv_cons: ∀des,d,e,i1,i2. @[i1] {d, e} @ des ≡ i2 → - i1 < d ∧ @[i1] des ≡ i2 ∨ - d ≤ i1 ∧ @[i1 + e] des ≡ i2. +lemma at_inv_cons: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 → + i1 < d ∧ @⦃i1, des⦄ ≡ i2 ∨ + d ≤ i1 ∧ @⦃i1 + e, des⦄ ≡ i2. /2 width=3/ qed-. -lemma at_inv_cons_lt: ∀des,d,e,i1,i2. @[i1] {d, e} @ des ≡ i2 → - i1 < d → @[i1] des ≡ i2. +lemma at_inv_cons_lt: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 → + i1 < d → @⦃i1, des⦄ ≡ i2. #des #d #e #i1 #e2 #H elim (at_inv_cons … H) -H * // #Hdi1 #_ #Hi1d lapply (le_to_lt_to_lt … Hdi1 Hi1d) -Hdi1 -Hi1d #Hd elim (lt_refl_false … Hd) qed-. -lemma at_inv_cons_ge: ∀des,d,e,i1,i2. @[i1] {d, e} @ des ≡ i2 → - d ≤ i1 → @[i1 + e] des ≡ i2. +lemma at_inv_cons_ge: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 → + d ≤ i1 → @⦃i1 + e, des⦄ ≡ i2. #des #d #e #i1 #e2 #H elim (at_inv_cons … H) -H * // #Hi1d #_ #Hdi1 lapply (le_to_lt_to_lt … Hdi1 Hi1d) -Hdi1 -Hi1d #Hd diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_gr2.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_gr2.ma index f7e42e334..20ce856d6 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_gr2.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_gr2.ma @@ -18,7 +18,7 @@ include "basic_2/unfold/gr2.ma". (* Main properties **********************************************************) -theorem at_mono: ∀des,i,i1. @[i] des ≡ i1 → ∀i2. @[i] des ≡ i2 → i1 = i2. +theorem at_mono: ∀des,i,i1. @⦃i, des⦄ ≡ i1 → ∀i2. @⦃i, des⦄ ≡ i2 → i1 = i2. #des #i #i1 #H elim H -des -i -i1 [ #i #x #H <(at_inv_nil … H) -x // | #des #d #e #i #i1 #Hid #_ #IHi1 #x #H diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrop.ma index fe11428dc..6ca2f73df 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrop.ma @@ -21,7 +21,7 @@ include "basic_2/unfold/ldrops.ma". lemma ldrops_ldrop_trans: ∀L1,L,des. ⇩*[des] L1 ≡ L → ∀L2,i. ⇩[0, i] L ≡ L2 → ∃∃L0,des0,i0. ⇩[0, i0] L1 ≡ L0 & ⇩*[des0] L0 ≡ L2 & - @[i] des ≡ i0 & des ▭ i ≡ des0. + @⦃i, des⦄ ≡ i0 & des ▭ i ≡ des0. #L1 #L #des #H elim H -L1 -L -des [ /2 width=7/ | #L1 #L3 #L #des3 #d #e #_ #HL3 #IHL13 #L2 #i #HL2 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 f447d729a..40158acbe 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma @@ -61,7 +61,7 @@ qed-. (* Basic_1: was: lift1_lref *) lemma lifts_inv_lref1: ∀T2,des,i1. ⇧*[des] #i1 ≡ T2 → - ∃∃i2. @[i1] des ≡ i2 & T2 = #i2. + ∃∃i2. @⦃i1, des⦄ ≡ i2 & T2 = #i2. #T2 #des elim des -des [ #i1 #H <(lifts_inv_nil … H) -H /2 width=3/ | #d #e #des #IH #i1 #H diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift.ma index 23a488072..6ad3ff015 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift.ma @@ -32,7 +32,7 @@ lemma lifts_lift_trans_le: ∀T1,T,des. ⇧*[des] T1 ≡ T → ∀T2. ⇧[0, 1] qed-. (* Basic_1: was: lift1_free (right to left) *) -lemma lifts_lift_trans: ∀des,i,i0. @[i] des ≡ i0 → +lemma lifts_lift_trans: ∀des,i,i0. @⦃i, des⦄ ≡ i0 → ∀des0. des + 1 ▭ i + 1 ≡ des0 + 1 → ∀T1,T0. ⇧*[des0] T1 ≡ T0 → ∀T2. ⇧[O, i0 + 1] T0 ≡ T2 → diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma index 8885b2339..ec5037e86 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma @@ -54,7 +54,7 @@ fact ltpss_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e. elim (ltpss_ldrop_trans_be … HL01 … HLK1 ? ?) -HL01 -HLK1 // /2 width=2/ #X #H #HLK0 elim (ltpss_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct lapply (tpss_fwd_tw … HV01) #H2 - lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 /2 width=1/ -H2 #H + lapply (transitive_le (#{K1} + #{V0}) … H1) -H1 /2 width=1/ -H2 #H lapply (tpss_trans_eq … HV01 HV12) -V1 #HV02 lapply (IH … HV02 … HK01 ? ?) -IH -HV02 -HK01 [1,3: // |2,4: skip | normalize /2 width=1/ | /2 width=6/ ] diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma index d0f964186..dd2c219ff 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma @@ -155,7 +155,7 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → #[T1] ≤ #[T2]. +lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → #{T1} ≤ #{T2}. #L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 // #T #T2 #_ #HT2 #IHT1 lapply (tps_fwd_tw … HT2) -HT2 #HT2 diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma index 1e2a48000..166ba5d7e 100644 --- a/matita/matita/lib/basics/star.ma +++ b/matita/matita/lib/basics/star.ma @@ -47,7 +47,7 @@ qed. (* star *) inductive star (A:Type[0]) (R:relation A) (a:A): A → Prop ≝ |sstep: ∀b,c.star A R a b → R b c → star A R a c - |refl: star A R a a. + |srefl: star A R a a. lemma R_to_star: ∀A,R,a,b. R a b → star A R a b. #A #R #a #b /2/ -- 2.39.2