From e0827239f4b44f2af9c7f88c4c7c41f2a193ae37 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 17 Mar 2012 16:51:06 +0000 Subject: [PATCH] - basics: some support for abstract triangular confluence (which subject reduction is an instance of) - predefined_virtuals: more Alt-L shortcuts - lambda_delta: more properties on computation, some annotations, improved Makefile --- matita/matita/contribs/lambda_delta/Makefile | 20 +- .../lambda_delta/basic_2/basic_1.orig | 712 ++++++++++++++++++ .../contribs/lambda_delta/basic_2/basic_1.txt | 41 - .../lambda_delta/basic_2/computation/cpe.ma | 35 + .../basic_2/computation/cpe_cpe.ma | 28 + .../lambda_delta/basic_2/computation/cprs.ma | 5 +- .../basic_2/computation/cprs_cprs.ma | 5 + .../basic_2/computation/cprs_ltpr.ma | 32 + .../lambda_delta/basic_2/computation/csn.ma | 5 +- .../basic_2/computation/csn_cprs.ma | 11 - .../basic_2/computation/csn_lift.ma | 11 + .../lambda_delta/basic_2/grammar/lenv.ma | 2 + .../basic_2/grammar/lenv_weight.ma | 3 +- .../contribs/lambda_delta/basic_2/notation.ma | 8 + .../lambda_delta/basic_2/reducibility/cnf.ma | 1 + .../lambda_delta/basic_2/reducibility/cpr.ma | 3 +- .../basic_2/substitution/ldrop.ma | 4 +- .../basic_2/unfold/lifts_vector.ma | 2 + matita/matita/contribs/lambda_delta/orig.sh | 4 + matita/matita/lib/basics/star.ma | 7 + matita/matita/predefined_virtuals.ml | 1 + 21 files changed, 876 insertions(+), 64 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/basic_1.orig create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/cpe_cpe.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/cprs_ltpr.ma create mode 100644 matita/matita/contribs/lambda_delta/orig.sh diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile index 005b69df7..71dff0f41 100644 --- a/matita/matita/contribs/lambda_delta/Makefile +++ b/matita/matita/contribs/lambda_delta/Makefile @@ -1,9 +1,13 @@ -H = @ -XOA_DIR = ../../../components/binaries/xoa -XOA = xoa.native +H = @ +XOA_DIR = ../../../components/binaries/xoa +XOA = xoa.native -CONF = ground_2/xoa.conf.xml -TARGETS = ground_2/xoa_natation.ma ground_2/xoa.ma +CONF = ground_2/xoa.conf.xml +TARGETS = ground_2/xoa_natation.ma ground_2/xoa.ma + +ORIG = . ./orig.sh + +ORIGS = basic_2/basic_1.orig PACKAGES = ground_2 basic_2 apps_2 @@ -17,6 +21,12 @@ $(TARGETS): $(CONF) @echo " EXEC $(XOA) $(CONF)" $(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) $(CONF) +# orig ####################################################################### + +orig: $(ORIGS) + @echo " ORIG basic_2" + $(H)$(ORIG) basic_2 < $(ORIGS) + # stats ###################################################################### stats: $(PACKAGES:%=%.stats) diff --git a/matita/matita/contribs/lambda_delta/basic_2/basic_1.orig b/matita/matita/contribs/lambda_delta/basic_2/basic_1.orig new file mode 100644 index 000000000..0b48e942f --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.orig @@ -0,0 +1,712 @@ +aplus/props / aplus_ahead_simpl +aplus/props / aplus_asort_le_simpl +aplus/props / aplus_asort_O_simpl +aplus/props / aplus_asort_simpl +aplus/props / aplus_assoc +aplus/props / aplus_asucc +aplus/props / aplus_asucc_false +aplus/props / aplus_inj +aplus/props / aplus_reg_r +aplus/props / aplus_sort_O_S_simpl +aplus/props / aplus_sort_S_S_simpl +aprem/fwd / aprem_gen_head_O +aprem/fwd / aprem_gen_head_S +aprem/fwd / aprem_gen_sort +aprem/props / aprem_asucc +aprem/props / aprem_repl +arity/aprem / arity_aprem +arity/cimp / arity_cimp_conf +arity/fwd / arity_gen_abst +arity/fwd / arity_gen_appl +arity/fwd / arity_gen_appls +arity/fwd / arity_gen_bind +arity/fwd / arity_gen_cast +arity/fwd / arity_gen_lift +arity/fwd / arity_gen_lref +arity/fwd / arity_gen_sort +arity/lift1 / arity_lift1 +arity/pr3 / arity_sred_pr2 +arity/pr3 / arity_sred_pr3 +arity/pr3 / arity_sred_wcpr0_pr0 +arity/pr3 / arity_sred_wcpr0_pr1 +arity/props / arity_appls_abbr +arity/props / arity_appls_bind +arity/props / arity_appls_cast +arity/props / arity_lift +arity/props / arity_mono +arity/props / arity_repellent +arity/props / node_inh +arity/subst0 / arity_fsubst0 +arity/subst0 / arity_gen_cvoid +arity/subst0 / arity_gen_cvoid_subst0 +arity/subst0 / arity_subst0 +asucc/fwd / asucc_gen_head +asucc/fwd / asucc_gen_sort +cimp/props / cimp_bind +cimp/props / cimp_flat_dx +cimp/props / cimp_flat_sx +cimp/props / cimp_getl_conf +clear/drop / drop_clear +clear/drop / drop_clear_O +clear/drop / drop_clear_S +clear/fwd / clear_gen_all +clear/fwd / clear_gen_bind +clear/fwd / clear_gen_flat +clear/fwd / clear_gen_flat_r +clear/fwd / clear_gen_sort +clear/props / clear_cle +clear/props / clear_clear +clear/props / clear_ctail +clear/props / clear_mono +clear/props / clear_trans +clen/getl / getl_ctail_clen +clen/getl / getl_gen_tail +cnt/props / cnt_lift +C/props / chead_ctail +C/props / clt_cong +C/props / clt_head +C/props / clt_thead +C/props / clt_wf_ind +C/props clt_wf q_ind +C/props / c_tail_ind +csuba/arity / arity_appls_appl +csuba/arity / csuba_arity +csuba/arity / csuba_arity_rev +csuba/clear / csuba_clear_conf +csuba/clear / csuba_clear_trans +csuba/drop / csuba_drop_abbr +csuba/drop / csuba_drop_abbr_rev +csuba/drop / csuba_drop_abst +csuba/drop / csuba_drop_abst_rev +csuba/fwd / csuba_gen_abbr +csuba/fwd / csuba_gen_abbr_rev +csuba/fwd / csuba_gen_abst +csuba/fwd / csuba_gen_abst_rev +csuba/fwd / csuba_gen_bind +csuba/fwd / csuba_gen_bind_rev +csuba/fwd / csuba_gen_flat +csuba/fwd / csuba_gen_flat_rev +csuba/fwd / csuba_gen_void +csuba/fwd / csuba_gen_void_rev +csuba/getl / csuba_getl_abbr +csuba/getl / csuba_getl_abbr_rev +csuba/getl / csuba_getl_abst +csuba/getl / csuba_getl_abst_rev +csuba/props / csuba_refl +csubc/arity / csubc_arity_conf +csubc/arity / csubc_arity_trans +csubc/clear / csubc_clear_conf +csubc/csuba / csubc_csuba +csubc/drop1 / csubc_drop1_conf_rev +csubc/drop1 / drop1_csubc_trans +csubc/drop / csubc_drop_conf_O +csubc/drop / csubc_drop_conf_rev +csubc/drop / drop_csubc_trans +csubc/fwd / csubc_gen_head_l +csubc/fwd / csubc_gen_head_r +csubc/fwd / csubc_gen_sort_l +csubc/fwd / csubc_gen_sort_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_eq +csubst0/drop / csubst0_drop_eq_back +csubst0/drop / csubst0_drop_gt +csubst0/drop / csubst0_drop_gt_back +csubst0/drop / csubst0_drop_lt +csubst0/drop / csubst0_drop_lt_back +csubst0/fwd / csubst0_gen_head +csubst0/fwd / csubst0_gen_S_bind_2 +csubst0/fwd / csubst0_gen_sort +csubst0/getl / csubst0_getl_ge +csubst0/getl / csubst0_getl_ge_back +csubst0/getl / csubst0_getl_lt +csubst0/getl / csubst0_getl_lt_back +csubst0/props / csubst0_both_bind +csubst0/props / csubst0_fst_bind +csubst0/props / csubst0_snd_bind +csubst1/fwd / csubst1_gen_head +csubst1/getl / csubst1_getl_ge +csubst1/getl / csubst1_getl_ge_back +csubst1/getl / csubst1_getl_lt +csubst1/getl / getl_csubst1 +csubst1/props / csubst1_bind +csubst1/props / csubst1_flat +csubst1/props / csubst1_head +csubt/clear / csubt_clear_conf +csubt/csuba / csubt_csuba +csubt/drop / csubt_drop_abbr +csubt/drop / csubt_drop_abst +csubt/drop / csubt_drop_flat +csubt/fwd / csubt_gen_abbr +csubt/fwd / csubt_gen_abst +csubt/fwd / csubt_gen_bind +csubt/fwd / csubt_gen_flat +csubt/getl / csubt_getl_abbr +csubt/getl / csubt_getl_abst +csubt/pc3 / csubt_pc3 +csubt/pc3 / csubt_pr2 +csubt/props / csubt_refl +csubt/ty3 / csubt_ty3 +csubt/ty3 / csubt_ty3_ld +csubv/clear / csubv_clear_conf +csubv/clear / csubv_clear_conf_void +csubv/drop / csubv_drop_conf +csubv/getl / csubv_getl_conf +csubv/getl / csubv_getl_conf_void +csubv/props / csubv_bind_same +csubv/props / csubv_refl +drop1/fwd / drop1_gen_pcons +drop1/fwd / drop1_gen_pnil +drop1/getl / drop1_getl_trans +drop1/props / drop1_cons_tail +drop1/props / drop1_skip_bind +drop1/props / drop1_trans +drop/fwd / drop_gen_drop +drop/fwd / drop_gen_refl +drop/fwd / drop_gen_skip_l +drop/fwd / drop_gen_skip_r +drop/fwd / drop_gen_sort +drop/props / drop_conf_ge +drop/props / drop_conf_lt +drop/props / drop_conf_rev +drop/props / drop_ctail +drop/props / drop_mono +drop/props / drop_S +drop/props / drop_skip_bind +drop/props / drop_skip_flat +drop/props / drop_trans_ge +drop/props / drop_trans_le +ex0/props / aplus_gz_ge +ex0/props / aplus_gz_le +ex0/props / leq_leqz +ex0/props / leqz_leq +ex0/props / next_plus_gz +ex1/props / ex1_arity +ex1/props ex1 leq_sort_SS +ex1/props / ex1_ty3 +ex2/props / ex2_arity +ex2/props / ex2_nf2 +flt/props / flt_arith0 +flt/props / flt_arith1 +flt/props / flt_arith2 +flt/props / flt_shift +flt/props / flt_thead_dx +flt/props / flt_thead_sx +flt/props / flt_trans +flt/props / flt_wf_ind +flt/props flt_wf q_ind +fsubst0/fwd / fsubst0_gen_base +getl/clear / clear_getl_trans +getl/clear / getl_clear_bind +getl/clear / getl_clear_conf +getl/clear / getl_clear_trans +getl/dec / getl_dec +getl/drop / drop_getl_trans_ge +getl/drop / drop_getl_trans_le +getl/drop / drop_getl_trans_lt +getl/drop / getl_conf_ge_drop +getl/drop / getl_drop +getl/drop / getl_drop_conf_ge +getl/drop / getl_drop_conf_lt +getl/drop / getl_drop_conf_rev +getl/drop / getl_drop_trans +getl/flt / getl_flt +getl/fwd / getl_gen_2 +getl/fwd / getl_gen_all +getl/fwd / getl_gen_bind +getl/fwd / getl_gen_flat +getl/fwd / getl_gen_O +getl/fwd / getl_gen_S +getl/fwd / getl_gen_sort +getl/getl / getl_conf_le +getl/getl / getl_trans +getl/props / getl_ctail +getl/props / getl_flat +getl/props / getl_head +getl/props / getl_mono +getl/props / getl_refl +iso/fwd / iso_flats_flat_bind_false +iso/fwd / iso_flats_lref_bind_false +iso/fwd / iso_gen_head +iso/fwd / iso_gen_lref +iso/fwd / iso_gen_sort +iso/props / iso_refl +iso/props / iso_trans +leq/asucc / asucc_inj +leq/asucc / asucc_repl +leq/asucc / leq_ahead_asucc_false +leq/asucc / leq_asucc +leq/asucc / leq_asucc_false +leq/fwd / leq_gen_head1 +leq/fwd / leq_gen_head2 +leq/fwd / leq_gen_sort1 +leq/fwd / leq_gen_sort2 +leq/props / ahead_inj_snd +leq/props / leq_ahead_false_1 +leq/props / leq_ahead_false_2 +leq/props / leq_eq +leq/props / leq_refl +leq/props / leq_sym +leq/props / leq_trans +lift1/fwd / lift1_bind +lift1/fwd / lift1_cons_tail +lift1/fwd / lift1_flat +lift1/fwd / lift1_lref +lift1/fwd / lift1_sort +lift1/fwd / lifts1_cons +lift1/fwd / lifts1_flat +lift1/fwd / lifts1_nil +lift1/props / lift1_free +lift1/props / lift1_lift1 +lift1/props / lift1_xhg +lift1/props / lifts1_xhg +lift/fwd / lift_bind +lift/fwd / lift_flat +lift/fwd / lift_gen_bind +lift/fwd / lift_gen_flat +lift/fwd / lift_gen_head +lift/fwd / lift_gen_lref +lift/fwd / lift_gen_lref_false +lift/fwd / lift_gen_lref_ge +lift/fwd / lift_gen_lref_lt +lift/fwd / lift_gen_sort +lift/fwd / lift_head +lift/fwd / lift_lref_ge +lift/fwd / lift_lref_lt +lift/fwd / lift_sort +lift/props / lift_d +lift/props / lift_free +lift/props / lift_gen_lift +lift/props / lift_inj +lift/props / lift_lref_gt +lift/props / lift_r +lift/props / lifts_inj +lift/props / lifts_tapp +lift/props / thead_x_lift_y_y +lift/tlt / lift_tlt_dx +lift/tlt / lift_weight +lift/tlt / lift_weight_add +lift/tlt / lift_weight_add_O +lift/tlt / lift_weight_map +llt/props / llt_head_dx +llt/props / llt_head_sx +llt/props / llt_repl +llt/props / llt_trans +llt/props / llt_wf_ind +llt/props llt_wf q_ind +llt/props / lweight_repl +next_plus/props / next_plus_assoc +next_plus/props / next_plus_lt +next_plus/props / next_plus_next +nf2/arity / arity_nf2_inv_all +nf2/dec / nf2_dec +nf2/fwd / nf2_gen_abbr +nf2/fwd / nf2_gen_abst +nf2/fwd / nf2_gen_beta +nf2/fwd / nf2_gen_cast +nf2/fwd / nf2_gen_flat +nf2/fwd / nf2_gen_lref +nf2/fwd nf2_gen nf2_gen_aux +nf2/fwd / nf2_gen_void +nf2/iso / nf2_iso_appls_lref +nf2/lift1 / nf2_lift1 +nf2/pr3 / nf2_pr3_confluence +nf2/pr3 / nf2_pr3_unfold +nf2/props / nf2_abst +nf2/props / nf2_abst_shift +nf2/props / nf2_appl_lref +nf2/props / nf2_appls_lref +nf2/props / nf2_csort_lref +nf2/props / nf2_lift +nf2/props / nf2_lref_abst +nf2/props / nf2_sort +nf2/props / nfs2_tapp +pc1/props / pc1_head +pc1/props / pc1_head_1 +pc1/props / pc1_head_2 +pc1/props / pc1_pr0_r +pc1/props / pc1_pr0_u +pc1/props / pc1_pr0_u2 +pc1/props / pc1_pr0_x +pc1/props / pc1_refl +pc1/props / pc1_s +pc1/props / pc1_t +pc3/dec / pc3_abst_dec +pc3/dec / pc3_dec +pc3/fsubst0 / pc3_fsubst0 +pc3/fsubst0 / pc3_pr2_fsubst0 +pc3/fsubst0 / pc3_pr2_fsubst0_back +pc3/fwd / pc3_gen_abst +pc3/fwd / pc3_gen_abst_shift +pc3/fwd / pc3_gen_lift +pc3/fwd / pc3_gen_lift_abst +pc3/fwd / pc3_gen_not_abst +pc3/fwd / pc3_gen_sort +pc3/fwd / pc3_gen_sort_abst +pc3/left / pc3_ind_left +pc3/left pc3_ind_left pc3_left_pc3 +pc3/left pc3_ind_left pc3_left_pr3 +pc3/left pc3_ind_left pc3_left_sym +pc3/left pc3_ind_left pc3_left_trans +pc3/left pc3_ind_left pc3_pc3_left +pc3/nf2 / pc3_nf2 +pc3/nf2 / pc3_nf2_unfold +pc3/pc1 / pc3_pc1 +pc3/props / clear_pc3_trans +pc3/props / pc3_eta +pc3/props / pc3_head_1 +pc3/props / pc3_head_12 +pc3/props / pc3_head_2 +pc3/props / pc3_head_21 +pc3/props / pc3_lift +pc3/props / pc3_pr0_pr2_t +pc3/props / pc3_pr2_pr2_t +pc3/props / pc3_pr2_pr3_t +pc3/props / pc3_pr2_r +pc3/props / pc3_pr2_u +pc3/props / pc3_pr2_u2 +pc3/props / pc3_pr2_x +pc3/props / pc3_pr3_conf +pc3/props / pc3_pr3_pc3_t +pc3/props / pc3_pr3_r +pc3/props / pc3_pr3_t +pc3/props / pc3_pr3_x +pc3/props / pc3_refl +pc3/props / pc3_s +pc3/props / pc3_t +pc3/props / pc3_thin_dx +pc3/subst1 / pc3_gen_cabbr +pc3/wcpr0 / pc3_wcpr0 +pc3/wcpr0 pc3_wcpr0 pc3_wcpr0_t_aux +pc3/wcpr0 / pc3_wcpr0_t +pr0/dec / nf0_dec +pr0/fwd / pr0_gen_abbr +pr0/fwd / pr0_gen_abst +pr0/fwd / pr0_gen_appl +pr0/fwd / pr0_gen_cast +pr0/fwd / pr0_gen_lift +pr0/fwd / pr0_gen_lref +pr0/fwd / pr0_gen_sort +pr0/fwd / pr0_gen_void +pr0/pr0 / pr0_confluence +pr0/pr0 pr0_confluence pr0_cong_delta +pr0/pr0 pr0_confluence pr0_cong_upsilon_cong +pr0/pr0 pr0_confluence pr0_cong_upsilon_delta +pr0/pr0 pr0_confluence pr0_cong_upsilon_refl +pr0/pr0 pr0_confluence pr0_cong_upsilon_zeta +pr0/pr0 pr0_confluence pr0_delta_delta +pr0/pr0 pr0_confluence pr0_delta_tau +pr0/pr0 pr0_confluence pr0_upsilon_upsilon +pr0/props / pr0_lift +pr0/props / pr0_subst0 +pr0/props / pr0_subst0_back +pr0/props / pr0_subst0_fwd +pr0/subst1 / pr0_delta1 +pr0/subst1 / pr0_subst1 +pr0/subst1 / pr0_subst1_back +pr0/subst1 / pr0_subst1_fwd +pr1/pr1 / pr1_confluence +pr1/pr1 / pr1_strip +pr1/props / pr1_comp +pr1/props / pr1_eta +pr1/props / pr1_head_1 +pr1/props / pr1_head_2 +pr1/props / pr1_pr0 +pr1/props / pr1_t +pr2/clen / pr2_gen_cbind +pr2/clen / pr2_gen_cflat +pr2/clen / pr2_gen_ctail +pr2/fwd / pr2_gen_abbr +pr2/fwd / pr2_gen_abst +pr2/fwd / pr2_gen_appl +pr2/fwd / pr2_gen_cast +pr2/fwd / pr2_gen_csort +pr2/fwd / pr2_gen_lift +pr2/fwd / pr2_gen_lref +pr2/fwd / pr2_gen_sort +pr2/fwd / pr2_gen_void +pr2/pr2 / pr2_confluence +pr2/pr2 pr2_confluence pr2_delta_delta +pr2/pr2 pr2_confluence pr2_free_delta +pr2/pr2 pr2_confluence pr2_free_free +pr2/props / clear_pr2_trans +pr2/props / pr2_cflat +pr2/props / pr2_change +pr2/props / pr2_ctail +pr2/props / pr2_head_1 +pr2/props / pr2_head_2 +pr2/props / pr2_lift +pr2/props / pr2_thin_dx +pr2/subst1 / pr2_delta1 +pr2/subst1 / pr2_gen_cabbr +pr2/subst1 / pr2_subst1 +pr3/fwd / pr3_gen_abbr +pr3/fwd / pr3_gen_abst +pr3/fwd / pr3_gen_appl +pr3/fwd / pr3_gen_bind +pr3/fwd / pr3_gen_cast +pr3/fwd / pr3_gen_lift +pr3/fwd / pr3_gen_lref +pr3/fwd / pr3_gen_sort +pr3/fwd / pr3_gen_void +pr3/iso / pr3_iso_appl_bind +pr3/iso / pr3_iso_appls_abbr +pr3/iso / pr3_iso_appls_appl_bind +pr3/iso / pr3_iso_appls_beta +pr3/iso / pr3_iso_appls_bind +pr3/iso / pr3_iso_appls_cast +pr3/iso / pr3_iso_beta +pr3/pr1 / pr3_pr1 +pr3/pr3 / pr3_confluence +pr3/pr3 / pr3_strip +pr3/props / clear_pr3_trans +pr3/props / pr3_cflat +pr3/props / pr3_eta +pr3/props / pr3_flat +pr3/props / pr3_head_1 +pr3/props / pr3_head_12 +pr3/props / pr3_head_2 +pr3/props / pr3_head_21 +pr3/props / pr3_lift +pr3/props / pr3_pr0_pr2_t +pr3/props / pr3_pr2 +pr3/props / pr3_pr2_pr2_t +pr3/props / pr3_pr2_pr3_t +pr3/props / pr3_pr3_pr3_t +pr3/props / pr3_t +pr3/props / pr3_thin_dx +pr3/subst1 / pr3_gen_cabbr +pr3/subst1 / pr3_subst1 +pr3/wcpr0 / pr3_wcpr0_t +r/props / r_arith0 +r/props / r_arith1 +r/props / r_dis +r/props / r_minus +r/props / r_plus +r/props / r_plus_sym +r/props / r_S +r/props / s_r +sc3/arity / sc3_arity +sc3/arity / sc3_arity_csubc +sc3/props / sc3_abbr +sc3/props / sc3_abst +sc3/props / sc3_appl +sc3/props / sc3_arity_gen +sc3/props / sc3_bind +sc3/props / sc3_cast +sc3/props / sc3_lift +sc3/props / sc3_lift1 +sc3/props sc3_props sc3_sn3_abst +sc3/props / sc3_repl +sc3/props / sc3_sn3 +sn3/fwd / sn3_gen_bind +sn3/fwd / sn3_gen_cflat +sn3/fwd / sn3_gen_flat +sn3/fwd / sn3_gen_head +sn3/fwd / sn3_gen_lift +sn3/lift1 / sns3_lifts1 +sn3/nf2 / nf2_sn3 +sn3/nf2 / sn3_nf2 +sn3/props / sn3_abbr +sn3/props / sn3_appl_abbr +sn3/props / sn3_appl_appl +sn3/props / sn3_appl_appls +sn3/props / sn3_appl_beta +sn3/props / sn3_appl_bind +sn3/props / sn3_appl_cast +sn3/props / sn3_appl_lref +sn3/props / sn3_appls_abbr +sn3/props / sn3_appls_beta +sn3/props / sn3_appls_bind +sn3/props / sn3_appls_cast +sn3/props / sn3_appls_lref +sn3/props / sn3_beta +sn3/props / sn3_bind +sn3/props / sn3_cast +sn3/props / sn3_cdelta +sn3/props / sn3_cflat +sn3/props / sn3_change +sn3/props / sn3_cpr3_trans +sn3/props / sn3_gen_def +sn3/props / sn3_lift +sn3/props / sn3_pr2_intro +sn3/props / sn3_pr3_trans +sn3/props / sn3_shift +sn3/props / sns3_lifts +s/props / minus_s_s +s/props / s_arith0 +s/props / s_arith1 +s/props / s_inc +s/props / s_inj +s/props / s_le +s/props / s_lt +s/props / s_minus +s/props / s_plus +s/props / s_plus_sym +s/props / s_S +sty0/fwd / sty0_gen_appl +sty0/fwd / sty0_gen_bind +sty0/fwd / sty0_gen_cast +sty0/fwd / sty0_gen_lref +sty0/fwd / sty0_gen_sort +sty0/props / sty0_correct +sty0/props / sty0_lift +sty1/cnt / sty1_cnt +sty1/props / sty1_abbr +sty1/props / sty1_appl +sty1/props / sty1_bind +sty1/props / sty1_cast2 +sty1/props / sty1_correct +sty1/props / sty1_lift +sty1/props / sty1_trans +subst0/dec / dnf_dec +subst0/dec / dnf_dec2 +subst0/fwd / subst0_gen_head +subst0/fwd / subst0_gen_lift_false +subst0/fwd / subst0_gen_lift_ge +subst0/fwd / subst0_gen_lift_lt +subst0/fwd / subst0_gen_lref +subst0/fwd / subst0_gen_sort +subst0/props / subst0_lift_ge +subst0/props / subst0_lift_ge_s +subst0/props / subst0_lift_ge_S +subst0/props / subst0_lift_lt +subst0/props / subst0_refl +subst0/subst0 / subst0_confluence_eq +subst0/subst0 / subst0_confluence_lift +subst0/subst0 / subst0_confluence_neq +subst0/subst0 / subst0_subst0 +subst0/subst0 / subst0_subst0_back +subst0/subst0 / subst0_trans +subst0/tlt / subst0_tlt +subst0/tlt / subst0_tlt_head +subst0/tlt / subst0_weight_le +subst0/tlt / subst0_weight_lt +subst1/fwd / subst1_gen_head +subst1/fwd / subst1_gen_lift_eq +subst1/fwd / subst1_gen_lift_ge +subst1/fwd / subst1_gen_lift_lt +subst1/fwd / subst1_gen_lref +subst1/fwd / subst1_gen_sort +subst1/props / subst1_ex +subst1/props / subst1_head +subst1/props / subst1_lift_ge +subst1/props / subst1_lift_lt +subst1/props / subst1_lift_S +subst1/subst1 / subst1_confluence_eq +subst1/subst1 / subst1_confluence_lift +subst1/subst1 / subst1_confluence_neq +subst1/subst1 / subst1_subst1 +subst1/subst1 / subst1_subst1_back +subst1/subst1 / subst1_trans +subst/fwd / subst_head +subst/fwd / subst_lref_eq +subst/fwd / subst_lref_gt +subst/fwd / subst_lref_lt +subst/fwd / subst_sort +subst/props / subst_lift_SO +subst/props / subst_subst0 +T/dec / abst_dec +T/dec / bind_dec_not +T/dec / binder_dec +T/dec / term_dec +T/dec terms_props bind_dec +T/dec terms_props flat_dec +T/dec terms_props kind_dec +tlist/props / tcons_tapp_ex +tlist/props / theads_tapp +tlist/props / tlist_ind_rev +tlist/props / tslt_wf_ind +tlist/props tslt_wf q_ind +tlt/props / tlt_head_dx +tlt/props / tlt_head_sx +tlt/props / tlt_trans +tlt/props / tlt_wf_ind +tlt/props tlt_wf q_ind +tlt/props / wadd_le +tlt/props / wadd_lt +tlt/props / wadd_O +tlt/props / weight_add_O +tlt/props / weight_add_S +tlt/props / weight_eq +tlt/props / weight_le +T/props / not_abbr_abst +T/props / not_abbr_void +T/props / not_abst_void +T/props / not_void_abst +T/props / thead_x_y_y +T/props / tweight_lt +ty3/arity / ty3_arity +ty3/arity_props / ty3_acyclic +ty3/arity_props / ty3_predicative +ty3/arity_props / ty3_repellent +ty3/arity_props / ty3_sn3 +ty3/dec / ty3_inference +ty3/fsubst0 / ty3_csubst0 +ty3/fsubst0 / ty3_fsubst0 +ty3/fsubst0 / ty3_subst0 +ty3/fwd / ty3_gen_appl +ty3/fwd / ty3_gen_bind +ty3/fwd / ty3_gen_cast +ty3/fwd / ty3_gen_lref +ty3/fwd / ty3_gen_sort +ty3/fwd / tys3_gen_cons +ty3/fwd / tys3_gen_nil +ty3/fwd_nf2 / ty3_gen_appl_nf2 +ty3/fwd_nf2 / ty3_inv_appls_lref_nf2 +ty3/fwd_nf2 / ty3_inv_lref_lref_nf2 +ty3/fwd_nf2 / ty3_inv_lref_nf2 +ty3/fwd_nf2 / ty3_inv_lref_nf2_pc3 +ty3/nf2 ty3_nf2_gen ty3_nf2_inv_abst_aux +ty3/nf2 / ty3_nf2_inv_abst +ty3/nf2 / ty3_nf2_inv_abst_premise_csort +ty3/nf2 / ty3_nf2_inv_all +ty3/nf2 / ty3_nf2_inv_sort +ty3/pr3 / ty3_sred_pr0 +ty3/pr3 / ty3_sred_pr1 +ty3/pr3 / ty3_sred_pr2 +ty3/pr3 / ty3_sred_pr3 +ty3/pr3 / ty3_sred_wcpr0_pr0 +ty3/pr3_props / ty3_cred_pr2 +ty3/pr3_props / ty3_cred_pr3 +ty3/pr3_props / ty3_gen_lift +ty3/pr3_props / ty3_sconv +ty3/pr3_props / ty3_sconv_pc3 +ty3/pr3_props / ty3_sred_back +ty3/pr3_props / ty3_tred +ty3/props / ty3_correct +ty3/props / ty3_gen_abst_abst +ty3/props / ty3_getl_subst0 +ty3/props / ty3_lift +ty3/props / ty3_typecheck +ty3/props / ty3_unique +ty3/sty0 / ty3_sty0 +ty3/subst1 / ty3_gen_cabbr +ty3/subst1 / ty3_gen_cvoid +wcpr0/fwd / wcpr0_gen_head +wcpr0/fwd / wcpr0_gen_sort +wcpr0/getl / wcpr0_drop +wcpr0/getl / wcpr0_drop_back +wcpr0/getl / wcpr0_getl +wcpr0/getl / wcpr0_getl_back +wf3/clear / clear_wf3_trans +wf3/clear / wf3_clear_conf +wf3/fwd / wf3_gen_bind1 +wf3/fwd / wf3_gen_flat1 +wf3/fwd / wf3_gen_head2 +wf3/fwd / wf3_gen_sort1 +wf3/getl / getl_wf3_trans +wf3/getl / wf3_getl_conf +wf3/props / ty3_shift1 +wf3/props / wf3_idem +wf3/props / wf3_mono +wf3/props / wf3_total +wf3/props / wf3_ty3 +wf3/ty3 / wf3_pc3_conf +wf3/ty3 / wf3_pr2_conf +wf3/ty3 / wf3_pr3_conf +wf3/ty3 / wf3_ty3_conf 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 dcb49f2ce..ca83c049a 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt +++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt @@ -47,9 +47,6 @@ asucc/fwd asucc_gen_head cnt/props cnt_lift C/props clt_wf__q_ind C/props clt_wf_ind -C/props chead_ctail -C/props clt_thead (ctail) -C/props c_tail_ind csuba/arity csuba_arity csuba/arity csuba_arity_rev csuba/arity arity_appls_appl @@ -103,7 +100,6 @@ csubv/getl csubv_getl_conf_void csubv/props csubv_bind_same csubv/props csubv_refl drop1/props drop1_cons_tail -drop/props drop_ctail ex0/props aplus_gz_le ex0/props aplus_gz_ge ex0/props next_plus_gz @@ -132,18 +128,10 @@ leq/props leq_trans leq/props leq_ahead_false_1 leq/props leq_ahead_false_2 lift1/fwd lift1_cons_tail - -# check ############################################################# - -lift1/fwd lifts1_flat lift1/fwd lifts1_nil lift1/fwd lifts1_cons -lift1/props lift1_free lift/props thead_x_lift_y_y lift/props lifts_tapp - -# waiting #################################################################### - lift/props lifts_inj llt/props lweight_repl llt/props llt_repl @@ -156,8 +144,6 @@ next_plus/props next_plus_assoc next_plus/props next_plus_next next_plus/props next_plus_lt nf2/arity arity_nf2_inv_all -nf2/dec nf2_dec - nf2/fwd nf2_gen_lref nf2/fwd nf2_gen_abst nf2/fwd nf2_gen_cast @@ -165,15 +151,9 @@ nf2/fwd nf2_gen_beta nf2/fwd nf2_gen_flat nf2/fwd nf2_gen__nf2_gen_aux nf2/fwd nf2_gen_abbr - nf2/fwd nf2_gen_void -nf2/iso nf2_iso_appls_lref -nf2/pr3 nf2_pr3_unfold -nf2/pr3 nf2_pr3_confluence - nf2/props nfs2_tapp nf2/props nf2_appls_lref - pc1/props pc1_pr0_r pc1/props pc1_pr0_x pc1/props pc1_refl @@ -184,7 +164,6 @@ pc1/props pc1_head_2 pc1/props pc1_t pc1/props pc1_pr0_u2 pc1/props pc1_head - pc3/dec pc3_dec pc3/dec pc3_abst_dec pc3/fsubst0 pc3_pr2_fsubst0 @@ -232,9 +211,6 @@ pc3/wcpr0 pc3_wcpr0__pc3_wcpr0_t_aux pc3/wcpr0 pc3_wcpr0_t pc3/wcpr0 pc3_wcpr0 pr0/fwd pr0_gen_void - -# check ############################################################# - pr0/dec nf0_dec pr0/subst1 pr0_subst1_back pr0/subst1 pr0_subst1_fwd @@ -246,30 +222,13 @@ pr1/props pr1_head_1 pr1/props pr1_head_2 pr1/props pr1_comp pr1/props pr1_eta -pr2/clen pr2_gen_ctail pr2/fwd pr2_gen_void -pr2/props pr2_ctail pr2/subst1 pr2_gen_cabbr pr3/fwd pr3_gen_void pr3/pr1 pr3_pr1 - -pr3/pr3 pr3_strip -pr3/props pr3_thin_dx -pr3/props pr3_head_1 -pr3/props pr3_head_2 -pr3/props pr3_head_21 -pr3/props pr3_head_12 pr3/props pr3_eta -pr3/subst1 pr3_subst1 pr3/subst1 pr3_gen_cabbr -sn3/props sn3_cpr3_trans - -sn3/props sn3_shift -sn3/props sn3_change -sn3/props sn3_gen_def -sn3/props sn3_cdelta sn3/props sns3_lifts - sty0/fwd sty0_gen_sort sty0/fwd sty0_gen_lref sty0/fwd sty0_gen_bind diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma new file mode 100644 index 000000000..22d7ea92a --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma @@ -0,0 +1,35 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/cprs.ma". +include "basic_2/computation/csn.ma". + +(* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************) + +definition cpe: lenv → relation term ≝ + λL,T1,T2. L ⊢ T1 ➡* T2 ∧ L ⊢ 𝐍[T2]. + +interpretation "context-sensitive parallel evaluation (term)" + 'PEval L T1 T2 = (cpe L T1 T2). + +(* Basic_properties *********************************************************) + +(* Basic_1: was: nf2_sn3 *) +lemma cpe_csn: ∀L,T1. L ⊢ ⬇* T1 → ∃T2. L ⊢ T1 ➡* 𝐍[T2]. +#L #T1 #H @(csn_ind … H) -T1 +#T1 #_ #IHT1 +elim (cnf_dec L T1) /3 width=3/ +* #T #H1T1 #H2T1 +elim (IHT1 … H1T1 H2T1) -IHT1 -H2T1 #T2 * /4 width=3/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cpe_cpe.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cpe_cpe.ma new file mode 100644 index 000000000..2c3b8b841 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cpe_cpe.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/cprs_cprs.ma". +include "basic_2/computation/cpe.ma". + +(* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************) + +(* Main properties *********************************************************) + +(* Basic_1: was: nf2_pr3_confluence *) +theorem cpe_mono: ∀L,T,T1. L ⊢ T ➡* 𝐍[T1] → ∀T2. L ⊢ T ➡* 𝐍[T2] → T1 = T2. +#L #T #T1 * #H1T1 #H2T1 #T2 * #H1T2 #H2T2 +elim (cprs_conf … H1T1 … H1T2) -T #T #HT1 +>(cprs_inv_cnf1 … HT1 H2T1) -T1 #HT2 +>(cprs_inv_cnf1 … HT2 H2T2) -T2 // +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma index 5ea230f9b..6314894c2 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma @@ -60,6 +60,7 @@ lemma cprs_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 → /3 width=3/ qed. +(* Basic_1: was only: pr3_thin_dx *) lemma cprs_flat_dx: ∀I,L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L ⊢ T1 ➡* T2 → L ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2. #I #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind … HT12) -T2 /3 width=1/ @@ -86,13 +87,15 @@ elim (cpr_inv_cast1 … HU2) -HU2 /3 width=3/ * #W2 #T2 #HW2 #HT2 #H destruct /4 width=5/ qed-. +(* Basic_1: was: nf2_pr3_unfold *) lemma cprs_inv_cnf1: ∀L,T,U. L ⊢ T ➡* U → L ⊢ 𝐍[T] → T = U. #L #T #U #H @(cprs_ind_dx … H) -T // #T0 #T #H1T0 #_ #IHT #H2T0 lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/ qed-. -(* Basic_1: removed theorems 6: +(* Basic_1: removed theorems 10: clear_pr3_trans pr3_cflat pr3_gen_bind + pr3_head_1 pr3_head_2 pr3_head_21 pr3_head_12 pr3_iso_appl_bind pr3_iso_appls_appl_bind pr3_iso_appls_bind *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma index ca3fe09da..518c2bd07 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma @@ -40,6 +40,11 @@ lemma cpr_abbr2: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡ T lapply (lcpr_cpr_trans (L. ⓓV1) … HT12) /2 width=1/ qed. +(* Basic_1: was: pr3_strip *) +lemma cprs_strip: ∀L,T1,T. L ⊢ T ➡* T1 → ∀T2. L ⊢ T ➡ T2 → + ∃∃T0. L ⊢ T1 ➡ T0 & L ⊢ T2 ➡* T0. +/3 width=3/ qed. + (* Advanced inversion lemmas ************************************************) (* Basic_1: was pr3_gen_appl *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_ltpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_ltpr.ma new file mode 100644 index 000000000..8859a46d6 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_ltpr.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/reducibility/cpr_ltpr.ma". +include "basic_2/computation/cprs.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) + +(* Properties concerning parallel unfold on terms ***************************) + +(* Basic_1: was only: pr3_subst1 *) +lemma cprs_tpss_ltpr: ∀L1,T1,U1,d,e. L1 ⊢ T1 [d, e] ▶* U1 → + ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → + ∃∃U2. L2 ⊢ U1 ➡* U2 & L2 ⊢ T2 [d, e] ▶* U2. +#L1 #T1 #U1 #d #e #HTU1 #L2 #HL12 #T2 #HT12 elim HT12 -T2 +[ #T2 #HT12 + elim (cpr_tpss_ltpr … HL12 … HT12 … HTU1) -L1 -T1 /3 width=3/ +| #T #T2 #_ #HT2 * #U #HU1 #HTU + elim (cpr_tpss_ltpr … HT2 … HTU) -L1 -T // /3 width=3/ +] +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma index 14655cdee..27c79d1b6 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma @@ -82,8 +82,9 @@ qed. lemma csn_fwd_flat_dx: ∀I,L,V,T. L ⊢ ⬇* ⓕ{I} V. T → L ⊢ ⬇* T. /2 width=5/ qed-. -(* Basic_1: removed theorems 10: - sn3_gen_cflat sn3_cflat +(* Basic_1: removed theorems 14: + sn3_cdelta + sn3_gen_cflat sn3_cflat sn3_cpr3_trans sn3_shift sn3_change sn3_appl_cast sn3_appl_beta sn3_appl_lref sn3_appl_abbr sn3_appl_appls sn3_bind sn3_appl_bind sn3_appls_bind *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma index 530fde74c..c32947631 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma @@ -88,17 +88,6 @@ qed. lemma csn_cprs_trans: ∀L,T1. L ⊢ ⬇* T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬇* T2. /4 width=3/ qed. -(* Basic_1: was: nf2_sn3 *) -lemma csn_cwn: ∀L,T1. L ⊢ ⬇* T1 → - ∃∃T2. L ⊢ T1 ➡* T2 & L ⊢ 𝐍[T2]. -#L #T1 #H elim H -T1 #T1 #_ #IHT1 -elim (cnf_dec L T1) -[ -IHT1 /2 width=3/ -| * #T2 #HLT12 #HT12 - elim (IHT1 T2 ? ?) -IHT1 // /2 width=1/ -HT12 /3 width=3/ -] -qed. - (* Main eliminators *********************************************************) lemma csn_ind_cprs: ∀L. ∀R:predicate term. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma index b658f9bc8..93e22f77a 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma @@ -88,6 +88,17 @@ elim (eq_false_inv_tpair_dx … H2) -H2 ] qed. +(* Advanced inversion lemmas ************************************************) + +(* Basic_1: was: sn3_gen_def *) +lemma csn_inv_lref_abbr: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓓV → L ⊢ ⬇* #i → K ⊢ ⬇* V. +#L #K #V #i #HLK #Hi +elim (lift_total V 0 (i+1)) #V0 #HV0 +lapply (ldrop_fwd_ldrop2 … HLK) #H0LK +@(csn_inv_lift … H0LK … HV0) -H0LK +@(csn_cpr_trans … Hi) -Hi /2 width=6/ +qed-. + (* Main properties **********************************************************) theorem csn_acp: acp cpr (eq …) (csn …). 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 dc2c643b9..ba94738a8 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma @@ -36,3 +36,5 @@ interpretation "abbreviation (local environment)" interpretation "abstraction (local environment)" 'DxAbst L T = (LPair L Abst T). + +(* Basic_1: removed theorems 2: chead_ctail c_tail_ind *) 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 bc8ffce87..990b5c5d0 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 @@ -24,4 +24,5 @@ let rec lw L ≝ match L with interpretation "weight (local environment)" 'Weight L = (lw L). -(* Basic_1: removed theorems 2: clt_cong clt_head *) +(* Basic_1: removed theorems 2: clt_cong clt_head clt_thead *) +(* Basic_1: note: clt_thead should be renamed clt_ctail *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index a9fca999c..ce9a370e2 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -146,6 +146,10 @@ notation "hvbox( ⇩ [ d , break e ] break L1 ≡ break L2 )" non associative with precedence 45 for @{ 'RDrop $d $e $L1 $L2 }. +notation "hvbox( L ⊢ break ⌘ [ T ] ≡ break k )" + non associative with precedence 45 + for @{ 'ICM $L $T $k }. + notation "hvbox( T1 break [ d , break e ] ▶ break T2 )" non associative with precedence 45 for @{ 'PSubst $T1 $d $e $T2 }. @@ -274,6 +278,10 @@ notation "hvbox( L1 ⊢ ➡* break L2 )" non associative with precedence 45 for @{ 'CPRedStar $L1 $L2 }. +notation "hvbox( L ⊢ break term 90 T1 ➡* break 𝐍 [ T2 ] )" + non associative with precedence 45 + for @{ 'PEval $L $T1 $T2 }. + notation "hvbox( ⬇ * T )" non associative with precedence 45 for @{ 'SN $T }. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma index b97150df7..00647e43c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma @@ -30,6 +30,7 @@ lemma cnf_sort: ∀L,k. L ⊢ 𝐍[⋆k]. >(cpr_inv_sort1 … H) // qed. +(* Basic_1: was: nf2_dec *) axiom cnf_dec: ∀L,T1. L ⊢ 𝐍[T1] ∨ ∃∃T2. L ⊢ T1 ➡ T2 & (T1 = T2 → False). 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 fdbc9458f..953145592 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma @@ -107,8 +107,9 @@ elim (tpr_inv_cast1 … H) -H /3 width=3/ elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/ qed-. -(* Basic_1: removed theorems 4: +(* Basic_1: removed theorems 6: pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans + pr2_gen_ctail pr2_ctail Basic_1: removed local theorems 3: pr2_free_free pr2_free_delta pr2_delta_delta *) 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 e667c7cde..3dfc35639 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma @@ -211,8 +211,8 @@ lemma ldrop_fwd_O1_length: ∀L1,L2,e. ⇩[0, e] L1 ≡ L2 → |L2| = |L1| - e. ] qed-. -(* Basic_1: removed theorems 49: - drop_skip_flat +(* Basic_1: removed theorems 50: + drop_ctail 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 diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma index b757b9cb7..1690c9f66 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma @@ -29,6 +29,7 @@ interpretation "generic relocation (vector)" (* Basic inversion lemmas ***************************************************) +(* Basic_1: was: lifts1_flat (left to right) *) lemma lifts_inv_applv1: ∀V1s,U1,T2,des. ⇧*[des] Ⓐ V1s. U1 ≡ T2 → ∃∃V2s,U2. ⇧*[des] V1s ≡ V2s & ⇧*[des] U1 ≡ U2 & T2 = Ⓐ V2s. U2. @@ -44,6 +45,7 @@ qed-. (* Basic properties *********************************************************) +(* Basic_1: was: lifts1_flat (right to left) *) lemma lifts_applv: ∀V1s,V2s,des. ⇧*[des] V1s ≡ V2s → ∀T1,T2. ⇧*[des] T1 ≡ T2 → ⇧*[des] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2. diff --git a/matita/matita/contribs/lambda_delta/orig.sh b/matita/matita/contribs/lambda_delta/orig.sh new file mode 100644 index 000000000..83b1fa183 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/orig.sh @@ -0,0 +1,4 @@ +F=`find $1 -name "*.ma" -or -name "*.txt"` +while read A A A; do + if grep -q "$A" $F; then true; else echo $A; fi +done diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma index bac2e771c..bff1aaeef 100644 --- a/matita/matita/lib/basics/star.ma +++ b/matita/matita/lib/basics/star.ma @@ -191,3 +191,10 @@ lemma TC_star_ind_dx: ∀A,R. reflexive A R → #A #R #HR #a2 #P #Ha2 #H #a1 #Ha12 @(TC_star_ind_dx_aux … HR … Ha2 H … Ha12) // qed-. + +definition Conf3: ∀A. relation A → relation A → Prop ≝ λA,S,R. + ∀a,a1. S a1 a → ∀a2. R a1 a2 → S a2 a. + +lemma TC_Conf3: ∀A,S,R. Conf3 A S R → Conf3 A S (TC … R). +#A #S #R #HSR #a #a1 #Ha1 #a2 #H elim H -a2 /2 width=3/ +qed. diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 98e9f1e61..b276fe4bb 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1503,6 +1503,7 @@ let load_predefined_virtuals () = ;; let predefined_classes = [ + ["#"; "⌘"; ]; ["-"; "÷"; "⊢"; ]; ["="; "≃"; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; ]; ["→"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; -- 2.39.2