From c60524dec7ace912c416a90d6b926bee8553250b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 26 Oct 2014 19:07:45 +0000 Subject: [PATCH] - some renaming according to the written version of basic_2 - more destructing lemmas invoked in place of buggy destructs --- .../lambdadelta/apps_2/web/apps_2.ldw.xml | 32 +- .../basic_2/computation/cprs_lift.ma | 8 +- .../lambdadelta/basic_2/computation/cpxs.ma | 24 +- .../basic_2/computation/cpxs_cpxs.ma | 2 +- .../basic_2/computation/cpxs_lift.ma | 32 +- .../computation/{cpxs_leq.ma => cpxs_lreq.ma} | 6 +- .../basic_2/computation/cpxs_tsts.ma | 12 +- .../lambdadelta/basic_2/computation/csx.ma | 8 +- .../basic_2/computation/csx_lift.ma | 14 +- .../basic_2/computation/csx_tsts_vector.ma | 6 +- .../basic_2/computation/fpbg_fpbs.ma | 4 +- .../basic_2/computation/fpbg_lift.ma | 2 +- .../basic_2/computation/fpbs_lift.ma | 12 +- .../basic_2/computation/fsb_csx.ma | 6 +- .../lambdadelta/basic_2/computation/gcp.ma | 16 +- .../basic_2/computation/gcp_aaa.ma | 8 +- .../lambdadelta/basic_2/computation/gcp_cr.ma | 12 +- .../lambdadelta/basic_2/computation/lcosx.ma | 46 +-- .../basic_2/computation/lcosx_cpx.ma | 34 +- .../basic_2/computation/lpxs_lleq.ma | 58 +-- .../basic_2/computation/lsubc_drop.ma | 28 +- .../basic_2/computation/lsubc_drops.ma | 2 +- .../lambdadelta/basic_2/computation/lsx.ma | 70 ++-- .../basic_2/computation/lsx_alt.ma | 78 ++-- .../basic_2/computation/lsx_csx.ma | 22 +- .../basic_2/computation/lsx_drop.ma | 54 +-- .../basic_2/computation/lsx_lpx.ma | 38 +- .../basic_2/computation/lsx_lpxs.ma | 30 +- .../lambdadelta/basic_2/computation/scpds.ma | 18 +- .../basic_2/computation/scpds_aaa.ma | 4 +- .../basic_2/computation/scpds_lift.ma | 12 +- .../basic_2/computation/scpds_scpds.ma | 70 ++-- .../lambdadelta/basic_2/dynamic/lsubsv.ma | 52 +-- .../basic_2/dynamic/lsubsv_lstas.ma | 58 +-- .../basic_2/dynamic/lsubsv_lsuba.ma | 4 +- .../basic_2/dynamic/lsubsv_scpds.ma | 8 +- .../lambdadelta/basic_2/dynamic/lsubsv_snv.ma | 4 +- .../lambdadelta/basic_2/dynamic/shnv.ma | 24 +- .../lambdadelta/basic_2/dynamic/snv.ma | 22 +- .../lambdadelta/basic_2/dynamic/snv_aaa.ma | 10 +- .../lambdadelta/basic_2/dynamic/snv_da_lpr.ma | 42 +- .../lambdadelta/basic_2/dynamic/snv_lift.ma | 46 +-- .../lambdadelta/basic_2/dynamic/snv_lpr.ma | 28 +- .../lambdadelta/basic_2/dynamic/snv_lstas.ma | 30 +- .../basic_2/dynamic/snv_lstas_lpr.ma | 84 ++-- .../basic_2/dynamic/snv_preserve.ma | 30 +- .../lambdadelta/basic_2/dynamic/snv_scpes.ma | 116 +++--- .../basic_2/equivalence/cpcs_cpcs.ma | 16 +- .../lambdadelta/basic_2/equivalence/scpes.ma | 18 +- .../basic_2/equivalence/scpes_aaa.ma | 4 +- .../basic_2/equivalence/scpes_cpcs.ma | 20 +- .../basic_2/equivalence/scpes_scpes.ma | 48 +-- .../basic_2/examples/ex_cpr_omega.ma | 4 +- .../basic_2/examples/ex_fpbg_refl.ma | 4 +- .../basic_2/examples/ex_snv_eta.ma | 12 +- .../lambdadelta/basic_2/grammar/aarity.ma | 20 +- .../lambdadelta/basic_2/grammar/item.ma | 6 + .../lambdadelta/basic_2/grammar/lenv.ma | 6 +- .../basic_2/grammar/lenv_append.ma | 18 +- .../basic_2/grammar/lenv_length.ma | 16 +- .../lambdadelta/basic_2/grammar/leq.ma | 192 --------- .../lambdadelta/basic_2/grammar/lreq.ma | 192 +++++++++ .../grammar/{leq_leq.ma => lreq_lreq.ma} | 42 +- .../lambdadelta/basic_2/grammar/term.ma | 12 +- .../lambdadelta/basic_2/multiple/cpys.ma | 116 +++--- .../lambdadelta/basic_2/multiple/cpys_alt.ma | 76 ++-- .../lambdadelta/basic_2/multiple/cpys_cpys.ma | 98 ++--- .../lambdadelta/basic_2/multiple/cpys_lift.ma | 164 ++++---- .../lambdadelta/basic_2/multiple/drops.ma | 44 +-- .../basic_2/multiple/drops_drop.ma | 4 +- .../lambdadelta/basic_2/multiple/fleq.ma | 18 +- .../lambdadelta/basic_2/multiple/fleq_fleq.ma | 12 +- .../lambdadelta/basic_2/multiple/fqup.ma | 4 +- .../lambdadelta/basic_2/multiple/fqus.ma | 2 +- .../lambdadelta/basic_2/multiple/frees.ma | 108 ++--- .../basic_2/multiple/frees_append.ma | 26 +- .../basic_2/multiple/frees_lift.ma | 98 ++--- .../multiple/{frees_leq.ma => frees_lreq.ma} | 20 +- .../lambdadelta/basic_2/multiple/lifts.ma | 40 +- .../basic_2/multiple/lifts_lift.ma | 16 +- .../lambdadelta/basic_2/multiple/lleq.ma | 106 ++--- .../lambdadelta/basic_2/multiple/lleq_alt.ma | 18 +- .../basic_2/multiple/lleq_alt_rec.ma | 32 +- .../lambdadelta/basic_2/multiple/lleq_drop.ma | 92 ++--- .../lambdadelta/basic_2/multiple/lleq_fqus.ma | 4 +- .../lambdadelta/basic_2/multiple/lleq_lleq.ma | 14 +- .../lambdadelta/basic_2/multiple/lleq_llor.ma | 6 +- .../multiple/{lleq_leq.ma => lleq_lreq.ma} | 20 +- .../lambdadelta/basic_2/multiple/llor.ma | 14 +- .../lambdadelta/basic_2/multiple/llor_alt.ma | 16 +- .../lambdadelta/basic_2/multiple/llor_drop.ma | 16 +- .../lambdadelta/basic_2/multiple/llpx_sn.ma | 182 ++++----- .../basic_2/multiple/llpx_sn_alt.ma | 18 +- .../basic_2/multiple/llpx_sn_alt_rec.ma | 172 ++++---- .../basic_2/multiple/llpx_sn_drop.ma | 302 +++++++------- .../basic_2/multiple/llpx_sn_frees.ma | 12 +- .../basic_2/multiple/llpx_sn_llor.ma | 6 +- .../basic_2/multiple/llpx_sn_lpx_sn.ma | 6 +- .../{llpx_sn_leq.ma => llpx_sn_lreq.ma} | 46 +-- .../lambdadelta/basic_2/multiple/mr2.ma | 54 +-- .../lambdadelta/basic_2/multiple/mr2_minus.ma | 54 +-- .../lambdadelta/basic_2/multiple/mr2_mr2.ma | 8 +- .../lambdadelta/basic_2/multiple/mr2_plus.ma | 12 +- .../contribs/lambdadelta/basic_2/names.txt | 11 +- .../basic_2/notation/relations/cosn_5.ma | 4 +- .../basic_2/notation/relations/degree_6.ma | 4 +- .../notation/relations/dpconvstar_8.ma | 4 +- .../basic_2/notation/relations/dpredstar_7.ma | 4 +- .../basic_2/notation/relations/freestar_4.ma | 4 +- .../basic_2/notation/relations/lazyeq_4.ma | 4 +- .../basic_2/notation/relations/lazyeq_7.ma | 4 +- .../basic_2/notation/relations/lazyor_5.ma | 4 +- .../basic_2/notation/relations/lrsubeq_4.ma | 4 +- .../basic_2/notation/relations/midiso_4.ma | 4 +- .../notation/relations/nativevalid_6.ma | 4 +- .../basic_2/notation/relations/psubst_6.ma | 4 +- .../notation/relations/psubststar_6.ma | 4 +- .../notation/relations/psubststaralt_6.ma | 4 +- .../basic_2/notation/relations/rdrop_3.ma | 4 +- .../basic_2/notation/relations/rdrop_4.ma | 4 +- .../basic_2/notation/relations/rdrop_5.ma | 4 +- .../basic_2/notation/relations/rdropstar_3.ma | 4 +- .../basic_2/notation/relations/rdropstar_4.ma | 4 +- .../basic_2/notation/relations/rlift_4.ma | 4 +- .../basic_2/notation/relations/rliftstar_3.ma | 4 +- .../basic_2/notation/relations/sn_6.ma | 4 +- .../basic_2/notation/relations/snalt_6.ma | 4 +- .../notation/relations/statictypestar_6.ma | 4 +- .../lambdadelta/basic_2/reduction/cir_lift.ma | 8 +- .../lambdadelta/basic_2/reduction/cix.ma | 8 +- .../lambdadelta/basic_2/reduction/cix_lift.ma | 8 +- .../lambdadelta/basic_2/reduction/cnr_lift.ma | 16 +- .../lambdadelta/basic_2/reduction/cnx.ma | 18 +- .../lambdadelta/basic_2/reduction/cnx_crx.ma | 4 +- .../lambdadelta/basic_2/reduction/cnx_lift.ma | 16 +- .../lambdadelta/basic_2/reduction/cpr.ma | 24 +- .../lambdadelta/basic_2/reduction/cpr_lift.ma | 50 +-- .../basic_2/reduction/cpr_llpx_sn.ma | 4 +- .../lambdadelta/basic_2/reduction/cpx.ma | 32 +- .../lambdadelta/basic_2/reduction/cpx_cix.ma | 2 +- .../lambdadelta/basic_2/reduction/cpx_lift.ma | 86 ++-- .../basic_2/reduction/cpx_llpx_sn.ma | 4 +- .../reduction/{cpx_leq.ma => cpx_lreq.ma} | 10 +- .../lambdadelta/basic_2/reduction/crr_lift.ma | 44 +-- .../lambdadelta/basic_2/reduction/crx.ma | 18 +- .../lambdadelta/basic_2/reduction/crx_lift.ma | 48 +-- .../lambdadelta/basic_2/reduction/fpb_lift.ma | 4 +- .../basic_2/reduction/fpbq_lift.ma | 4 +- .../lambdadelta/basic_2/reduction/lpr_drop.ma | 10 +- .../lambdadelta/basic_2/reduction/lpx_drop.ma | 4 +- .../basic_2/reduction/lpx_frees.ma | 6 +- .../lambdadelta/basic_2/reduction/lpx_lleq.ma | 56 +-- .../lambdadelta/basic_2/static/aaa_lift.ma | 38 +- .../lambdadelta/basic_2/static/aaa_lifts.ma | 2 +- .../contribs/lambdadelta/basic_2/static/da.ma | 108 ++--- .../lambdadelta/basic_2/static/da_aaa.ma | 2 +- .../lambdadelta/basic_2/static/da_da.ma | 24 +- .../lambdadelta/basic_2/static/da_lift.ma | 48 +-- .../lambdadelta/basic_2/static/lsuba.ma | 24 +- .../lambdadelta/basic_2/static/lsubd.ma | 42 +- .../lambdadelta/basic_2/static/lsubd_da.ma | 28 +- .../lambdadelta/basic_2/static/lsubd_lsubd.ma | 6 +- .../contribs/lambdadelta/basic_2/static/sd.ma | 90 ++--- .../contribs/lambdadelta/basic_2/static/sh.ma | 18 +- .../lambdadelta/basic_2/substitution/cpy.ma | 228 +++++------ .../basic_2/substitution/cpy_cpy.ma | 76 ++-- .../basic_2/substitution/cpy_lift.ma | 226 +++++------ .../basic_2/substitution/cpy_nlift.ma | 18 +- .../lambdadelta/basic_2/substitution/drop.ma | 370 +++++++++--------- .../basic_2/substitution/drop_append.ma | 32 +- .../basic_2/substitution/drop_drop.ma | 182 ++++----- .../{drop_leq.ma => drop_lreq.ma} | 54 +-- .../lambdadelta/basic_2/substitution/fqu.ma | 16 +- .../lambdadelta/basic_2/substitution/fquq.ma | 8 +- .../basic_2/substitution/fquq_alt.ma | 6 +- .../lambdadelta/basic_2/substitution/gget.ma | 38 +- .../basic_2/substitution/gget_gget.ma | 22 +- .../lambdadelta/basic_2/substitution/lift.ma | 362 ++++++++--------- .../basic_2/substitution/lift_lift.ma | 196 +++++----- .../basic_2/substitution/lift_lift_vector.ma | 6 +- .../basic_2/substitution/lift_neg.ma | 36 +- .../basic_2/substitution/lift_vector.ma | 32 +- .../basic_2/substitution/lpx_sn_drop.ma | 42 +- .../lambdadelta/basic_2/substitution/lsuby.ma | 178 ++++----- .../basic_2/substitution/lsuby_lsuby.ma | 10 +- .../lambdadelta/basic_2/unfold/lstas.ma | 166 ++++---- .../lambdadelta/basic_2/unfold/lstas_aaa.ma | 26 +- .../lambdadelta/basic_2/unfold/lstas_da.ma | 70 ++-- .../lambdadelta/basic_2/unfold/lstas_lift.ma | 138 +++---- .../basic_2/unfold/lstas_llpx_sn.ma | 20 +- .../lambdadelta/basic_2/unfold/lstas_lstas.ma | 86 ++-- .../lambdadelta/basic_2/web/basic_2.ldw.xml | 46 +-- .../lambdadelta/basic_2/web/basic_2_src.tbl | 14 +- .../lambdadelta/ground_2/web/ground_2.ldw.xml | 8 +- 194 files changed, 3870 insertions(+), 3875 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/computation/{cpxs_leq.ma => cpxs_lreq.ma} (88%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/grammar/lreq.ma rename matita/matita/contribs/lambdadelta/basic_2/grammar/{leq_leq.ma => lreq_lreq.ma} (50%) rename matita/matita/contribs/lambdadelta/basic_2/multiple/{frees_leq.ma => frees_lreq.ma} (64%) rename matita/matita/contribs/lambdadelta/basic_2/multiple/{lleq_leq.ma => lleq_lreq.ma} (71%) rename matita/matita/contribs/lambdadelta/basic_2/multiple/{llpx_sn_leq.ma => llpx_sn_lreq.ma} (53%) rename matita/matita/contribs/lambdadelta/basic_2/reduction/{cpx_leq.ma => cpx_lreq.ma} (81%) rename matita/matita/contribs/lambdadelta/basic_2/substitution/{drop_leq.ma => drop_lreq.ma} (64%) diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml index f13d943f8..e4499a294 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml @@ -10,32 +10,30 @@ applications of λδ version 2. In particular it contains the components below. - - Martin-Löf's Type Theory with one universe - using λδ as theory of expressions. - - - The validation algorithm for λδ as implemented in - Helena 0.8. - + + + Martin-Löf's Type Theory with one universe + using λδ as theory of expressions. + + + + The validation algorithm for λδ as implemented in + Helena 0.8. +
Summary of the Specification
Here is a numerical acount of the specification's contents and its timeline. - Nodes are counted according to the "intrinsinc complexity measure" - [F. Guidi: "Procedural Representation of CIC Proof Terms" - Journal of Automated Reasoning 44(1-2), Springer (February 2010), - pp. 53-78]. - + The Applications directory is started. - + The Functional component is started inside the specification of λδ version 2. - + The MLTT1 component is started. @@ -48,9 +46,5 @@
-
Physical Structure of the Specification
- The source files are grouped in directories, - one for each component. -
Stage "B" - + Context-sensitive subject equivalence for native type assignment. Stage "A": "Weakening the Applicability Condition" - + Iterated static type assignment defined (more elegantly) as a primitive notion. - + Preservation of stratified native validity for context-sensitive computation on terms. - + Strong qrst-normalization for simply typed terms. - + Lazy equivalence on local environments addded as q-step to rst-computation on closures (anniversary milestone). - + Parametrized slicing of local environments comprises both versions of this operation (one from basic_1, the other used in basic_2 till now). - + Passive support for global environments. - + Reaxiomatized β-reductum as in rt-reduction. - + Context-sensitive strong rt-normalization for simply typed terms. - + Reaxiomatized substitution and reduction commute with respect to subclosure (anniversary milestone). - + Mutual recursive preservation of stratified native validity for rst-computation on closures. - + Confluence for context-free parallel reduction on closures. - + Term binders polarized to control ζ-reduction (not released). - + Context-sensitive subject equivalence for atomic arity assignment (anniversary milestone). - + Context-sensitive strong normalization for simply typed terms. - + Support for abstract candidates of reducibility. - + Confluence for context-sensitive parallel reduction on terms. - + Confluence for context-free parallel reduction on terms. - + Specification starts. @@ -113,9 +109,5 @@
-
Physical Structure of the Specification
- The source files are grouped in directories, - one for each component. -
- + Natural numbers with infinity. - + Specification starts. @@ -30,9 +30,5 @@
-
Physical Structure of the Specification
- The source files are grouped in directories, - one for each plane. -