From: Ferruccio Guidi Date: Sat, 27 Aug 2011 13:59:35 +0000 (+0000) Subject: - the shift function is now defined and cpr_shift_fwd is proved X-Git-Tag: make_still_working~2324 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b264ad188cb0023a16dae105b037357fa75c5c1a;p=helm.git - the shift function is now defined and cpr_shift_fwd is proved - tentative definition of the structures for the wh normal forms - definition of lists without the [...] notation - some refactoring and annotating (we separate lemmas from facts) --- diff --git a/matita/matita/contribs/lambda-delta/Basic-2/Basic-1.txt b/matita/matita/contribs/lambda-delta/Basic-2/Basic-1.txt new file mode 100644 index 000000000..4742d0faa --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/Basic-1.txt @@ -0,0 +1,675 @@ +# waiting #################################################################### + +aplus/props aplus_reg_r +aplus/props aplus_assoc +aplus/props aplus_asucc +aplus/props aplus_sort_O_S_simpl +aplus/props aplus_sort_S_S_simpl +aplus/props aplus_asort_O_simpl +aplus/props aplus_asort_le_simpl +aplus/props aplus_asort_simpl +aplus/props aplus_ahead_simpl +aplus/props aplus_asucc_false +aplus/props aplus_inj +aprem/fwd aprem_gen_sort +aprem/fwd aprem_gen_head_O +aprem/fwd aprem_gen_head_S +aprem/props aprem_repl +aprem/props aprem_asucc +arity/aprem arity_aprem +arity/cimp arity_cimp_conf +arity/fwd arity_gen_sort +arity/fwd arity_gen_lref +arity/fwd arity_gen_bind +arity/fwd arity_gen_abst +arity/fwd arity_gen_appl +arity/fwd arity_gen_cast +arity/fwd arity_gen_appls +arity/fwd arity_gen_lift +arity/lift1 arity_lift1 +arity/pr3 arity_sred_wcpr0_pr0 +arity/pr3 arity_sred_wcpr0_pr1 +arity/pr3 arity_sred_pr2 +arity/pr3 arity_sred_pr3 +arity/props node_inh +arity/props arity_lift +arity/props arity_mono +arity/props arity_repellent +arity/props arity_appls_cast +arity/props arity_appls_abbr +arity/props arity_appls_bind +arity/subst0 arity_gen_cvoid_subst0 +arity/subst0 arity_gen_cvoid +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 c_tail_ind + +# waiting #################################################################### + +csuba/arity csuba_arity +csuba/arity csuba_arity_rev +csuba/arity arity_appls_appl +csuba/clear csuba_clear_conf +csuba/clear csuba_clear_trans +csuba/drop csuba_drop_abbr +csuba/drop csuba_drop_abst +csuba/drop csuba_drop_abst_rev +csuba/drop csuba_drop_abbr_rev +csuba/fwd csuba_gen_abbr +csuba/fwd csuba_gen_void +csuba/fwd csuba_gen_abst +csuba/fwd csuba_gen_flat +csuba/fwd csuba_gen_bind +csuba/fwd csuba_gen_abst_rev +csuba/fwd csuba_gen_void_rev +csuba/fwd csuba_gen_abbr_rev +csuba/fwd csuba_gen_flat_rev +csuba/fwd csuba_gen_bind_rev +csuba/getl csuba_getl_abbr +csuba/getl csuba_getl_abst +csuba/getl csuba_getl_abst_rev +csuba/getl csuba_getl_abbr_rev +csuba/props csuba_refl +csubc/arity csubc_arity_conf +csubc/arity csubc_arity_trans +csubc/clear csubc_clear_conf +csubc/csuba csubc_csuba +csubc/drop1 drop1_csubc_trans +csubc/drop1 csubc_drop1_conf_rev +csubc/drop csubc_drop_conf_O +csubc/drop drop_csubc_trans +csubc/drop csubc_drop_conf_rev +csubc/fwd csubc_gen_sort_l +csubc/fwd csubc_gen_head_l +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 +csubt/drop csubt_drop_abbr +csubt/drop csubt_drop_abst +csubt/fwd csubt_gen_abbr +csubt/fwd csubt_gen_abst +csubt/fwd csubt_gen_flat +csubt/fwd csubt_gen_bind +csubt/getl csubt_getl_abbr +csubt/getl csubt_getl_abst +csubt/pc3 csubt_pr2 +csubt/pc3 csubt_pc3 +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_pnil +drop1/fwd drop1_gen_pcons +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 +ex0/props leqz_leq +ex0/props leq_leqz +ex1/props ex1__leq_sort_SS +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 +leq/asucc leq_ahead_asucc_false +leq/asucc leq_asucc_false +leq/fwd leq_gen_sort1 +leq/fwd leq_gen_head1 +leq/fwd leq_gen_sort2 +leq/fwd leq_gen_head2 +leq/props ahead_inj_snd +leq/props leq_refl +leq/props leq_eq +leq/props leq_sym +leq/props leq_trans +leq/props leq_ahead_false_1 +leq/props leq_ahead_false_2 +lift1/fwd lift1_sort +lift1/fwd lift1_lref +lift1/fwd lift1_bind +lift1/fwd lift1_flat +lift1/fwd lift1_cons_tail +lift1/fwd lifts1_flat +lift1/fwd lifts1_nil +lift1/fwd lifts1_cons +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 +llt/props llt_head_sx +llt/props llt_head_dx +llt/props llt_wf__q_ind +llt/props llt_wf_ind +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 +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/lift1 nf2_lift1 +nf2/pr3 nf2_pr3_unfold +nf2/pr3 nf2_pr3_confluence +nf2/props nf2_sort +nf2/props nf2_csort_lref +nf2/props nf2_abst +nf2/props nf2_abst_shift +nf2/props nfs2_tapp +nf2/props nf2_appls_lref +nf2/props nf2_appl_lref +nf2/props nf2_lref_abst +nf2/props nf2_lift +pc1/props pc1_pr0_r +pc1/props pc1_pr0_x +pc1/props pc1_refl +pc1/props pc1_pr0_u +pc1/props pc1_s +pc1/props pc1_head_1 +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 +pc3/fsubst0 pc3_pr2_fsubst0_back +pc3/fsubst0 pc3_fsubst0 +pc3/fwd pc3_gen_sort +pc3/fwd pc3_gen_abst +pc3/fwd pc3_gen_abst_shift +pc3/fwd pc3_gen_lift +pc3/fwd pc3_gen_not_abst +pc3/fwd pc3_gen_lift_abst +pc3/fwd pc3_gen_sort_abst +pc3/left pc3_ind_left__pc3_left_pr3 +pc3/left pc3_ind_left__pc3_left_trans +pc3/left pc3_ind_left__pc3_left_sym +pc3/left pc3_ind_left__pc3_left_pc3 +pc3/left pc3_ind_left__pc3_pc3_left +pc3/left pc3_ind_left +pc3/nf2 pc3_nf2 +pc3/nf2 pc3_nf2_unfold +pc3/pc1 pc3_pc1 +pc3/props clear_pc3_trans +pc3/props pc3_pr2_r +pc3/props pc3_pr2_x +pc3/props pc3_pr3_r +pc3/props pc3_pr3_x +pc3/props pc3_pr3_t +pc3/props pc3_refl +pc3/props pc3_s +pc3/props pc3_thin_dx +pc3/props pc3_head_1 +pc3/props pc3_head_2 +pc3/props pc3_pr2_u +pc3/props pc3_t +pc3/props pc3_pr2_u2 +pc3/props pc3_pr3_conf +pc3/props pc3_head_12 +pc3/props pc3_head_21 +pc3/props pc3_pr0_pr2_t +pc3/props pc3_pr2_pr2_t +pc3/props pc3_pr2_pr3_t +pc3/props pc3_pr3_pc3_t +pc3/props pc3_lift +pc3/props pc3_eta +pc3/subst1 pc3_gen_cabbr +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 +pr1/props pr1_t +pr1/props pr1_head_1 +pr1/props pr1_head_2 +pr1/props pr1_comp +pr1/props pr1_eta +pr2/clen pr2_gen_ctail +pr2/clen pr2_gen_cbind +pr2/clen pr2_gen_cflat +pr2/fwd pr2_gen_sort +pr2/fwd pr2_gen_lref +pr2/fwd pr2_gen_abst +pr2/fwd pr2_gen_cast +pr2/fwd pr2_gen_csort +pr2/fwd pr2_gen_appl +pr2/fwd pr2_gen_abbr +pr2/fwd pr2_gen_void +pr2/fwd pr2_gen_lift +pr2/pr2 pr2_confluence__pr2_free_free +pr2/pr2 pr2_confluence__pr2_free_delta +pr2/pr2 pr2_confluence__pr2_delta_delta +pr2/pr2 pr2_confluence +pr2/props pr2_thin_dx +pr2/props pr2_head_1 +pr2/props pr2_head_2 +pr2/props clear_pr2_trans +pr2/props pr2_cflat +pr2/props pr2_ctail +pr2/props pr2_change +pr2/props pr2_lift +pr2/subst1 pr2_delta1 +pr2/subst1 pr2_subst1 +pr2/subst1 pr2_gen_cabbr +pr3/fwd pr3_gen_sort +pr3/fwd pr3_gen_abst +pr3/fwd pr3_gen_cast +pr3/fwd pr3_gen_lift +pr3/fwd pr3_gen_lref +pr3/fwd pr3_gen_void +pr3/fwd pr3_gen_abbr +pr3/fwd pr3_gen_appl +pr3/fwd pr3_gen_bind +pr3/iso pr3_iso_appls_abbr +pr3/iso pr3_iso_appls_cast +pr3/iso pr3_iso_appl_bind +pr3/iso pr3_iso_appls_appl_bind +pr3/iso pr3_iso_appls_bind +pr3/iso pr3_iso_beta +pr3/iso pr3_iso_appls_beta +pr3/pr1 pr3_pr1 +pr3/pr3 pr3_strip +pr3/pr3 pr3_confluence +pr3/props clear_pr3_trans +pr3/props pr3_pr2 +pr3/props pr3_t +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_cflat +pr3/props pr3_flat +pr3/props pr3_pr0_pr2_t +pr3/props pr3_pr2_pr2_t +pr3/props pr3_pr2_pr3_t +pr3/props pr3_pr3_pr3_t +pr3/props pr3_lift +pr3/props pr3_eta +pr3/subst1 pr3_subst1 +pr3/subst1 pr3_gen_cabbr +pr3/wcpr0 pr3_wcpr0_t +sc3/arity sc3_arity_csubc +sc3/arity sc3_arity +sc3/props sc3_arity_gen +sc3/props sc3_repl +sc3/props sc3_lift +sc3/props sc3_lift1 +sc3/props sc3_abbr +sc3/props sc3_cast +sc3/props sc3_props__sc3_sn3_abst +sc3/props sc3_sn3 +sc3/props sc3_abst +sc3/props sc3_bind +sc3/props sc3_appl +sn3/fwd sn3_gen_bind +sn3/fwd sn3_gen_flat +sn3/fwd sn3_gen_head +sn3/fwd sn3_gen_cflat +sn3/fwd sn3_gen_lift +sn3/lift1 sns3_lifts1 +sn3/nf2 sn3_nf2 +sn3/nf2 nf2_sn3 +sn3/props sn3_pr3_trans +sn3/props sn3_pr2_intro +sn3/props sn3_cast +sn3/props sn3_cflat +sn3/props sn3_shift +sn3/props sn3_change +sn3/props sn3_gen_def +sn3/props sn3_cdelta +sn3/props sn3_cpr3_trans +sn3/props sn3_bind +sn3/props sn3_beta +sn3/props sn3_appl_lref +sn3/props sn3_appl_abbr +sn3/props sn3_appl_cast +sn3/props sn3_appl_bind +sn3/props sn3_appl_appl +sn3/props sn3_appl_beta +sn3/props sn3_appl_appls +sn3/props sn3_appls_lref +sn3/props sn3_appls_cast +sn3/props sn3_appls_bind +sn3/props sn3_appls_beta +sn3/props sn3_lift +sn3/props sn3_abbr +sn3/props sn3_appls_abbr +sn3/props sns3_lifts +sty0/fwd sty0_gen_sort +sty0/fwd sty0_gen_lref +sty0/fwd sty0_gen_bind +sty0/fwd sty0_gen_appl +sty0/fwd sty0_gen_cast +sty0/props sty0_lift +sty0/props sty0_correct +sty1/cnt sty1_cnt +sty1/props sty1_trans +sty1/props sty1_bind +sty1/props sty1_appl +sty1/props sty1_lift +sty1/props sty1_correct +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_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_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 +subst/fwd subst_lref_eq +subst/fwd subst_lref_gt +subst/fwd subst_head +subst/props subst_lift_SO +subst/props subst_subst0 +T/dec terms_props__bind_dec +T/dec bind_dec_not +T/dec terms_props__flat_dec +T/dec terms_props__kind_dec +T/dec term_dec +T/dec binder_dec +T/dec abst_dec +tlist/props tslt_wf__q_ind +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 +T/props not_abst_void +T/props thead_x_y_y +T/props tweight_lt +ty3/arity ty3_arity +ty3/arity_props ty3_predicative +ty3/arity_props ty3_repellent +ty3/arity_props ty3_acyclic +ty3/arity_props ty3_sn3 +ty3/dec ty3_inference +ty3/fsubst0 ty3_fsubst0 +ty3/fsubst0 ty3_csubst0 +ty3/fsubst0 ty3_subst0 +ty3/fwd ty3_gen_sort +ty3/fwd ty3_gen_lref +ty3/fwd ty3_gen_bind +ty3/fwd ty3_gen_appl +ty3/fwd ty3_gen_cast +ty3/fwd tys3_gen_nil +ty3/fwd tys3_gen_cons +ty3/fwd_nf2 ty3_gen_appl_nf2 +ty3/fwd_nf2 ty3_inv_lref_nf2_pc3 +ty3/fwd_nf2 ty3_inv_lref_nf2 +ty3/fwd_nf2 ty3_inv_appls_lref_nf2 +ty3/fwd_nf2 ty3_inv_lref_lref_nf2 +ty3/nf2 ty3_nf2_inv_abst_premise_csort +ty3/nf2 ty3_nf2_inv_all +ty3/nf2 ty3_nf2_inv_sort +ty3/nf2 ty3_nf2_gen__ty3_nf2_inv_abst_aux +ty3/nf2 ty3_nf2_inv_abst +ty3/pr3 ty3_sred_wcpr0_pr0 +ty3/pr3 ty3_sred_pr0 +ty3/pr3 ty3_sred_pr1 +ty3/pr3 ty3_sred_pr2 +ty3/pr3 ty3_sred_pr3 +ty3/pr3_props ty3_cred_pr2 +ty3/pr3_props ty3_cred_pr3 +ty3/pr3_props ty3_gen_lift +ty3/pr3_props ty3_tred +ty3/pr3_props ty3_sconv_pc3 +ty3/pr3_props ty3_sred_back +ty3/pr3_props ty3_sconv +ty3/props ty3_lift +ty3/props ty3_correct +ty3/props ty3_unique +ty3/props ty3_gen_abst_abst +ty3/props ty3_typecheck +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 +wf3/fwd wf3_gen_bind1 +wf3/fwd wf3_gen_flat1 +wf3/fwd wf3_gen_head2 +wf3/getl wf3_getl_conf +wf3/getl getl_wf3_trans +wf3/props wf3_mono +wf3/props wf3_total +wf3/props ty3_shift1 +wf3/props wf3_idem +wf3/props wf3_ty3 +wf3/ty3 wf3_pr2_conf +wf3/ty3 wf3_pr3_conf +wf3/ty3 wf3_pc3_conf +wf3/ty3 wf3_ty3_conf 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 new file mode 100644 index 000000000..df96372be --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/cl_shift.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Basic-2/grammar/cl_weight.ma". + +(* SHIFT OF A CLOSURE *******************************************************) + +let rec shift L T on L ≝ match L with +[ LSort ⇒ T +| LPair L I V ⇒ shift L (𝕓{I} V. T) +]. + +interpretation "shift (closure)" 'Append L T = (shift L T). + +(* Basic properties *********************************************************) + +lemma tw_shift: ∀L,T. #[L, T] ≤ #[L @ T]. +#L elim L // +#K #I #V #IHL #T +@transitive_le [3: @IHL |2: /2/ | skip ] +qed. + + 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 new file mode 100644 index 000000000..b501ef3e5 --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/cl_weight.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Basic-2/grammar/lenv_weight.ma". + +(* WEIGHT OF A CLOSURE ******************************************************) + +definition cw: lenv → term → ? ≝ λL,T. #[L] + #[T]. + +interpretation "weight (closure)" 'Weight L T = (cw L T). + +(* Basic properties *********************************************************) + +lemma cw_shift: ∀K,I,V,T. #[K. 𝕓{I} V, T] < #[K, 𝕓{I} V. T]. +normalize // +qed. + +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. 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 3db6ebf53..37b5d18af 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma @@ -18,7 +18,7 @@ * [ suggested invocation to start formal specifications with ] *) -include "Ground-2/ground.ma". +include "Ground-2/list.ma". include "Basic-2/notation.ma". (* BINARY ITEMS *************************************************************) @@ -44,3 +44,9 @@ inductive item2: Type[0] ≝ coercion item2_of_bind2: ∀I:bind2.item2 ≝ Bind on _I:bind2 to item2. coercion item2_of_flat2: ∀I:flat2.item2 ≝ Flat on _I:flat2 to item2. + +(* Basic-1: removed theorems 19: + 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 +*) 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 437730a83..2321e7b0d 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 @@ -14,9 +14,8 @@ include "Basic-2/grammar/lenv.ma". -(* LENGTH *******************************************************************) +(* LENGTH OF A LOCAL ENVIRONMENT ********************************************) -(* the length of a local environment *) let rec length L ≝ match L with [ LSort ⇒ 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 1d918d3a8..950d70c4a 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 @@ -15,21 +15,11 @@ include "Basic-2/grammar/term_weight.ma". include "Basic-2/grammar/lenv.ma". -(* WEIGHTS ******************************************************************) +(* WEIGHT OF A LOCAL ENVIRONMENT ********************************************) -(* the weight of a local environment *) let rec lw L ≝ match L with [ LSort ⇒ 0 -| LPair L _ V ⇒ lw L + #V +| LPair L _ V ⇒ lw L + #[V] ]. interpretation "weight (local environment)" 'Weight L = (lw L). - -(* the weight of a closure *) -definition cw: lenv → term → ? ≝ λL,T. #L + #T. - -interpretation "weight (closure)" 'Weight L T = (cw L T). - -axiom cw_wf_ind: ∀P:lenv→term→Prop. - (∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → P L1 T1) → P L2 T2) → - ∀L,T. P L T. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/leq.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/leq.ma new file mode 100644 index 000000000..7612bcb85 --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/leq.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Basic-2/grammar/lenv_length.ma". + +(* LOCAL ENVIRONMENT EQUALITY ***********************************************) + +inductive leq: lenv → nat → nat → lenv → Prop ≝ +| leq_sort: ∀d,e. leq (⋆) d e (⋆) +| leq_OO: ∀L1,L2. leq L1 0 0 L2 +| leq_eq: ∀L1,L2,I,V,e. leq L1 0 e L2 → leq (L1. 𝕓{I} V) 0 (e + 1) (L2.𝕓{I} V) +| leq_skip: ∀L1,L2,I1,I2,V1,V2,d,e. + leq L1 d e L2 → leq (L1. 𝕓{I1} V1) (d + 1) e (L2. 𝕓{I2} V2) +. + +interpretation "local environment equality" 'Eq L1 d e L2 = (leq L1 d e L2). + +(* Basic properties *********************************************************) + +lemma leq_refl: ∀d,e,L. L [d, e] ≈ L. +#d elim d -d +[ #e elim e -e // #e #IHe #L elim L -L /2/ +| #d #IHd #e #L elim L -L /2/ +] +qed. + +lemma leq_sym: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → L2 [d, e] ≈ L1. +#L1 #L2 #d #e #H elim H -H L1 L2 d e /2/ +qed. + +lemma leq_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≈ L2 → 0 < d → + ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≈ L2. 𝕓{I2} V2. + +#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2/ +qed. + +(* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/sh.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/sh.ma index e6188a882..bec437a75 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/sh.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/sh.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Ground-2/ground.ma". +include "Ground-2/list.ma". (* SORT HIERARCHY ***********************************************************) 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 2cd284655..309df0b3f 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/term.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/term.ma @@ -25,7 +25,7 @@ inductive term: Type[0] ≝ interpretation "sort (term)" 'Star k = (TSort k). -interpretation "local reference (term)" 'Weight i = (TLRef i). +interpretation "local reference (term)" 'LRef i = (TLRef i). interpretation "term construction (binary)" 'SItem I T1 T2 = (TPair I T1 T2). 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 new file mode 100644 index 000000000..4b4958e00 --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/term_simple.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Basic-2/grammar/term.ma". + +(* SIMPLE (NEUTRAL) TERMS ***************************************************) + +inductive simple: term → Prop ≝ + | simple_sort: ∀k. simple (⋆k) + | simple_lref: ∀i. simple (#i) + | simple_flat: ∀I,V,T. simple (𝕗{I} V. T) +. + +interpretation "simple (term)" 'Simple T = (simple T). + +(* Basic inversion lemmas ***************************************************) + +fact simple_inv_bind_aux: ∀T. 𝕊[T] → ∀J,W,U. T = 𝕓{J} W. U → False. +#T * -T +[ #k #J #W #U #H destruct +| #k #J #W #U #H destruct +| #I #V #T #J #W #U #H destruct +] +qed. + +lemma simple_inv_bind: ∀I,V,T. 𝕊[𝕓{I} V. T] → False. +/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 5d880eb6e..3e7063507 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 @@ -14,9 +14,8 @@ include "Basic-2/grammar/term.ma". -(* WEIGHT *******************************************************************) +(* WEIGHT OF A TERM *********************************************************) -(* the weight of a term *) let rec tw T ≝ match T with [ TSort _ ⇒ 1 | TLRef _ ⇒ 1 @@ -25,6 +24,8 @@ let rec tw T ≝ match T with interpretation "weight (term)" 'Weight T = (tw T). -axiom tw_wf_ind: ∀P:term→Prop. - (∀T2. (∀T1. # T1 < # T2 → P T1) → P T2) → - ∀T. P T. +(* Basic properties *********************************************************) + +axiom tw_wf_ind: ∀R:term→Prop. + (∀T2. (∀T1. #[T1] < #[T2] → R T1) → R T2) → + ∀T. R T. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/thom.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/thom.ma new file mode 100644 index 000000000..660fff5bf --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/thom.ma @@ -0,0 +1,51 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Basic-2/grammar/term_simple.ma". + +(* HOMOMORPHIC TERMS ********************************************************) + +inductive thom: term → term → Prop ≝ + | thom_sort: ∀k. thom (⋆k) (⋆k) + | thom_lref: ∀i. thom (#i) (#i) + | thom_abst: ∀V1,V2,T1,T2. thom (𝕚{Abst} V1. T1) (𝕚{Abst} V2. T2) + | thom_appl: ∀V1,V2,T1,T2. thom T1 T2 → 𝕊[T1] → 𝕊[T2] → + thom (𝕚{Appl} V1. T1) (𝕚{Appl} V2. T2) +. + +interpretation "homomorphic (term)" 'napart T1 T2 = (thom T1 T2). + +(* Basic properties *********************************************************) + +lemma thom_sym: ∀T1,T2. T1 ≈ T2 → T2 ≈ T1. +#T1 #T2 #H elim H -H T1 T2 /2/ +qed. + +lemma thom_refl2: ∀T1,T2. T1 ≈ T2 → T2 ≈ T2. +#T1 #T2 #H elim H -H T1 T2 /2/ +qed. + +lemma thom_refl1: ∀T1,T2. T1 ≈ T2 → T1 ≈ T1. +/3/ qed. + +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. + +lemma simple_thom_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝕊[T2] → 𝕊[T1]. +/3/ qed. + +(* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/names.txt b/matita/matita/contribs/lambda-delta/Basic-2/names.txt index 2a030fb4f..c33d5a8ea 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/names.txt +++ b/matita/matita/contribs/lambda-delta/Basic-2/names.txt @@ -1,9 +1,17 @@ NAMING CONVENTIONS FOR METAVARIABLES +A,B : arity +C,D : candidate of reducibility +E,F,G : reserved: future use H : reserved: transient premise IH : reserved: inductive premise I,J : item K,L : local environment +M,N : reserved: future use +O : reserved: standard library +P,Q : reserved: future use +R : generic predicate (relation) +S : reserved: standard library T,U,V,W: term X,Y,Z : reserved: transient objet denoted by a capital letter diff --git a/matita/matita/contribs/lambda-delta/Basic-2/notation.ma b/matita/matita/contribs/lambda-delta/Basic-2/notation.ma index d4dd5a5de..653365be8 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/notation.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/notation.ma @@ -24,27 +24,27 @@ notation "hvbox( ⋆ term 90 k )" non associative with precedence 90 for @{ 'Star $k }. -notation "hvbox( 𝕚 { I } break (term 90 T1) . break (term 90 T) )" +notation "hvbox( # term 90 k )" + non associative with precedence 90 + for @{ 'LRef $k }. + +notation "hvbox( 𝕚 { I } break term 90 T1 . break term 90 T )" non associative with precedence 90 for @{ 'SItem $I $T1 $T }. -notation "hvbox( 𝕓 { I } break (term 90 T1) . break (term 90 T) )" +notation "hvbox( 𝕓 { I } break term 90 T1 . break term 90 T )" non associative with precedence 90 for @{ 'SBind $I $T1 $T }. -notation "hvbox( 𝕗 { I } break (term 90 T1) . break (term 90 T) )" +notation "hvbox( 𝕗 { I } break term 90 T1 . break term 90 T )" non associative with precedence 90 for @{ 'SFlat $I $T1 $T }. -notation "hvbox( T . break 𝕓 { I } break (term 90 T1) )" +notation "hvbox( T . break 𝕓 { I } break term 90 T1 )" non associative with precedence 89 for @{ 'DBind $T $I $T1 }. -(* -notation "hvbox( | L | )" - non associative with precedence 70 - for @{ 'Length $L }. -*) -notation "hvbox( # term 90 x )" + +notation "hvbox( # [ x ] )" non associative with precedence 90 for @{ 'Weight $x }. @@ -52,12 +52,16 @@ notation "hvbox( # [ x , break y ] )" non associative with precedence 90 for @{ 'Weight $x $y }. -(* Substitution *************************************************************) +notation "hvbox( 𝕊 [ T ] )" + non associative with precedence 45 + for @{ 'Simple $T }. notation "hvbox( T1 break [ d , break e ] ≈ break T2 )" non associative with precedence 45 for @{ 'Eq $T1 $d $e $T2 }. +(* Substitution *************************************************************) + notation "hvbox( ↑ [ d , break e ] break T1 ≡ break T2 )" non associative with precedence 45 for @{ 'RLift $T1 $d $e $T2 }. @@ -76,7 +80,7 @@ notation "hvbox( T1 ⇒ break T2 )" non associative with precedence 45 for @{ 'PRed $T1 $T2 }. -notation "hvbox( L ⊢ break (term 90 T1) ⇒ break T2 )" +notation "hvbox( L ⊢ break term 90 T1 ⇒ break T2 )" non associative with precedence 45 for @{ 'PRed $L $T1 $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 245cadff9..e06b8fa6d 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "Basic-2/grammar/cl_shift.ma". include "Basic-2/reduction/tpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) @@ -63,3 +64,17 @@ lemma cpr_cast: ∀L,V,T1,T2. qed. (* Basic inversion lemmas ***************************************************) + +lemma cpr_inv_lsort: ∀T1,T2. ⋆ ⊢ T1 ⇒ T2 → T1 ⇒ T2. +#T1 #T2 * #T #HT normalize #HT2 +<(tps_inv_refl0 … HT2) -HT2 // +qed. + +(* Basic forward lemmas *****************************************************) + +lemma cpr_shift_fwd: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → L @ T1 ⇒ L @ T2. +#L elim L -L +[ /2/ +| normalize /3/ +]. +qed. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/lcpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/lcpr.ma index 3098a2456..03ed43683 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/lcpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/lcpr.ma @@ -28,8 +28,8 @@ interpretation (* Basic inversion lemmas ***************************************************) -lemma lcpr_inv_item1_aux: ∀L1,L2. L1 ⊢ ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 → - ∃∃K2,V2. K1 ⊢ ⇒ K2 & K2 ⊢ V1 ⇒ V2 & L2 = K2. 𝕓{I} V2. +fact lcpr_inv_item1_aux: ∀L1,L2. L1 ⊢ ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 → + ∃∃K2,V2. K1 ⊢ ⇒ K2 & K2 ⊢ V1 ⇒ V2 & L2 = K2. 𝕓{I} V2. #L1 #L2 * -L1 L2 [ #K1 #I #V1 #H destruct | #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct - K1 I V1 /2 width=5/ 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 ac3ff7bf6..902bc96da 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/ltpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/ltpr.ma @@ -28,8 +28,8 @@ interpretation (* Basic inversion lemmas ***************************************************) -lemma ltpr_inv_item1_aux: ∀L1,L2. L1 ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 → - ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2. +fact ltpr_inv_item1_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 | #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct - K1 I V1 /2 width=5/ 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 8e162bb2c..e6dfc2c1d 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma @@ -52,7 +52,7 @@ qed. (* Basic inversion lemmas ***************************************************) -lemma tpr_inv_sort1_aux: ∀U1,U2. U1 ⇒ U2 → ∀k. U1 = ⋆k → U2 = ⋆k. +fact tpr_inv_sort1_aux: ∀U1,U2. U1 ⇒ U2 → ∀k. U1 = ⋆k → U2 = ⋆k. #U1 #U2 * -U1 U2 [ #k0 #k #H destruct -k0 // | #i #k #H destruct @@ -68,7 +68,7 @@ qed. lemma tpr_inv_sort1: ∀k,U2. ⋆k ⇒ U2 → U2 = ⋆k. /2/ qed. -lemma tpr_inv_lref1_aux: ∀U1,U2. U1 ⇒ U2 → ∀i. U1 = #i → U2 = #i. +fact tpr_inv_lref1_aux: ∀U1,U2. U1 ⇒ U2 → ∀i. U1 = #i → U2 = #i. #U1 #U2 * -U1 U2 [ #k #i #H destruct | #j #i #H destruct -j // @@ -84,12 +84,12 @@ qed. lemma tpr_inv_lref1: ∀i,U2. #i ⇒ U2 → U2 = #i. /2/ qed. -lemma tpr_inv_bind1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 → - (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 & - ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T & - U2 = 𝕚{I} V2. T - )∨ - ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr. +fact tpr_inv_bind1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 → + (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 & + ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T & + U2 = 𝕚{I} V2. T + ) ∨ + ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr. #U1 #U2 * -U1 U2 [ #k #I #V #T #H destruct | #i #I #V #T #H destruct @@ -120,16 +120,16 @@ lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕚{Abbr} V1. T1 ⇒ U2 → elim (tpr_inv_bind1 … H) -H * /3 width=7/ qed. -lemma tpr_inv_appl1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,U0. U1 = 𝕚{Appl} V1. U0 → - ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 & - U2 = 𝕚{Appl} V2. T2 - | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 & - U0 = 𝕚{Abst} W. T1 & - U2 = 𝕓{Abbr} V2. T2 - | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 & - ↑[0,1] V2 ≡ V & - U0 = 𝕚{Abbr} W1. T1 & - U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2. +fact tpr_inv_appl1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,U0. U1 = 𝕚{Appl} V1. U0 → + ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 & + U2 = 𝕚{Appl} V2. T2 + | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 & + U0 = 𝕚{Abst} W. T1 & + U2 = 𝕓{Abbr} V2. T2 + | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 & + ↑[0,1] V2 ≡ V & + U0 = 𝕚{Abbr} W1. T1 & + U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2. #U1 #U2 * -U1 U2 [ #k #V #T #H destruct | #i #V #T #H destruct @@ -155,9 +155,9 @@ lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕚{Appl} V1. U0 ⇒ U2 → U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2. /2/ qed. -lemma tpr_inv_cast1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Cast} V1. T1 → - (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Cast} V2. T2) - ∨ T1 ⇒ U2. +fact tpr_inv_cast1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Cast} V1. T1 → + (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Cast} V2. T2) + ∨ T1 ⇒ U2. #U1 #U2 * -U1 U2 [ #k #V #T #H destruct | #i #V #T #H destruct @@ -193,11 +193,11 @@ lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 → ] qed. -lemma tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i → - ∨∨ T1 = #i - | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i & - T1 = 𝕚{Abbr} V. T - | ∃∃V,T. T ⇒ #i & T1 = 𝕚{Cast} V. T. +fact tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i → + ∨∨ T1 = #i + | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i & + T1 = 𝕚{Abbr} V. T + | ∃∃V,T. T ⇒ #i & T1 = 𝕚{Cast} V. T. #T1 #T2 * -T1 T2 [ #k #i #H destruct | #j #i /2/ 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 f3afe6f21..a748416f0 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 @@ -96,8 +96,8 @@ qed. (* Advanced inversion lemmas ************************************************) -lemma tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abst} V1. T1 → - ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2. +fact tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abst} V1. T1 → + ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2. #U1 #U2 * -U1 U2 [ #k #V #T #H destruct | #i #V #T #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 d0ae3fa90..aa55eb8b5 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 @@ -20,15 +20,15 @@ include "Basic-2/reduction/tpr_tps.ma". (* Confluence lemmas ********************************************************) -lemma tpr_conf_sort_sort: ∀k. ∃∃X. ⋆k ⇒ X & ⋆k ⇒ X. +fact tpr_conf_sort_sort: ∀k. ∃∃X. ⋆k ⇒ X & ⋆k ⇒ X. /2/ qed. -lemma tpr_conf_lref_lref: ∀i. ∃∃X. #i ⇒ X & #i ⇒ X. +fact tpr_conf_lref_lref: ∀i. ∃∃X. #i ⇒ X & #i ⇒ X. /2/ qed. -lemma tpr_conf_flat_flat: +fact tpr_conf_flat_flat: ∀I,V0,V1,T0,T1,V2,T2. ( - ∀X0:term. #X0 < #V0 + #T0 + 1 → + ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → ∃∃X. X1 ⇒ X & X2 ⇒ X ) → @@ -39,9 +39,9 @@ elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 elim (IH … HT01 … HT02) -HT01 HT02 /3 width=5/ qed. -lemma tpr_conf_flat_beta: +fact tpr_conf_flat_beta: ∀V0,V1,T1,V2,W0,U0,T2. ( - ∀X0:term. #X0 < #V0 + (#W0 + #U0 + 1) + 1 → + ∀X0:term. #[X0] < #[V0] + (#[W0] + #[U0] + 1) + 1 → ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → ∃∃X. X1 ⇒ X & X2 ⇒ X ) → @@ -54,9 +54,9 @@ elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 elim (IH … HT02 … HU01) -HT02 HU01 IH /3 width=5/ qed. -lemma tpr_conf_flat_theta: +fact tpr_conf_flat_theta: ∀V0,V1,T1,V2,V,W0,W2,U0,U2. ( - ∀X0:term. #X0 < #V0 + (#W0 + #U0 + 1) + 1 → + ∀X0:term. #[X0] < #[V0] + (#[W0] + #[U0] + 1) + 1 → ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → ∃∃X. X1 ⇒ X & X2 ⇒ X ) → @@ -91,9 +91,9 @@ elim (tpr_inv_abbr1 … H) -H * ] qed. -lemma tpr_conf_flat_cast: +fact tpr_conf_flat_cast: ∀X2,V0,V1,T0,T1. ( - ∀X0:term. #X0 < #V0 + # T0 + 1 → + ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → ∃∃X. X1 ⇒ X & X2 ⇒ X ) → @@ -103,9 +103,9 @@ lemma tpr_conf_flat_cast: elim (IH … HT01 … HT02) -HT01 HT02 IH /3/ qed. -lemma tpr_conf_beta_beta: +fact tpr_conf_beta_beta: ∀W0:term. ∀V0,V1,T0,T1,V2,T2. ( - ∀X0:term. #X0 < #V0 + (#W0 + #T0 + 1) + 1 → + ∀X0:term. #[X0] < #[V0] + (#[W0] + #[T0] + 1) + 1 → ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → ∃∃X. X1 ⇒ X & X2 ⇒ X ) → @@ -116,9 +116,9 @@ elim (IH … HV01 … HV02) -HV01 HV02 // elim (IH … HT01 … HT02) -HT01 HT02 IH /3 width=5/ qed. -lemma tpr_conf_delta_delta: +fact tpr_conf_delta_delta: ∀I1,V0,V1,T0,T1,TT1,V2,T2,TT2. ( - ∀X0:term. #X0 < #V0 +#T0 + 1→ + ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → ∃∃X. X1 ⇒ X & X2 ⇒ X ) → @@ -135,9 +135,9 @@ elim (tps_conf … 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. -lemma tpr_conf_delta_zeta: +fact tpr_conf_delta_zeta: ∀X2,V0,V1,T0,T1,TT1,T2. ( - ∀X0:term. #X0 < #V0 +#T0 + 1→ + ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → ∃∃X. X1 ⇒ X & X2 ⇒ X ) → @@ -151,9 +151,9 @@ lapply (tw_lift … HTT20) -HTT20 #HTT20 elim (IH … HTX2 … HTT2) -HTX2 HTT2 IH /3/ qed. -lemma tpr_conf_theta_theta: +fact tpr_conf_theta_theta: ∀VV1,V0,V1,W0,W1,T0,T1,V2,VV2,W2,T2. ( - ∀X0:term. #X0 < #V0 + (#W0 + #T0 + 1) + 1 → + ∀X0:term. #[X0] < #[V0] + (#[W0] + #[T0] + 1) + 1 → ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → ∃∃X. X1 ⇒ X & X2 ⇒ X ) → @@ -170,9 +170,9 @@ lapply (tpr_lift … HV2 … HVV2 … HVV) -HV2 HVV2 HVV #HVV2 @ex2_1_intro [2,3: @tpr_bind |1:skip ] /2 width=5/ (**) (* /4 width=5/ is too slow *) qed. -lemma tpr_conf_zeta_zeta: +fact tpr_conf_zeta_zeta: ∀V0:term. ∀X2,TT0,T0,T1,T2. ( - ∀X0:term. #X0 < #V0 + #TT0 + 1 → + ∀X0:term. #[X0] < #[V0] + #[TT0] + 1 → ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → ∃∃X. X1 ⇒ X & X2 ⇒ X ) → @@ -185,9 +185,9 @@ lapply (tw_lift … HTT20) -HTT20 #HTT20 elim (IH … HT01 … HTX2) -HT01 HTX2 IH /2/ qed. -lemma tpr_conf_tau_tau: +fact tpr_conf_tau_tau: ∀V0,T0:term. ∀X2,T1. ( - ∀X0:term. #X0 < #V0 + #T0 + 1 → + ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → ∃∃X. X1 ⇒ X & X2 ⇒ X ) → @@ -199,9 +199,10 @@ qed. (* Confluence ***************************************************************) -lemma tpr_conf_aux: +fact tpr_conf_aux: ∀Y0:term. ( - ∀X0:term. #X0 < #Y0 → ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → + ∀X0:term. #[X0] < #[Y0] → + ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → ∃∃X. X1 ⇒ X & X2 ⇒ X ) → ∀X0,X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → X0 = Y0 → 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 a6752fac6..149fabde3 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma @@ -12,11 +12,12 @@ (* *) (**************************************************************************) -include "Basic-2/substitution/leq.ma". +include "Basic-2/grammar/leq.ma". include "Basic-2/substitution/lift.ma". (* DROPPING *****************************************************************) +(* Basic-1: includes: drop_skip_bind *) inductive drop: lenv → nat → nat → lenv → Prop ≝ | drop_sort: ∀d,e. drop (⋆) d e (⋆) | drop_comp: ∀L1,L2,I,V. drop L1 0 0 L2 → drop (L1. 𝕓{I} V) 0 0 (L2. 𝕓{I} V) @@ -30,7 +31,7 @@ interpretation "dropping" 'RDrop L1 d e L2 = (drop L1 d e L2). (* Basic inversion lemmas ***************************************************) -lemma drop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 → L1 = L2. +fact drop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 → L1 = L2. #d #e #L1 #L2 #H elim H -H d e L1 L2 [ // | #L1 #L2 #I #V #_ #IHL12 #H1 #H2 @@ -42,11 +43,12 @@ lemma drop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 ] qed. +(* Basic-1: was: drop_gen_refl *) lemma drop_inv_refl: ∀L1,L2. ↓[0, 0] L1 ≡ L2 → L1 = L2. /2 width=5/ qed. -lemma drop_inv_sort1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → L1 = ⋆ → - L2 = ⋆. +fact drop_inv_sort1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → L1 = ⋆ → + L2 = ⋆. #d #e #L1 #L2 * -d e L1 L2 [ // | #L1 #L2 #I #V #_ #H destruct @@ -55,13 +57,14 @@ lemma drop_inv_sort1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → L1 = ⋆ → ] qed. +(* Basic-1: was: drop_gen_sort *) lemma drop_inv_sort1: ∀d,e,L2. ↓[d, e] ⋆ ≡ L2 → L2 = ⋆. /2 width=5/ qed. -lemma drop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → - ∀K,I,V. L1 = K. 𝕓{I} V → - (e = 0 ∧ L2 = K. 𝕓{I} V) ∨ - (0 < e ∧ ↓[d, e - 1] K ≡ L2). +fact drop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → + ∀K,I,V. L1 = K. 𝕓{I} V → + (e = 0 ∧ L2 = K. 𝕓{I} V) ∨ + (0 < e ∧ ↓[d, e - 1] K ≡ L2). #d #e #L1 #L2 * -d e L1 L2 [ #d #e #_ #K #I #V #H destruct | #L1 #L2 #I #V #HL12 #H #K #J #W #HX destruct -L1 I V @@ -76,6 +79,7 @@ lemma drop_inv_O1: ∀e,K,I,V,L2. ↓[0, e] K. 𝕓{I} V ≡ L2 → (0 < e ∧ ↓[0, e - 1] K ≡ L2). /2/ qed. +(* Basic-1: was: drop_gen_drop *) lemma drop_inv_drop1: ∀e,K,I,V,L2. ↓[0, e] K. 𝕓{I} V ≡ L2 → 0 < e → ↓[0, e - 1] K ≡ L2. #e #K #I #V #L2 #H #He @@ -83,11 +87,11 @@ elim (drop_inv_O1 … H) -H * // #H destruct -e; elim (lt_refl_false … He) qed. -lemma drop_inv_skip1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → - ∀I,K1,V1. L1 = K1. 𝕓{I} V1 → - ∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 & - ↑[d - 1, e] V2 ≡ V1 & - L2 = K2. 𝕓{I} V2. +fact drop_inv_skip1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → + ∀I,K1,V1. L1 = K1. 𝕓{I} V1 → + ∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 & + ↑[d - 1, e] V2 ≡ V1 & + L2 = K2. 𝕓{I} V2. #d #e #L1 #L2 * -d e L1 L2 [ #d #e #_ #I #K #V #H destruct | #L1 #L2 #I #V #_ #H elim (lt_refl_false … H) @@ -97,17 +101,18 @@ lemma drop_inv_skip1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → ] qed. +(* Basic-1: was: drop_gen_skip_l *) lemma drop_inv_skip1: ∀d,e,I,K1,V1,L2. ↓[d, e] K1. 𝕓{I} V1 ≡ L2 → 0 < d → ∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 & ↑[d - 1, e] V2 ≡ V1 & L2 = K2. 𝕓{I} V2. /2/ qed. -lemma drop_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → - ∀I,K2,V2. L2 = K2. 𝕓{I} V2 → - ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & - ↑[d - 1, e] V2 ≡ V1 & - L1 = K1. 𝕓{I} V1. +fact drop_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → + ∀I,K2,V2. L2 = K2. 𝕓{I} V2 → + ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & + ↑[d - 1, e] V2 ≡ V1 & + L1 = K1. 𝕓{I} V1. #d #e #L1 #L2 * -d e L1 L2 [ #d #e #_ #I #K #V #H destruct | #L1 #L2 #I #V #_ #H elim (lt_refl_false … H) @@ -117,6 +122,7 @@ lemma drop_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → ] qed. +(* Basic-1: was: drop_gen_skip_r *) lemma drop_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. @@ -124,6 +130,7 @@ lemma drop_inv_skip2: ∀d,e,I,L1,K2,V2. ↓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < (* Basic properties *********************************************************) +(* Basic-1: was by definition: drop_refl *) lemma drop_refl: ∀L. ↓[0, 0] L ≡ L. #L elim L -L /2/ qed. @@ -159,6 +166,7 @@ qed. (* Basic forvard lemmas *****************************************************) +(* Basic-1: was: drop_S *) lemma drop_fwd_drop2: ∀L1,I2,K2,V2,e. ↓[O, e] L1 ≡ K2. 𝕓{I2} V2 → ↓[O, e + 1] L1 ≡ K2. #L1 elim L1 -L1 @@ -194,3 +202,12 @@ lemma drop_fwd_O1_length: ∀L1,L2,e. ↓[0, e] L1 ≡ L2 → |L2| = |L1| - e. ] ] qed. + +(* Basic-1: removed theorems 18: + 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 +*) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop_drop.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop_drop.ma index 03a8e31dd..297b21f11 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop_drop.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop_drop.ma @@ -19,6 +19,7 @@ include "Basic-2/substitution/drop.ma". (* Main properties **********************************************************) +(* Basic-1: was: drop_mono *) theorem drop_mono: ∀d,e,L,L1. ↓[d, e] L ≡ L1 → ∀L2. ↓[d, e] L ≡ L2 → L1 = L2. #d #e #L #L1 #H elim H -H d e L L1 @@ -36,6 +37,7 @@ theorem drop_mono: ∀d,e,L,L1. ↓[d, e] L ≡ L1 → ] qed. +(* Basic-1: was: drop_conf_ge *) theorem drop_conf_ge: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 + e1 ≤ e2 → ↓[0, e2 - e1] L1 ≡ L2. @@ -55,6 +57,7 @@ theorem drop_conf_ge: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → ] qed. +(* Basic-1: was: drop_conf_lt *) theorem drop_conf_lt: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → ∀e2,K2,I,V2. ↓[0, e2] L ≡ K2. 𝕓{I} V2 → e2 < d1 → let d ≝ d1 - e2 - 1 in @@ -76,6 +79,7 @@ theorem drop_conf_lt: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → ] qed. +(* Basic-1: was: drop_trans_le *) theorem drop_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → ∀e2,L2. ↓[0, e2] L ≡ L2 → e2 ≤ d1 → ∃∃L0. ↓[0, e2] L1 ≡ L0 & ↓[d1 - e2, e1] L0 ≡ L2. @@ -99,6 +103,7 @@ theorem drop_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → ] qed. +(* Basic-1: was: drop_trans_ge *) theorem drop_trans_ge: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 ≤ e2 → ↓[0, e1 + e2] L1 ≡ L2. #d1 #e1 #L1 #L #H elim H -H d1 e1 L1 L @@ -121,5 +126,6 @@ theorem drop_trans_ge_comm: ∀d1,e1,e2,L1,L2,L. #e1 #e1 #e2 >commutative_plus /2 width=5/ qed. +(* Basic-1: was: drop_conf_rev *) axiom drop_div: ∀e1,L1,L. ↓[0, e1] L1 ≡ L → ∀e2,L2. ↓[0, e2] L2 ≡ L → ∃∃L0. ↓[0, e1] L0 ≡ L2 & ↓[e1, e2] L0 ≡ L1. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/leq.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/leq.ma deleted file mode 100644 index 7612bcb85..000000000 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/leq.ma +++ /dev/null @@ -1,48 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "Basic-2/grammar/lenv_length.ma". - -(* LOCAL ENVIRONMENT EQUALITY ***********************************************) - -inductive leq: lenv → nat → nat → lenv → Prop ≝ -| leq_sort: ∀d,e. leq (⋆) d e (⋆) -| leq_OO: ∀L1,L2. leq L1 0 0 L2 -| leq_eq: ∀L1,L2,I,V,e. leq L1 0 e L2 → leq (L1. 𝕓{I} V) 0 (e + 1) (L2.𝕓{I} V) -| leq_skip: ∀L1,L2,I1,I2,V1,V2,d,e. - leq L1 d e L2 → leq (L1. 𝕓{I1} V1) (d + 1) e (L2. 𝕓{I2} V2) -. - -interpretation "local environment equality" 'Eq L1 d e L2 = (leq L1 d e L2). - -(* Basic properties *********************************************************) - -lemma leq_refl: ∀d,e,L. L [d, e] ≈ L. -#d elim d -d -[ #e elim e -e // #e #IHe #L elim L -L /2/ -| #d #IHd #e #L elim L -L /2/ -] -qed. - -lemma leq_sym: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → L2 [d, e] ≈ L1. -#L1 #L2 #d #e #H elim H -H L1 L2 d e /2/ -qed. - -lemma leq_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≈ L2 → 0 < d → - ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≈ L2. 𝕓{I2} V2. - -#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2/ -qed. - -(* Basic inversion lemmas ***************************************************) 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 7526f0c45..3f9eadf43 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma @@ -77,20 +77,20 @@ qed. (* Basic forward lemmas *****************************************************) -lemma tw_lift: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → #T1 = #T2. +lemma tw_lift: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → #[T1] = #[T2]. #d #e #T1 #T2 #H elim H -d e T1 T2; normalize // qed. (* Basic inversion lemmas ***************************************************) -lemma lift_inv_refl_aux: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → e = 0 → T1 = T2. +fact lift_inv_refl_aux: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → e = 0 → T1 = T2. #d #e #T1 #T2 #H elim H -H d e T1 T2 /3/ qed. lemma lift_inv_refl: ∀d,T1,T2. ↑[d, 0] T1 ≡ T2 → T1 = T2. /2/ qed. -lemma lift_inv_sort1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T1 = ⋆k → T2 = ⋆k. +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 // [ #i #d #e #_ #k #H destruct | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct @@ -101,8 +101,8 @@ qed. lemma lift_inv_sort1: ∀d,e,T2,k. ↑[d,e] ⋆k ≡ T2 → T2 = ⋆k. /2 width=5/ qed. -lemma lift_inv_lref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T1 = #i → - (i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)). +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)). #d #e #T1 #T2 * -d e T1 T2 [ #k #d #e #i #H destruct | #j #d #e #Hj #i #Hi destruct /3/ @@ -128,10 +128,10 @@ lemma lift_inv_lref1_ge: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → d ≤ i → T2 = #( elim (lt_refl_false … Hdd) qed. -lemma lift_inv_bind1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → - ∀I,V1,U1. T1 = 𝕓{I} V1.U1 → - ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 & - T2 = 𝕓{I} V2. U2. +fact lift_inv_bind1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → + ∀I,V1,U1. T1 = 𝕓{I} V1.U1 → + ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 & + T2 = 𝕓{I} V2. U2. #d #e #T1 #T2 * -d e T1 T2 [ #k #d #e #I #V1 #U1 #H destruct | #i #d #e #_ #I #V1 #U1 #H destruct @@ -146,10 +146,10 @@ lemma lift_inv_bind1: ∀d,e,T2,I,V1,U1. ↑[d,e] 𝕓{I} V1. U1 ≡ T2 → T2 = 𝕓{I} V2. U2. /2/ qed. -lemma lift_inv_flat1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → - ∀I,V1,U1. T1 = 𝕗{I} V1.U1 → - ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 & - T2 = 𝕗{I} V2. U2. +fact lift_inv_flat1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → + ∀I,V1,U1. T1 = 𝕗{I} V1.U1 → + ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 & + T2 = 𝕗{I} V2. U2. #d #e #T1 #T2 * -d e T1 T2 [ #k #d #e #I #V1 #U1 #H destruct | #i #d #e #_ #I #V1 #U1 #H destruct @@ -164,7 +164,7 @@ lemma lift_inv_flat1: ∀d,e,T2,I,V1,U1. ↑[d,e] 𝕗{I} V1. U1 ≡ T2 → T2 = 𝕗{I} V2. U2. /2/ qed. -lemma lift_inv_sort2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k. +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 // [ #i #d #e #_ #k #H destruct | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct @@ -175,8 +175,8 @@ qed. lemma lift_inv_sort2: ∀d,e,T1,k. ↑[d,e] T1 ≡ ⋆k → T1 = ⋆k. /2 width=5/ qed. -lemma 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)). +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)). #d #e #T1 #T2 * -d e T1 T2 [ #k #d #e #i #H destruct | #j #d #e #Hj #i #Hi destruct /3/ @@ -202,10 +202,10 @@ lemma lift_inv_lref2_ge: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → d + e ≤ i → T1 elim (plus_lt_false … Hdd) qed. -lemma lift_inv_bind2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → - ∀I,V2,U2. T2 = 𝕓{I} V2.U2 → - ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 & - T1 = 𝕓{I} V1. U1. +fact lift_inv_bind2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → + ∀I,V2,U2. T2 = 𝕓{I} V2.U2 → + ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 & + T1 = 𝕓{I} V1. U1. #d #e #T1 #T2 * -d e T1 T2 [ #k #d #e #I #V2 #U2 #H destruct | #i #d #e #_ #I #V2 #U2 #H destruct @@ -220,10 +220,10 @@ lemma lift_inv_bind2: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡ 𝕓{I} V2. U2 → T1 = 𝕓{I} V1. U1. /2/ qed. -lemma lift_inv_flat2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → - ∀I,V2,U2. T2 = 𝕗{I} V2.U2 → - ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 & - T1 = 𝕗{I} V1. U1. +fact lift_inv_flat2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → + ∀I,V2,U2. T2 = 𝕗{I} V2.U2 → + ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 & + T1 = 𝕗{I} V1. U1. #d #e #T1 #T2 * -d e T1 T2 [ #k #d #e #I #V2 #U2 #H destruct | #i #d #e #_ #I #V2 #U2 #H destruct 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 fc0851097..d2e71ed7d 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma @@ -113,11 +113,11 @@ qed. (* Basic inversion lemmas ***************************************************) -lemma tps_inv_lref1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → ∀i. T1 = #i → - T2 = #i ∨ - ∃∃K,V. d ≤ i & i < d + e & - ↓[O, i] L ≡ K. 𝕓{Abbr} V & - ↑[O, i + 1] V ≡ T2. +fact tps_inv_lref1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → ∀i. T1 = #i → + T2 = #i ∨ + ∃∃K,V. d ≤ i & i < d + e & + ↓[O, i] L ≡ K. 𝕓{Abbr} V & + ↑[O, i + 1] V ≡ T2. #L #T1 #T2 #d #e * -L T1 T2 d e [ #L #k #d #e #i #H destruct | /2/ @@ -134,11 +134,11 @@ lemma tps_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ≫ T2 → ↑[O, i + 1] V ≡ T2. /2/ qed. -lemma tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 → - ∀I,V1,T1. U1 = 𝕓{I} V1. T1 → - ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & - L. 𝕓{I} V1 ⊢ T1 [d + 1, e] ≫ T2 & - U2 = 𝕓{I} V2. T2. +fact tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 → + ∀I,V1,T1. U1 = 𝕓{I} V1. T1 → + ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & + L. 𝕓{I} V1 ⊢ T1 [d + 1, e] ≫ T2 & + U2 = 𝕓{I} V2. T2. #d #e #L #U1 #U2 * -d e L U1 U2 [ #L #k #d #e #I #V1 #T1 #H destruct | #L #i #d #e #I #V1 #T1 #H destruct @@ -154,10 +154,10 @@ lemma tps_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫ U2 → U2 = 𝕓{I} V2. T2. /2/ qed. -lemma tps_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 → - ∀I,V1,T1. U1 = 𝕗{I} V1. T1 → - ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L ⊢ T1 [d, e] ≫ T2 & - U2 = 𝕗{I} V2. T2. +fact tps_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 → + ∀I,V1,T1. U1 = 𝕗{I} V1. T1 → + ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L ⊢ T1 [d, e] ≫ T2 & + U2 = 𝕗{I} V2. T2. #d #e #L #U1 #U2 * -d e L U1 U2 [ #L #k #d #e #I #V1 #T1 #H destruct | #L #i #d #e #I #V1 #T1 #H destruct @@ -171,3 +171,18 @@ lemma tps_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 & U2 = 𝕗{I} V2. T2. /2/ qed. + +fact tps_inv_refl0_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → e = 0 → T1 = T2. +#L #T1 #T2 #d #e #H elim H -H L T1 T2 d e +[ // +| // +| #L #K #V #W #i #d #e #Hdi #Hide #_ #_ #H destruct -e; + lapply (le_to_lt_to_lt … Hdi … Hide) -Hdi Hide (commutative_plus p) (le_O_to_eq_O … H) -H // +| #b #IHb #c elim c -c // + #c #_ #a #Hcb + lapply (le_S_S_to_le … Hcb) -Hcb #Hcb + minus_plus @eq_f2 /2/ +qed. + +lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b. +#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2/ +qed. + +lemma arith_c1: ∀a,b,c1. a + c1 - (b + c1) = a - b. +// qed. + +lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b. +#x #a #b #c1 >plus_plus_comm_23 // +qed. + +lemma arith_d1: ∀a,b,c1. c1 ≤ b → a + c1 + (b - c1) = a + b. +/2/ qed. + +lemma arith_e2: ∀a,c1,c2. a ≤ c1 → c1 + c2 - (c1 - a + c2) = a. +/3/ qed. + +lemma arith_f1: ∀a,b,c1. a + b ≤ c1 → c1 - (c1 - a - b) = a + b. +#a #b #c1 #H >minus_plus minus_plus >minus_plus @monotonic_le_plus_r @monotonic_le_minus_l // +qed. diff --git a/matita/matita/contribs/lambda-delta/Ground-2/ground.ma b/matita/matita/contribs/lambda-delta/Ground-2/ground.ma deleted file mode 100644 index 11b2a8d92..000000000 --- a/matita/matita/contribs/lambda-delta/Ground-2/ground.ma +++ /dev/null @@ -1,185 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "arithmetics/nat.ma". -include "Ground-2/xoa_props.ma". - -(* ARITHMETICAL PROPERTIES **************************************************) - -lemma plus_S_eq_O_false: ∀n,m. n + S m = 0 → False. -#n #m (commutative_plus p) (le_O_to_eq_O … H) -H // -| #b #IHb #c elim c -c // - #c #_ #a #Hcb - lapply (le_S_S_to_le … Hcb) -Hcb #Hcb - minus_plus @eq_f2 /2/ -qed. - -lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b. -#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2/ -qed. - -lemma arith_c1: ∀a,b,c1. a + c1 - (b + c1) = a - b. -// qed. - -lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b. -#x #a #b #c1 >plus_plus_comm_23 // -qed. - -lemma arith_d1: ∀a,b,c1. c1 ≤ b → a + c1 + (b - c1) = a + b. -/2/ qed. - -lemma arith_e2: ∀a,c1,c2. a ≤ c1 → c1 + c2 - (c1 - a + c2) = a. -/3/ qed. - -lemma arith_f1: ∀a,b,c1. a + b ≤ c1 → c1 - (c1 - a - b) = a + b. -#a #b #c1 #H >minus_plus minus_plus >minus_plus @monotonic_le_plus_r @monotonic_le_minus_l // -qed. diff --git a/matita/matita/contribs/lambda-delta/Ground-2/list.ma b/matita/matita/contribs/lambda-delta/Ground-2/list.ma new file mode 100644 index 000000000..1b64bacce --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Ground-2/list.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "Ground-2/arith.ma". +include "Ground-2/notation.ma". + +(* LISTS ********************************************************************) + +inductive list (A:Type[0]) : Type[0] := + | nil : list A + | cons: A -> list A -> list A. + +interpretation "nil (list)" 'Nil = (nil ?). + +interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl). + +let rec append A (l1: list A) l2 on l1 ≝ + match l1 with + [ nil ⇒ l2 + | cons hd tl ⇒ hd :: append A tl l2 + ]. + +interpretation "append (list)" 'Append l1 l2 = (append ? l1 l2). diff --git a/matita/matita/contribs/lambda-delta/Ground-2/notation.ma b/matita/matita/contribs/lambda-delta/Ground-2/notation.ma new file mode 100644 index 000000000..dab6b4982 --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Ground-2/notation.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +(* Lists ********************************************************************) + +notation "hvbox( hd break :: tl )" + right associative with precedence 47 + for @{'Cons $hd $tl}. + +notation "hvbox( l1 break @ l2)" + right associative with precedence 47 + for @{'Append $l1 $l2 }. diff --git a/matita/matita/contribs/lambda-delta/Makefile b/matita/matita/contribs/lambda-delta/Makefile index 978291c7d..6bf2516d4 100644 --- a/matita/matita/contribs/lambda-delta/Makefile +++ b/matita/matita/contribs/lambda-delta/Makefile @@ -5,43 +5,56 @@ XOA = xoa.native CONF = Ground-2/xoa.conf.xml TARGETS = Ground-2/xoa_natation.ma Ground-2/xoa.ma +PACKAGES = Ground-2 Basic-2 + all: +# xoa ######################################################################## + xoa: $(TARGETS) $(TARGETS): $(CONF) @echo " EXEC $(XOA) $(CONF)" $(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) $(CONF) -stats: MAS = $(shell find -name "*.ma") +# stats ###################################################################### + +stats: $(PACKAGES:%=%.stats) -stats: CHARS = $(shell cat $(MAS) | wc -c) +%.stats: MAS = $(shell find $* -name "*.ma") -stats: +%.stats: CHARS = $(shell cat $(MAS) | wc -c) + +%.stats: + @printf '\e[1;40;37m' + @printf '%-15s %-42s' 'Statistics for:' $* + @printf '\e[0m\n' @printf '\e[1;40;35m' @printf '%-8s %6i' Chars $(CHARS) @printf ' %-8s %5i' Lines `cat $(MAS) | wc -l` @printf ' %-6s %3i' Pages `echo $$(($(CHARS) / 5120))` + @printf ' %-10s' '' @printf '\e[0m\n' @printf '\e[1;40;36m' @printf '%-8s %6i' Sources `ls $(MAS) | wc -l` - @printf ' %-27s' '' + @printf ' %-40s' '' # @printf ' %-8s %5i' Objs `ls *.vo | wc -l` # @printf ' %-6s %3i' Files `ls *.v | wc -l` @printf '\e[0m\n' @printf '\e[1;40;32m' @printf '%-8s %6i' Theorems `grep theorem $(MAS) | wc -l` @printf ' %-8s %5i' Lemmas `grep lemma $(MAS) | wc -l` - @printf ' %-6s %3i' Proofs `grep qed $(MAS) | wc -l` -# @printf ' %-9s %3i' Generated `grep Derive *.v | wc -l` + @printf ' %-6s %3i' Facts `grep fact $(MAS) | wc -l` + @printf ' %-6s %3i' Proofs `grep qed $(MAS) | wc -l` @printf '\e[0m\n' @printf '\e[1;40;33m' @printf '%-8s %6i' Defs `grep "definition\|let rec\|inductive\|record" $(MAS) | wc -l` - @printf ' %-27s' '' + @printf ' %-40s' '' # @printf ' %-8s %5i' Local `grep "Local" *.v | wc -l` @printf '\e[0m\n' @printf '\e[1;40;31m' @printf '%-8s %6i' Axioms `grep axiom $(MAS) | wc -l` @printf ' %-8s %5i' Comments `grep "(\*[^*]*$$" $(MAS) | wc -l` @printf ' %-6s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l` + @printf ' %-10s' '' @printf '\e[0m\n'