From: Ferruccio Guidi Date: Sun, 19 Oct 2014 21:56:33 +0000 (+0000) Subject: - grafiteParser: we added the comand "defined" as a presentational X-Git-Tag: make_still_working~814 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5a35a42e23b2f343f0241eeb6648bf05f31720db;p=helm.git - grafiteParser: we added the comand "defined" as a presentational alternative to "qed" for definitions. - lambdadelta: we added an example about extended validity vs. restricted validity + some minor corrections --- diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 0a2103c9a..ba58eda87 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -507,6 +507,7 @@ EXTEND grafite_ncommand: [ [ IDENT "qed" ; i = index -> G.NQed (loc,i) + | IDENT "defined" ; i = index -> G.NQed (loc,i) (* FG: presentational qed for definitions *) | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> let attrs = `Provided, nflavour, `Regular in diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index e985b7e59..9b90b9997 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -132,9 +132,10 @@ define STATS_TEMPLATE $$(STT_$(1)): P1 = $$(shell grep "^theorem " $$(MAS_$(1)) | wc -l) $$(STT_$(1)): P2 = $$(shell grep "^lemma " $$(MAS_$(1)) | wc -l) $$(STT_$(1)): P3 = $$(shell grep "^fact " $$(MAS_$(1)) | wc -l) - $$(STT_$(1)): P4 = $$(shell grep qed $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): P4 = $$(shell grep "qed[.-]" $$(MAS_$(1)) | wc -l) $$(STT_$(1)): C1 = $$(shell grep "^inductive \|^record " $$(MAS_$(1)) | wc -l) $$(STT_$(1)): C2 = $$(shell grep "^definition \|^let rec " $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): C3 = $$(shell grep "defined[.-]" $$(MAS_$(1)) | wc -l) $$(STT_$(1)): M1 = $$(shell grep "^axiom " $$(MAS_$(1)) | wc -l) $$(STT_$(1)): M2 = $$(shell grep "$$(OPEN)\*[^*:]*$$$$" $$(MAS_$(1)) | wc -l) $$(STT_$(1)): M3 = $$(shell grep "(\*\*)" $$(MAS_$(1)) | wc -l) @@ -164,7 +165,8 @@ $$(STT_$(1)): $$(MAS_$(1)) $(1)/$(1)_probe.txt $(1)/$(1)_mac.txt @printf '\x1B[1;40;33m' @printf '%-8s %6i' Declared $$(C1) @printf ' %-8s %4i' Defined $$(C2) - @printf ' %-29s' '' + @printf ' %-7s %7i' Proved $$(C3) + @printf ' %-11s' '' @printf '\x1B[0m\n' @printf '\x1B[1;40;31m' @printf '%-8s %6i' Axioms $$(M1) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma index c8359a549..c87433c2d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma @@ -16,7 +16,7 @@ include "basic_2/notation/relations/btsn_5.ma". include "basic_2/reduction/fpb.ma". include "basic_2/computation/csx.ma". -(* "QRST" STRONGLY NORMALIZING TERMS ****************************************) +(* "QRST" STRONGLY NORMALIZING CLOSURES *************************************) inductive fsb (h) (g): relation3 genv lenv term ≝ | fsb_intro: ∀G1,L1,T1. ( diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma index 6dff4c048..5a8d5d240 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma @@ -16,7 +16,7 @@ include "basic_2/computation/fpbs_aaa.ma". include "basic_2/computation/csx_aaa.ma". include "basic_2/computation/fsb_csx.ma". -(* "QRST" STRONGLY NORMALIZING TERMS ****************************************) +(* "QRST" STRONGLY NORMALIZING CLOSURES *************************************) (* Main properties **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma index 00fe4a67e..c132dae87 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma @@ -16,7 +16,7 @@ include "basic_2/notation/relations/btsnalt_5.ma". include "basic_2/computation/fpbg_fpbs.ma". include "basic_2/computation/fsb.ma". -(* "QRST" STRONGLY NORMALIZING TERMS ****************************************) +(* "QRST" STRONGLY NORMALIZING CLOSURES *************************************) (* Note: alternative definition of fsb *) inductive fsba (h) (g): relation3 genv lenv term ≝ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma index 54284a0b1..d424374a6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma @@ -18,7 +18,7 @@ include "basic_2/computation/csx_fpbs.ma". include "basic_2/computation/lsx_csx.ma". include "basic_2/computation/fsb_alt.ma". -(* "QRST" STRONGLY NORMALIZING TERMS ****************************************) +(* "QRST" STRONGLY NORMALIZING CLOSURES *************************************) (* Advanced propreties on context-sensitive extended normalizing terms ******) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma index d947c016f..d663b3009 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "basic_2/static/da_aaa.ma". -include "basic_2/computation/csx_aaa.ma". include "basic_2/computation/scpds_aaa.ma". include "basic_2/dynamic/snv.ma". @@ -38,10 +37,6 @@ lemma snv_fwd_aaa: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃A. ⦃G, L⦄ ] qed-. -lemma snv_fwd_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ⦃G, L⦄ ⊢ ⬊*[h, g] T. -#h #g #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2 by aaa_csx/ -qed-. - (* Advanced forward lemmas **************************************************) lemma snv_fwd_da: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃l. ⦃G, L⦄ ⊢ T ▪[h, g] l. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_fsb.ma new file mode 100644 index 000000000..466f19627 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_fsb.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/fsb_aaa.ma". +include "basic_2/dynamic/snv_aaa.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +(* forward lemmas on "qrst" strongly normalizing closures *********************) + +lemma snv_fwd_fsb: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ⦥[h, g] ⦃G, L, T⦄. +#h #g #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2 by aaa_fsb/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_snv_eta.ma b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_snv_eta.ma new file mode 100644 index 000000000..2320cb5bd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_snv_eta.ma @@ -0,0 +1,61 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dynamic/snv.ma". + +(* EXAMPLES *****************************************************************) + +(* Extended validy (basic?_2) vs. restricted validity (basic_1) *************) + +(* extended validity of a closure, last arg of snv_appl > 1 *) +lemma snv_extended: ∀h,g,a,G,L,k. ⦃G, L.ⓛ⋆k.ⓛⓛ{a}⋆k.⋆k.ⓛ#0⦄ ⊢ ⓐ#2.#0 ¡[h, g]. +#h #g #a #G #L #k elim (deg_total h g k) +#l #Hl @(snv_appl … a … (⋆k) … (⋆k) (0+1+1)) +[ /4 width=5 by snv_lref, drop_drop_lt/ +| /4 width=13 by snv_bind, snv_lref/ +| /5 width=6 by lstas_scpds, lstas_succ, da_ldec, da_sort, drop_drop_lt/ +| @(lstas_scpds … (l+1+1)) + /5 width=11 by lstas_bind, lstas_succ, da_bind, da_ldec, da_sort, lift_bind/ +] +qed. + +(* restricted validity of the η-expanded closure, last arg of snv_appl = 1 **) +lemma snv_restricted: ∀h,g,a,G,L,k. ⦃G, L.ⓛ⋆k.ⓛⓛ{a}⋆k.⋆k.ⓛⓛ{a}⋆k.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ¡[h, g]. +#h #g #a #G #L #k elim (deg_total h g k) +#l #Hl @(snv_appl … a … (⋆k) … (ⓐ#0.#2) (0+1)) +[ /4 width=5 by snv_lref, drop_drop_lt/ +| @snv_lref [4: // |1,2,3: skip ] + @snv_bind // + @(snv_appl … a … (⋆k) … (⋆k) (0+1)) + [ @snv_lref [4: // |1,2,3: skip ] // + | @snv_lref [4: /2 width=1 by drop_drop_lt/ |1,2,3: skip ] @snv_bind // + | @(lstas_scpds … (l+1)) /3 width=6 by da_sort, da_ldec, lstas_succ/ + | @(lstas_scpds … (l+1)) /3 width=8 by lstas_succ, lstas_bind, drop_drop, lift_bind/ + @da_ldec [3: /2 width=1 by drop_drop_lt/ |1,2: skip ] /3 width=1 by da_sort, da_bind/ + ] +| /5 width=6 by lstas_scpds, lstas_succ, da_ldec, da_sort, drop_drop_lt/ +| @(lstas_scpds … (l+1+1)) // + [ @da_ldec [3: // |1,2: skip ] + @da_bind @da_flat @da_ldec [3: /2 width=1 by drop_drop_lt/ |1,2: skip ] + /3 width=1 by da_sort, da_bind/ + | @lstas_succ [4: // |1,2: skip ] + [2: @lstas_bind | skip ] + [2: @lstas_appl | skip ] + [2: @lstas_zero + [4: /2 width=1 by drop_drop_lt/ |5: /2 width=2 by lstas_bind/ |*: skip ] + |1: skip ] + /4 width=2 by lift_flat, lift_bind, lift_lref_ge_minus, lift_lref_lt/ + ] +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma index acdc78ac6..5e31749e1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma @@ -29,7 +29,7 @@ record sd (h:sh): Type[0] ≝ { definition deg_O: relation nat ≝ λk,l. l = 0. definition sd_O: ∀h. sd h ≝ λh. mk_sd h deg_O …. -// /2 width=1/ /2 width=2/ qed. +/2 width=2 by le_n_O_to_eq, le_n, ex_intro/ defined. inductive deg_SO (h:sh) (k:nat) (k0:nat): predicate nat ≝ | deg_SO_pos : ∀l0. (next h)^l0 k0 = k → deg_SO h k k0 (l0 + 1) @@ -46,7 +46,7 @@ fact deg_SO_inv_pos_aux: ∀h,k,k0,l0. deg_SO h k k0 l0 → ∀l. l0 = l + 1 → qed. lemma deg_SO_inv_pos: ∀h,k,k0,l0. deg_SO h k k0 (l0 + 1) → (next h)^l0 k0 = k. -/2 width=3/ qed-. +/2 width=3 by deg_SO_inv_pos_aux/ qed-. lemma deg_SO_refl: ∀h,k. deg_SO h k k 1. #h #k @(deg_SO_pos … 0 ?) // @@ -62,24 +62,27 @@ lemma deg_SO_gt: ∀h,k1,k2. k1 < k2 → deg_SO h k1 k2 0. lapply (nexts_le h k2 l) #H2 lapply (le_to_lt_to_lt … H2 H1) -h -l #H elim (lt_refl_false … H) +] qed. definition sd_SO: ∀h. nat → sd h ≝ λh,k. mk_sd h (deg_SO h k) …. [ #k0 - lapply (nexts_dec h k0 k) * [ * /3 width=2/ | /4 width=2/ ] + lapply (nexts_dec h k0 k) * + [ * /3 width=2 by deg_SO_pos, ex_intro/ | /4 width=2 by deg_SO_zero, ex_intro/ ] | #K0 #l1 #l2 * [ #l01 ] #H1 * [1,3: #l02 ] #H2 // [ < H2 in H1; -H2 #H lapply (nexts_inj … H) -H #H destruct // - | elim H1 /2 width=2/ - | elim H2 /2 width=2/ + | elim H1 /2 width=2 by ex_intro/ + | elim H2 /2 width=2 by ex_intro/ ] | #k0 #l0 * - [ #l #H destruct elim l -l normalize /2 width=1/ + [ #l #H destruct elim l -l normalize + /2 width=1 by deg_SO_gt, deg_SO_pos, next_lt/ | #H1 @deg_SO_zero * #l #H2 destruct - @H1 -H1 @(ex_intro … (S l)) /2 width=1/ (**) (* explicit constructor *) + @H1 -H1 @(ex_intro … (S l)) /2 width=1 by sym_eq/ (**) (* explicit constructor *) ] ] -qed. +defined. let rec sd_l (h:sh) (k:nat) (l:nat) on l : sd h ≝ match l with @@ -97,7 +100,7 @@ lemma deg_inv_pred: ∀h,g,k,l. deg h g (next h k) (l+1) → deg h g k (l+2). elim (deg_total h g k) #l0 #H0 lapply (deg_next … H0) #H2 lapply (deg_mono … H1 H2) -H1 -H2 #H -<(associative_plus l 1 1) >H H iter_SO iter_SO on precedence qed + defined rec record return