From d38087520d6ce1d696b28da40f3811291fc8a311 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 14 Nov 2011 17:14:06 +0000 Subject: [PATCH] - we proved that context-free reduction admits no one-step loops --- .../contribs/lambda_delta/Basic_2/Basic_1.txt | 19 +- .../lambda_delta/Basic_2/grammar/item.ma | 3 +- .../lambda_delta/Basic_2/grammar/lsubs.ma | 8 +- .../lambda_delta/Basic_2/grammar/term.ma | 8 +- .../Basic_2/grammar/term_simple.ma | 2 +- .../Basic_2/grammar/term_weight.ma | 1 + .../lambda_delta/Basic_2/grammar/thom.ma | 4 +- .../contribs/lambda_delta/Basic_2/notation.ma | 4 + .../lambda_delta/Basic_2/reducibility/cpr.ma | 6 +- .../Basic_2/reducibility/cpr_cpr.ma | 7 +- .../Basic_2/reducibility/cpr_lift.ma | 7 +- .../lambda_delta/Basic_2/reducibility/ltpr.ma | 10 +- .../Basic_2/reducibility/ltpr_ldrop.ma | 4 +- .../lambda_delta/Basic_2/reducibility/tnf.ma | 20 +- .../lambda_delta/Basic_2/reducibility/tpr.ma | 31 ++- .../Basic_2/reducibility/tpr_lift.ma | 2 +- .../lambda_delta/Basic_2/reducibility/trf.ma | 14 +- .../Basic_2/substitution/ldrop.ma | 22 +- .../Basic_2/substitution/ldrop_ldrop.ma | 2 +- .../lambda_delta/Basic_2/substitution/lift.ma | 207 ++++++++++++------ .../Basic_2/substitution/lift_lift.ma | 4 +- .../lambda_delta/Basic_2/substitution/ltps.ma | 14 +- .../Basic_2/substitution/ltps_ldrop.ma | 24 +- .../lambda_delta/Basic_2/substitution/tps.ma | 31 ++- .../Basic_2/substitution/tps_lift.ma | 3 +- .../lambda_delta/Basic_2/unfold/ltpss.ma | 8 +- .../Basic_2/unfold/ltpss_ldrop.ma | 24 +- .../lambda_delta/Basic_2/unfold/ltpss_tpss.ma | 4 +- .../lambda_delta/Basic_2/unfold/tpss.ma | 10 +- .../lambda_delta/Basic_2/unfold/tpss_lift.ma | 6 +- .../lambda_delta/Basic_2/unfold/tsubst.ma | 23 ++ .../contribs/lambda_delta/Ground_2/arith.ma | 15 +- 32 files changed, 342 insertions(+), 205 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/unfold/tsubst.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 4aa9ec978..b7fa79e70 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt +++ b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt @@ -265,15 +265,9 @@ pr1/props pr1_head_2 pr1/props pr1_comp pr1/props pr1_eta pr2/clen pr2_gen_ctail -pr2/subst1 pr2_gen_cabbr - -# check ###################################################################### - pr2/fwd pr2_gen_void pr2/props pr2_ctail - -# waiting #################################################################### - +pr2/subst1 pr2_gen_cabbr pr3/fwd pr3_gen_sort pr3/fwd pr3_gen_abst pr3/fwd pr3_gen_cast @@ -374,9 +368,6 @@ sty1/props sty1_lift sty1/props sty1_correct sty1/props sty1_abbr sty1/props sty1_cast2 -subst0/dec dnf_dec2 -subst0/dec dnf_dec -subst1/props subst1_ex subst/fwd subst_sort subst/fwd subst_lref_lt subst/fwd subst_lref_eq @@ -384,7 +375,6 @@ subst/fwd subst_lref_gt subst/fwd subst_head subst/props subst_lift_SO subst/props subst_subst0 -T/dec bind_dec_not T/dec binder_dec T/dec abst_dec tlist/props tslt_wf__q_ind @@ -392,11 +382,6 @@ tlist/props tslt_wf_ind tlist/props theads_tapp tlist/props tcons_tapp_ex tlist/props tlist_ind_rev -T/props not_abbr_abst -T/props not_void_abst -T/props not_abbr_void -T/props not_abst_void -T/props tweight_lt ty3/arity ty3_arity ty3/arity_props ty3_predicative ty3/arity_props ty3_repellent @@ -461,3 +446,5 @@ wf3/ty3 wf3_pr2_conf wf3/ty3 wf3_pr3_conf wf3/ty3 wf3_pc3_conf wf3/ty3 wf3_ty3_conf + +# check ###################################################################### diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma index 8851da3cb..56c5a2b8c 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma @@ -67,8 +67,9 @@ axiom flat2_eq_dec: ∀I1,I2:flat2. Decidable (I1 = I2). (* Basic_1: was: kind_dec *) axiom item2_eq_dec: ∀I1,I2:item2. Decidable (I1 = I2). -(* Basic_1: removed theorems 19: +(* Basic_1: removed theorems 21: s_S s_plus s_plus_sym s_minus minus_s_s s_le s_lt s_inj s_inc s_arith0 s_arith1 r_S r_plus r_plus_sym r_minus r_dis s_r r_arith0 r_arith1 + not_abbr_abst bind_dec_not *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma index 83169d811..cf90a6134 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma @@ -43,8 +43,8 @@ lemma TC_lsubs_conf: ∀S,R. lsubs_conf S R → lsubs_conf S (λL. (TC … (R L) ] qed. -lemma lsubs_eq: ∀L1,L2,e. L1 [0, e] ≼ L2 → ∀I,V. - L1. 𝕓{I} V [0, e + 1] ≼ L2.𝕓{I} V. +lemma lsubs_bind_eq: ∀L1,L2,e. L1 [0, e] ≼ L2 → ∀I,V. + L1. 𝕓{I} V [0, e + 1] ≼ L2.𝕓{I} V. #L1 #L2 #e #HL12 #I #V elim I -I /2/ qed. @@ -78,7 +78,7 @@ fact lsubs_fwd_length_full1_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → qed. lemma lsubs_fwd_length_full1: ∀L1,L2. L1 [0, |L1|] ≼ L2 → |L1| ≤ |L2|. -/2 width=5/ qed. +/2 width=5/ qed-. fact lsubs_fwd_length_full2_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → d = 0 → e = |L2| → |L2| ≤ |L1|. @@ -93,4 +93,4 @@ fact lsubs_fwd_length_full2_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → qed. lemma lsubs_fwd_length_full2: ∀L1,L2. L1 [0, |L2|] ≼ L2 → |L2| ≤ |L1|. -/2 width=5/ qed. +/2 width=5/ qed-. 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 f119e6de0..376061b70 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma @@ -46,7 +46,7 @@ lemma discr_tpair_xy_x: ∀I,T,V. 𝕔{I} V. T = V → False. (generalize in match e1) -e1 >e0 normalize *) -I /2/ (**) (* destruct: one quality is not simplified, the destucted equality is not erased *) ] -qed. +qed-. (* Basic_1: was: thead_x_y_y *) lemma discr_tpair_xy_y: ∀I,V,T. 𝕔{I} V. T = T → False. @@ -54,9 +54,13 @@ lemma discr_tpair_xy_y: ∀I,V,T. 𝕔{I} V. T = T → False. [ #J #H destruct | #J #W #U #_ #IHU #H destruct -I V /2/ (**) (* destruct: the destucted equality is not erased *) ] -qed. +qed-. (* Basic properties *********************************************************) (* Basic_1: was: term_dec *) axiom term_eq_dec: ∀T1,T2:term. Decidable (T1 = T2). + +(* Basic_1: removed theorems 3: + not_void_abst not_abbr_void not_abst_void +*) 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 be508e49c..cd387ee02 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 @@ -33,4 +33,4 @@ fact simple_inv_bind_aux: ∀T. 𝕊[T] → ∀J,W,U. T = 𝕓{J} W. U → False qed. lemma simple_inv_bind: ∀I,V,T. 𝕊[𝕓{I} V. T] → False. -/2 width=6/ qed. +/2 width=6/ qed-. 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 24150f0bc..874f030f6 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 @@ -25,6 +25,7 @@ interpretation "weight (term)" 'Weight T = (tw T). (* Basic properties *********************************************************) +(* Basic_1: was: tweight_lt *) lemma tw_pos: ∀T. 1 ≤ #[T]. #T elim T -T /2/ qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma index 32bae83d3..d796e10ba 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma @@ -42,10 +42,10 @@ lemma simple_thom_repl_dx: ∀T1,T2. T1 ≈ T2 → 𝕊[T1] → 𝕊[T2]. #T1 #T2 #H elim H -H T1 T2 // #V1 #V2 #T1 #T2 #H elim (simple_inv_bind … H) -qed. +qed. (**) (* remove from index *) lemma simple_thom_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝕊[T2] → 𝕊[T1]. -/3/ qed. +/3/ qed-. (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma index b0ac4ff32..7704c6581 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma @@ -100,6 +100,10 @@ notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≫* break T2 )" non associative with precedence 45 for @{ 'PSubstStar $L $T1 $d $e $T2 }. +notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≡ break T2 )" + non associative with precedence 45 + for @{ 'TSubst $L $T1 $d $e $T2 }. + (* Reducibility *************************************************************) notation "hvbox( ℝ [ T ] )" diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma index 13a5ca150..90bd96d4d 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma @@ -64,14 +64,14 @@ qed. lemma cpr_inv_atom: ∀T1,T2. ⋆ ⊢ T1 ⇒ T2 → T1 ⇒ T2. #T1 #T2 * #T #HT normalize #HT2 <(tpss_inv_refl_O2 … HT2) -HT2 // -qed. +qed-. (* Basic_1: was: pr2_gen_sort *) lemma cpr_inv_sort1: ∀L,T2,k. L ⊢ ⋆k ⇒ T2 → T2 = ⋆k. #L #T2 #k * #X #H >(tpr_inv_atom1 … H) -H #H >(tpss_inv_sort1 … H) -H // -qed. +qed-. (* Basic_1: was: pr2_gen_cast *) lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ 𝕔{Cast} V1. T1 ⇒ U2 → ( @@ -82,7 +82,7 @@ lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ 𝕔{Cast} V1. T1 ⇒ U2 → ( elim (tpr_inv_cast1 … H) -H /3/ * #V #T #HV1 #HT1 #H destruct -X; elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct -U2 /4 width=5/ -qed. +qed-. (* Basic_1: removed theorems 5: pr2_head_1 pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma index 2f0e31391..005e9b0d4 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma @@ -39,10 +39,10 @@ qed. lemma cpr_shift_fwd: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → L @ T1 ⇒ L @ T2. #L elim L -L -[ /2/ -| normalize /3/ +[ #T1 #T2 #HT12 @(cpr_inv_atom … HT12) +| normalize /3 width=1/ ]. -qed. +qed-. (* Main properties **********************************************************) @@ -55,4 +55,3 @@ elim (tpr_tpss_ltpr ? L … HU1 … HUT1) -U1 // #U1 #HTU1 #HU1 elim (tpr_tpss_ltpr ? L … HU2 … HUT2) -U2 // #U2 #HTU2 #HU2 elim (tpss_conf_eq … HU1 … HU2) -U /3 width=5/ 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 4c2101504..457cb1b7d 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 @@ -24,7 +24,8 @@ lemma cpr_cdelta: ∀L,K,V1,W1,W2,i. ↓[0, i] L ≡ K. 𝕓{Abbr} V1 → K ⊢ V1 [0, |L| - i - 1] ≫* W1 → ↑[0, i + 1] W1 ≡ W2 → L ⊢ #i ⇒ W2. #L #K #V1 #W1 #W2 #i #HLK #HVW1 #HW12 -@ex2_1_intro [2: // | skip | @tpss_subst /2 width=6/ ] (**) (* /4 width=6/ is too slow *) +lapply (ldrop_fwd_ldrop2_length … HLK) #Hi +@ex2_1_intro [2: // | skip | @tpss_subst /width=6/ ] (**) (* /3 width=6/ is too slow *) qed. (* Advanced inversion lemmas ************************************************) @@ -40,12 +41,12 @@ lemma cpr_inv_lref1: ∀L,T2,i. L ⊢ #i ⇒ T2 → >(tpr_inv_atom1 … H) -H #H elim (tpss_inv_lref1 … H) -H /2/ * /3 width=6/ -qed. +qed-. (* Basic_1: was: pr2_gen_abst *) lemma cpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 → ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2. -/2/ qed. +/2/ qed-. (* Relocation properties ****************************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma index ecb0ad08c..b3ba2ff44 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma @@ -43,7 +43,7 @@ qed. (* Basic_1: was: wcpr0_gen_sort *) lemma ltpr_inv_atom1: ∀L2. ⋆ ⇒ L2 → L2 = ⋆. -/2/ qed. +/2/ qed-. fact ltpr_inv_pair1_aux: ∀L1,L2. L1 ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 → ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2. @@ -56,7 +56,7 @@ qed. (* Basic_1: was: wcpr0_gen_head *) lemma ltpr_inv_pair1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ⇒ L2 → ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2. -/2/ qed. +/2/ qed-. fact ltpr_inv_atom2_aux: ∀L1,L2. L1 ⇒ L2 → L2 = ⋆ → L1 = ⋆. #L1 #L2 * -L1 L2 @@ -66,7 +66,7 @@ fact ltpr_inv_atom2_aux: ∀L1,L2. L1 ⇒ L2 → L2 = ⋆ → L1 = ⋆. qed. lemma ltpr_inv_atom2: ∀L1. L1 ⇒ ⋆ → L1 = ⋆. -/2/ qed. +/2/ qed-. fact ltpr_inv_pair2_aux: ∀L1,L2. L1 ⇒ L2 → ∀K2,I,V2. L2 = K2. 𝕓{I} V2 → ∃∃K1,V1. K1 ⇒ K2 & V1 ⇒ V2 & L1 = K1. 𝕓{I} V1. @@ -78,12 +78,12 @@ qed. lemma ltpr_inv_pair2: ∀L1,K2,I,V2. L1 ⇒ K2. 𝕓{I} V2 → ∃∃K1,V1. K1 ⇒ K2 & V1 ⇒ V2 & L1 = K1. 𝕓{I} V1. -/2/ qed. +/2/ qed-. (* Basic forward lemmas *****************************************************) lemma ltpr_fwd_length: ∀L1,L2. L1 ⇒ L2 → |L1| = |L2|. #L1 #L2 #H elim H -H L1 L2; normalize // -qed. +qed-. (* Basic_1: removed theorems 2: wcpr0_getl wcpr0_getl_back *) 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 485c00fd1..b24c0bad2 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 @@ -19,7 +19,7 @@ include "Basic_2/reducibility/ltpr.ma". (* Basic_1: was: wcpr0_ldrop *) lemma ltpr_ldrop_conf: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀L2. L1 ⇒ L2 → - ∃∃K2. ↓[d, e] L2 ≡ K2 & K1 ⇒ K2. + ∃∃K2. ↓[d, e] L2 ≡ K2 & K1 ⇒ K2. #L1 #K1 #d #e #H elim H -H L1 K1 d e [ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/ | #K1 #I #V1 #X #H @@ -36,7 +36,7 @@ qed. (* Basic_1: was: wcpr0_ldrop_back *) lemma ltpr_ldrop_trans: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀K2. K1 ⇒ K2 → - ∃∃L2. ↓[d, e] L2 ≡ K2 & L1 ⇒ L2. + ∃∃L2. ↓[d, e] L2 ≡ K2 & L1 ⇒ L2. #L1 #K1 #d #e #H elim H -H L1 K1 d e [ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/ | #K1 #I #V1 #X #H 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 5868a5c93..a9a262efe 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma @@ -32,7 +32,7 @@ lemma tnf_inv_abst: ∀V,T. ℕ[𝕔{Abst}V.T] → ℕ[V] ∧ ℕ[T]. [ #V2 #HV2 lapply (HVT1 (𝕔{Abst}V2.T1) ?) -HVT1 /2/ -HV2 #H destruct -V1 T1 // | #T2 #HT2 lapply (HVT1 (𝕔{Abst}V1.T2) ?) -HVT1 /2/ -HT2 #H destruct -V1 T1 // ] -qed. +qed-. lemma tnf_inv_appl: ∀V,T. ℕ[𝕔{Appl}V.T] → ∧∧ ℕ[V] & ℕ[T] & 𝕊[T]. #V1 #T1 #HVT1 @and3_intro @@ -43,13 +43,23 @@ lemma tnf_inv_appl: ∀V,T. ℕ[𝕔{Appl}V.T] → ∧∧ ℕ[V] & ℕ[T] & 𝕊 lapply (H (𝕔{Abbr}W1.𝕔{Appl}V2.U1) ?) -H /2/ -HV12 #H destruct | lapply (H (𝕔{Abbr}V1.U1) ?) -H /2/ #H destruct ] +qed-. + +lemma tnf_inv_abbr: ∀V,T. ℕ[𝕔{Abbr}V.T] → False. +#V #T #H elim (is_lift_dec T 0 1) +[ * #U #HTU + lapply (H U ?) -H /2 width=3/ #H destruct -U; + elim (lift_inv_pair_xy_y … HTU) +| #HT + elim (tps_full (⋆) V T (⋆. 𝕓{Abbr} V) 0 ?) // #T2 #T1 #HT2 #HT12 + lapply (H (𝕓{Abbr}V.T2) ?) -H /2/ -HT2 #H destruct -T /3 width=2/ +] qed. -axiom tnf_inv_abbr: ∀V,T. ℕ[𝕔{Abbr}V.T] → False. - lemma tnf_inv_cast: ∀V,T. ℕ[𝕔{Cast}V.T] → False. -#V #T #H lapply (H T ?) -H /2/ -qed. +#V #T #H lapply (H T ?) -H /2 width=1/ #H +@(discr_tpair_xy_y … H) +qed-. (* Basic properties *********************************************************) 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 db2c8c69f..f2818ea72 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "Basic_2/grammar/term_simple.ma". include "Basic_2/substitution/tps.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) @@ -42,7 +43,7 @@ interpretation (* Basic properties *********************************************************) lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ⇒ V2 → T1 ⇒ T2 → - 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. + 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. /2/ qed. (* Basic_1: was by definition: pr0_refl *) @@ -67,7 +68,7 @@ qed. (* Basic_1: was: pr0_gen_sort pr0_gen_lref *) lemma tpr_inv_atom1: ∀I,U2. 𝕒{I} ⇒ U2 → U2 = 𝕒{I}. -/2/ qed. +/2/ qed-. fact tpr_inv_bind1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 → (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 & @@ -92,7 +93,7 @@ lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 → U2 = 𝕓{I} V2. T ) ∨ ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr. -/2/ qed. +/2/ qed-. (* Basic_1: was pr0_gen_abbr *) lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 → @@ -103,7 +104,7 @@ lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 → ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2. #V1 #T1 #U2 #H elim (tpr_inv_bind1 … H) -H * /3 width=7/ -qed. +qed-. fact tpr_inv_flat1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,U0. U1 = 𝕗{I} V1. U0 → ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 & @@ -141,7 +142,7 @@ lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 → U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 & I = Appl | (U0 ⇒ U2 ∧ I = Cast). -/2/ qed. +/2/ qed-. (* Basic_1: was pr0_gen_appl *) lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 → @@ -156,7 +157,21 @@ lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 → U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2. #V1 #U0 #U2 #H elim (tpr_inv_flat1 … H) -H * /3 width=12/ #_ #H destruct -qed. +qed-. + +(* Note: the main property of simple terms *) +lemma tpr_inv_appl1_simple: ∀V1,T1,U. 𝕔{Appl} V1. T1 ⇒ U → 𝕊[T1] → + ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & + U = 𝕔{Appl} V2. T2. +#V1 #T1 #U #H #HT1 +elim (tpr_inv_appl1 … H) -H * +[ /2 width=5/ +| #V2 #W #W1 #W2 #_ #_ #H #_ destruct -T1; + elim (simple_inv_bind … HT1) +| #V2 #V #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct -T1; + elim (simple_inv_bind … HT1) +] +qed-. (* Basic_1: was: pr0_gen_cast *) lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕔{Cast} V1. T1 ⇒ U2 → @@ -167,7 +182,7 @@ elim (tpr_inv_flat1 … H) -H * /3 width=5/ [ #V2 #W #W1 #W2 #_ #_ #_ #_ #H destruct | #V2 #W #W1 #W2 #T2 #U1 #_ #_ #_ #_ #_ #_ #H destruct ] -qed. +qed-. fact tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i → ∨∨ T1 = #i @@ -190,7 +205,7 @@ lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i → | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i & T1 = 𝕔{Abbr} V. T | ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T. -/2/ qed. +/2/ qed-. (* Basic_1: removed theorems 3: pr0_subst0_back pr0_subst0_fwd pr0_subst0 diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma index 0c8235765..a30dcddac 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma @@ -118,4 +118,4 @@ qed. (* Basic_1: was pr0_gen_abst *) lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 → ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2. -/2/ qed. +/2/ qed-. 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 d0050452b..ccdf59224 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma @@ -54,7 +54,7 @@ fact trf_inv_atom_aux: ∀I,T. ℝ[T] → T = 𝕒{I} → False. qed. lemma trf_inv_atom: ∀I. ℝ[𝕒{I}] → False. -/2/ qed. +/2/ qed-. fact trf_inv_abst_aux: ∀W,U,T. ℝ[T] → T = 𝕔{Abst} W. U → ℝ[W] ∨ ℝ[U]. #W #U #T * -T @@ -69,7 +69,7 @@ fact trf_inv_abst_aux: ∀W,U,T. ℝ[T] → T = 𝕔{Abst} W. U → ℝ[W] ∨ qed. lemma trf_inv_abst: ∀V,T. ℝ[𝕔{Abst}V.T] → ℝ[V] ∨ ℝ[T]. -/2/ qed. +/2/ qed-. fact trf_inv_appl_aux: ∀W,U,T. ℝ[T] → T = 𝕔{Appl} W. U → ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False). @@ -86,22 +86,22 @@ fact trf_inv_appl_aux: ∀W,U,T. ℝ[T] → T = 𝕔{Appl} W. U → qed. lemma trf_inv_appl: ∀W,U. ℝ[𝕔{Appl}W.U] → ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False). -/2/ qed. +/2/ qed-. lemma tif_inv_abbr: ∀V,T. 𝕀[𝕔{Abbr}V.T] → False. -/2/ qed. +/2/ qed-. lemma tif_inv_abst: ∀V,T. 𝕀[𝕔{Abst}V.T] → 𝕀[V] ∧ 𝕀[T]. -/4/ qed. +/4/ qed-. lemma tif_inv_appl: ∀V,T. 𝕀[𝕔{Appl}V.T] → ∧∧ 𝕀[V] & 𝕀[T] & 𝕊[T]. #V #T #HVT @and3_intro /3/ generalize in match HVT -HVT; elim T -T // * // * #U #T #_ #_ #H elim (H ?) -H /2/ -qed. +qed-. lemma tif_inv_cast: ∀V,T. 𝕀[𝕔{Cast}V.T] → False. -/2/ qed. +/2/ qed-. (* Basic properties *********************************************************) 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 838ef0fed..ffd44c5aa 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma @@ -45,7 +45,7 @@ qed. (* Basic_1: was: ldrop_gen_refl *) lemma ldrop_inv_refl: ∀L1,L2. ↓[0, 0] L1 ≡ L2 → L1 = L2. -/2 width=5/ qed. +/2 width=5/ qed-. fact ldrop_inv_atom1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → L1 = ⋆ → L2 = ⋆. @@ -59,7 +59,7 @@ qed. (* Basic_1: was: ldrop_gen_sort *) lemma ldrop_inv_atom1: ∀d,e,L2. ↓[d, e] ⋆ ≡ L2 → L2 = ⋆. -/2 width=5/ qed. +/2 width=5/ qed-. fact ldrop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → ∀K,I,V. L1 = K. 𝕓{I} V → @@ -76,7 +76,7 @@ qed. lemma ldrop_inv_O1: ∀e,K,I,V,L2. ↓[0, e] K. 𝕓{I} V ≡ L2 → (e = 0 ∧ L2 = K. 𝕓{I} V) ∨ (0 < e ∧ ↓[0, e - 1] K ≡ L2). -/2/ qed. +/2/ qed-. (* Basic_1: was: ldrop_gen_ldrop *) lemma ldrop_inv_ldrop1: ∀e,K,I,V,L2. @@ -84,7 +84,7 @@ lemma ldrop_inv_ldrop1: ∀e,K,I,V,L2. #e #K #I #V #L2 #H #He elim (ldrop_inv_O1 … H) -H * // #H destruct -e; elim (lt_refl_false … He) -qed. +qed-. fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → ∀I,K1,V1. L1 = K1. 𝕓{I} V1 → @@ -105,7 +105,7 @@ lemma ldrop_inv_skip1: ∀d,e,I,K1,V1,L2. ↓[d, e] K1. 𝕓{I} V1 ≡ L2 → 0 ∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 & ↑[d - 1, e] V2 ≡ V1 & L2 = K2. 𝕓{I} V2. -/2/ qed. +/2/ qed-. fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → ∀I,K2,V2. L2 = K2. 𝕓{I} V2 → @@ -125,7 +125,7 @@ qed. lemma ldrop_inv_skip2: ∀d,e,I,L1,K2,V2. ↓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < d → ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & ↑[d - 1, e] V2 ≡ V1 & L1 = K1. 𝕓{I} V1. -/2/ qed. +/2/ qed-. (* Basic properties *********************************************************) @@ -135,7 +135,7 @@ lemma ldrop_refl: ∀L. ↓[0, 0] L ≡ L. qed. lemma ldrop_ldrop_lt: ∀L1,L2,I,V,e. - ↓[0, e - 1] L1 ≡ L2 → 0 < e → ↓[0, e] L1. 𝕓{I} V ≡ L2. + ↓[0, e - 1] L1 ≡ L2 → 0 < e → ↓[0, e] L1. 𝕓{I} V ≡ L2. #L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) /2/ qed. @@ -181,7 +181,7 @@ lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ↓[O, e] L1 ≡ K2. 𝕓{I2} V2 → | @ldrop_ldrop >(plus_minus_m_m e 1) /2/ ] ] -qed. +qed-. lemma ldrop_fwd_lw: ∀L1,L2,d,e. ↓[d, e] L1 ≡ L2 → #[L2] ≤ #[L1]. #L1 #L2 #d #e #H elim H -H L1 L2 d e // normalize @@ -189,7 +189,7 @@ lemma ldrop_fwd_lw: ∀L1,L2,d,e. ↓[d, e] L1 ≡ L2 → #[L2] ≤ #[L1]. | #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 >(tw_lift … HV21) -HV21 /2/ ] -qed. +qed-. lemma ldrop_fwd_ldrop2_length: ∀L1,I2,K2,V2,e. ↓[0, e] L1 ≡ K2. 𝕓{I2} V2 → e < |L1|. @@ -201,7 +201,7 @@ lemma ldrop_fwd_ldrop2_length: ∀L1,I2,K2,V2,e. | lapply (IHL1 … H) -IHL1 H #HeK1 whd in ⊢ (? ? %) /2/ ] ] -qed. +qed-. lemma ldrop_fwd_O1_length: ∀L1,L2,e. ↓[0, e] L1 ≡ L2 → |L2| = |L1| - e. #L1 elim L1 -L1 @@ -213,7 +213,7 @@ lemma ldrop_fwd_O1_length: ∀L1,L2,e. ↓[0, e] L1 ≡ L2 → |L2| = |L1| - e. >minus_le_minus_minus_comm // ] ] -qed. +qed-. (* Basic_1: removed theorems 49: ldrop_skip_flat diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma index 1af7c0db8..a495bbdcb 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma @@ -34,7 +34,7 @@ theorem ldrop_mono: ∀d,e,L,L1. ↓[d, e] L ≡ L1 → >(lift_inj … HVT1 … HVT2) -HVT1 HVT2 >(IHLK1 … HLK2) -IHLK1 HLK2 // ] -qed. +qed-. (* Basic_1: was: ldrop_conf_ge *) theorem ldrop_conf_ge: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → 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 1934c37bc..7d0f43c81 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma @@ -34,59 +34,6 @@ inductive lift: nat → nat → relation term ≝ interpretation "relocation" 'RLift d e T1 T2 = (lift d e T1 T2). -(* Basic properties *********************************************************) - -(* Basic_1: was: lift_lref_gt *) -lemma lift_lref_ge_minus: ∀d,e,i. d + e ≤ i → ↑[d, e] #(i - e) ≡ #i. -#d #e #i #H >(plus_minus_m_m i e) in ⊢ (? ? ? ? %) /3/ -qed. - -(* Basic_1: was: lift_r *) -lemma lift_refl: ∀T,d. ↑[d, 0] T ≡ T. -#T elim T -T -[ * #i // #d elim (lt_or_ge i d) /2/ -| * /2/ -] -qed. - -lemma lift_total: ∀T1,d,e. ∃T2. ↑[d,e] T1 ≡ T2. -#T1 elim T1 -T1 -[ * #i /2/ #d #e elim (lt_or_ge i d) /3/ -| * #I #V1 #T1 #IHV1 #IHT1 #d #e - elim (IHV1 d e) -IHV1 #V2 #HV12 - [ elim (IHT1 (d+1) e) -IHT1 /3/ - | elim (IHT1 d e) -IHT1 /3/ - ] -] -qed. - -(* Basic_1: was: lift_free (right to left) *) -lemma lift_split: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → ∀d2,e1. - d1 ≤ d2 → d2 ≤ d1 + e1 → e1 ≤ e2 → - ∃∃T. ↑[d1, e1] T1 ≡ T & ↑[d2, e2 - e1] T ≡ T2. -#d1 #e2 #T1 #T2 #H elim H -H d1 e2 T1 T2 -[ /3/ -| #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_ - lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4/ -| #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12 - lapply (transitive_le …(i+e1) Hd21 ?) /2/ -Hd21 #Hd21 - <(arith_d1 i e2 e1) // /3/ -| /3/ -| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 - elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b - elim (IHT (d2+1) … ? ? He12) /3 width = 5/ -| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 - elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b - elim (IHT d2 … ? ? He12) /3 width = 5/ -] -qed. - -(* Basic forward lemmas *****************************************************) - -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. - (* Basic inversion lemmas ***************************************************) fact lift_inv_refl_aux: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → e = 0 → T1 = T2. @@ -94,7 +41,7 @@ fact lift_inv_refl_aux: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → e = 0 → T1 = T2. qed. lemma lift_inv_refl: ∀d,T1,T2. ↑[d, 0] T1 ≡ T2 → T1 = T2. -/2/ qed. +/2/ qed-. fact lift_inv_sort1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T1 = ⋆k → T2 = ⋆k. #d #e #T1 #T2 * -d e T1 T2 // @@ -105,7 +52,7 @@ fact lift_inv_sort1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T1 = ⋆k qed. lemma lift_inv_sort1: ∀d,e,T2,k. ↑[d,e] ⋆k ≡ T2 → T2 = ⋆k. -/2 width=5/ qed. +/2 width=5/ qed-. fact lift_inv_lref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T1 = #i → (i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)). @@ -121,19 +68,19 @@ qed. lemma lift_inv_lref1: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → (i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)). -/2/ qed. +/2/ qed-. lemma lift_inv_lref1_lt: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → i < d → T2 = #i. #d #e #T2 #i #H elim (lift_inv_lref1 … H) -H * // #Hdi #_ #Hid lapply (le_to_lt_to_lt … Hdi Hid) -Hdi Hid #Hdd elim (lt_refl_false … Hdd) -qed. +qed-. lemma lift_inv_lref1_ge: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → d ≤ i → T2 = #(i + e). #d #e #T2 #i #H elim (lift_inv_lref1 … H) -H * // #Hid #_ #Hdi lapply (le_to_lt_to_lt … Hdi Hid) -Hdi Hid #Hdd elim (lt_refl_false … Hdd) -qed. +qed-. fact lift_inv_gref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀p. T1 = §p → T2 = §p. #d #e #T1 #T2 * -d e T1 T2 // @@ -144,7 +91,7 @@ fact lift_inv_gref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀p. T1 = §p → qed. lemma lift_inv_gref1: ∀d,e,T2,p. ↑[d,e] §p ≡ T2 → T2 = §p. -/2 width=5/ qed. +/2 width=5/ qed-. fact lift_inv_bind1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀I,V1,U1. T1 = 𝕓{I} V1.U1 → @@ -163,7 +110,7 @@ qed. lemma lift_inv_bind1: ∀d,e,T2,I,V1,U1. ↑[d,e] 𝕓{I} V1. U1 ≡ T2 → ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 & T2 = 𝕓{I} V2. U2. -/2/ qed. +/2/ qed-. fact lift_inv_flat1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀I,V1,U1. T1 = 𝕗{I} V1.U1 → @@ -182,7 +129,7 @@ qed. lemma lift_inv_flat1: ∀d,e,T2,I,V1,U1. ↑[d,e] 𝕗{I} V1. U1 ≡ T2 → ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 & T2 = 𝕗{I} V2. U2. -/2/ qed. +/2/ qed-. fact lift_inv_sort2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k. #d #e #T1 #T2 * -d e T1 T2 // @@ -194,7 +141,7 @@ qed. (* Basic_1: was: lift_gen_sort *) lemma lift_inv_sort2: ∀d,e,T1,k. ↑[d,e] T1 ≡ ⋆k → T1 = ⋆k. -/2 width=5/ qed. +/2 width=5/ qed-. fact lift_inv_lref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T2 = #i → (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)). @@ -211,23 +158,30 @@ qed. (* Basic_1: was: lift_gen_lref *) lemma lift_inv_lref2: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)). -/2/ qed. +/2/ qed-. (* Basic_1: was: lift_gen_lref_lt *) lemma lift_inv_lref2_lt: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → i < d → T1 = #i. #d #e #T1 #i #H elim (lift_inv_lref2 … H) -H * // #Hdi #_ #Hid lapply (le_to_lt_to_lt … Hdi Hid) -Hdi Hid #Hdd elim (plus_lt_false … Hdd) -qed. +qed-. (* Basic_1: was: lift_gen_lref_false *) +lemma lift_inv_lref2_be: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → + d ≤ i → i < d + e → False. +#d #e #T1 #i #H elim (lift_inv_lref2 … H) -H * +[ #H1 #_ #H2 #_ | #H2 #_ #_ #H1 ] +lapply (le_to_lt_to_lt … H2 H1) -H2 H1 #H +elim (lt_refl_false … H) +qed-. (* Basic_1: was: lift_gen_lref_ge *) lemma lift_inv_lref2_ge: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → d + e ≤ i → T1 = #(i - e). #d #e #T1 #i #H elim (lift_inv_lref2 … H) -H * // #Hid #_ #Hdi lapply (le_to_lt_to_lt … Hdi Hid) -Hdi Hid #Hdd elim (plus_lt_false … Hdd) -qed. +qed-. fact lift_inv_gref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀p. T2 = §p → T1 = §p. #d #e #T1 #T2 * -d e T1 T2 // @@ -238,7 +192,7 @@ fact lift_inv_gref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀p. T2 = §p → qed. lemma lift_inv_gref2: ∀d,e,T1,p. ↑[d,e] T1 ≡ §p → T1 = §p. -/2 width=5/ qed. +/2 width=5/ qed-. fact lift_inv_bind2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀I,V2,U2. T2 = 𝕓{I} V2.U2 → @@ -258,7 +212,7 @@ qed. lemma lift_inv_bind2: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡ 𝕓{I} V2. U2 → ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 & T1 = 𝕓{I} V1. U1. -/2/ qed. +/2/ qed-. fact lift_inv_flat2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀I,V2,U2. T2 = 𝕗{I} V2.U2 → @@ -278,7 +232,124 @@ qed. lemma lift_inv_flat2: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡ 𝕗{I} V2. U2 → ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 & T1 = 𝕗{I} V1. U1. -/2/ qed. +/2/ qed-. + +lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ↑[d, e] 𝕔{I} V. T ≡ V → False. +#d #e #J #V elim V -V +[ * #i #T #H + [ lapply (lift_inv_sort2 … H) -H #H destruct + | elim (lift_inv_lref2 … H) -H * #_ #H destruct + | lapply (lift_inv_gref2 … H) -H #H destruct + ] +| * #I #W2 #U2 #IHW2 #_ #T #H + [ elim (lift_inv_bind2 … H) -H #W1 #U1 #HW12 #_ #H destruct -J T W1 /2/ + | elim (lift_inv_flat2 … H) -H #W1 #U1 #HW12 #_ #H destruct -J T W1 /2/ + ] +] +qed-. + +lemma lift_inv_pair_xy_y: ∀I,T,V,d,e. ↑[d, e] 𝕔{I} V. T ≡ T → False. +#J #T elim T -T +[ * #i #V #d #e #H + [ lapply (lift_inv_sort2 … H) -H #H destruct + | elim (lift_inv_lref2 … H) -H * #_ #H destruct + | lapply (lift_inv_gref2 … H) -H #H destruct + ] +| * #I #W2 #U2 #_ #IHU2 #V #d #e #H + [ elim (lift_inv_bind2 … H) -H #W1 #U1 #_ #HU12 #H destruct -J U1 W1 /2/ + | elim (lift_inv_flat2 … H) -H #W1 #U1 #_ #HU12 #H destruct -J U1 W1 /2/ + ] +] +qed-. + +(* Basic forward lemmas *****************************************************) + +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-. + +(* Basic properties *********************************************************) + +(* Basic_1: was: lift_lref_gt *) +lemma lift_lref_ge_minus: ∀d,e,i. d + e ≤ i → ↑[d, e] #(i - e) ≡ #i. +#d #e #i #H >(plus_minus_m_m i e) in ⊢ (? ? ? ? %) /3 width=2/ +qed. + +(* Basic_1: was: lift_r *) +lemma lift_refl: ∀T,d. ↑[d, 0] T ≡ T. +#T elim T -T +[ * #i // #d elim (lt_or_ge i d) /2/ +| * /2/ +] +qed. + +lemma lift_total: ∀T1,d,e. ∃T2. ↑[d,e] T1 ≡ T2. +#T1 elim T1 -T1 +[ * #i /2/ #d #e elim (lt_or_ge i d) /3/ +| * #I #V1 #T1 #IHV1 #IHT1 #d #e + elim (IHV1 d e) -IHV1 #V2 #HV12 + [ elim (IHT1 (d+1) e) -IHT1 /3/ + | elim (IHT1 d e) -IHT1 /3/ + ] +] +qed. + +(* Basic_1: was: lift_free (right to left) *) +lemma lift_split: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → + ∀d2,e1. d1 ≤ d2 → d2 ≤ d1 + e1 → e1 ≤ e2 → + ∃∃T. ↑[d1, e1] T1 ≡ T & ↑[d2, e2 - e1] T ≡ T2. +#d1 #e2 #T1 #T2 #H elim H -H d1 e2 T1 T2 +[ /3/ +| #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_ + lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4/ +| #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12 + lapply (transitive_le …(i+e1) Hd21 ?) /2/ -Hd21 #Hd21 + <(arith_d1 i e2 e1) // /3/ +| /3/ +| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 + elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b + elim (IHT (d2+1) … ? ? He12) /3 width=5/ +| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 + elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b + elim (IHT d2 … ? ? He12) /3 width=5/ +] +qed. + +(* Basic_1: was only: dnf_dec2 dnf_dec *) +lemma is_lift_dec: ∀T2,d,e. Decidable (∃T1. ↑[d,e] T1 ≡ T2). +#T1 elim T1 -T1 +[ * [1,3: /3 width=2/ ] #i #d #e + elim (lt_dec i d) #Hid + [ /4 width=2/ + | lapply (false_lt_to_le … Hid) -Hid #Hid + elim (lt_dec i (d + e)) #Hide + [ @or_intror * #T1 #H + elim (lift_inv_lref2_be … H Hid Hide) + | lapply (false_lt_to_le … Hide) -Hide /4 width=2/ + ] + ] +| * #I #V2 #T2 #IHV2 #IHT2 #d #e + [ elim (IHV2 d e) -IHV2 + [ * #V1 #HV12 elim (IHT2 (d+1) e) -IHT2 + [ * #T1 #HT12 @or_introl /3/ + | -V1 #HT2 @or_intror * #X #H + elim (lift_inv_bind2 … H) -H /3 width=2/ + ] + | -IHT2 #HV2 @or_intror * #X #H + elim (lift_inv_bind2 … H) -H /3 width=2/ + ] + | elim (IHV2 d e) -IHV2 + [ * #V1 #HV12 elim (IHT2 d e) -IHT2 + [ * #T1 #HT12 /4 width=2/ + | -V1 #HT2 @or_intror * #X #H + elim (lift_inv_flat2 … H) -H /3 width=2/ + ] + | -IHT2 #HV2 @or_intror * #X #H + elim (lift_inv_flat2 … H) -H /3 width=2/ + ] + ] +] +qed. (* Basic_1: removed theorems 7: lift_head lift_gen_head diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma index 6feb72e03..5bc36f943 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma @@ -34,7 +34,7 @@ theorem lift_inj: ∀d,e,T1,U. ↑[d,e] T1 ≡ U → ∀T2. ↑[d,e] T2 ≡ U | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX elim (lift_inv_flat2 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/ ] -qed. +qed-. (* Basic_1: was: lift_gen_lift *) theorem lift_div_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → @@ -84,7 +84,7 @@ theorem lift_mono: ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX elim (lift_inv_flat1 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/ ] -qed. +qed-. (* Basic_1: was: lift_free (left to right) *) theorem lift_trans_be: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → 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 06201e8e5..43c13fb22 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma @@ -65,7 +65,7 @@ fact ltps_inv_refl_O2_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → e = 0 → L1 = L2. qed. lemma ltps_inv_refl_O2: ∀d,L1,L2. L1 [d, 0] ≫ L2 → L1 = L2. -/2/ qed. +/2/ qed-. fact ltps_inv_atom1_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → L1 = ⋆ → L2 = ⋆. @@ -78,7 +78,7 @@ fact ltps_inv_atom1_aux: ∀d,e,L1,L2. qed. lemma ltps_inv_atom1: ∀d,e,L2. ⋆ [d, e] ≫ L2 → L2 = ⋆. -/2 width=5/ qed. +/2 width=5/ qed-. fact ltps_inv_tps21_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → d = 0 → 0 < e → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 → @@ -96,7 +96,7 @@ qed. lemma ltps_inv_tps21: ∀e,K1,I,V1,L2. K1. 𝕓{I} V1 [0, e] ≫ L2 → 0 < e → ∃∃K2,V2. K1 [0, e - 1] ≫ K2 & K2 ⊢ V1 [0, e - 1] ≫ V2 & L2 = K2. 𝕓{I} V2. -/2 width=5/ qed. +/2 width=5/ qed-. fact ltps_inv_tps11_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → 0 < d → ∀I,K1,V1. L1 = K1. 𝕓{I} V1 → @@ -116,7 +116,7 @@ lemma ltps_inv_tps11: ∀d,e,I,K1,V1,L2. K1. 𝕓{I} V1 [d, e] ≫ L2 → 0 < d ∃∃K2,V2. K1 [d - 1, e] ≫ K2 & K2 ⊢ V1 [d - 1, e] ≫ V2 & L2 = K2. 𝕓{I} V2. -/2/ qed. +/2/ qed-. fact ltps_inv_atom2_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → L2 = ⋆ → L1 = ⋆. @@ -129,7 +129,7 @@ fact ltps_inv_atom2_aux: ∀d,e,L1,L2. qed. lemma ltps_inv_atom2: ∀d,e,L1. L1 [d, e] ≫ ⋆ → L1 = ⋆. -/2 width=5/ qed. +/2 width=5/ qed-. fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → d = 0 → 0 < e → ∀K2,I,V2. L2 = K2. 𝕓{I} V2 → @@ -147,7 +147,7 @@ qed. lemma ltps_inv_tps22: ∀e,L1,K2,I,V2. L1 [0, e] ≫ K2. 𝕓{I} V2 → 0 < e → ∃∃K1,V1. K1 [0, e - 1] ≫ K2 & K2 ⊢ V1 [0, e - 1] ≫ V2 & L1 = K1. 𝕓{I} V1. -/2 width=5/ qed. +/2 width=5/ qed-. fact ltps_inv_tps12_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → 0 < d → ∀I,K2,V2. L2 = K2. 𝕓{I} V2 → @@ -167,7 +167,7 @@ lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ≫ K2. 𝕓{I} V2 → 0 < d ∃∃K1,V1. K1 [d - 1, e] ≫ K2 & K2 ⊢ V1 [d - 1, e] ≫ V2 & L1 = K1. 𝕓{I} V1. -/2/ qed. +/2/ qed-. (* Basic_1: removed theorems 27: csubst0_clear_O csubst0_ldrop_lt csubst0_ldrop_gt csubst0_ldrop_eq diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma index 32501c8e6..5482e2407 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma @@ -17,8 +17,8 @@ include "Basic_2/substitution/ltps.ma". (* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************) lemma ltps_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → - d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2. + ∀L2,e2. ↓[0, e2] L0 ≡ L2 → + d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2. #L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H // | // @@ -34,8 +34,8 @@ lemma ltps_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → qed. lemma ltps_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → - d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2. + ∀L2,e2. ↓[0, e2] L0 ≡ L2 → + d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2. #L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H // | // @@ -51,8 +51,8 @@ lemma ltps_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → qed. lemma ltps_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → - ∃∃L. L2 [0, d1 + e1 - e2] ≫ L & ↓[0, e2] L1 ≡ L. + ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → + ∃∃L. L2 [0, d1 + e1 - e2] ≫ L & ↓[0, e2] L1 ≡ L. #L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2/ | normalize #L #I #V #L2 #e2 #HL2 #_ #He2 @@ -73,8 +73,8 @@ lemma ltps_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → qed. lemma ltps_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → - ∃∃L. L [0, d1 + e1 - e2] ≫ L2 & ↓[0, e2] L1 ≡ L. + ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → + ∃∃L. L [0, d1 + e1 - e2] ≫ L2 & ↓[0, e2] L1 ≡ L. #L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2/ | normalize #L #I #V #L2 #e2 #HL2 #_ #He2 @@ -95,8 +95,8 @@ lemma ltps_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → qed. lemma ltps_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 → - ∃∃L. L2 [d1 - e2, e1] ≫ L & ↓[0, e2] L1 ≡ L. + ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 → + ∃∃L. L2 [d1 - e2, e1] ≫ L & ↓[0, e2] L1 ≡ L. #L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2/ | /2/ @@ -113,8 +113,8 @@ lemma ltps_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → qed. lemma ltps_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 → - ∃∃L. L [d1 - e2, e1] ≫ L2 & ↓[0, e2] L1 ≡ L. + ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 → + ∃∃L. L [d1 - e2, e1] ≫ L2 & ↓[0, e2] L1 ≡ L. #L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2/ | /2/ 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 7ab9fba13..744c00b81 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma @@ -50,6 +50,23 @@ lemma tps_refl: ∀T,L,d,e. L ⊢ T [d, e] ≫ T. #I elim I -I /2/ qed. +(* Basic_1: was: subst1_ex *) +lemma tps_full: ∀K,V,T1,L,d. ↓[0, d] L ≡ (K. 𝕓{Abbr} V) → + ∃∃T2,T. L ⊢ T1 [d, 1] ≫ T2 & ↑[d, 1] T ≡ T2. +#K #V #T1 elim T1 -T1 +[ * #i #L #d #HLK /2/ + elim (lt_or_eq_or_gt i d) #Hid [ /3/ |3: /3/ ] + destruct -d; + elim (lift_total V 0 (i+1)) #W #HVW + elim (lift_split … HVW i i ? ? ?) // (lt i (plus d h)) -> (EX u1 | t1 = (lift (minus (plus d h) (S i)) (S i) u1)). *) - lemma tps_inv_lift1_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 → d ≤ dt → dt ≤ d + e → d + e ≤ dt + et → 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 582c2caa0..456a3aae0 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma @@ -29,7 +29,7 @@ lemma ltpss_ind: ∀d,e,L1. ∀R: lenv → Prop. R L1 → (∀L,L2. L1 [d, e] ≫* L → L [d, e] ≫ L2 → R L → R L2) → ∀L2. L1 [d, e] ≫* L2 → R L2. #d #e #L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) // -qed. +qed-. (* Basic properties *********************************************************) @@ -45,13 +45,13 @@ lemma ltpss_refl: ∀L,d,e. L [d, e] ≫* L. lemma ltpss_inv_refl_O2: ∀d,L1,L2. L1 [d, 0] ≫* L2 → L1 = L2. #d #L1 #L2 #H @(ltpss_ind … H) -L2 // #L #L2 #_ #HL2 #IHL <(ltps_inv_refl_O2 … HL2) -HL2 // -qed. +qed-. lemma ltpss_inv_atom1: ∀d,e,L2. ⋆ [d, e] ≫* L2 → L2 = ⋆. #d #e #L2 #H @(ltpss_ind … H) -L2 // #L #L2 #_ #HL2 #IHL destruct -L >(ltps_inv_atom1 … HL2) -HL2 // -qed. +qed-. fact ltpss_inv_atom2_aux: ∀d,e,L1,L2. L1 [d, e] ≫* L2 → L2 = ⋆ → L1 = ⋆. @@ -61,7 +61,7 @@ lapply (ltps_inv_atom2 … HL2) -HL2 /2/ qed. lemma ltpss_inv_atom2: ∀d,e,L1. L1 [d, e] ≫* ⋆ → L1 = ⋆. -/2 width=5/ qed. +/2 width=5/ qed-. (* fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → d = 0 → 0 < e → ∀K2,I,V2. L2 = K2. 𝕓{I} V2 → diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ldrop.ma index 1fc4ed7e6..14d529db8 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ldrop.ma @@ -18,20 +18,20 @@ include "Basic_2/unfold/ltpss.ma". (* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************) lemma ltpss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → - d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2. + ∀L2,e2. ↓[0, e2] L0 ≡ L2 → + d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2. #L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1 /3 width=6/ qed. lemma ltpss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → - d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2. + ∀L2,e2. ↓[0, e2] L0 ≡ L2 → + d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2. #L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 /3 width=6/ qed. lemma ltpss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → - ∃∃L. L2 [0, d1 + e1 - e2] ≫* L & ↓[0, e2] L1 ≡ L. + ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → + ∃∃L. L2 [0, d1 + e1 - e2] ≫* L & ↓[0, e2] L1 ≡ L. #L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1 [ /2/ | #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1 @@ -41,8 +41,8 @@ lemma ltpss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 → qed. lemma ltpss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → - ∃∃L. L [0, d1 + e1 - e2] ≫* L2 & ↓[0, e2] L1 ≡ L. + ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → + ∃∃L. L [0, d1 + e1 - e2] ≫* L2 & ↓[0, e2] L1 ≡ L. #L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 [ /2/ | #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1 @@ -52,8 +52,8 @@ lemma ltpss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 → qed. lemma ltpss_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 → - ∃∃L. L2 [d1 - e2, e1] ≫* L & ↓[0, e2] L1 ≡ L. + ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 → + ∃∃L. L2 [d1 - e2, e1] ≫* L & ↓[0, e2] L1 ≡ L. #L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1 [ /2/ | #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #He2d1 @@ -63,8 +63,8 @@ lemma ltpss_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 → qed. lemma ltpss_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 → - ∃∃L. L [d1 - e2, e1] ≫* L2 & ↓[0, e2] L1 ≡ L. + ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 → + ∃∃L. L [d1 - e2, e1] ≫* L2 & ↓[0, e2] L1 ≡ L. #L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 [ /2/ | #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #He2d1 diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma index 367093b0a..af49f1c05 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma @@ -153,7 +153,7 @@ lemma ltpss_fwd_tpss21: ∀e,K1,I,V1,L2. 0 < e → K1. 𝕓{I} V1 [0, e] ≫* L2 lapply (ltps_tps_trans_eq … HV2 … HK2) -HV2 #HV2 lapply (ltpss_tpss_trans_eq … HK1 … HV2) -HV2 #HV2 /3 width=5/ ] -qed. +qed-. lemma ltpss_fwd_tpss11: ∀d,e,I,K1,V1,L2. 0 < d → K1. 𝕓{I} V1 [d, e] ≫* L2 → ∃∃K2,V2. K1 [d - 1, e] ≫* K2 & @@ -166,4 +166,4 @@ lemma ltpss_fwd_tpss11: ∀d,e,I,K1,V1,L2. 0 < d → K1. 𝕓{I} V1 [d, e] ≫* lapply (ltps_tps_trans_eq … HV2 … HK2) -HV2 #HV2 lapply (ltpss_tpss_trans_eq … HK1 … HV2) -HV2 #HV2 /3 width=5/ ] -qed. +qed-. 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 44587e3bd..62eb25d49 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma @@ -28,7 +28,7 @@ lemma tpss_ind: ∀d,e,L,T1. ∀R: term → Prop. R T1 → (∀T,T2. L ⊢ T1 [d, e] ≫* T → L ⊢ T [d, e] ≫ T2 → R T → R T2) → ∀T2. L ⊢ T1 [d, e] ≫* T2 → R T2. #d #e #L #T1 #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) // -qed. +qed-. (* Basic properties *********************************************************) @@ -105,7 +105,7 @@ lemma tpss_inv_sort1: ∀L,T2,k,d,e. L ⊢ ⋆k [d, e] ≫* T2 → T2 = ⋆k. | #T #T2 #_ #HT2 #IHT destruct -T >(tps_inv_sort1 … HT2) -HT2 // ] -qed. +qed-. lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫* U2 → ∃∃V2,T2. L ⊢ V1 [d, e] ≫* V2 & @@ -117,7 +117,7 @@ lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫* U2 elim (tps_inv_bind1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H lapply (tpss_lsubs_conf … HT1 (L. 𝕓{I} V2) ?) -HT1 /3 width=5/ ] -qed. +qed-. lemma tpss_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕗{I} V1. T1 [d, e] ≫* U2 → ∃∃V2,T2. L ⊢ V1 [d, e] ≫* V2 & L ⊢ T1 [d, e] ≫* T2 & @@ -127,11 +127,11 @@ lemma tpss_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕗{I} V1. T1 [d, e] ≫* U2 | #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct -U; elim (tps_inv_flat1 … HU2) -HU2 /3 width=5/ ] -qed. +qed-. lemma tpss_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ≫* T2 → T1 = T2. #L #T1 #T2 #d #H @(tpss_ind … H) -H T2 [ // | #T #T2 #_ #HT2 #IHT <(tps_inv_refl_O2 … HT2) -HT2 // ] -qed. +qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma index 244ad9e9e..2ba57a9c5 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma @@ -54,7 +54,7 @@ lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ 𝕒{I} [d, e] ≫* T2 → @or_intror @(ex6_4_intro … Hdi Hide HLK … HVT2 HI) /2/ (**) (* /4 width=10/ is too slow *) ] ] -qed. +qed-. lemma tpss_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ≫* T2 → T2 = #i ∨ @@ -65,13 +65,13 @@ lemma tpss_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ≫* T2 → #L #T2 #i #d #e #H elim (tpss_inv_atom1 … H) -H /2/ * #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct -i /3 width=6/ -qed. +qed-. lemma tpss_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫* T2 → ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2. #L #T1 #T2 #d #H #K #V #HLK @(tpss_ind … H) -H T2 // #T #T2 #_ #HT2 #IHT <(tps_inv_refl_SO2 … HT2 … HLK) // -qed. +qed-. (* Relocation properties ****************************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tsubst.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tsubst.ma new file mode 100644 index 000000000..7d31f3bd9 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tsubst.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tpss.ma". + +(* SUBSTITUTION ON TERMS ****************************************************) + +definition tsubst: nat → nat → lenv → relation term ≝ + λd,e,L,T1,T2. ∃∃T. L ⊢ T1 [d, e] ≫* T & ↑[d, e] T2 ≡ T. + +interpretation "substitution (term)" + 'TSubst L T1 d e T2 = (tsubst d e L T1 T2). diff --git a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma index 187e0f49b..5d043c140 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma @@ -17,13 +17,18 @@ include "Ground_2/star.ma". (* ARITHMETICAL PROPERTIES **************************************************) +lemma false_lt_to_le: ∀x,y. (x < y → False) → y ≤ x. +#x #y #H elim (decidable_lt x y) [2: /2 width=1/ ] +#Hxy elim (H Hxy) +qed-. + axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2). axiom lt_dec: ∀n1,n2. Decidable (n1 < n2). lemma plus_S_eq_O_false: ∀n,m. n + S m = 0 → False. #n #m