alternative to "qed" for definitions.
- lambdadelta: we added an example about extended validity vs.
restricted validity + some minor corrections
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<def>> (* ≝ *); body = term -> body ] ->
let attrs = `Provided, nflavour, `Regular in
$$(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)
@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)
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. (
include "basic_2/computation/csx_aaa.ma".
include "basic_2/computation/fsb_csx.ma".
-(* "QRST" STRONGLY NORMALIZING TERMS ****************************************)
+(* "QRST" STRONGLY NORMALIZING CLOSURES *************************************)
(* Main properties **********************************************************)
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 ≝
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 ******)
(**************************************************************************)
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".
]
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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
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)
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 ?) //
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
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 <plus_minus_m_m // /2 width=3 by transitive_le/
+<(associative_plus l 1 1) >H <plus_minus_m_m /2 width=3 by transitive_le/
qed-.
lemma deg_inv_prec: ∀h,g,k,l,l0. deg h g ((next h)^l k) (l0+1) → deg h g k (l+l0+1).
lemma deg_iter: ∀h,g,k,l1,l2. deg h g k l1 → deg h g ((next h)^l2 k) (l1-l2).
#h #g #k #l1 #l2 @(nat_ind_plus … l2) -l2 [ <minus_n_O // ]
-#l2 #IHl2 #Hkl1 >iter_SO <minus_plus /3 width=1/
+#l2 #IHl2 #Hkl1 >iter_SO <minus_plus /3 width=1 by deg_next/
qed.
lemma deg_next_SO: ∀h,g,k,l. deg h g k (l+1) → deg h g (next h k) l.
qed.
lemma sd_l_correct: ∀h,l,k. deg h (sd_l h k l) k l.
-#h #l @(nat_ind_plus … l) -l // #l @(nat_ind_plus … l) -l // /3 width=1 by deg_inv_pred/
+#h #l @(nat_ind_plus … l) -l // #l @(nat_ind_plus … l) -l /3 width=1 by deg_inv_pred/
qed.
}.
definition sh_N: sh ≝ mk_sh S ….
-// qed.
+// defined.
(* Basic properties *********************************************************)
lemma nexts_le: ∀h,k,l. k ≤ (next h)^l k.
#h #k #l elim l -l // normalize #l #IHl
lapply (next_lt h ((next h)^l k)) #H
-lapply (le_to_lt_to_lt … IHl H) -IHl -H /2 width=2/
+lapply (le_to_lt_to_lt … IHl H) -IHl -H /2 width=2 by lt_to_le/
qed.
lemma nexts_lt: ∀h,k,l. k < (next h)^(l+1) k.
class "wine"
[ { "examples" * } {
[ { "terms with special features" * } {
- [ "ex_sta_ldec" + "ex_cpr_omega" + "ex_fpbg_refl" * ]
+ [ "ex_sta_ldec" + "ex_cpr_omega" + "ex_fpbg_refl" + "ex_snv_eta" * ]
}
]
}
]
[ { "stratified native validity" * } {
[ "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ]
- [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_scpes" + "snv_preserve" * ]
+ [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_fsb" + "snv_scpes" + "snv_preserve" * ]
}
]
}
<keyword>on</keyword>
<keyword>precedence</keyword>
<keyword>qed</keyword>
+ <keyword>defined</keyword>
<keyword>rec</keyword>
<keyword>record</keyword>
<keyword>return</keyword>
projects / helm.git / commitdiff