From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
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/?p=helm.git;a=commitdiff_plain;h=5a35a42e23b2f343f0241eeb6648bf05f31720db

- 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<def>> (* ≝ *); 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 <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).
@@ -111,7 +114,7 @@ qed-.
 
 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.
@@ -124,5 +127,5 @@ lemma sd_l_SS: ∀h,k,l. sd_l h k (l + 2) = sd_l h (next h k) (l + 1).
 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.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/sh.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sh.ma
index bab748f75..0d09320cc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/sh.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/sh.ma
@@ -23,14 +23,14 @@ record sh: Type[0] ≝ {
 }.
 
 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.
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 1723a0005..c31b9bf06 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
@@ -12,7 +12,7 @@ table {
    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" * ]
           }
         ]
      }
@@ -52,7 +52,7 @@ table {
         ]
         [ { "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" * ]
           }
         ]
      }
diff --git a/matita/matita/matita.lang b/matita/matita/matita.lang
index ea9d31828..713b71810 100644
--- a/matita/matita/matita.lang
+++ b/matita/matita/matita.lang
@@ -134,6 +134,7 @@
           <keyword>on</keyword>
           <keyword>precedence</keyword>
           <keyword>qed</keyword>
+          <keyword>defined</keyword>
           <keyword>rec</keyword>
           <keyword>record</keyword>
           <keyword>return</keyword>