From: Ferruccio Guidi Date: Tue, 19 Nov 2019 19:45:15 +0000 (+0100) Subject: λδ-2B is released X-Git-Tag: make_still_working~218 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=c7b50fec51b9a25d5bc536f44e54179fd53efb44 λδ-2B is released + some refactoring + extra spaces cleaned + web site update --- diff --git a/helm/www/lambdadelta/download/lambdadelta_2B.tar.bz2 b/helm/www/lambdadelta/download/lambdadelta_2B.tar.bz2 new file mode 100644 index 000000000..33786f969 Binary files /dev/null and b/helm/www/lambdadelta/download/lambdadelta_2B.tar.bz2 differ diff --git a/helm/www/lambdadelta/web/home/documentation_2.tbl b/helm/www/lambdadelta/web/home/documentation_2.tbl index ee523fda4..2cd06743e 100644 --- a/helm/www/lambdadelta/web/home/documentation_2.tbl +++ b/helm/www/lambdadelta/web/home/documentation_2.tbl @@ -84,6 +84,14 @@ table { "Presentation at University of Bologna (slides)." * } ] + [ { name "ldV2b" "V2b." "" } { + "F. Guidi:" + + @@("html/version_2.html" "lambdadelta_2B") + + "(revised 2019-11)." + + "Formal specification for the proof assistant Matita 0.99.4 (scripts)." + + @@("html/documentation.html#bibtex" "BibTeX entry") ^ "." + * } + ] [ { name "ldV2a" "V2a." "" } { "F. Guidi:" + @@("html/version_2.html" "lambdadelta_2A1") + diff --git a/helm/www/lambdadelta/web/home/news.ldw.xml b/helm/www/lambdadelta/web/home/news.ldw.xml index 3f1c9f893..27e6dd460 100644 --- a/helm/www/lambdadelta/web/home/news.ldw.xml +++ b/helm/www/lambdadelta/web/home/news.ldw.xml @@ -12,6 +12,12 @@ Milestones + + The specification of + λδ-2B + is released. + + Second journal paper on λδ accepted for publication. @@ -22,16 +28,16 @@ - The specification of λδ version 2A1 is concluded. + The specification of λδ-2A is concluded. The corrected specification of Landau's "Grundlagen der Analysis" - is validated in a λProlog implementation of λδ version 3. + is validated in a λProlog implementation of λδ-3. - The specification of λδ version 1 is validated by + The specification of λδ-1A is validated by Matita 0.99.2. @@ -44,20 +50,21 @@ - The specification of λδ version 1 - is updated with backports from the abandoned specification of λδ version 2. + The specification of λδ-1A + is updated with backports from the abandoned specification of λδ-2. "Helena 0.8.2" is released. The corrected specification of Landau's "Grundlagen der Analysis" - is validated in λδ version 3. + is validated in λδ-3. - λδ version 2A1 + The specification of + λδ-2A is released. @@ -66,7 +73,7 @@ - First communication on λδ version 2. + First communication on λδ-2. @@ -96,13 +103,14 @@ - The specification of λδ version 2 + The specification of + λδ-2 and related topics is restarted in Matita 0.5. - The specification of λδ version 2 with Coq 7.3.1 is abandoned. + The specification of λδ-2 with Coq 7.3.1 is abandoned. @@ -119,7 +127,7 @@ - "Helena", a validator for λδ version 2, + "Helena", a validator for λδ-2, is available as a part of the HELM software. @@ -135,40 +143,41 @@ First procedural reconstruction for Matita 0.5 - of the λδ version 1 for Coq 7.3.1. + of the λδ-1A for Coq 7.3.1. The - HTML pages of the specification of λδ version 1 for Matita 0.5 + HTML pages of the specification of λδ-1A for Matita 0.5 are online. - The specification of λδ version 1 is concluded. + The specification of λδ-1A is concluded. - The specification of λδ version 2 is started with Coq 7.3.1 (false start). + The specification of λδ-2 is started with Coq 7.3.1 (false start). The - specification of λδ version 1 for Matita 0.4 + specification of λδ-1A for Matita 0.4 is online. - λδ version 1 + The specification of + λδ-1A is released. - First communication on λδ version 1. + First communication on λδ-1. - The specification of λδ version 1 + The specification of λδ-1 is started with Coq 7.3.1. diff --git a/helm/www/lambdadelta/web/home/versions.tbl b/helm/www/lambdadelta/web/home/versions.tbl index 0d84b3b1f..fa16e0667 100644 --- a/helm/www/lambdadelta/web/home/versions.tbl +++ b/helm/www/lambdadelta/web/home/versions.tbl @@ -16,9 +16,9 @@ table { class "orange" { [ { @@("html/specification#v2" "Version 2") * } { "\"basic_2\"" * } - { [ "\"B\"" @("http://matita.cs.unibo.it/" "Matita 0.99.3") - "October 2015" "November 2018" "" "" - "" * + { [ "\"B\"" @("http://matita.cs.unibo.it/" "Matita 0.99.4") + "October 2015" "November 2018" "November 2019" "" + @@("html/documentation#ldV2b" "V2b") * ] [ "\"A\"" @("http://matita.cs.unibo.it/" "Matita 0.99.2") "April 2011" "June 2014" "October 2014" "August 2015" diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 3e0228cb0..e22b7ec42 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -25,7 +25,7 @@ PRB_OPTS := $(XOA_OPTS) -g -i ORIG := . ./orig.sh ORIGS := basic_2/basic_1.orig -CONTRIB := lambdadelta_2 +CONTRIB := lambdadelta_2B WWW := ../../../../helm/www/lambdadelta @@ -260,8 +260,8 @@ trim: $(TRIMS:%=%.trimmed) # contrib #################################################################### contrib: - @echo " TAR -czf $(CONTRIB).tar.gz root $(XPACKAGES)" - $(H)tar -czf $(CONTRIB).tar.gz root $(XMAS) + @echo " TAR -cjf $(CONTRIB).tar.bz2 root $(XPACKAGES)" + $(H)tar -cjf $(CONTRIB).tar.bz2 root $(XMAS) # clean ###################################################################### diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snabstneg_1.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snabstneg_1.ma deleted file mode 100644 index a82ce4605..000000000 --- a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snabstneg_1.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) - -notation "hvbox( - 𝛌 . break term 55 T )" - non associative with precedence 55 - for @{ 'SnAbstNeg $T }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/sngref_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/sngref_2.ma deleted file mode 100644 index f28b669d1..000000000 --- a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/sngref_2.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) - -notation "hvbox( § term 90 p . break term 55 T )" - non associative with precedence 55 - for @{ 'SnGRef $p $T }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snitem1_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snitem1_2.ma deleted file mode 100644 index cef7a31fa..000000000 --- a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snitem1_2.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) - -notation "hvbox( ① { term 46 I } . break term 55 T )" - non associative with precedence 55 - for @{ 'SnItem1 $I $T }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snlref_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snlref_2.ma deleted file mode 100644 index 4f9311f1e..000000000 --- a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snlref_2.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) - -notation "hvbox( # term 90 i . break term 55 T )" - non associative with precedence 55 - for @{ 'SnLRef $i $T }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snproj_3.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snproj_3.ma deleted file mode 100644 index 3e985c331..000000000 --- a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snproj_3.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) - -notation "hvbox( 𝛑 { term 46 a } break term 55 T1 . break term 55 T2 )" - non associative with precedence 55 - for @{ 'SnProj $a $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snprojneg_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snprojneg_2.ma deleted file mode 100644 index c29417e3c..000000000 --- a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snprojneg_2.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) - -notation "hvbox( - 𝛑 term 55 T1 . break term 55 T2 )" - non associative with precedence 55 - for @{ 'SnProjNeg $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snprojpos_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snprojpos_2.ma deleted file mode 100644 index 74a573d60..000000000 --- a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snprojpos_2.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) - -notation "hvbox( + 𝛑 term 55 T1 . break term 55 T2 )" - non associative with precedence 55 - for @{ 'SnProjPos $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snstar_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snstar_2.ma deleted file mode 100644 index b4e1e0dac..000000000 --- a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snstar_2.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) - -notation "hvbox( ⋆ term 90 k . break term 55 T )" - non associative with precedence 55 - for @{ 'SnStar $k $T }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snabstneg_1.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snabstneg_1.ma new file mode 100644 index 000000000..a82ce4605 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snabstneg_1.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) + +notation "hvbox( - 𝛌 . break term 55 T )" + non associative with precedence 55 + for @{ 'SnAbstNeg $T }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/sngref_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/sngref_2.ma new file mode 100644 index 000000000..f28b669d1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/sngref_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) + +notation "hvbox( § term 90 p . break term 55 T )" + non associative with precedence 55 + for @{ 'SnGRef $p $T }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snitem1_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snitem1_2.ma new file mode 100644 index 000000000..cef7a31fa --- /dev/null +++ b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snitem1_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) + +notation "hvbox( ① { term 46 I } . break term 55 T )" + non associative with precedence 55 + for @{ 'SnItem1 $I $T }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snlref_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snlref_2.ma new file mode 100644 index 000000000..4f9311f1e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snlref_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) + +notation "hvbox( # term 90 i . break term 55 T )" + non associative with precedence 55 + for @{ 'SnLRef $i $T }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snproj_3.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snproj_3.ma new file mode 100644 index 000000000..3e985c331 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snproj_3.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) + +notation "hvbox( 𝛑 { term 46 a } break term 55 T1 . break term 55 T2 )" + non associative with precedence 55 + for @{ 'SnProj $a $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snprojneg_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snprojneg_2.ma new file mode 100644 index 000000000..c29417e3c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snprojneg_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) + +notation "hvbox( - 𝛑 term 55 T1 . break term 55 T2 )" + non associative with precedence 55 + for @{ 'SnProjNeg $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snprojpos_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snprojpos_2.ma new file mode 100644 index 000000000..74a573d60 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snprojpos_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) + +notation "hvbox( + 𝛑 term 55 T1 . break term 55 T2 )" + non associative with precedence 55 + for @{ 'SnProjPos $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snstar_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snstar_2.ma new file mode 100644 index 000000000..b4e1e0dac --- /dev/null +++ b/matita/matita/contribs/lambdadelta/alpha_1/notation/functions/snstar_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) + +notation "hvbox( ⋆ term 90 k . break term 55 T )" + non associative with precedence 55 + for @{ 'SnStar $k $T }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/syntax/term.ma b/matita/matita/contribs/lambdadelta/alpha_1/syntax/term.ma index 7b09c887d..4ba35edc6 100644 --- a/matita/matita/contribs/lambdadelta/alpha_1/syntax/term.ma +++ b/matita/matita/contribs/lambdadelta/alpha_1/syntax/term.ma @@ -18,14 +18,14 @@ include "static_2/notation/functions/snabstpos_2.ma". include "static_2/notation/functions/snabbr_3.ma". include "static_2/notation/functions/snabbrpos_2.ma". include "static_2/notation/functions/snabbrneg_2.ma". -include "alpha_1/notation/constructors/snitem1_2.ma". -include "alpha_1/notation/constructors/snstar_2.ma". -include "alpha_1/notation/constructors/snlref_2.ma". -include "alpha_1/notation/constructors/sngref_2.ma". -include "alpha_1/notation/constructors/snabstneg_1.ma". -include "alpha_1/notation/constructors/snproj_3.ma". -include "alpha_1/notation/constructors/snprojpos_2.ma". -include "alpha_1/notation/constructors/snprojneg_2.ma". +include "alpha_1/notation/functions/snitem1_2.ma". +include "alpha_1/notation/functions/snstar_2.ma". +include "alpha_1/notation/functions/snlref_2.ma". +include "alpha_1/notation/functions/sngref_2.ma". +include "alpha_1/notation/functions/snabstneg_1.ma". +include "alpha_1/notation/functions/snproj_3.ma". +include "alpha_1/notation/functions/snprojpos_2.ma". +include "alpha_1/notation/functions/snprojneg_2.ma". include "alpha_1/syntax/item.ma". (* TERMS ********************************************************************) diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/li.ma b/matita/matita/contribs/lambdadelta/apps_2/models/li.ma index b3ad39157..6975017c5 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/li.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/li.ma @@ -31,7 +31,7 @@ interpretation "local environment interpretation (model)" (* Basic inversion lemmas ***************************************************) -fact li_inv_abbr_aux (M) (gv): is_model M → +fact li_inv_abbr_aux (M) (gv): is_model M → ∀v,Y. v ϵ ⟦Y⟧{M}[gv] → ∀L,V. Y = L.ⓓV → ∃∃lv. lv ϵ ⟦L⟧[gv] & ⫯[0←⟦V⟧[gv,lv]]lv ≗ v. #M #gv #HM #v #Y #H elim H -v -Y diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma index 3d9e440a7..044866007 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma @@ -79,7 +79,7 @@ elim (lt_or_eq_or_gt j i) #Hij destruct ] qed-. -(* Properies with term interpretation ***************************************) +(* Properies with term interpretation ***************************************) lemma ti_comp (M): is_model M → ∀T,gv1,gv2. gv1 ≗ gv2 → ∀lv1,lv2. lv1 ≗ lv2 → diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma index 34e9de237..c401800d1 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs.ma @@ -40,7 +40,7 @@ fact vpushs_inv_atom_aux (M) (gv) (lv): is_model M → | #v #d #K #V #_ #_ #H destruct | #v #d #I #K #_ #_ #H destruct | #v1 #v2 #L #_ #Hv12 #IH #H destruct - /3 width=3 by veq_trans/ + /3 width=3 by veq_trans/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma index 8ac169986..d017bc16a 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/vpushs_fold.ma @@ -21,7 +21,7 @@ include "apps_2/models/vpushs.ma". lemma vpushs_fold (M): is_model M → is_extensional M → ∀L,T1,T2,gv,lv. - (∀v. L ⨁[gv] lv ≘ v → ⟦T1⟧[gv,v] ≗ ⟦T2⟧[gv,v]) → + (∀v. L ⨁[gv] lv ≘ v → ⟦T1⟧[gv,v] ≗ ⟦T2⟧[gv,v]) → ⟦L+T1⟧[gv,lv] ≗{M} ⟦L+T2⟧[gv,lv]. #M #H1M #H2M #L elim L -L [| #K * [| * ]] [ #T1 #T2 #gv #lv #H12 diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl index 34cf9f851..8499b43e3 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl @@ -82,12 +82,12 @@ class "capitalize italic" { 0 } class "italic" { 1 } (* - [ { "evaluation drop" * } { + [ { "evaluation drop" * } { [ "vdrop" + "( â«°{?}? )" + "( â«°{?}[?]? )" "vdrop_vlift" * ] } ] [ { "reduction and type machine" * } { [ "rtm" "rtm_step ( ? ⇨ ? )" * ] } - ] + ] *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma index 683c57b1f..ae42a2168 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma @@ -127,7 +127,7 @@ qed-. fact cnv_cpm_conf_lpr_bind_zeta_aux (h) (a) (G) (L) (V) (T): (∀G0,L0,T0. ⦃G,L,+ⓓV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → ⦃G,L⦄ ⊢ +ⓓV.T ![h,a] → - ∀V1. ⦃G,L⦄ ⊢V ➡[h] V1 → ∀n1,T1. ⦃G,L.ⓓV⦄ ⊢ T ➡[n1,h] T1 → + ∀V1. ⦃G,L⦄ ⊢V ➡[h] V1 → ∀n1,T1. ⦃G,L.ⓓV⦄ ⊢ T ➡[n1,h] T1 → ∀T2. ⇧*[1]T2 ≘ T → ∀n2,XT2. ⦃G,L⦄ ⊢ T2 ➡[n2,h] XT2 → ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G,L1⦄ ⊢ +ⓓV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ XT2 ➡*[n1-n2,h] T. @@ -136,7 +136,7 @@ fact cnv_cpm_conf_lpr_bind_zeta_aux (h) (a) (G) (L) (V) (T): #L1 #HL01 #L2 #HL02 elim (cnv_inv_bind … H0) -H0 #_ #HT0 lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HT20) -HT0 -[ /3 width=3 by drops_refl, drops_drop/ ] #HT2 +[ /3 width=3 by drops_refl, drops_drop/ ] #HT2 elim (cpm_inv_lifts_sn … HT01 (Ⓣ) … L0 … HT20) -HT01 [| /3 width=1 by drops_refl, drops_drop/ ] #XT1 #HXT1 #HXT12 elim (cnv_cpm_conf_lpr_sub … IH … HXT12 … HXT2 … HL01 … HL02) @@ -225,7 +225,7 @@ elim (cpm_inv_abbr1 … HX) -HX * #T #HT1 #HT2 -L0 -V0 -W0 -T0 /4 width=7 by cpms_theta_dx, cpms_appl_dx, cpms_bind_dx, ex2_intro/ | #X0 #HXT0 #H1X0 #H destruct - lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HXT0) -HT0 [ /3 width=3 by drops_refl, drops_drop/ ] #H2X0 + lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HXT0) -HT0 [ /3 width=3 by drops_refl, drops_drop/ ] #H2X0 elim (cpm_inv_lifts_sn … HT02 (Ⓣ) … L0 … HXT0) -HT02 [| /3 width=1 by drops_refl, drops_drop/ ] #X2 #HXT2 #HX02 elim (cnv_cpm_conf_lpr_sub … IH … H1X0 … HX02 … HL01 … HL02) [|*: /4 width=5 by fqup_fpbg, fqup_strap1, fqu_drop/ ] #T #HT1 #HT2 -L0 -V0 -W0 -T0 @@ -423,7 +423,7 @@ fact cnv_cpm_conf_lpr_aux (h) (a): @(cnv_cpm_conf_lpr_delta_delta_aux … IH1) -IH1 /1 width=13 by/ | #m2 #K2 #W2 #XW2 #i2 #HLK2 #_ #_ #H21 #H22 #K1 #V1 #XV1 #i1 #HLK1 #_ #_ #H11 destruct -a -XW2 -XV1 -HL2 -HL1 elim cnv_cpm_conf_lpr_delta_ell_aux /1 width=8 by/ - | #H21 #H22 #m1 #K1 #W1 #XW1 #i1 #HLK1 #HWX1 #HXW1 #H11 #H12 destruct -IH2 + | #H21 #H22 #m1 #K1 #W1 #XW1 #i1 #HLK1 #HWX1 #HXW1 #H11 #H12 destruct -IH2 [h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → - (∀G0,L0,T0. ⦃G,L,T1⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr h a G0 L0 T0) → + (∀G0,L0,T0. ⦃G,L,T1⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr h a G0 L0 T0) → Q n T1. #h #a #G #L #T2 #Q #IB1 #IB2 #n #T1 #H @(cpms_ind_sn … H) -n -T1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fqus.ma index 50e4edbee..7498e33c1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fqus.ma @@ -38,7 +38,7 @@ lemma cnv_fqu_conf (h) (a): [ elim (cnv_inv_appl … H) -H // | elim (cnv_inv_cast … H) -H // ] -| #I1 #G1 #L1 #T1 #U1 #HTU1 #HU +| #I1 #G1 #L1 #T1 #U1 #HTU1 #HU /4 width=7 by cnv_inv_lifts, drops_refl, drops_drop/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_fsb.ma index 5aea50a66..4d4cebd5e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_fsb.ma @@ -29,4 +29,4 @@ theorem nta_fwd_fsb (h) (a) (G) (L): #h #a #G #L #T #U #H elim (cnv_inv_cast … H) #X #HU #HT #_ #_ -X /3 width=2 by cnv_fwd_fsb, conj/ -qed-. +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma index 44dac970e..20bb43faf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma @@ -124,7 +124,7 @@ elim (cpms_inv_lref_sn … H2) -H2 * ] qed-. -lemma nta_inv_lref_sn_drops_cnv (h) (a) (G) (L): +lemma nta_inv_lref_sn_drops_cnv (h) (a) (G) (L): ∀X2,i. ⦃G,L⦄ ⊢ #i :[h,a] X2 → ∨∨ ∃∃K,V,W,U. ⇩*[i] L ≘ K.ⓓV & ⦃G,K⦄ ⊢ V :[h,a] W & ⇧*[↑i] W ≘ U & ⦃G,L⦄ ⊢ U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![h,a] | ∃∃K,W,U. ⇩*[i] L ≘ K. ⓛW & ⦃G,K⦄ ⊢ W ![h,a] & ⇧*[↑i] W ≘ U & ⦃G,L⦄ ⊢ U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![h,a]. diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_cpcs.ma index 8438e0307..6adb6f7ad 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_cpcs.ma @@ -32,5 +32,5 @@ lemma ntas_inv_zero (h) (a) (G) (L): ∀T1,T2. ⦃G,L⦄ ⊢ T1 :*[h,a,0] T2 → ∧∧ ⦃G,L⦄ ⊢ T1 ![h,a] & ⦃G,L⦄ ⊢ T2 ![h,a] & ⦃G,L⦄ ⊢ T1 ⬌*[h] T2. #h #a #G #L #T1 #T2 * #T0 #HT1 #HT2 #HT20 #HT10 -/3 width=3 by cprs_div, and3_intro/ +/3 width=3 by cprs_div, and3_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma index 245d44f9c..25a57d746 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma @@ -87,7 +87,7 @@ qed. theorem cpms_theta (n) (h) (G) (L): ∀V,V2. ⇧*[1] V ≘ V2 → ∀W1,W2. ⦃G,L⦄ ⊢ W1 ➡*[h] W2 → ∀T1,T2. ⦃G,L.ⓓW1⦄ ⊢ T1 ➡*[n,h] T2 → - ∀V1. ⦃G,L⦄ ⊢ V1 ➡*[h] V → + ∀V1. ⦃G,L⦄ ⊢ V1 ➡*[h] V → ∀p. ⦃G,L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ➡*[n,h] ⓓ{p}W2.ⓐV2.T2. #n #h #G #L #V #V2 #HV2 #W1 #W2 #HW12 #T1 #T2 #HT12 #V1 #H @(cprs_ind_sn … H) -V1 [ /2 width=3 by cpms_theta_rc/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_drops.ma index 66045be0e..cebbb8ed0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_drops.ma @@ -24,7 +24,7 @@ lemma cpts_lifts_sn (h) (n) (G): d_liftable2_sn … lifts (λL. cpts h G L n). /3 width=6 by d2_liftable_sn_ltc, cpt_lifts_sn/ qed-. -lemma cpts_lifts_bi (h) (n) (G): +lemma cpts_lifts_bi (h) (n) (G): d_liftable2_bi … lifts (λL. cpts h G L n). #h #n #G @d_liftable2_sn_bi /2 width=6 by cpts_lifts_sn, lifts_mono/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma index 4a0550473..5081b65ec 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma @@ -127,7 +127,7 @@ qed. lemma cpxs_theta_dx: ∀h,p,G,L,V1,V,V2,W1,W2,T1,T2. ⦃G,L⦄ ⊢ V1 ⬈[h] V → ⇧*[1] V ≘ V2 → ⦃G,L.ⓓW1⦄ ⊢ T1 ⬈*[h] T2 → ⦃G,L⦄ ⊢ W1 ⬈[h] W2 → ⦃G,L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ⬈*[h] ⓓ{p}W2.ⓐV2.T2. -#h #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2 +#h #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2 /4 width=9 by cpx_cpxs, cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_theta/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_reqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_reqx.ma index eb1444b26..64be00b99 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_reqx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_reqx.ma @@ -19,7 +19,7 @@ include "basic_2/rt_computation/cpxs_teqx.ma". (* Properties with sort-irrelevant equivalence for local environments *******) -(* Basic_2A1: was just: lleq_cpxs_trans *) +(* Basic_2A1: was just: lleq_cpxs_trans *) lemma reqx_cpxs_trans: ∀h,G,L0,T0,T1. ⦃G,L0⦄ ⊢ T0 ⬈*[h] T1 → ∀L2. L2 ≛[T0] L0 → ∃∃T. ⦃G,L2⦄ ⊢ T0 ⬈*[h] T & T ≛ T1. @@ -31,19 +31,19 @@ elim (teqx_cpxs_trans … H2 … H3) -T #U0 #H2 #H3 /3 width=5 by cpxs_strap2, teqx_trans, ex2_intro/ qed-. -(* Basic_2A1: was just: cpxs_lleq_conf *) +(* Basic_2A1: was just: cpxs_lleq_conf *) lemma cpxs_reqx_conf: ∀h,G,L0,T0,T1. ⦃G,L0⦄ ⊢ T0 ⬈*[h] T1 → ∀L2. L0 ≛[T0] L2 → ∃∃T. ⦃G,L2⦄ ⊢ T0 ⬈*[h] T & T ≛ T1. /3 width=3 by reqx_cpxs_trans, reqx_sym/ qed-. -(* Basic_2A1: was just: cpxs_lleq_conf_dx *) +(* Basic_2A1: was just: cpxs_lleq_conf_dx *) lemma cpxs_reqx_conf_dx: ∀h,G,L2,T1,T2. ⦃G,L2⦄ ⊢ T1 ⬈*[h] T2 → ∀L1. L1 ≛[T1] L2 → L1 ≛[T2] L2. #h #G #L2 #T1 #T2 #H @(cpxs_ind … H) -T2 /3 width=6 by cpx_reqx_conf_dx/ qed-. -(* Basic_2A1: was just: lleq_conf_sn *) +(* Basic_2A1: was just: lleq_conf_sn *) lemma cpxs_reqx_conf_sn: ∀h,G,L1,T1,T2. ⦃G,L1⦄ ⊢ T1 ⬈*[h] T2 → ∀L2. L1 ≛[T1] L2 → L1 ≛[T2] L2. /4 width=6 by cpxs_reqx_conf_dx, reqx_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqx.ma index 7af7b41b8..178a2c440 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqx.ma @@ -19,7 +19,7 @@ include "basic_2/rt_computation/cpxs.ma". (* Properties with sort-irrelevant equivalence for terms ********************) -lemma teqx_cpxs_trans: ∀h,U1,T1. U1 ≛ T1 → ∀G,L,T2. ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 → +lemma teqx_cpxs_trans: ∀h,U1,T1. U1 ≛ T1 → ∀G,L,T2. ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 → ∃∃U2. ⦃G,L⦄ ⊢ U1 ⬈*[h] U2 & U2 ≛ T2. #h #U1 #T1 #HUT1 #G #L #T2 #HT12 @(cpxs_ind … HT12) -T2 /2 width=3 by ex2_intro/ #T #T2 #_ #HT2 * #U #HU1 #HUT elim (teqx_cpx_trans … HUT … HT2) -T -T1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma index 31ebb2c77..d162f660a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma @@ -98,6 +98,6 @@ lemma csx_fwd_flat: ∀h,I,G,L,V,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓕ{I}V.T⦄ sn3_appl_appls sn3_bind sn3_appl_bind sn3_appls_bind *) (* Basic_2A1: removed theorems 6: - csxa_ind csxa_intro csxa_cpxs_trans csxa_intro_cpx + csxa_ind csxa_intro csxa_cpxs_trans csxa_intro_cpx csx_csxa csxa_csx *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma index 915866a22..4a5330d1e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma @@ -54,7 +54,7 @@ qed. (* Basic_1: was just: sn3_abbr *) (* Basic_2A1: was: csx_lref_bind *) -lemma csx_lref_pair_drops (h) (G): +lemma csx_lref_pair_drops (h) (G): ∀I,L,K,V,i. ⇩*[i] L ≘ K.ⓑ{I}V → ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃#i⦄. #h #G #I #L #K #V #i #HLK #HV diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple.ma index 7253cdb50..50e525ec4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple.ma @@ -30,7 +30,7 @@ elim (cpx_inv_appl1_simple … H1) // -H1 elim (tneqx_inv_pair … H2) -H2 [ #H elim H -H // | #HV0 @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10 - @(IHV … HLV0 … HV0) -HV0 /4 width=5 by csx_cpx_trans, cpx_pair_sn/ (**) (* full auto too slow *) + @(IHV … HLV0 … HV0) -HV0 /4 width=5 by csx_cpx_trans, cpx_pair_sn/ (**) (* full auto too slow *) | -IHV -HT1 /4 width=3 by csx_cpx_trans, cpx_pair_sn/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma index 258ba5107..696fee8ef 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma @@ -61,4 +61,4 @@ lemma fpbg_feqx_trans: ∀h,G1,G,L1,L,T1,T. ⦃G1,L1,T1⦄ >[h] ⦃G,L,T⦄ → lemma cpm_tneqx_cpm_fpbg (h) (G) (L): ∀n1,T1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → (T1 ≛ T → ⊥) → ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 → ⦃G,L,T1⦄ >[h] ⦃G,L,T2⦄. -/4 width=5 by fpbq_fpbs, cpm_fpbq, cpm_fpb, ex2_3_intro/ qed. +/4 width=5 by fpbq_fpbs, cpm_fpbq, cpm_fpb, ex2_3_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqup.ma index 25f0a3ffb..4fcd971bb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqup.ma @@ -32,7 +32,7 @@ lemma fpbs_teqx_trans: ∀h,G1,G2,L1,L2,T1,T. ⦃G1,L1,T1⦄ ≥[h] ⦃G2,L2,T lemma fqup_fpbs: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂+ ⦃G2,L2,T2⦄ → ⦃G1,L1,T1⦄ ≥[h] ⦃G2,L2,T2⦄. -#h #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +#h #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 /4 width=5 by fqu_fquq, fpbq_fquq, tri_step/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma index 3ab294cf9..f01561bc2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma @@ -66,7 +66,7 @@ lemma fpbs_cpxs_teqx_fqup_lpx_trans: ∀h,G1,G3,L1,L3,T1,T3. ⦃G1,L1,T1⦄ ≥ ∀T4. ⦃G3,L3⦄ ⊢ T3 ⬈*[h] T4 → ∀T5. T4 ≛ T5 → ∀G2,L4,T2. ⦃G3,L3,T5⦄ ⬂+ ⦃G2,L4,T2⦄ → ∀L2. ⦃G2,L4⦄ ⊢ ⬈[h] L2 → ⦃G1,L1,T1⦄ ≥ [h] ⦃G2,L2,T2⦄. -#h #G1 #G3 #L1 #L3 #T1 #T3 #H13 #T4 #HT34 #T5 #HT45 #G2 #L4 #T2 #H34 #L2 #HL42 +#h #G1 #G3 #L1 #L3 #T1 #T3 #H13 #T4 #HT34 #T5 #HT45 #G2 #L4 #T2 #H34 #L2 #HL42 @(fpbs_lpx_trans … HL42) -L2 (**) (* full auto too slow *) @(fpbs_fqup_trans … H34) -G2 -L4 -T2 /3 width=3 by fpbs_cpxs_trans, fpbs_teqx_trans/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma index 5b383e05d..98bed39de 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma @@ -31,7 +31,7 @@ lemma csx_fsb_fpbs: ∀h,G1,L1,T1. ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∀G2,L2,T2. ⦃G1,L1,T1⦄ ≥[h] ⦃G2,L2,T2⦄ → ≥[h] 𝐒⦃G2,L2,T2⦄. #h #G1 #L1 #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IHc #G2 #L2 #T2 @(fqup_wf_ind (Ⓣ) … G2 L2 T2) -G2 -L2 -T2 -#G0 #L0 #T0 #IHu #H10 +#G0 #L0 #T0 #IHu #H10 lapply (fpbs_csx_conf … H10) // -HT1 #HT0 generalize in match IHu; -IHu generalize in match H10; -H10 @(rsx_ind … (csx_rsx … HT0)) -L0 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqx.ma index b55d19073..918adc2aa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqx.ma @@ -21,7 +21,7 @@ include "basic_2/rt_computation/fsb.ma". lemma fsb_feqx_trans: ∀h,G1,L1,T1. ≥[h] 𝐒⦃G1,L1,T1⦄ → ∀G2,L2,T2. ⦃G1,L1,T1⦄ ≛ ⦃G2,L2,T2⦄ → ≥[h] 𝐒⦃G2,L2,T2⦄. -#h #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1 +#h #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1 #G1 #L1 #T1 #_ #IH #G2 #L2 #T2 #H12 @fsb_intro #G #L #T #H2 elim (feqx_fpb_trans … H12 … H2) -G2 -L2 -T2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma index 1d8e0eb7d..1fd7ea36b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma @@ -43,7 +43,7 @@ lemma fsb_ind_fpbg_fpbs: ∀h. ∀Q:relation3 genv lenv term. (∀G2,L2,T2. ⦃G1,L1,T1⦄ >[h] ⦃G2,L2,T2⦄ → Q G2 L2 T2) → Q G1 L1 T1 ) → - ∀G1,L1,T1. ≥[h] 𝐒⦃G1,L1,T1⦄ → + ∀G1,L1,T1. ≥[h] 𝐒⦃G1,L1,T1⦄ → ∀G2,L2,T2. ⦃G1,L1,T1⦄ ≥[h] ⦃G2,L2,T2⦄ → Q G2 L2 T2. #h #Q #IH1 #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1 #G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx.ma index 9521a9b27..05292539f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx.ma @@ -72,7 +72,7 @@ lemma jsx_inv_pair_sn (h) (G): | ∃∃K2. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ & L2 = K2.ⓧ. #h #G #I #K1 #L2 #V #H elim (jsx_inv_bind_sn … H) -H * [ /3 width=3 by ex2_intro, or_introl/ -| #J #K2 #X #HK12 #HX #H1 #H2 destruct /3 width=4 by ex3_intro, or_intror/ +| #J #K2 #X #HK12 #HX #H1 #H2 destruct /3 width=4 by ex3_intro, or_intror/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_csx.ma index b8e919b73..adeaa3f88 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_csx.ma @@ -27,7 +27,7 @@ lemma jsx_csx_conf (h) (G): (* Properties with strongly rt-normalizing referred local environments ******) -(* Note: Try by induction on the 2nd premise by generalizing V with f *) +(* Note: Try by induction on the 2nd premise by generalizing V with f *) lemma rsx_jsx_trans (h) (G): ∀L1,V. G ⊢ ⬈*[h,V] 𝐒⦃L1⦄ → ∀L2. G ⊢ L1 ⊒[h] L2 → G ⊢ ⬈*[h,V] 𝐒⦃L2⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma index 7ac21a90d..74eb68212 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma @@ -47,7 +47,7 @@ elim (drops_inv_bind1_isuni … H) -H [3,6: // |*: * -Hf ] [1,3: #Hf #H destruct -IH /3 width=3 by drops_refl, ex2_intro/ |2,4: #g #Hg #HK1 #H destruct - elim (IH … Hg … HK1) -K1 -Hg #Y2 #HY12 #HKY2 + elim (IH … Hg … HK1) -K1 -Hg #Y2 #HY12 #HKY2 /3 width=3 by drops_drop, ex2_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_ctc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_ctc.ma index 742a0038a..c3e72888b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_ctc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_ctc.ma @@ -20,7 +20,7 @@ include "basic_2/rt_computation/lprs.ma". (* Properties with contextual transitive closure ****************************) lemma lprs_CTC (h) (G): - ∀L1,L2. L1⪤[CTC … (λL. cpm h G L 0)] L2 → ⦃G,L1⦄⊢ ➡*[h] L2. + ∀L1,L2. L1⪤[CTC … (λL. cpm h G L 0)] L2 → ⦃G,L1⦄⊢ ➡*[h] L2. /3 width=3 by cprs_CTC, lex_co/ qed. (* Inversion lemmas with contextual transitive closure **********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx.ma index 06500ddc9..2671597f1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx.ma @@ -63,7 +63,7 @@ qed-. lemma rsx_fwd_flat_dx (h) (G): ∀I,L,V,T. G ⊢ ⬈*[h,ⓕ{I}V.T] 𝐒⦃L⦄ → G ⊢ ⬈*[h,T] 𝐒⦃L⦄. -#h #G #I #L #V #T #H +#h #G #I #L #V #T #H @(rsx_ind … H) -L #L1 #_ #IHL1 @rsx_intro #L2 #HL12 #HnL12 /4 width=3 by reqx_fwd_flat_dx/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma index 7abac34cd..5a4dd983c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma @@ -26,7 +26,7 @@ include "basic_2/rt_computation/rsx_fqup.ma". lemma rsx_lifts (h) (G): d_liftable1_isuni … (λL,T. G ⊢ ⬈*[h,T] 𝐒⦃L⦄). #h #G #K #T #H @(rsx_ind … H) -K #K1 #_ #IH #b #f #L1 #HLK1 #Hf #U #HTU @rsx_intro -#L2 #HL12 #HnL12 elim (lpx_drops_conf … HLK1 … HL12) +#L2 #HL12 #HnL12 elim (lpx_drops_conf … HLK1 … HL12) /5 width=9 by reqx_lifts_bi, lpx_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma index 70681cf76..0f4571262 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma @@ -40,7 +40,7 @@ qed-. lemma cnx_inv_abbr_neg: ∀h,G,L,V,T. ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃-ⓓV.T⦄ → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃V⦄ ∧ ⦃G,L.ⓓV⦄ ⊢ ⬈[h] 𝐍⦃T⦄. #h #G #L #V1 #T1 #HVT1 @conj -[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 +[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 | #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 ] #H elim (teqx_inv_pair … H) -H // diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma index 75e0211d5..8c9c5f5ef 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma @@ -30,7 +30,7 @@ inductive cpg (Rt:relation rtc) (h): rtc → relation4 genv lenv term term ≝ ⇧*[1] V2 ≘ W2 → cpg Rt h c G (L.ⓓV1) (#0) W2 | cpg_ell : ∀c,G,L,V1,V2,W2. cpg Rt h c G L V1 V2 → ⇧*[1] V2 ≘ W2 → cpg Rt h (c+𝟘𝟙) G (L.ⓛV1) (#0) W2 -| cpg_lref : ∀c,I,G,L,T,U,i. cpg Rt h c G L (#i) T → +| cpg_lref : ∀c,I,G,L,T,U,i. cpg Rt h c G L (#i) T → ⇧*[1] T ≘ U → cpg Rt h c G (L.ⓘ{I}) (#↑i) U | cpg_bind : ∀cV,cT,p,I,G,L,V1,V2,T1,T2. cpg Rt h cV G L V1 V2 → cpg Rt h cT G (L.ⓑ{I}V1) T1 T2 → @@ -69,7 +69,7 @@ qed. (* Basic inversion lemmas ***************************************************) fact cpg_inv_atom1_aux: ∀Rt,c,h,G,L,T1,T2. ⦃G,L⦄ ⊢ T1 ⬈[Rt,c,h] T2 → ∀J. T1 = ⓪{J} → - ∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘 + ∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘 | ∃∃s. J = Sort s & T2 = ⋆(⫯[h]s) & c = 𝟘𝟙 | ∃∃cV,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬈[Rt,cV,h] V2 & ⇧*[1] V2 ≘ T2 & L = K.ⓓV1 & J = LRef 0 & c = cV @@ -95,7 +95,7 @@ fact cpg_inv_atom1_aux: ∀Rt,c,h,G,L,T1,T2. ⦃G,L⦄ ⊢ T1 ⬈[Rt,c,h] T2 → qed-. lemma cpg_inv_atom1: ∀Rt,c,h,J,G,L,T2. ⦃G,L⦄ ⊢ ⓪{J} ⬈[Rt,c,h] T2 → - ∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘 + ∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘 | ∃∃s. J = Sort s & T2 = ⋆(⫯[h]s) & c = 𝟘𝟙 | ∃∃cV,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬈[Rt,cV,h] V2 & ⇧*[1] V2 ≘ T2 & L = K.ⓓV1 & J = LRef 0 & c = cV @@ -153,7 +153,7 @@ fact cpg_inv_bind1_aux: ∀Rt,c,h,G,L,U,U2. ⦃G,L⦄ ⊢ U ⬈[Rt,c,h] U2 → ∀p,J,V1,U1. U = ⓑ{p,J}V1.U1 → ∨∨ ∃∃cV,cT,V2,T2. ⦃G,L⦄ ⊢ V1 ⬈[Rt,cV,h] V2 & ⦃G,L.ⓑ{J}V1⦄ ⊢ U1 ⬈[Rt,cT,h] T2 & U2 = ⓑ{p,J}V2.T2 & c = ((↕*cV)∨cT) - | ∃∃cT,T. ⇧*[1] T ≘ U1 & ⦃G,L⦄ ⊢ T ⬈[Rt,cT,h] U2 & + | ∃∃cT,T. ⇧*[1] T ≘ U1 & ⦃G,L⦄ ⊢ T ⬈[Rt,cT,h] U2 & p = true & J = Abbr & c = cT+𝟙𝟘. #Rt #c #h #G #L #U #U2 * -c -G -L -U -U2 [ #I #G #L #q #J #W #U1 #H destruct @@ -191,7 +191,7 @@ qed-. lemma cpg_inv_abst1: ∀Rt,c,h,p,G,L,V1,T1,U2. ⦃G,L⦄ ⊢ ⓛ{p}V1.T1 ⬈[Rt,c,h] U2 → ∃∃cV,cT,V2,T2. ⦃G,L⦄ ⊢ V1 ⬈[Rt,cV,h] V2 & ⦃G,L.ⓛV1⦄ ⊢ T1 ⬈[Rt,cT,h] T2 & U2 = ⓛ{p}V2.T2 & c = ((↕*cV)∨cT). -#Rt #c #h #p #G #L #V1 #T1 #U2 #H elim (cpg_inv_bind1 … H) -H * +#Rt #c #h #p #G #L #V1 #T1 #U2 #H elim (cpg_inv_bind1 … H) -H * [ /3 width=8 by ex4_4_intro/ | #c #T #_ #_ #_ #H destruct ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma index 4a937f119..6893cf19e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma @@ -212,14 +212,14 @@ qed. lemma cpm_inv_gref1: ∀n,h,G,L,T2,l. ⦃G,L⦄ ⊢ §l ➡[n,h] T2 → T2 = §l ∧ n = 0. #n #h #G #L #T2 #l * #c #Hc #H elim (cpg_inv_gref1 … H) -H -#H1 #H2 destruct /3 width=1 by isrt_inv_00, conj/ +#H1 #H2 destruct /3 width=1 by isrt_inv_00, conj/ qed-. (* Basic_2A1: includes: cpr_inv_bind1 *) lemma cpm_inv_bind1: ∀n,h,p,I,G,L,V1,T1,U2. ⦃G,L⦄ ⊢ ⓑ{p,I}V1.T1 ➡[n,h] U2 → ∨∨ ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ➡[h] V2 & ⦃G,L.ⓑ{I}V1⦄ ⊢ T1 ➡[n,h] T2 & U2 = ⓑ{p,I}V2.T2 - | ∃∃T. ⇧*[1] T ≘ T1 & ⦃G,L⦄ ⊢ T ➡[n,h] U2 & + | ∃∃T. ⇧*[1] T ≘ T1 & ⦃G,L⦄ ⊢ T ➡[n,h] U2 & p = true & I = Abbr. #n #h #p #I #G #L #V1 #T1 #U2 * #c #Hc #H elim (cpg_inv_bind1 … H) -H * [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct @@ -252,7 +252,7 @@ lemma cpm_inv_abst1: ∀n,h,p,G,L,V1,T1,U2. ⦃G,L⦄ ⊢ ⓛ{p}V1.T1 ➡[n,h] U #n #h #p #G #L #V1 #T1 #U2 #H elim (cpm_inv_bind1 … H) -H [ /3 width=1 by or_introl/ -| * #T #_ #_ #_ #H destruct +| * #T #_ #_ #_ #H destruct ] qed-. @@ -260,7 +260,7 @@ lemma cpm_inv_abst_bi: ∀n,h,p1,p2,G,L,V1,V2,T1,T2. ⦃G,L⦄ ⊢ ⓛ{p1}V1.T1 ∧∧ ⦃G,L⦄ ⊢ V1 ➡[h] V2 & ⦃G,L.ⓛV1⦄ ⊢ T1 ➡[n,h] T2 & p1 = p2. #n #h #p1 #p2 #G #L #V1 #V2 #T1 #T2 #H elim (cpm_inv_abst1 … H) -H #XV #XT #HV #HT #H destruct -/2 width=1 by and3_intro/ +/2 width=1 by and3_intro/ qed-. (* Basic_1: includes: pr0_gen_appl pr2_gen_appl *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma index ee72b6149..e6555ec18 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma @@ -25,7 +25,7 @@ lemma cpr_flat: ∀h,I,G,L,V1,V2,T1,T2. ⦃G,L⦄ ⊢ V1 ➡[h] V2 → ⦃G,L⦄ ⊢ T1 ➡[h] T2 → ⦃G,L⦄ ⊢ ⓕ{I}V1.T1 ➡[h] ⓕ{I}V2.T2. #h * /2 width=1 by cpm_cast, cpm_appl/ -qed. +qed. (* Basic_1: was: pr2_head_1 *) lemma cpr_pair_sn: ∀h,I,G,L,V1,V2. ⦃G,L⦄ ⊢ V1 ➡[h] V2 → @@ -45,7 +45,7 @@ lemma cpr_inv_atom1: ∀h,J,G,L,T2. ⦃G,L⦄ ⊢ ⓪{J} ➡[h] T2 → [2,4:|*: /3 width=8 by or3_intro0, or3_intro1, or3_intro2, ex4_4_intro, ex4_3_intro/ ] [ #n #_ #_ #H destruct | #n #K #V1 #V2 #_ #_ #_ #_ #H destruct -] +] qed-. (* Basic_1: includes: pr0_gen_sort pr2_gen_sort *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma index 53f9d778d..fa110d8c4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma @@ -177,7 +177,7 @@ qed. lemma cpt_inv_gref_sn (h) (n) (G) (L) (l): ∀X2. ⦃G,L⦄ ⊢ §l ⬆[h,n] X2 → ∧∧ X2 = §l & n = 0. #h #n #G #L #l #X2 * #c #Hc #H elim (cpg_inv_gref1 … H) -H -#H1 #H2 destruct /2 width=1 by conj/ +#H1 #H2 destruct /2 width=1 by conj/ qed-. lemma cpt_inv_bind_sn (h) (n) (p) (I) (G) (L) (V1) (T1): diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma index f8978f460..7e1197873 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma @@ -77,7 +77,7 @@ qed. lemma cpx_beta: ∀h,p,G,L,V1,V2,W1,W2,T1,T2. ⦃G,L⦄ ⊢ V1 ⬈[h] V2 → ⦃G,L⦄ ⊢ W1 ⬈[h] W2 → ⦃G,L.ⓛW1⦄ ⊢ T1 ⬈[h] T2 → ⦃G,L⦄ ⊢ ⓐV1.ⓛ{p}W1.T1 ⬈[h] ⓓ{p}ⓝW2.V2.T2. -#h #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 * #cV #HV12 * #cW #HW12 * +#h #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 * #cV #HV12 * #cW #HW12 * /3 width=2 by cpg_beta, ex_intro/ qed. @@ -85,7 +85,7 @@ lemma cpx_theta: ∀h,p,G,L,V1,V,V2,W1,W2,T1,T2. ⦃G,L⦄ ⊢ V1 ⬈[h] V → ⇧*[1] V ≘ V2 → ⦃G,L⦄ ⊢ W1 ⬈[h] W2 → ⦃G,L.ⓓW1⦄ ⊢ T1 ⬈[h] T2 → ⦃G,L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ⬈[h] ⓓ{p}W2.ⓐV2.T2. -#h #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 * #cV #HV1 #HV2 * #cW #HW12 * +#h #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 * #cV #HV1 #HV2 * #cW #HW12 * /3 width=4 by cpg_theta, ex_intro/ qed. @@ -147,7 +147,7 @@ qed-. lemma cpx_inv_bind1: ∀h,p,I,G,L,V1,T1,U2. ⦃G,L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[h] U2 → ∨∨ ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬈[h] V2 & ⦃G,L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 & U2 = ⓑ{p,I}V2.T2 - | ∃∃T. ⇧*[1] T ≘ T1 & ⦃G,L⦄ ⊢ T ⬈[h] U2 & + | ∃∃T. ⇧*[1] T ≘ T1 & ⦃G,L⦄ ⊢ T ⬈[h] U2 & p = true & I = Abbr. #h #p #I #G #L #V1 #T1 #U2 * #c #H elim (cpg_inv_bind1 … H) -H * /4 width=5 by ex4_intro, ex3_2_intro, ex_intro, or_introl, or_intror/ @@ -224,7 +224,7 @@ lemma cpx_inv_flat1: ∀h,I,G,L,V1,U1,U2. ⦃G,L⦄ ⊢ ⓕ{I}V1.U1 ⬈[h] U2 /3 width=14 by or5_intro0, or5_intro3, or5_intro4, ex7_7_intro, ex6_6_intro, ex3_2_intro/ | elim (cpx_inv_cast1 … H) -H [ * ] /3 width=14 by or5_intro0, or5_intro1, or5_intro2, ex3_2_intro, conj/ -] +] qed-. (* Basic forward lemmas *****************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma index 6c1d31e77..3be9277cd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma @@ -101,7 +101,7 @@ qed-. lemma fquq_cpx_trans_tneqx: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂⸮[b] ⦃G2,L2,T2⦄ → ∀U2. ⦃G2,L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≛ U2 → ⊥) → ∃∃U1. ⦃G1,L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≛ U1 → ⊥ & ⦃G1,L1,U1⦄ ⬂⸮[b] ⦃G2,L2,U2⦄. -#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 elim H12 -H12 +#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 elim H12 -H12 [ #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_tneqx … H12 … HTU2 H) -T2 /3 width=4 by fqu_fquq, ex3_intro/ | * #HG #HL #HT destruct /3 width=4 by ex3_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_reqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_reqx.ma index de168279c..6dea95295 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_reqx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_reqx.ma @@ -22,7 +22,7 @@ include "basic_2/rt_transition/fpb.ma". (* Properties with sort-irrelevant equivalence for local environments *******) lemma teqx_fpb_trans: ∀h,U2,U1. U2 ≛ U1 → - ∀G1,G2,L1,L2,T1. ⦃G1,L1,U1⦄ ≻[h] ⦃G2,L2,T1⦄ → + ∀G1,G2,L1,L2,T1. ⦃G1,L1,U1⦄ ≻[h] ⦃G2,L2,T1⦄ → ∃∃L,T2. ⦃G1,L1,U2⦄ ≻[h] ⦃G2,L,T2⦄ & T2 ≛ T1 & L ≛[T1] L2. #h #U2 #U1 #HU21 #G1 #G2 #L1 #L2 #T1 * -G2 -L2 -T1 [ #G2 #L2 #T1 #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma index e875cac28..e8e183cb8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma @@ -37,7 +37,7 @@ lemma fpbq_refl (h): tri_reflexive … (fpbq h). /2 width=1 by fpbq_cpx/ qed. (* Basic_2A1: includes: cpr_fpbq *) -lemma cpm_fpbq (n) (h) (G) (L): ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → ⦃G,L,T1⦄ ≽[h] ⦃G,L,T2⦄. +lemma cpm_fpbq (n) (h) (G) (L): ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → ⦃G,L,T1⦄ ≽[h] ⦃G,L,T2⦄. /3 width=2 by fpbq_cpx, cpm_fwd_cpx/ qed. lemma lpr_fpbq (h) (G) (T): ∀L1,L2. ⦃G,L1⦄ ⊢ ➡[h] L2 → ⦃G,L1,T⦄ ≽[h] ⦃G,L2,T⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_lpr.ma index 184d91406..dcbe44401 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_lpr.ma @@ -97,7 +97,7 @@ fact cpr_conf_lpr_bind_zeta (h): ∀G,L,T. ⦃G0,L0,+ⓓV0.T0⦄ ⬂+ ⦃G,L,T⦄ → IH_cpr_conf_lpr h G L T ) → ∀V1. ⦃G0,L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G0,L0.ⓓV0⦄ ⊢ T0 ➡[h] T1 → - ∀T2. ⇧*[1]T2 ≘ T0 → ∀X2. ⦃G0,L0⦄ ⊢ T2 ➡[h] X2 → + ∀T2. ⇧*[1]T2 ≘ T0 → ∀X2. ⦃G0,L0⦄ ⊢ T2 ➡[h] X2 → ∀L1. ⦃G0,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0,L0⦄ ⊢ ➡[h] L2 → ∃∃T. ⦃G0,L1⦄ ⊢ +ⓓV1.T1 ➡[h] T & ⦃G0,L2⦄ ⊢ X2 ➡[h] T. #h #G0 #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma index b0b50cf3a..61b24fdae 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma @@ -134,7 +134,7 @@ elim (cpx_teqx_conf_rex … HT01 … HT02 L … L) -HT01 -HT02 qed-. lemma teqx_cpx_trans: ∀h,G,L,T2. ∀T0:term. T2 ≛ T0 → - ∀T1. ⦃G,L⦄ ⊢ T0 ⬈[h] T1 → + ∀T1. ⦃G,L⦄ ⊢ T0 ⬈[h] T1 → ∃∃T. ⦃G,L⦄ ⊢ T2 ⬈[h] T & T ≛ T1. #h #G #L #T2 #T0 #HT20 #T1 #HT01 elim (cpx_teqx_conf … HT01 T2) -HT01 /3 width=3 by teqx_sym, ex2_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index 28575ff0e..74e37e0da 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -7,7 +7,7 @@ head = "cic:/matita/lambdadelta/basic_2/ (core λδ version 2)" > -