From 90ee1e85245752414b93826aabe388409571187a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 1 Jun 2013 14:27:30 +0000 Subject: [PATCH] - basic_2: induction for preservation results now uses supclosure relation rather than weight on closures - app_2: "functional" component updated - we park delifting substitution for now --- .../apps_2/etc/MLTT1/genv_primitive.etc | 246 ++++++++++++++++++ .../apps_2/etc/MLTT1/judgement.etc | 33 +++ .../lambdadelta/apps_2/etc/MLTT1/notation.etc | 108 ++++++++ .../lambdadelta/apps_2/etc/MLTT1/syntax.etc | 45 ++++ .../dsubst.ma => etc/dsubst/dsubst.etc} | 4 + .../lambdadelta/apps_2/functional/lift.ma | 2 +- .../lambdadelta/apps_2/functional/notation.ma | 4 - .../lambdadelta/apps_2/functional/rtm.ma | 1 + .../lambdadelta/apps_2/web/apps_2_src.tbl | 18 +- .../lambdadelta/basic_2/dynamic/lsubsv_snv.ma | 8 +- .../lambdadelta/basic_2/dynamic/snv_lift.ma | 8 +- .../lambdadelta/basic_2/dynamic/snv_lpr.ma | 12 +- .../lambdadelta/basic_2/dynamic/snv_ssta.ma | 2 +- .../basic_2/dynamic/snv_ssta_lpr.ma | 4 +- .../lambdadelta/basic_2/dynamic/ygt.ma | 5 +- .../lambdadelta/basic_2/dynamic/ypr.ma | 3 +- .../lambdadelta/basic_2/dynamic/yprs.ma | 9 +- .../lambdadelta/basic_2/dynamic/ysc.ma | 2 +- .../lambdadelta/basic_2/relocation/fsup.ma | 13 +- .../lambdadelta/basic_2/substitution/fsupp.ma | 27 ++ .../lambdadelta/basic_2/substitution/fsups.ma | 5 + .../basic_2/substitution/lpss_ldrop.ma | 2 +- .../lambdadelta/basic_2/unfold/lpqs_ldrop.ma | 2 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 8 + 24 files changed, 522 insertions(+), 49 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/apps_2/etc/MLTT1/genv_primitive.etc create mode 100644 matita/matita/contribs/lambdadelta/apps_2/etc/MLTT1/judgement.etc create mode 100644 matita/matita/contribs/lambdadelta/apps_2/etc/MLTT1/notation.etc create mode 100644 matita/matita/contribs/lambdadelta/apps_2/etc/MLTT1/syntax.etc rename matita/matita/contribs/lambdadelta/apps_2/{functional/dsubst.ma => etc/dsubst/dsubst.etc} (95%) diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/MLTT1/genv_primitive.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/MLTT1/genv_primitive.etc new file mode 100644 index 000000000..bdb968e47 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/MLTT1/genv_primitive.etc @@ -0,0 +1,246 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "apps_2/MLTT1_1/syntax.ma". + +(* PRIMITIVE GLOBAL CONSTANTS **********************************************) + +(* symbolic names for referring the primitive global constants *) + +definition empty ≝ 0. (* empty type *) + +definition erec ≝ 1. (* empty eliminator *) + +definition one ≝ 2. (* unit type *) + +definition tt ≝ 3. (* unit constructor *) + +definition orec ≝ 4. (* unit eliminator *) + +definition nat ≝ 5. (* natural numbers type *) + +definition zero ≝ 6. (* natural numbers constructor: zero *) + +definition succ ≝ 7. (* natural numbers constructor: successor *) + +definition nrec ≝ 8. (* natural numbers eliminator *) + +definition ii ≝ 9. (* intensional identity type *) + +definition refl ≝ 10. (* intensional identity constructor *) + +definition irec ≝ 11. (* intensional identity eliminator *) + +definition sum ≝ 12. (* disjoint sum type *) + +definition sn ≝ 13. (* disjoint sum constructor: left *) + +definition dx ≝ 14. (* disjoint sum constructor: right *) + +definition srec ≝ 15. (* disjoint sum eliminator *) + +definition prod ≝ 16. (* dependent product type *) + +definition pair ≝ 17. (* dependent product constructor *) + +definition prec ≝ 18. (* dependent product eliminator *) + +definition fun ≝ 19. (* dependent function type *) + +definition abst ≝ 20. (* dependent function constructor *) + +definition ap ≝ 21. (* dependent function eliminator *) + +definition univ ≝ 22. (* first universe type *) + +definition ue ≝ 23. (* first universe constructor: empty *) + +definition uo ≝ 24. (* first universe constructor: one *) + +definition un ≝ 25. (* first universe constructor: nat *) + +definition ui ≝ 26. (* first universe constructor: ii *) + +definition us ≝ 27. (* first universe constructor: sum *) + +definition up ≝ 28. (* first universe constructor: union *) + +definition uf ≝ 29. (* first universe constructor: fun *) + +definition urec ≝ 30. (* first universe eliminator *) + +definition primitives ≝ 31. (* number of primitive constants *) + +(* primitive global environment *) + +definition Gp: lenv ≝ + ⋆ + Λ □ (* empty *) + Λ □ ⤏ □ (* erec *) + Λ □ (* one *) + Λ □ (* tt *) + Λ □ ⤏ □ ⤏ □ (* orec *) + Λ □ (* nat *) + Λ □ (* zero *) + Λ □ ⤏ □ (* succ *) + Λ □ ⤏ □ ⤏ (□ ⤏ □ ⤏ □) ⤏ □ (* nrec *) + Λ □ ⤏ □ ⤏ □ ⤏ □ (* ii *) + Λ □ ⤏ □ (* refl *) + Λ □ ⤏ (□ ⤏ □) ⤏ □ (* irec *) + Λ □ ⤏ □ ⤏ □ (* sum *) + Λ □ ⤏ □ (* sn *) + Λ □ ⤏ □ (* dx *) + Λ □ ⤏ (□ ⤏ □) ⤏ (□ ⤏ □) ⤏ □ (* srec *) + Λ □ ⤏ (□ ⤏ □) ⤏ □ (* prod *) + Λ □ ⤏ □ ⤏ □ (* pair *) + Λ □ ⤏ (□ ⤏ □ ⤏ □) ⤏ □ (* prec *) + Λ □ ⤏ (□ ⤏ □) ⤏ □ (* fun *) + Λ (□ ⤏ □) ⤏ □ (* abst *) + Λ □ ⤏ □ ⤏ □ (* ap *) + Λ □ (* univ *) + Λ □ (* ue *) + Λ □ (* uo *) + Λ □ (* un *) + Λ □ ⤏ □ ⤏ □ ⤏ □ (* ui *) + Λ □ ⤏ □ ⤏ □ (* us *) + Λ □ ⤏ (□ ⤏ □) ⤏ □ (* up *) + Λ □ ⤏ (□ ⤏ □) ⤏ □ (* uf *) + Λ □ ⤏ □ (* urec *) +. + +(* notation for applying the primitive constants *) + +interpretation + "empty type (MLTT)" + 'Empty = (TAtom (GRef empty)). + +interpretation + "empty eliminator (MLTT)" + 'ERec T = (TPair Appl T (TAtom (GRef erec))). + +interpretation + "unit type (MLTT)" + 'One = (TAtom (GRef one)). + +interpretation + "unit constructor (MLTT)" + 'TT = (TAtom (GRef tt)). + +interpretation + "unit eliminator (MLTT)" + 'SRec T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef srec)))). + +interpretation + "natural numbers type (MLTT)" + 'Nat = (TAtom (GRef nat)). + +interpretation + "natural numbers constructor: zero (MLTT)" + 'Zero = (TAtom (GRef zero)). + +interpretation + "natural numbers constructor: successor (MLTT)" + 'Succ T = (TPair Appl T (TAtom (GRef succ))). + +interpretation + "natural numbers eliminator (MLTT)" + 'NRec T1 T2 T3 = (TPair Appl T3 (TPair Appl T2 (TPair Appl T1 (TAtom (GRef nrec))))). + +interpretation + "intensional identity type (MLTT)" + 'II T1 T2 T3 = (TPair Appl T3 (TPair Appl T2 (TPair Appl T1 (TAtom (GRef ii))))). + +interpretation + "intensional identity constructor (MLTT)" + 'Refl T = (TPair Appl T (TAtom (GRef refl))). + +interpretation + "intensional identity eliminator (MLTT)" + 'IRec T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef irec)))). + +interpretation + "sum type (MLTT)" + 'Sum T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef sum)))). + +interpretation + "sum constructorL left (MLTT)" + 'Sn T = (TPair Appl T (TAtom (GRef sn))). + +interpretation + "sum constructor: right (MLTT)" + 'Dx T = (TPair Appl T (TAtom (GRef dx))). + +interpretation + "sum eliminator (MLTT)" + 'SRec T1 T2 T3 = (TPair Appl T3 (TPair Appl T2 (TPair Appl T1 (TAtom (GRef srec))))). + +interpretation + "product type (MLTT)" + 'Prod T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef prod)))). + +interpretation + "product constructor (MLTT)" + 'Pair T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef pair)))). + +interpretation + "product eliminator (MLTT)" + 'PRec T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef prec)))). + +interpretation + "function type (MLTT)" + 'Fun T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef fun)))). + +interpretation + "function constructor (MLTT)" + 'Abst T = (TPair Appl T (TAtom (GRef abst))). + +interpretation + "function eliminator (MLTT)" + 'AP T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef ap)))). + +interpretation + "first universe type (MLTT)" + 'Univ = (TAtom (GRef univ)). + +interpretation + "first universe constructor: empty (MLTT)" + 'UE = (TAtom (GRef ue)). + +interpretation + "first universe constructor: one (MLTT)" + 'UO = (TAtom (GRef us)). + +interpretation + "first universe constructor: nat (MLTT)" + 'UN = (TAtom (GRef un)). + +interpretation + "first universe constructor: ii (MLTT)" + 'UI T1 T2 T3 = (TPair Appl T3 (TPair Appl T2 (TPair Appl T1 (TAtom (GRef ui))))). + +interpretation + "first universe constructor: sum (MLTT)" + 'US T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef us)))). + +interpretation + "first universe constructor: product (MLTT)" + 'UP T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef up)))). + +interpretation + "first universe constructor: function (MLTT)" + 'UF T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef uf)))). + +interpretation + "first universe eliminator (MLTT)" + 'URec T = (TPair Appl T (TAtom (GRef urec))). diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/MLTT1/judgement.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/MLTT1/judgement.etc new file mode 100644 index 000000000..8baaaa461 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/MLTT1/judgement.etc @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold/delift.ma". +include "apps_2/MLTT1_1/genv_primitive.ma". + +(* JUDJEMENTS ***************************************************************) + +(* type judgement *) +inductive TJ: lenv → predicate term ≝ +| tj_weak : ∀L,V,T1,T2. TJ L V → TJ L T1 → ⇧[0,1] T1 ≡ T2 → TJ (L Λ V) T2 +| tj_empty: TJ (⋆) 𝔼 +| tj_one : TJ (⋆) 𝕆 +| tj_sum : ∀G,A,B. TJ G A → TJ G B → TJ G (A ⊕ B) +. + +(* element judgement *) +inductive EJ: lenv → relation term ≝ +| tj_erec: ∀L,V,T1,T2. + EJ L V 𝔼 → TJ (L Λ 𝔼) T1 → L Δ V ⊢ T1 [0,1] ≡ T2 → EJ L 𝕖𝕣[V] T2 +| tj_tt : EJ (⋆) 𝕥 𝕆 +. diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/MLTT1/notation.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/MLTT1/notation.etc new file mode 100644 index 000000000..fa2268d5e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/MLTT1/notation.etc @@ -0,0 +1,108 @@ +(**************************************************************************) +(* ___ *) +(* ||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 MARTIN-LÖF TYPE THEORY WITH ONE UNIVERSE (MLTT1) ************) + +(* Syntax extension *********************************************************) + +notation "hvbox( □ )" + non associative with precedence 90 + for @{ 'Box }. + +notation "hvbox(T1 break ⤏ T2)" + right associative with precedence 65 + for @{ 'TImp $T1 $T2 }. + +notation "hvbox( L break Λ T )" + left associative with precedence 60 + for @{ 'LAbst $L $T }. + +notation "hvbox( L break Δ T )" + left associative with precedence 60 + for @{ 'LAbbr $L $T }. + +notation "hvbox( Λ T )" + non associative with precedence 65 + for @{ 'TAbst $T }. + +(* Primitive global constants ***********************************************) + +notation "hvbox( 𝔼 )" + non associative with precedence 90 + for @{ 'Empty }. + +notation "hvbox( 𝕖𝕣 [ T ] )" + non associative with precedence 90 + for @{ 'ERec $T }. + +notation "hvbox( 𝕆 )" + non associative with precedence 90 + for @{ 'One }. + +notation "hvbox( 𝕥 )" + non associative with precedence 90 + for @{ 'TT }. + +notation "hvbox( 𝕠𝕣 [ T1 , break T2 ] )" + non associative with precedence 90 + for @{ 'ORec $T1 $T2 }. +(* +notation "hvbox( ℕ )" + non associative with precedence 90 + for @{ 'Nat }. + +notation "hvbox( 𝕫 )" + non associative with precedence 90 + for @{ 'Zero }. + +notation "hvbox( 𝕤 [ T ] )" + non associative with precedence 90 + for @{ 'Succ $T }. + +notation "hvbox( 𝕟𝕣 [ T1 , break T2 , break T3 ] )" + non associative with precedence 90 + for @{ 'NRec $T1 $T2 $3 }. +*) +notation "hvbox( T1 ⊕ T2 )" + left associative with precedence 70 + for @{ 'Sum $T1 $T2 }. + +notation "hvbox( 𝕤𝕟 [ T ] )" + non associative with precedence 90 + for @{ 'Sn $T }. + +notation "hvbox( 𝕕𝕩 [ T ] )" + non associative with precedence 90 + for @{ 'Dx $T }. + +notation "hvbox( 𝕤𝕣 [ T1 , break T2 , break T3 ] )" + non associative with precedence 90 + for @{ 'SRec $T1 $T2 $3 }. +(* +notation "hvbox( 𝕌 )" + non associative with precedence 90 + for @{ 'Univ }. + +notation "hvbox( 𝕖 )" + non associative with precedence 90 + for @{ 'UE }. + +notation "hvbox( 𝕠 )" + non associative with precedence 90 + for @{ 'UO }. + +notation "hvbox( 𝕟 )" + non associative with precedence 90 + for @{ 'UN }. +*) diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/MLTT1/syntax.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/MLTT1/syntax.etc new file mode 100644 index 000000000..8ee237f27 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/MLTT1/syntax.etc @@ -0,0 +1,45 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* MARTIN-LÖF TYPE THEORY WITH ONE UNIVERSE (MLTT1): MATITA SOURCE FILES + * Specification started: 2011 December 12 + * - Patience on me to gain peace and perfection! - + *) + +include "basic_2/grammar/lenv.ma". +include "apps_2/MLTT1_1/notation.ma". + +(* EXTENDED NOTATION ********************************************************) + +definition sort ≝ 0. + +interpretation + "global definition" + 'LAbbr L T = (LPair L Abbr T). + +interpretation + "global declaration" + 'LAbst L T = (LPair L Abst T). + +interpretation + "atom (arity)" + 'Box = (TAtom (Sort sort)). + +interpretation + "function (arity)" + 'TImp T1 T2 = (TPair Abst T1 T2). + +interpretation + "function (term)" + 'TAbst T = (TPair Abst (TAtom (Sort sort)) T). diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/dsubst.ma b/matita/matita/contribs/lambdadelta/apps_2/etc/dsubst/dsubst.etc similarity index 95% rename from matita/matita/contribs/lambdadelta/apps_2/functional/dsubst.ma rename to matita/matita/contribs/lambdadelta/apps_2/etc/dsubst/dsubst.etc index c43cd1d74..18827d555 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/dsubst.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/etc/dsubst/dsubst.etc @@ -12,6 +12,10 @@ (* *) (**************************************************************************) +notation "hvbox( [ term 46 d ⬐ break term 46 V ] break term 46 T )" + non associative with precedence 46 + for @{ 'DSubst $V $d $T }. + include "basic_2/unfold/delift_lift.ma". include "apps_2/functional/lift.ma". diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/lift.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/lift.ma index bf05ea36a..92c791912 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/lift.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/lift.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/substitution/lift.ma". +include "basic_2/relocation/lift.ma". include "apps_2/functional/notation.ma". (* FUNCTIONAL RELOCATION ****************************************************) diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma index f830afff1..9039ce783 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma @@ -22,10 +22,6 @@ notation "hvbox( ↑ [ term 46 d , break term 46 e ] break term 46 T )" non associative with precedence 46 for @{ 'Lift $d $e $T }. -notation "hvbox( [ term 46 d ⬐ break term 46 V ] break term 46 T )" - non associative with precedence 46 - for @{ 'DSubst $V $d $T }. - notation "hvbox( T1 ⇨ break term 46 T2 )" non associative with precedence 45 for @{ 'SRed $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma index c7acff72e..5153b713f 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma @@ -14,6 +14,7 @@ include "basic_2/grammar/term_vector.ma". include "basic_2/grammar/genv.ma". +include "apps_2/functional/notation.ma". (* REDUCTION AND TYPE MACHINE ***********************************************) 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 627c05d6e..3bd24d90e 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 @@ -9,7 +9,8 @@ table { ] } ] - class "yellow" +(* + class "orange" [ { "MLTT1" * } { [ { "" * } { [ "genv_primitive" "judgement" * ] @@ -17,22 +18,15 @@ table { ] } ] - class "orange" +*) + class "red" [ { "functional" * } { [ { "reduction and type machine" * } { [ "rtm" "rtm_step ( ? ⇨ ? )" * ] } ] - [ { "unfold" * } { - [ "lift ( ↑[?,?] ? )" "subst ( [?←?] ? )" * ] - } - ] - } - ] - class "red" - [ { "examples" * } { - [ { "" * } { - [ "" * ] + [ { "relocation" * } { + [ "lift ( ↑[?,?] ? )" * ] } ] } diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma index 896875371..eed454bae 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma @@ -31,9 +31,9 @@ fact snv_lsubsv_aux: ∀h,g,L0,T0. [ #i #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2 elim (snv_inv_lref … H) -H #I2 #K2 #W2 #HLK2 #HW2 elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -HL12 #X #H #HLK1 - lapply (ldrop_pair2_fwd_fw … HLK2 (#i)) -HLK2 #HLK2 elim (lsubsv_inv_pair2 … H) -H * #K1 - [ #HK12 #H destruct /4 width=8 by snv_lref, fw_ygt/ (**) (* auto too slow without trace *) + [ #HK12 #H destruct + /5 width=8 by snv_lref, fsupp_ygt, fsupp_lref/ (**) (* auto too slow without trace *) | #W1 #V1 #V2 #l #HV1 #_ #_ #_ #_ #_ #H #_ destruct /2 width=5/ ] | #p #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2 -IH1 @@ -50,11 +50,11 @@ fact snv_lsubsv_aux: ∀h,g,L0,T0. lapply (cpcs_cprs_strap1 … HW10 … HW0) -W0 #H elim (cpcs_inv_cprs … H) -H #W0 #HW10 #HW0 lapply (dxprs_cprs_trans … (ⓛ{a}W0.U2) HTU ?) [ /2 width=1/ ] -HTU -HW0 - /4 width=8 by snv_appl, fw_ygt/ (**) (* auto too slow without trace *) + /4 width=8 by snv_appl, fsupp_ygt/ (**) (* auto too slow without trace *) | #W #T #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2 elim (snv_inv_cast … H) -H #U #l #HW #HT #HTU #HUW lapply (lsubsv_cpcs_trans … HL12 … HUW) -HUW #HUW elim (lsubsv_ssta_trans … HTU … HL12) -HTU #U0 #HTU0 #HU0 - lapply (cpcs_trans … HU0 … HUW) -U /4 width=4 by snv_cast, fw_ygt/ (**) (* auto too slow without trace *) + lapply (cpcs_trans … HU0 … HUW) -U /4 width=4 by snv_cast, fsupp_ygt/ (**) (* auto too slow without trace *) ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma index 966760b80..0a1feae91 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma @@ -86,11 +86,13 @@ lemma snv_fsup_conf: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → [ #I1 #L1 #V1 #H elim (snv_inv_lref … H) -H #I2 #L2 #V2 #H #HV2 lapply (ldrop_inv_refl … H) -H #H destruct // -|2,3: #a #I #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H // -|4,5: * #L1 #V1 #T1 #H +|2: * +|5: /3 width=7 by snv_inv_lift/ +] +[1,3: #a #I #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H // +|2,4: * #L1 #V1 #T1 #H [1,3: elim (snv_inv_appl … H) -H // |2,4: elim (snv_inv_cast … H) -H // ] -| /3 width=7 by snv_inv_lift/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma index 44a77627c..db1058f75 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma @@ -33,12 +33,12 @@ fact snv_cpr_lpr_aux: ∀h,g,L0,T0. elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1 elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct - lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKL + lapply (fsupp_lref … HLK1) #HKL elim (cpr_inv_lref1 … H2) -H2 [ #H destruct -HLK1 lapply (IH1 … HV12 … HK12) -IH1 -HV12 -HK12 // -HV1 [ /2 width=1/ ] -HKL /2 width=5/ | * #K0 #V0 #W0 #H #HVW0 #W0 -HV12 - lapply (ldrop_mono … H … HLK1) -HLK1 -H #H destruct + lapply (ldrop_mono … H … HLK1) -HLK1 -H #H destruct lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2 lapply (IH1 … HVW0 … HK12) -IH1 -HVW0 -HK12 // -HV1 [ /2 width=1/ ] -HKL /3 width=7/ ] @@ -80,17 +80,17 @@ fact snv_cpr_lpr_aux: ∀h,g,L0,T0. lapply (IH1 … HT20 … HT202 … (L2.ⓛW20) ?) [1,2: /2 width=1/ ] -HT20 #HT2 lapply (IH2 … HVW2) // [ @(ygt_yprs_trans … L1 L1 … V1) (**) (* auto /4 width=5/ is a bit slow even with trace *) - [ /2 width=1 by fw_ygt/ + [ /2 width=1 by fsupp_ygt/ | /3 width=1 by cprs_lpr_yprs, cpr_cprs/ ] ] #HW2 elim (snv_fwd_ssta … HW20) #l0 #U20 #HWU20 elim (ssta_fwd_correct … HVW2) [g] ⦃L2, T2⦄. -/3 width=1/ qed. +lemma fsupp_ygt: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄. +#h #g #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -L2 -T2 /3 width=1/ /3 width=4/ +qed. lemma cprs_ygt: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → h ⊢ ⦃L, T1⦄ >[g] ⦃L, T2⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma index b1c75077e..0167f4cd3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma @@ -12,13 +12,14 @@ (* *) (**************************************************************************) +include "basic_2/relocation/fsup.ma". include "basic_2/reduction/lpr.ma". include "basic_2/dynamic/lsubsv.ma". (* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) inductive ypr (h) (g) (L1) (T1): relation2 lenv term ≝ -| ypr_fw : ∀L2,T2. ♯{L2, T2} < ♯{L1, T1} → ypr h g L1 T1 L2 T2 +| ypr_fsup : ∀L2,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ypr h g L1 T1 L2 T2 | ypr_lpr : ∀L2. L1 ⊢ ➡ L2 → ypr h g L1 T1 L2 T1 | ypr_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → ypr h g L1 T1 L1 T2 | ypr_ssta : ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, T2⦄ → ypr h g L1 T1 L1 T2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma index 2bf1ae018..08461cda5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/substitution/fsupp.ma". include "basic_2/computation/lprs.ma". include "basic_2/dynamic/ypr.ma". @@ -52,9 +53,11 @@ lemma yprs_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L, T⦄ h ⊢ ⦃L, T⦄ ≥[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄. /2 width=4/ qed-. -lemma fw_yprs: ∀h,g,L1,L2,T1,T2. ♯{L2, T2} < ♯{L1, T1} → - h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄. -/3 width=1/ qed. +(* Note: this is a general property of bi_TC *) +lemma fsupp_yprs: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → + h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄. +#h #g #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -L2 -T2 /3 width=1/ /3 width=4/ +qed. lemma cprs_yprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → h ⊢ ⦃L, T1⦄ ≥[g] ⦃L, T2⦄. #h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=4 by ypr_cpr, yprs_strap1/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma index 88d19aea1..d779eb15f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma @@ -17,7 +17,7 @@ include "basic_2/dynamic/ypr.ma". (* "BIG TREE" PROPER PARALLEL REDUCTION FOR CLOSURES ************************) inductive ysc (h) (g) (L1) (T1): relation2 lenv term ≝ -| ysc_fw : ∀L2,T2. ♯{L2, T2} < ♯{L1, T1} → ysc h g L1 T1 L2 T2 +| ysc_fsup : ∀L2,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ysc h g L1 T1 L2 T2 | ysc_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → ysc h g L1 T1 L1 T2 | ysc_ssta : ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, T2⦄ → ysc h g L1 T1 L1 T2 | ysc_lsubsv: ∀L2. h ⊢ L2 ¡⊑[g] L1 → (L1 = L2 → ⊥) → ysc h g L1 T1 L2 T1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma index 6b0ee2185..cffa08c68 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma @@ -18,9 +18,8 @@ include "basic_2/relocation/ldrop.ma". inductive fsup: bi_relation lenv term ≝ | fsup_lref : ∀I,L,V. fsup (L.ⓑ{I}V) (#0) L V -| fsup_bind_sn: ∀a,I,L,V,T. fsup L (ⓑ{a,I}V.T) L V +| fsup_pair_sn: ∀I,L,V,T. fsup L (②{I}V.T) L V | fsup_bind_dx: ∀a,I,L,V,T. fsup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T -| fsup_flat_sn: ∀I,L,V,T. fsup L (ⓕ{I}V.T) L V | fsup_flat_dx: ∀I,L,V,T. fsup L (ⓕ{I}V.T) L T | fsup_ldrop : ∀L1,K1,K2,T1,T2,U1,d,e. ⇩[d, e] L1 ≡ K1 → ⇧[d, e] T1 ≡ U1 → @@ -57,11 +56,11 @@ qed-. fact fsup_fwd_length_lref1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀i. T1 = #i → |L2| < |L1|. #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 -[ 6: #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct - lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1 - elim (lift_inv_lref2 … HTU1) -HTU1 * #Hdei #H destruct - @(lt_to_le_to_lt … HLK1) /2 width=2/ -| normalize // |2,3: #a +[5: #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct + lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1 + elim (lift_inv_lref2 … HTU1) -HTU1 * #Hdei #H destruct + @(lt_to_le_to_lt … HLK1) /2 width=2/ +| normalize // |3: #a ] #I #L #V #T #j #H destruct qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma index a35be783f..149a6bd82 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma @@ -52,6 +52,33 @@ lemma fsupp_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃ ⦃L, T⦄ → ⦃L, T ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄. /2 width=4/ qed. +lemma fsupp_lref: ∀I,K,V,i,L. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃L, #i⦄ ⊃+ ⦃K, V⦄. +/3 width=2/ qed. + +lemma fsupp_pair_sn: ∀I,L,V,T. ⦃L, ②{I}V.T⦄ ⊃+ ⦃L, V⦄. +/2 width=1/ qed. + +lemma fsupp_bind_dx: ∀a,K,I,V,T. ⦃K, ⓑ{a,I}V.T⦄ ⊃+ ⦃K.ⓑ{I}V, T⦄. +/2 width=1/ qed. + +lemma fsupp_flat_dx: ∀I,L,V,T. ⦃L, ⓕ{I}V.T⦄ ⊃+ ⦃L, T⦄. +/2 width=1/ qed. + +lemma fsupp_flat_dx_pair_sn: ∀I1,I2,L,V1,V2,T. ⦃L, ⓕ{I1}V1.②{I2}V2.T⦄ ⊃+ ⦃L, V2⦄. +/2 width=4/ qed. + +lemma fsupp_bind_dx_flat_dx: ∀a,I1,I2,L,V1,V2,T. ⦃L, ⓑ{a,I1}V1.ⓕ{I2}V2.T⦄ ⊃+ ⦃L.ⓑ{I1}V1, T⦄. +/2 width=4/ qed. + +lemma fsupp_flat_dx_bind_dx: ∀a,I1,I2,L,V1,V2,T. ⦃L, ⓕ{I1}V1.ⓑ{a,I2}V2.T⦄ ⊃+ ⦃L.ⓑ{I2}V2, T⦄. +/2 width=4/ qed. +(* +lemma fsupp_append_sn: ∀I,L,K,V,T. ⦃L.ⓑ{I}V@@K, T⦄ ⊃+ ⦃L, V⦄. +#I #L #K #V * +[ * #i +normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/ (**) (* auto too slow without trace *) +qed. +*) (* Basic forward lemmas *****************************************************) lemma fsupp_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma index e2a52aeef..d915b89f1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma @@ -63,6 +63,11 @@ lemma fsups_fsupp_fsupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃* ⦃L, T⦄ → lemma fsupp_fsups_fsupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃+ ⦃L, T⦄ → ⦃L, T⦄ ⊃* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄. /2 width=4/ qed. +(* +lemma fsups_pippo: ∀L,T. ⦃L, T⦄ ⊃+ ⦃L, #0⦄. +#L * * +[ #i +*) (* Basic forward lemmas *****************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_ldrop.ma index 17fa5b45f..4237c7666 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpss_ldrop.ma @@ -34,7 +34,7 @@ lemma lpss_ldrop_trans_O1: dropable_dx lpss. lemma fsup_cpss_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ▶* U2 → ∃∃L,U1. L1 ⊢ ▶* L & L ⊢ T1 ▶* U1 & ⦃L, U1⦄ ⊃ ⦃L2, U2⦄. -#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ] +#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [2: * ] [1,2,3,4,5: /3 width=5/ ] #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2 elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HT2 elim (lift_total T d e) #U #HTU diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_ldrop.ma index 2b838d285..854420d60 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpqs_ldrop.ma @@ -34,7 +34,7 @@ lemma lpqs_ldrop_trans_O1: dropable_dx lpqs. lemma fsup_cpqs_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ➤* U2 → ∃∃L,U1. L1 ⊢ ➤* L & L ⊢ T1 ➤* U1 & ⦃L, U1⦄ ⊃ ⦃L2, U2⦄. -#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ] +#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [2: * ] [1,2,3,4,5: /3 width=5/ ] #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2 elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HT2 elim (lift_total T d e) #U #HTU diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 96b64d882..799c4c950 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -10,6 +10,14 @@ table { } ] (* + class "wine" + [ { "examples" * } { + [ { "" * } { + [ "" * ] + } + ] + } + ] class "magenta" [ { "higher order dynamic typing" * } { [ { "higher order native type assignment" * } { -- 2.39.2