From: Ferruccio Guidi Date: Fri, 2 Sep 2011 20:23:07 +0000 (+0000) Subject: - the theory of parallel substitution of local environments (ltps) is ready X-Git-Tag: make_still_working~2322 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cd0870e2572a77bd69bda4b8c403c30b569c58b9;p=helm.git - the theory of parallel substitution of local environments (ltps) is ready - the theory of context-free parallel reduction of local environments (ltpr) is ready - the proof of the substitution lemma for context-free parallel reduction is started ... - some renaming and annotating --- 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 4742d0faa..f308d157b 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/Basic-1.txt +++ b/matita/matita/contribs/lambda-delta/Basic-2/Basic-1.txt @@ -44,22 +44,12 @@ arity/subst0 arity_fsubst0 arity/subst0 arity_subst0 asucc/fwd asucc_gen_sort asucc/fwd asucc_gen_head - -# check ###################################################################### - -clen/getl getl_ctail_clen -clen/getl getl_gen_tail cnt/props cnt_lift -C/props clt_cong -C/props clt_head C/props clt_wf__q_ind C/props clt_wf_ind C/props chead_ctail -C/props clt_thead +C/props clt_thead (ctail) C/props c_tail_ind - -# waiting #################################################################### - csuba/arity csuba_arity csuba/arity csuba_arity_rev csuba/arity arity_appls_appl @@ -99,34 +89,6 @@ csubc/fwd csubc_gen_sort_r csubc/fwd csubc_gen_head_r csubc/getl csubc_getl_conf csubc/props csubc_refl -csubst0/clear csubst0_clear_O -csubst0/clear csubst0_clear_O_back -csubst0/clear csubst0_clear_S -csubst0/clear csubst0_clear_trans -csubst0/drop csubst0_drop_gt -csubst0/drop csubst0_drop_gt_back -csubst0/drop csubst0_drop_lt -csubst0/drop csubst0_drop_eq -csubst0/drop csubst0_drop_eq_back -csubst0/drop csubst0_drop_lt_back -csubst0/fwd csubst0_gen_sort -csubst0/fwd csubst0_gen_head -csubst0/fwd csubst0_gen_S_bind_2 -csubst0/getl csubst0_getl_ge -csubst0/getl csubst0_getl_lt -csubst0/getl csubst0_getl_ge_back -csubst0/getl csubst0_getl_lt_back -csubst0/props csubst0_snd_bind -csubst0/props csubst0_fst_bind -csubst0/props csubst0_both_bind -csubst1/fwd csubst1_gen_head -csubst1/getl csubst1_getl_ge -csubst1/getl csubst1_getl_lt -csubst1/getl csubst1_getl_ge_back -csubst1/getl getl_csubst1 -csubst1/props csubst1_head -csubst1/props csubst1_bind -csubst1/props csubst1_flat csubt/clear csubt_clear_conf csubt/csuba csubt_csuba csubt/drop csubt_drop_flat @@ -156,9 +118,7 @@ drop1/getl drop1_getl_trans drop1/props drop1_skip_bind drop1/props drop1_cons_tail drop1/props drop1_trans - drop/props drop_ctail - ex0/props aplus_gz_le ex0/props aplus_gz_ge ex0/props next_plus_gz @@ -169,55 +129,7 @@ ex1/props ex1_arity ex1/props ex1_ty3 ex2/props ex2_nf2 ex2/props ex2_arity - -# check ###################################################################### - -flt/props flt_thead_sx -flt/props flt_thead_dx -flt/props flt_shift -flt/props flt_arith0 -flt/props flt_arith1 -flt/props flt_arith2 -flt/props flt_trans -flt/props flt_wf__q_ind -flt/props flt_wf_ind fsubst0/fwd fsubst0_gen_base -getl/clear clear_getl_trans -getl/clear getl_clear_trans -getl/clear getl_clear_bind -getl/clear getl_clear_conf -getl/dec getl_dec -getl/drop getl_drop -getl/drop getl_drop_conf_lt -getl/drop getl_drop_conf_ge -getl/drop getl_conf_ge_drop -getl/drop getl_drop_conf_rev -getl/drop drop_getl_trans_lt -getl/drop drop_getl_trans_le -getl/drop drop_getl_trans_ge -getl/drop getl_drop_trans -getl/flt getl_flt -getl/fwd getl_gen_all -getl/fwd getl_gen_sort -getl/fwd getl_gen_O -getl/fwd getl_gen_S -getl/fwd getl_gen_2 -getl/fwd getl_gen_flat -getl/fwd getl_gen_bind -getl/getl getl_conf_le -getl/getl getl_trans -getl/props getl_refl -getl/props getl_head -getl/props getl_flat -getl/props getl_ctail -getl/props getl_mono -iso/fwd iso_gen_sort -iso/fwd iso_gen_lref -iso/fwd iso_gen_head -iso/fwd iso_flats_lref_bind_false -iso/fwd iso_flats_flat_bind_false -iso/props iso_refl -iso/props iso_trans leq/asucc asucc_repl leq/asucc asucc_inj leq/asucc leq_asucc @@ -246,34 +158,9 @@ lift1/props lift1_lift1 lift1/props lift1_xhg lift1/props lifts1_xhg lift1/props lift1_free -lift/fwd lift_sort -lift/fwd lift_lref_lt -lift/fwd lift_lref_ge -lift/fwd lift_head -lift/fwd lift_bind -lift/fwd lift_flat -lift/fwd lift_gen_sort -lift/fwd lift_gen_lref -lift/fwd lift_gen_lref_lt -lift/fwd lift_gen_lref_false -lift/fwd lift_gen_lref_ge -lift/fwd lift_gen_head -lift/fwd lift_gen_bind -lift/fwd lift_gen_flat lift/props thead_x_lift_y_y -lift/props lift_r -lift/props lift_lref_gt lift/props lifts_tapp -lift/props lift_inj -lift/props lift_gen_lift lift/props lifts_inj -lift/props lift_free -lift/props lift_d -lift/tlt lift_weight_map -lift/tlt lift_weight -lift/tlt lift_weight_add -lift/tlt lift_weight_add_O -lift/tlt lift_tlt_dx llt/props lweight_repl llt/props llt_repl llt/props llt_trans @@ -366,31 +253,6 @@ pc3/wcpr0 pc3_wcpr0__pc3_wcpr0_t_aux pc3/wcpr0 pc3_wcpr0_t pc3/wcpr0 pc3_wcpr0 pr0/dec nf0_dec -pr0/fwd pr0_gen_sort -pr0/fwd pr0_gen_lref -pr0/fwd pr0_gen_abst -pr0/fwd pr0_gen_appl -pr0/fwd pr0_gen_cast -pr0/fwd pr0_gen_abbr -pr0/fwd pr0_gen_void -pr0/fwd pr0_gen_lift -pr0/pr0 pr0_confluence__pr0_cong_upsilon_refl -pr0/pr0 pr0_confluence__pr0_cong_upsilon_cong -pr0/pr0 pr0_confluence__pr0_cong_upsilon_delta -pr0/pr0 pr0_confluence__pr0_cong_upsilon_zeta -pr0/pr0 pr0_confluence__pr0_cong_delta -pr0/pr0 pr0_confluence__pr0_upsilon_upsilon -pr0/pr0 pr0_confluence__pr0_delta_delta -pr0/pr0 pr0_confluence__pr0_delta_tau -pr0/pr0 pr0_confluence -pr0/props pr0_lift -pr0/props pr0_subst0_back -pr0/props pr0_subst0_fwd -pr0/props pr0_subst0 -pr0/subst1 pr0_delta1 -pr0/subst1 pr0_subst1_back -pr0/subst1 pr0_subst1_fwd -pr0/subst1 pr0_subst1 pr1/pr1 pr1_strip pr1/pr1 pr1_confluence pr1/props pr1_pr0 @@ -400,6 +262,9 @@ pr1/props pr1_head_2 pr1/props pr1_comp pr1/props pr1_eta pr2/clen pr2_gen_ctail + +# check ###################################################################### + pr2/clen pr2_gen_cbind pr2/clen pr2_gen_cflat pr2/fwd pr2_gen_sort @@ -528,43 +393,16 @@ sty1/props sty1_abbr sty1/props sty1_cast2 subst0/dec dnf_dec2 subst0/dec dnf_dec -subst0/fwd subst0_gen_sort -subst0/fwd subst0_gen_lref -subst0/fwd subst0_gen_head -subst0/fwd subst0_gen_lift_lt -subst0/fwd subst0_gen_lift_false -subst0/fwd subst0_gen_lift_ge -subst0/props subst0_refl -subst0/props subst0_lift_lt -subst0/props subst0_lift_ge -subst0/props subst0_lift_ge_S -subst0/props subst0_lift_ge_s -subst0/subst0 subst0_subst0 -subst0/subst0 subst0_subst0_back -subst0/subst0 subst0_trans -subst0/subst0 subst0_confluence_neq -subst0/subst0 subst0_confluence_eq -subst0/subst0 subst0_confluence_lift -subst0/tlt subst0_weight_le -subst0/tlt subst0_weight_lt -subst0/tlt subst0_tlt_head -subst0/tlt subst0_tlt -subst1/fwd subst1_gen_sort -subst1/fwd subst1_gen_lref -subst1/fwd subst1_gen_head +subst1/fwd subst1_gen_lift_ge subst1/fwd subst1_gen_lift_lt subst1/fwd subst1_gen_lift_eq -subst1/fwd subst1_gen_lift_ge -subst1/props subst1_head -subst1/props subst1_lift_lt subst1/props subst1_lift_ge +subst1/props subst1_lift_lt subst1/props subst1_ex subst1/props subst1_lift_S subst1/subst1 subst1_subst1 subst1/subst1 subst1_subst1_back subst1/subst1 subst1_trans -subst1/subst1 subst1_confluence_neq -subst1/subst1 subst1_confluence_eq subst1/subst1 subst1_confluence_lift subst/fwd subst_sort subst/fwd subst_lref_lt @@ -585,18 +423,6 @@ tlist/props tslt_wf_ind tlist/props theads_tapp tlist/props tcons_tapp_ex tlist/props tlist_ind_rev -tlt/props wadd_le -tlt/props wadd_lt -tlt/props wadd_O -tlt/props weight_le -tlt/props weight_eq -tlt/props weight_add_O -tlt/props weight_add_S -tlt/props tlt_trans -tlt/props tlt_head_sx -tlt/props tlt_head_dx -tlt/props tlt_wf__q_ind -tlt/props tlt_wf_ind T/props not_abbr_abst T/props not_void_abst T/props not_abbr_void @@ -650,12 +476,6 @@ ty3/props ty3_getl_subst0 ty3/sty0 ty3_sty0 ty3/subst1 ty3_gen_cabbr ty3/subst1 ty3_gen_cvoid -wcpr0/fwd wcpr0_gen_sort -wcpr0/fwd wcpr0_gen_head -wcpr0/getl wcpr0_drop -wcpr0/getl wcpr0_drop_back -wcpr0/getl wcpr0_getl -wcpr0/getl wcpr0_getl_back 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/grammar/cl_shift.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/cl_shift.ma index 50898bbef..d72b6c4cb 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/cl_shift.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/cl_shift.ma @@ -17,7 +17,7 @@ include "Basic-2/grammar/lenv.ma". (* SHIFT OF A CLOSURE *******************************************************) let rec shift L T on L ≝ match L with -[ LSort ⇒ T +[ LAtom ⇒ T | LPair L I V ⇒ shift L (𝕓{I} V. T) ]. 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 899da0720..35bf32a9d 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 @@ -23,10 +23,14 @@ interpretation "weight (closure)" 'Weight L T = (cw L T). (* Basic properties *********************************************************) +(* Basic-1: was: flt_wf__q_ind *) + +(* Basic-1: was: flt_wf_ind *) axiom cw_wf_ind: ∀R:lenv→term→Prop. (∀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: ∀K,I,V,T. #[K. 𝕓{I} V, T] < #[K, 𝕔{I} V. T]. normalize // qed. @@ -36,3 +40,7 @@ lemma tw_shift: ∀L,T. #[L, T] ≤ #[L @ T]. #K #I #V #IHL #T @transitive_le [3: @IHL |2: /2/ | skip ] qed. + +(* Basic-1: removed theorems 6: + flt_thead_sx flt_thead_dx flt_arith0 flt_arith1 flt_arith2 flt_trans +*) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv.ma index ad903c9d1..dfec09808 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv.ma @@ -18,10 +18,10 @@ include "Basic-2/grammar/term.ma". (* local environments *) inductive lenv: Type[0] ≝ -| LSort: lenv (* empty *) +| LAtom: lenv (* empty *) | LPair: lenv → bind2 → term → lenv (* binary binding construction *) . -interpretation "sort (local environment)" 'Star = LSort. +interpretation "sort (local environment)" 'Star = LAtom. interpretation "environment binding construction (binary)" 'DBind L I T = (LPair L I T). diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv_length.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv_length.ma index 2321e7b0d..23e445907 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv_length.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/lenv_length.ma @@ -17,7 +17,7 @@ include "Basic-2/grammar/lenv.ma". (* LENGTH OF A LOCAL ENVIRONMENT ********************************************) let rec length L ≝ match L with -[ LSort ⇒ 0 +[ LAtom ⇒ 0 | LPair L _ _ ⇒ length L + 1 ]. 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 950d70c4a..9f45673ba 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 @@ -18,8 +18,10 @@ include "Basic-2/grammar/lenv.ma". (* WEIGHT OF A LOCAL ENVIRONMENT ********************************************) let rec lw L ≝ match L with -[ LSort ⇒ 0 +[ LAtom ⇒ 0 | LPair L _ V ⇒ lw L + #[V] ]. interpretation "weight (local environment)" 'Weight L = (lw L). + +(* Basic-1: removed theorems 2: clt_cong clt_head *) 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 a960e48d1..443cc2abc 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 @@ -28,3 +28,9 @@ interpretation "weight (term)" 'Weight T = (tw T). axiom tw_wf_ind: ∀R:term→Prop. (∀T2. (∀T1. #[T1] < #[T2] → R T1) → R T2) → ∀T. R T. + +(* Basic-1: removed theorems 11: + wadd_le wadd_lt wadd_O weight_le weight_eq weight_add_O + weight_add_S tlt_trans tlt_head_sx tlt_head_dx tlt_wf_ind + removed local theorems 1: q_ind +*) 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 34af6f9f4..876bd7fd9 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/thom.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/thom.ma @@ -48,3 +48,9 @@ lemma simple_thom_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝕊[T2] → 𝕊[T1]. /3/ qed. (* Basic inversion lemmas ***************************************************) + + +(* Basic-1: removed theorems 7: + iso_gen_sort iso_gen_lref iso_gen_head iso_refl iso_trans + iso_flats_lref_bind_false iso_flats_flat_bind_false +*) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/notation.ma b/matita/matita/contribs/lambda-delta/Basic-2/notation.ma index 8f068effd..287ce0564 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/notation.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/notation.ma @@ -78,6 +78,10 @@ notation "hvbox( ↓ [ d , break e ] break L1 ≡ break L2 )" non associative with precedence 45 for @{ 'RDrop $L1 $d $e $L2 }. +notation "hvbox( T1 break [ d , break e ] ≫ break T2 )" + non associative with precedence 45 + for @{ 'PSubst $T1 $d $e $T2 }. + notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≫ break T2 )" non associative with precedence 45 for @{ 'PSubst $L $T1 $d $e $T2 }. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma index de7daa04b..fb79bdebc 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma @@ -67,7 +67,7 @@ qed. lemma cpr_inv_lsort: ∀T1,T2. ⋆ ⊢ T1 ⇒ T2 → T1 ⇒ T2. #T1 #T2 * #T #HT normalize #HT2 -<(tps_inv_refl0 … HT2) -HT2 // +<(tps_inv_refl_O2 … HT2) -HT2 // qed. (* Basic forward lemmas *****************************************************) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/ltpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/ltpr.ma index 902bc96da..97ef4901a 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/ltpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/ltpr.ma @@ -26,9 +26,26 @@ interpretation "context-free parallel reduction (environment)" 'PRed L1 L2 = (ltpr L1 L2). +(* Basic properties *********************************************************) + +lemma ltpr_refl: ∀L:lenv. L ⇒ L. +#L elim L -L /2/ +qed. + (* Basic inversion lemmas ***************************************************) -fact ltpr_inv_item1_aux: ∀L1,L2. L1 ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 → +fact ltpr_inv_atom1_aux: ∀L1,L2. L1 ⇒ L2 → L1 = ⋆ → L2 = ⋆. +#L1 #L2 * -L1 L2 +[ // +| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct +] +qed. + +(* Basic-1: was: wcpr0_gen_sort *) +lemma ltpr_inv_atom1: ∀L2. ⋆ ⇒ L2 → L2 = ⋆. +/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. #L1 #L2 * -L1 L2 [ #K1 #I #V1 #H destruct @@ -36,6 +53,31 @@ fact ltpr_inv_item1_aux: ∀L1,L2. L1 ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 ] qed. -lemma ltpr_inv_item1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ⇒ L2 → +(* 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. + +fact ltpr_inv_atom2_aux: ∀L1,L2. L1 ⇒ L2 → L2 = ⋆ → L1 = ⋆. +#L1 #L2 * -L1 L2 +[ // +| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct +] +qed. + +lemma ltpr_inv_atom2: ∀L1. L1 ⇒ ⋆ → L1 = ⋆. +/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. +#L1 #L2 * -L1 L2 +[ #K2 #I #V2 #H destruct +| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #K #J #W #H destruct -K2 I V2 /2 width=5/ +] +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. + +(* Basic-1: removed theorems 2: wcpr0_getl wcpr0_getl_back *) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/ltpr_drop.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/ltpr_drop.ma new file mode 100644 index 000000000..99c0ae0d4 --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/ltpr_drop.ma @@ -0,0 +1,54 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reduction/tpr_lift.ma". +include "Basic-2/reduction/ltpr.ma". + +(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) + +(* Basic-1: was: wcpr0_drop *) +lemma ltpr_drop_conf: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀L2. L1 ⇒ L2 → + ∃∃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/ +| #L1 #K1 #I #V1 #HLK1 #_ #X #H + <(drop_inv_refl … HLK1) -HLK1 K1; + elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/ +| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H + elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct -X; + elim (IHLK1 … HL12) -IHLK1 HL12 /3/ +| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H + elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct -X; + elim (tpr_inv_lift … HV12 … HWV1) -HV12 HWV1; + elim (IHLK1 … HL12) -IHLK1 HL12 /3 width=5/ +] +qed. + +(* Basic-1: was: wcpr0_drop_back *) +lemma ltpr_drop_trans: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀K2. K1 ⇒ K2 → + ∃∃L2. ↓[d, e] L2 ≡ K2 & L1 ⇒ L2. +#L1 #K1 #d #e #H elim H -H L1 K1 d e +[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/ +| #L1 #K1 #I #V1 #HLK1 #_ #X #H + >(drop_inv_refl … HLK1) -HLK1 L1; + elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/ +| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12 + elim (IHLK1 … HK12) -IHLK1 HK12 /3 width=5/ +| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H + elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct -X; + elim (lift_total W2 d e) #V2 #HWV2 + lapply (tpr_lift … HW12 … HWV1 … HWV2) -HW12 HWV1; + elim (IHLK1 … HK12) -IHLK1 HK12 /3 width=5/ +] +qed. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma index 3d441c931..fdfc4f08b 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma @@ -185,3 +185,30 @@ lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i → T1 = 𝕔{Abbr} V. T | ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T. /2/ qed. +(* +pr0/fwd pr0_gen_sort +pr0/fwd pr0_gen_lref +pr0/fwd pr0_gen_abst +pr0/fwd pr0_gen_appl +pr0/fwd pr0_gen_cast +pr0/fwd pr0_gen_abbr +pr0/fwd pr0_gen_void +pr0/fwd pr0_gen_lift +pr0/pr0 pr0_confluence__pr0_cong_upsilon_refl +pr0/pr0 pr0_confluence__pr0_cong_upsilon_cong +pr0/pr0 pr0_confluence__pr0_cong_upsilon_delta +pr0/pr0 pr0_confluence__pr0_cong_upsilon_zeta +pr0/pr0 pr0_confluence__pr0_cong_delta +pr0/pr0 pr0_confluence__pr0_upsilon_upsilon +pr0/pr0 pr0_confluence__pr0_delta_delta +pr0/pr0 pr0_confluence__pr0_delta_tau +pr0/pr0 pr0_confluence +pr0/props pr0_lift +pr0/props pr0_subst0_back +pr0/props pr0_subst0_fwd +pr0/props pr0_subst0 +pr0/subst1 pr0_delta1 +pr0/subst1 pr0_subst1_back +pr0/subst1 pr0_subst1_fwd +pr0/subst1 pr0_subst1 +*) \ No newline at end of file diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma index 66e872eae..412a0a2ed 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma @@ -102,7 +102,7 @@ fact tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕔{Abst} V1. T1 | #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct | #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct | #I #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct -I V1 T1; - <(tps_inv_refl1 … HT2 ? ? ?) -HT2 T /2 width=5/ + <(tps_inv_refl_SO2 … HT2 ? ? ?) -HT2 T /2 width=5/ | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct | #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct | #V #T1 #T2 #_ #V0 #T0 #H destruct diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma index 27f09e20a..43c48d0f2 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -include "Basic-2/substitution/tps_tps.ma". -include "Basic-2/reduction/tpr_lift.ma". include "Basic-2/reduction/tpr_tps.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) @@ -128,7 +126,7 @@ elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 elim (IH … HT01 … HT02) -HT01 HT02 IH // #T #HT1 #HT2 elim (tpr_tps_bind … HV1 HT1 … HTT1) -HT1 HTT1 #U1 #TTU1 #HTU1 elim (tpr_tps_bind … HV2 HT2 … HTT2) -HT2 HTT2 #U2 #TTU2 #HTU2 -elim (tps_conf … HTU1 … HTU2) -HTU1 HTU2 #U #HU1 #HU2 +elim (tps_conf_eq … HTU1 … HTU2) -HTU1 HTU2 #U #HU1 #HU2 @ex2_1_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *) qed. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma index 3a00c62c6..af61e0a3f 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma @@ -12,15 +12,51 @@ (* *) (**************************************************************************) -include "Basic-2/reduction/ltpr.ma". +include "Basic-2/substitution/tps_tps.ma". +include "Basic-2/reduction/ltpr_drop.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) -axiom tpr_tps_ltpr: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. T1 ⇒ T2 → - ∀d,e,U1. L1 ⊢ T1 [d, e] ≫ U1 → +axiom tpr_tps_ltpr: ∀T1,T2. T1 ⇒ T2 → + ∀L1,d,e,U1. L1 ⊢ T1 [d, e] ≫ U1 → + ∀L2. L1 ⇒ L2 → ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫ U2. +(* +#T1 #T2 #H elim H -H T1 T2 +[ #I #L1 #d #e #X #H + elim (tps_inv_atom1 … H) -H + [ #H destruct -X /2/ + | * #K1 #V1 #i #Hdi #Hide #HLK1 #HVU1 #H #L2 #HL12 destruct -I; + elim (ltpr_drop_conf … HLK1 … HL12) -HLK1 HL12 #X #HLK2 #H + elim (ltpr_inv_pair1 … H) -H #K2 #V2 #_ #HV12 #H destruct -X; + elim (lift_total V2 0 (i+1)) #U2 #HVU2 + lapply (tpr_lift … HV12 … HVU1 … HVU2) -HV12 HVU1 #HU12 + @ex2_1_intro [2: @HU12 | skip | /2/ ] (**) (* /3 width=6/ is too slow *) + ] +| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12 + elim (tps_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct -X; + elim (IHV12 … HVW1 … HL12) -IHV12 HVW1; + elim (IHT12 … HTU1 … HL12) -IHT12 HTU1 HL12 /3 width=5/ +| #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12 + elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct -X; + elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct -Y; + elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2 + elim (IHT12 … HTT1 (L2. 𝕓{Abst} W) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2 + lapply (tps_leq_repl … HTT2 (L2. 𝕓{Abbr} V2) ?) -HTT2 /3 width=5/ +| #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12 + elim (tps_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct -X; + elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2 + elim (IHT12 … HTT1 (L2. 𝕓{I} V2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2 +(*lapply (tps_leq_repl … HTT2 (L2. 𝕓{I} VV2) ?) -HTT2 /2/ #HTT2 *) + elim (tps_conf_neq … HTU2 … HTT2 ?) -HTU2 HTT2 T2 /2/ #T2 #HUT2 #HTT2 + @ex2_1_intro + [2: @tpr_delta [4: @HVV12 |5: @HTT12 |1,2: skip |6: ] (*|6: ]1,2: skip ]*) + |1: skip + |3: @tps_bind [@HVV2 | @HUT2 ] + ] +*) lemma tpr_tps_bind: ∀I,V1,V2,T1,T2,U1. V1 ⇒ V2 → T1 ⇒ T2 → ⋆. 𝕓{I} V1 ⊢ T1 [0, 1] ≫ U1 → ∃∃U2. U1 ⇒ U2 & ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ U2. -/3 width=5/ qed. +/3 width=7/ qed. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma index 65aaf3d4e..b7d8801b2 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma @@ -203,11 +203,17 @@ lemma drop_fwd_O1_length: ∀L1,L2,e. ↓[0, e] L1 ≡ L2 → |L2| = |L1| - e. ] qed. -(* Basic-1: removed theorems 18: +(* Basic-1: removed theorems 49: drop_skip_flat cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf drop_clear drop_clear_O drop_clear_S clear_gen_sort clear_gen_bind clear_gen_flat clear_gen_flat_r - clear_gen_all clear_clear clear_mono clear_trans clear_ctail - clear_cle + clear_gen_all clear_clear clear_mono clear_trans clear_ctail clear_cle + getl_ctail_clen getl_gen_tail clear_getl_trans getl_clear_trans + getl_clear_bind getl_clear_conf getl_dec getl_drop getl_drop_conf_lt + getl_drop_conf_ge getl_conf_ge_drop getl_drop_conf_rev + drop_getl_trans_lt drop_getl_trans_le drop_getl_trans_ge + getl_drop_trans getl_flt getl_gen_all getl_gen_sort getl_gen_O + getl_gen_S getl_gen_2 getl_gen_flat getl_gen_bind getl_conf_le + getl_trans getl_refl getl_head getl_flat getl_ctail getl_mono *) 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 0a4e1715a..48e37d630 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma @@ -16,6 +16,9 @@ include "Basic-2/grammar/term_weight.ma". (* RELOCATION ***************************************************************) +(* Basic-1: includes: + lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat +*) inductive lift: term → nat → nat → term → Prop ≝ | lift_sort : ∀k,d,e. lift (⋆k) d e (⋆k) | lift_lref_lt: ∀i,d,e. i < d → lift (#i) d e (#i) @@ -32,10 +35,12 @@ interpretation "relocation" 'RLift T1 d e T2 = (lift T1 d e 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/ @@ -54,6 +59,7 @@ lemma lift_total: ∀T1,d,e. ∃T2. ↑[d,e] T1 ≡ T2. ] 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. @@ -170,6 +176,7 @@ fact lift_inv_sort2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k ] 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. @@ -184,16 +191,21 @@ fact lift_inv_lref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T2 = #i → ] 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. +(* 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. +(* Basic-1: was: lift_gen_lref_false *) + +(* 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 @@ -213,6 +225,7 @@ fact lift_inv_bind2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ] qed. +(* Basic-1: was: lift_gen_bind *) 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. @@ -231,7 +244,14 @@ fact lift_inv_flat2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ] qed. +(* Basic-1: was: lift_gen_flat *) 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. + +(* Basic-1: removed theorems 7: + lift_head lift_gen_head + lift_weight_map lift_weight lift_weight_add lift_weight_add_O + lift_tlt_dx +*) 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 ba69f0f71..f9c99457d 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 @@ -18,6 +18,7 @@ include "Basic-2/substitution/lift.ma". (* Main properies ***********************************************************) +(* Basic-1: was: lift_inj *) theorem lift_inj: ∀d,e,T1,U. ↑[d,e] T1 ≡ U → ∀T2. ↑[d,e] T2 ≡ U → T1 = T2. #d #e #T1 #U #H elim H -H d e T1 U [ #k #d #e #X #HX @@ -33,6 +34,7 @@ theorem lift_inj: ∀d,e,T1,U. ↑[d,e] T1 ≡ U → ∀T2. ↑[d,e] T2 ≡ U ] qed. +(* Basic-1: was: lift_gen_lift *) theorem lift_div_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → ∀d2,e2,T2. ↑[d2 + e1, e2] T2 ≡ T → d1 ≤ d2 → @@ -78,6 +80,7 @@ theorem lift_mono: ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 ] qed. +(* Basic-1: was: lift_free (left to right) *) theorem lift_trans_be: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → d1 ≤ d2 → d2 ≤ d1 + e1 → ↑[d1, e1 + e2] T1 ≡ T2. @@ -103,6 +106,7 @@ theorem lift_trans_be: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → ] qed. +(* Basic-1: was: lift_d (right to left) *) theorem lift_trans_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → d2 ≤ d1 → ∃∃T0. ↑[d2, e2] T1 ≡ T0 & ↑[d1 + e2, e1] T0 ≡ T2. @@ -127,6 +131,7 @@ theorem lift_trans_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → ] qed. +(* Basic-1: was: lift_d (left to right) *) theorem lift_trans_ge: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → d1 + e1 ≤ d2 → ∃∃T0. ↑[d2 - e1, e2] T1 ≡ T0 & ↑[d1, e1] T0 ≡ T2. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps.ma new file mode 100644 index 000000000..fc94df3ec --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps.ma @@ -0,0 +1,182 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Basic-2/substitution/tps.ma". + +(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************) + +(* Basic-1: includes: csubst1_bind *) +inductive ltps: lenv → nat → nat → lenv → Prop ≝ +| ltps_atom: ∀d,e. ltps (⋆) d e (⋆) +| ltps_pair: ∀L,I,V. ltps (L. 𝕓{I} V) 0 0 (L. 𝕓{I} V) +| ltps_tps2: ∀L1,L2,I,V1,V2,e. + ltps L1 0 e L2 → L2 ⊢ V1 [0, e] ≫ V2 → + ltps (L1. 𝕓{I} V1) 0 (e + 1) L2. 𝕓{I} V2 +| ltps_tps1: ∀L1,L2,I,V1,V2,d,e. + ltps L1 d e L2 → L2 ⊢ V1 [d, e] ≫ V2 → + ltps (L1. 𝕓{I} V1) (d + 1) e (L2. 𝕓{I} V2) +. + +interpretation "parallel substritution (local environment)" + 'PSubst L1 d e L2 = (ltps L1 d e L2). + +(* Basic properties *********************************************************) + +lemma ltps_tps2_lt: ∀L1,L2,I,V1,V2,e. + L1 [0, e - 1] ≫ L2 → L2 ⊢ V1 [0, e - 1] ≫ V2 → + 0 < e → L1. 𝕓{I} V1 [0, e] ≫ L2. 𝕓{I} V2. +#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He +>(plus_minus_m_m e 1) /2/ +qed. + +lemma ltps_tps1_lt: ∀L1,L2,I,V1,V2,d,e. + L1 [d - 1, e] ≫ L2 → L2 ⊢ V1 [d - 1, e] ≫ V2 → + 0 < d → L1. 𝕓{I} V1 [d, e] ≫ L2. 𝕓{I} V2. +#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd +>(plus_minus_m_m d 1) /2/ +qed. + +(* Basic-1: was by definition: csubst1_refl *) +lemma ltps_refl: ∀L,d,e. L [d, e] ≫ L. +#L elim L -L // +#L #I #V #IHL * /2/ * /2/ +qed. + +(* Basic inversion lemmas ***************************************************) + +fact ltps_inv_refl_O2_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → e = 0 → L1 = L2. +#d #e #L1 #L2 #H elim H -H d e L1 L2 // +[ #L1 #L2 #I #V1 #V2 #e #_ #_ #_ #H + elim (plus_S_eq_O_false … H) +| #L1 #L2 #I #V1 #V2 #d #e #_ #HV12 #IHL12 #He destruct -e + >(IHL12 ?) -IHL12 // >(tps_inv_refl_O2 … HV12) // +] +qed. + +lemma ltps_inv_refl_O2: ∀d,L1,L2. L1 [d, 0] ≫ L2 → L1 = L2. +/2/ qed. + +fact ltps_inv_atom1_aux: ∀d,e,L1,L2. + L1 [d, e] ≫ L2 → L1 = ⋆ → L2 = ⋆. +#d #e #L1 #L2 * -d e L1 L2 +[ // +| #L #I #V #H destruct +| #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct +| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct +] +qed. + +lemma drop_inv_atom1: ∀d,e,L2. ⋆ [d, e] ≫ L2 → L2 = ⋆. +/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 → + ∃∃K2,V2. K1 [0, e - 1] ≫ K2 & + K2 ⊢ V1 [0, e - 1] ≫ V2 & + L2 = K2. 𝕓{I} V2. +#d #e #L1 #L2 * -d e L1 L2 +[ #d #e #_ #_ #K1 #I #V1 #H destruct +| #L1 #I #V #_ #H elim (lt_refl_false … H) +| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K1 #J #W1 #H destruct -L1 I V1 /2 width=5/ +| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H) +] +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. + +fact ltps_inv_tps11_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → 0 < d → + ∀I,K1,V1. L1 = K1. 𝕓{I} V1 → + ∃∃K2,V2. K1 [d - 1, e] ≫ K2 & + K2 ⊢ V1 [d - 1, e] ≫ V2 & + L2 = K2. 𝕓{I} V2. +#d #e #L1 #L2 * -d e L1 L2 +[ #d #e #_ #I #K1 #V1 #H destruct +| #L #I #V #H elim (lt_refl_false … H) +| #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H) +| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K1 #W1 #H destruct -L1 I V1 + /2 width=5/ +] +qed. + +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. + +fact ltps_inv_atom2_aux: ∀d,e,L1,L2. + L1 [d, e] ≫ L2 → L2 = ⋆ → L1 = ⋆. +#d #e #L1 #L2 * -d e L1 L2 +[ // +| #L #I #V #H destruct +| #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct +| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct +] +qed. + +lemma drop_inv_atom2: ∀d,e,L1. L1 [d, e] ≫ ⋆ → L1 = ⋆. +/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 → + ∃∃K1,V1. K1 [0, e - 1] ≫ K2 & + K2 ⊢ V1 [0, e - 1] ≫ V2 & + L1 = K1. 𝕓{I} V1. +#d #e #L1 #L2 * -d e L1 L2 +[ #d #e #_ #_ #K1 #I #V1 #H destruct +| #L1 #I #V #_ #H elim (lt_refl_false … H) +| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K2 #J #W2 #H destruct -L2 I V2 /2 width=5/ +| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H) +] +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. + +fact ltps_inv_tps12_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → 0 < d → + ∀I,K2,V2. L2 = K2. 𝕓{I} V2 → + ∃∃K1,V1. K1 [d - 1, e] ≫ K2 & + K2 ⊢ V1 [d - 1, e] ≫ V2 & + L1 = K1. 𝕓{I} V1. +#d #e #L1 #L2 * -d e L1 L2 +[ #d #e #_ #I #K2 #V2 #H destruct +| #L #I #V #H elim (lt_refl_false … H) +| #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H) +| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K2 #W2 #H destruct -L2 I V2 + /2 width=5/ +] +qed. + +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. + +(* Basic-1: removed theorems 27: + 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 + csubst0_gen_sort csubst0_gen_head csubst0_getl_ge csubst0_getl_lt + csubst0_gen_S_bind_2 csubst0_getl_ge_back csubst0_getl_lt_back + 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 + +*) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_drop.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_drop.ma new file mode 100644 index 000000000..07b8cfdc2 --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_drop.ma @@ -0,0 +1,131 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Basic-2/substitution/ltps.ma". + +(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************) + +lemma ltps_drop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → + ∀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 >(drop_inv_sort1 … H) -H // +| // +| normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12 + lapply (plus_le_weak … He12) #He2 + lapply (drop_inv_drop1 … H ?) -H // #HK0L2 + lapply (IHK01 … HK0L2 ?) -IHK01 HK0L2 /2/ +| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 + lapply (plus_le_weak … Hd1e2) #He2 + lapply (drop_inv_drop1 … H ?) -H // #HK0L2 + lapply (IHK01 … HK0L2 ?) -IHK01 HK0L2 /2/ +] +qed. + +lemma ltps_drop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → + ∀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 >(drop_inv_sort1 … H) -H // +| // +| normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12 + lapply (plus_le_weak … He12) #He2 + lapply (drop_inv_drop1 … H ?) -H // #HK0L2 + lapply (IHK10 … HK0L2 ?) -IHK10 HK0L2 /2/ +| #K0 #K1 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 + lapply (plus_le_weak … Hd1e2) #He2 + lapply (drop_inv_drop1 … H ?) -H // #HK0L2 + lapply (IHK10 … HK0L2 ?) -IHK10 HK0L2 /2/ +] +qed. + +lemma ltps_drop_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. +#L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1 +[ #d1 #e1 #L2 #e2 #H >(drop_inv_sort1 … H) -H /2/ +| normalize #L #I #V #L2 #e2 #HL2 #_ #He2 + lapply (le_n_O_to_eq … He2) -He2 #H destruct -e2; + lapply (drop_inv_refl … HL2) -HL2 #H destruct -L2 /2/ +| normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #_ #He21 + lapply (drop_inv_O1 … H) -H * * #He2 #HK0L2 + [ destruct -IHK01 He21 e2 L2 plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 #He2de1 + lapply (plus_le_weak … Hd1e2) #He2 + (drop_inv_sort1 … H) -H /2/ +| normalize #L #I #V #L2 #e2 #HL2 #_ #He2 + lapply (le_n_O_to_eq … He2) -He2 #H destruct -e2; + lapply (drop_inv_refl … HL2) -HL2 #H destruct -L2 /2/ +| normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #_ #He21 + lapply (drop_inv_O1 … H) -H * * #He2 #HK0L2 + [ destruct -IHK10 He21 e2 L2 plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 #He2de1 + lapply (plus_le_weak … Hd1e2) #He2 + (drop_inv_sort1 … H) -H /2/ +| /2/ +| normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #_ #L2 #e2 #H #He2 + lapply (le_n_O_to_eq … He2) -He2 #He2 destruct -e2; + lapply (drop_inv_refl … H) -H #H destruct -L2 /3/ +| #K0 #K1 #I #V0 #V1 #d1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #He2d1 + lapply (drop_inv_O1 … H) -H * * #He2 #HK0L2 + [ destruct -IHK01 He2d1 e2 L2 (drop_inv_sort1 … H) -H /2/ +| /2/ +| normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #_ #L2 #e2 #H #He2 + lapply (le_n_O_to_eq … He2) -He2 #He2 destruct -e2; + lapply (drop_inv_refl … H) -H #H destruct -L2 /3/ +| #K1 #K0 #I #V1 #V0 #d1 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #He2d1 + lapply (drop_inv_O1 … H) -H * * #He2 #HK0L2 + [ destruct -IHK10 He2d1 e2 L2 (lift_mono … HVT1 … HVT2) -HVT1 /2/ + | -Hd1 Hde1 * #K2 #V2 #_ #_ #HLK2 #HVT2 + lapply (drop_mono … HLK1 … HLK2) -HLK1 HLK2 #H destruct -V1 K1 + >(lift_mono … HVT1 … HVT2) -HVT1 HVT2 /2/ ] -| #L #I #V0 #V1 #T0 #T1 #d #e #_ #_ #IHV01 #IHT01 #X #HX +| #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X; elim (IHV01 … HV02) -IHV01 HV02 #V #HV1 #HV2 elim (IHT01 … HT02) -IHT01 HT02 #T #HT1 #HT2 - @ex2_1_intro - [2: @tps_bind [4: @(tps_leq_repl … HT1) /2/ |2: skip ] - |1: skip - |3: @tps_bind [2: @(tps_leq_repl … HT2) /2/ ] - ] // (**) (* /5/ is too slow *) -| #L #I #V0 #V1 #T0 #T1 #d #e #_ #_ #IHV01 #IHT01 #X #HX + lapply (tps_leq_repl … HT1 (L. 𝕓{I} V1) ?) -HT1 /2/ + lapply (tps_leq_repl … HT2 (L. 𝕓{I} V2) ?) -HT2 /3 width=5/ +| #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X; elim (IHV01 … HV02) -IHV01 HV02; elim (IHT01 … HT02) -IHT01 HT02 /3 width=5/ ] qed. +(* Basic-1: was: subst1_confluence_neq *) +theorem tps_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 [d1, e1] ≫ T1 → + ∀L2,T2,d2,e2. L2 ⊢ T0 [d2, e2] ≫ T2 → + (d1 + e1 ≤ d2 ∨ d2 + e2 ≤ d1) → + ∃∃T. L2 ⊢ T1 [d2, e2] ≫ T & L1 ⊢ T2 [d1, e1] ≫ T. +#L1 #T0 #T1 #d1 #e1 #H elim H -H L1 T0 T1 d1 e1 +[ /2/ +| #L1 #K1 #V1 #T1 #i0 #d1 #e1 #Hd1 #Hde1 #HLK1 #HVT1 #L2 #T2 #d2 #e2 #H1 #H2 + elim (tps_inv_lref1 … H1) -H1 + [ #H destruct -T2 /4/ + | -HLK1 HVT1 * #K2 #V2 #Hd2 #Hde2 #_ #_ elim H2 -H2 #Hded + [ -Hd1 Hde2; + lapply (transitive_le … Hded Hd2) -Hded Hd2 #H + lapply (lt_to_le_to_lt … Hde1 H) -Hde1 H #H + elim (lt_refl_false … H) + | -Hd2 Hde1; + lapply (transitive_le … Hded Hd1) -Hded Hd1 #H + lapply (lt_to_le_to_lt … Hde2 H) -Hde2 H #H + elim (lt_refl_false … H) + ] + ] +| #L1 #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #L2 #X #d2 #e2 #HX #H + elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X; + elim (IHV01 … HV02 H) -IHV01 HV02 #V #HV1 #HV2 + elim (IHT01 … HT02 ?) -IHT01 HT02 + [ -H #T #HT1 #HT2 + lapply (tps_leq_repl … HT1 (L2. 𝕓{I} V1) ?) -HT1 /2/ + lapply (tps_leq_repl … HT2 (L1. 𝕓{I} V2) ?) -HT2 /3 width=5/ + | -HV1 HV2 >plus_plus_comm_23 >plus_plus_comm_23 in ⊢ (? ? %) elim H -H #H + [ @or_introl | @or_intror ] /2 by monotonic_le_plus_l/ (**) (* /3/ is too slow *) + ] +| #L1 #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #L2 #X #d2 #e2 #HX #H + elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X; + elim (IHV01 … HV02 H) -IHV01 HV02; + elim (IHT01 … HT02 H) -IHT01 HT02 H /3 width=5/ +] +qed. + theorem tps_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 [d1, e1] ≫ T0 → ∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫ T2 → d2 + e2 ≤ d1 → ∃∃T. L ⊢ T1 [d2, e2] ≫ T & L ⊢ T [d1, e1] ≫ T2.