From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 28 Feb 2021 19:38:50 +0000 (+0100)
Subject: update in gruound
X-Git-Tag: make_still_working~155
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ae626612bff9c3746dd7647bbada791c737e348c;p=helm.git

update in gruound

+ library refactored and restyled
+ recomm updated
---

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/bGroundLib.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/bGroundLib.mrc
new file mode 100644
index 000000000..fdc932735
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/bGroundLib.mrc
@@ -0,0 +1,6 @@
+PcsAnd b "" true false
+eq
+land
+lsub
+compose, function composition
+ctc, contextual transitive closure
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/dGroundLib.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/dGroundLib.mrc
new file mode 100644
index 000000000..c829279fd
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/dGroundLib.mrc
@@ -0,0 +1,9 @@
+PccFor d "" true false
+GROUND NOTATION, GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ
+RELATIONS
+FUNCTIONS
+LOGIC
+BOOLEANS
+LISTS
+STREAMS
+GENERATED LIBRARY
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml
index 19128fb63..f39e07e03 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml
@@ -48,10 +48,16 @@ let write_component st =
   write_mli cmod
 
 let write_index st =
+  let p = float (List.length st.ET.mods) in
+  let p =
+    if p > 0. then truncate (log10 p) else -1
+  in
+  let ps = Printf.sprintf "%%0%uu" (succ p) in
+  let fmt = Scanf.format_from_string ps "%u" in
   let cmod = Filename.concat st.ET.cdir "recommGc" in
   let och = open_out (cmod ^ ".ml") in
   let iter i name =
-    Printf.fprintf och "module G%03u = RecommGc%s\n" (succ i) name
+    Printf.fprintf och "module G%(%u%) = RecommGc%s\n" fmt (succ i) name
   in
   List.iteri iter st.ET.mods;
   close_out och;
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/pGroundLib.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/pGroundLib.mrc
new file mode 100644
index 000000000..5b2fc18af
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/pGroundLib.mrc
@@ -0,0 +1,2 @@
+PcsPar p "" true false
+(with reflexivity)
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/rGroundArith.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/rGroundArith.mrc
index bfc2730fc..ac34215e1 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/rGroundArith.mrc
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/rGroundArith.mrc
@@ -8,7 +8,7 @@ PREDECESSOR
 ADDITION
 SUBTRACTION
 LEFT SUBTRACTION
-MAXIMUM, MAXIMUN
+MAXIMUM
 ORDER
 STRICT ORDER
 ARITHMETICAL PROPERTIES
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/rGroundLib.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/rGroundLib.mrc
new file mode 100644
index 000000000..7c2382e22
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/rGroundLib.mrc
@@ -0,0 +1,10 @@
+PccFor r "" true false
+CONJUNCTION
+DISJUNCTION
+EXTENSIONAL EQUIVALENCE
+TRANSITIVE CLOSURE
+LABELLED TRANSITIVE CLOSURE
+NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE
+HEAD AND TAIL
+ITERATED TAIL
+LENGTH
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml
index b3fd0b550..58f1f1001 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml
@@ -1,10 +1,14 @@
-module G001 = RecommGcbGroundArith
-module G002 = RecommGcbGroundCounters
-module G003 = RecommGcdGroundArith
-module G004 = RecommGcdGroundCounters
-module G005 = RecommGcpGroundArith
-module G006 = RecommGcrGroundArith
-module G007 = RecommGcrGroundCounters
-module G008 = RecommGcsAttr
-module G009 = RecommGcsMain
-module G010 = RecommGcsWith
+module G01 = RecommGcbGroundArith
+module G02 = RecommGcbGroundCounters
+module G03 = RecommGcbGroundLib
+module G04 = RecommGcdGroundArith
+module G05 = RecommGcdGroundCounters
+module G06 = RecommGcdGroundLib
+module G07 = RecommGcpGroundArith
+module G08 = RecommGcpGroundLib
+module G09 = RecommGcrGroundArith
+module G10 = RecommGcrGroundCounters
+module G11 = RecommGcrGroundLib
+module G12 = RecommGcsAttr
+module G13 = RecommGcsMain
+module G14 = RecommGcsWith
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundLib.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundLib.ml
new file mode 100644
index 000000000..94db88ed7
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundLib.ml
@@ -0,0 +1,17 @@
+module T = RecommTypes
+module R = RecommPcsAnd
+
+let step k st outs ins =
+  if st <> T.OO then k st outs ins else
+  match ins with
+  | "ctc" :: tl -> k T.OK ("ctc" :: outs) tl
+  | "contextual" :: "transitive" :: "closure" :: tl -> k T.OK ("ctc" :: outs) tl
+  | "compose" :: tl -> k T.OK ("compose" :: outs) tl
+  | "function" :: "composition" :: tl -> k T.OK ("compose" :: outs) tl
+  | "lsub" :: tl -> k T.OK ("lsub" :: outs) tl
+  | "land" :: tl -> k T.OK ("land" :: outs) tl
+  | "eq" :: tl -> k T.OK ("eq" :: outs) tl
+  | _ -> k T.OO outs ins
+
+let main =
+  R.register_b step
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundLib.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundLib.mli
new file mode 100644
index 000000000..e69de29bb
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundLib.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundLib.ml
new file mode 100644
index 000000000..7fda12b7c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundLib.ml
@@ -0,0 +1,19 @@
+module T = RecommTypes
+module R = RecommPccFor
+
+let step k st outs ins =
+  if st <> T.OO then k st outs ins else
+  match ins with
+  | "GENERATED" :: "LIBRARY" :: tl -> k T.OK ("LIBRARY" :: "GENERATED" :: outs) tl
+  | "STREAMS" :: tl -> k T.OK ("STREAMS" :: outs) tl
+  | "LISTS" :: tl -> k T.OK ("LISTS" :: outs) tl
+  | "BOOLEANS" :: tl -> k T.OK ("BOOLEANS" :: outs) tl
+  | "LOGIC" :: tl -> k T.OK ("LOGIC" :: outs) tl
+  | "FUNCTIONS" :: tl -> k T.OK ("FUNCTIONS" :: outs) tl
+  | "RELATIONS" :: tl -> k T.OK ("RELATIONS" :: outs) tl
+  | "GROUND" :: "NOTATION" :: tl -> k T.OK ("NOTATION" :: "GROUND" :: outs) tl
+  | "GENERAL" :: "NOTATION" :: "USED" :: "BY" :: "THE" :: "FORMAL" :: "SYSTEM" :: "\206\187\206\180" :: tl -> k T.OK ("NOTATION" :: "GROUND" :: outs) tl
+  | _ -> k T.OO outs ins
+
+let main =
+  R.register_d step
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundLib.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundLib.mli
new file mode 100644
index 000000000..e69de29bb
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundLib.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundLib.ml
new file mode 100644
index 000000000..085f6dff6
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundLib.ml
@@ -0,0 +1,11 @@
+module T = RecommTypes
+module R = RecommPcsPar
+
+let step k st outs ins =
+  if st <> T.OO then k st outs ins else
+  match ins with
+  | "(with" :: "reflexivity)" :: tl -> k T.OK ("reflexivity)" :: "(with" :: outs) tl
+  | _ -> k T.OO outs ins
+
+let main =
+  R.register_p step
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundLib.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundLib.mli
new file mode 100644
index 000000000..e69de29bb
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml
index 091cc7f5f..136681a29 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml
@@ -8,7 +8,6 @@ let step k st outs ins =
   | "STRICT" :: "ORDER" :: tl -> k T.OK ("ORDER" :: "STRICT" :: outs) tl
   | "ORDER" :: tl -> k T.OK ("ORDER" :: outs) tl
   | "MAXIMUM" :: tl -> k T.OK ("MAXIMUM" :: outs) tl
-  | "MAXIMUN" :: tl -> k T.OK ("MAXIMUM" :: outs) tl
   | "LEFT" :: "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: "LEFT" :: outs) tl
   | "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: outs) tl
   | "ADDITION" :: tl -> k T.OK ("ADDITION" :: outs) tl
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundLib.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundLib.ml
new file mode 100644
index 000000000..644497245
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundLib.ml
@@ -0,0 +1,19 @@
+module T = RecommTypes
+module R = RecommPccFor
+
+let step k st outs ins =
+  if st <> T.OO then k st outs ins else
+  match ins with
+  | "LENGTH" :: tl -> k T.OK ("LENGTH" :: outs) tl
+  | "ITERATED" :: "TAIL" :: tl -> k T.OK ("TAIL" :: "ITERATED" :: outs) tl
+  | "HEAD" :: "AND" :: "TAIL" :: tl -> k T.OK ("TAIL" :: "AND" :: "HEAD" :: outs) tl
+  | "NAT-LABELED" :: "REFLEXIVE" :: "AND" :: "TRANSITIVE" :: "CLOSURE" :: tl -> k T.OK ("CLOSURE" :: "TRANSITIVE" :: "AND" :: "REFLEXIVE" :: "NAT-LABELED" :: outs) tl
+  | "LABELLED" :: "TRANSITIVE" :: "CLOSURE" :: tl -> k T.OK ("CLOSURE" :: "TRANSITIVE" :: "LABELLED" :: outs) tl
+  | "TRANSITIVE" :: "CLOSURE" :: tl -> k T.OK ("CLOSURE" :: "TRANSITIVE" :: outs) tl
+  | "EXTENSIONAL" :: "EQUIVALENCE" :: tl -> k T.OK ("EQUIVALENCE" :: "EXTENSIONAL" :: outs) tl
+  | "DISJUNCTION" :: tl -> k T.OK ("DISJUNCTION" :: outs) tl
+  | "CONJUNCTION" :: tl -> k T.OK ("CONJUNCTION" :: outs) tl
+  | _ -> k T.OO outs ins
+
+let main =
+  R.register_r step
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundLib.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundLib.mli
new file mode 100644
index 000000000..e69de29bb
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.ml
index 091bb2d12..8d00bb812 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.ml
@@ -6,6 +6,8 @@ let step k st outs ins =
   if st = T.KO then k st outs ins else
   match ins with
   | "with" :: tl -> k T.OK ("with" :: outs) tl
+  | "of" :: tl -> k T.OK ("with" :: outs) tl
+  | "for" :: tl -> k T.OK ("with" :: outs) tl
   | _ -> k T.OO outs ins
 
 let main =
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll b/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll
index 99ff840af..83a289247 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll
@@ -5,6 +5,7 @@
 
   let keys = [|
     "Note";
+    "NOTE";
   |]
 
   let heads = [|
@@ -37,9 +38,9 @@
     aux (String.length s - 1)
 
   let disambiguate_word s =
-    if is_uppercase_ascii s then EP.CW s else
     if Array.mem s keys then EP.KW s else
     if Array.mem s heads then EP.HW s else
+    if is_uppercase_ascii s then EP.CW s else
     EP.SW s
 
   let log s =
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml
index e0f3f1d70..187a2984b 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml
@@ -13,8 +13,8 @@ let string_length_utf8 s =
   in
   l - aux 0 0
 
-let complete s =
-  let l = !width - string_length_utf8 s - 6 in
+let complete s n =
+  let l = !width - string_length_utf8 s - 5 - n in
   if l < 0 then begin
     Printf.eprintf "overfull: %S\n" s;
     ""
@@ -30,13 +30,16 @@ let out_src och = function
   | ET.Mark s             ->
     Printf.fprintf och "(* *%s*)" s
   | ET.Key (s1, s2)       ->
-    Printf.fprintf och "(* %s%s*)" s1 s2
+    let s3 =
+      if s1 = "NOTE" then complete (s1^s2) 0 else ""
+    in
+    Printf.fprintf och "(* %s%s%s*)" s1 s2 s3
   | ET.Title ss           ->
     let s = String.concat " " ss in
-    Printf.fprintf och "(* %s %s*)" s (complete s)
+    Printf.fprintf och "(* %s %s*)" s (complete s 1)
   | ET.Slice ss           ->
     let s = String.capitalize_ascii (String.concat " " ss) in
-    Printf.fprintf och "(* %s %s*)" s (complete s)
+    Printf.fprintf och "(* %s %s*)" s (complete s 1)
   | ET.Other (s1, s2, s3) ->
     Printf.fprintf och "%s%s%s" s1 s2 s3
 
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml
index 41a787dbd..4111798fc 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml
@@ -14,6 +14,7 @@ let k_for k st outs ins =
   if st <> ET.OK then k ET.KO outs ins else
   match ins with
   | "FOR" :: tl -> !d_line (k_exit k) ET.OO ("FOR" :: outs) tl
+  | "OF" :: tl -> !d_line (k_exit k) ET.OO ("FOR" :: outs) tl
   | _           -> k ET.KO outs ins
 
 let k_or k st outs ins =
diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/sWith.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/sWith.mrc
index ecd022556..f057ad614 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/sWith.mrc
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/sWith.mrc
@@ -1,2 +1,2 @@
 check s "GcsMain" false false
-with
+with, of, for
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_max.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_max.ma
index 0ad906540..b877b8649 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_max.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_max.ma
@@ -35,9 +35,7 @@ lemma nle_max_dx_refl_sn (m) (n): m ≤ (m ∨ n).
 qed.
 
 lemma nle_max_dx_refl_dx (m) (n): n ≤ (m ∨ n).
-#m #n @(nat_ind_2_succ … n m) -m -n //
-#m #n #IH <nmax_succ_bi /2 width=1 by nle_succ_bi/
-qed.
+// qed.
 
 (* Basic destructions with nmax *********************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/ground/generated/insert_eq_1.ma b/matita/matita/contribs/lambdadelta/ground/generated/insert_eq_1.ma
new file mode 100644
index 000000000..4652c2e86
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/generated/insert_eq_1.ma
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "basics/relations.ma".
+
+(* GENERATED LIBRARY ********************************************************)
+
+lemma insert_eq_1 (T1) (a1) (Q1,Q2:predicate T1):
+      (∀b1. Q1 b1 → a1 = b1 → Q2 b1) → Q1 a1 → Q2 a1.
+/2 width=1 by/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/generated/pull_2.ma b/matita/matita/contribs/lambdadelta/ground/generated/pull_2.ma
new file mode 100644
index 000000000..dd1411ebb
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/generated/pull_2.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 "basics/pts.ma".
+
+(* GENERATED LIBRARY ********************************************************)
+
+lemma pull_2 (A1:Type[0])
+             (A2:Type[0])
+             (A:A1→A2→Type[0]):
+             (∀x2,x1. A x1 x2) →
+             (∀x1,x2. A x1 x2).
+/2 width=1 by/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/generated/pull_4.ma b/matita/matita/contribs/lambdadelta/ground/generated/pull_4.ma
new file mode 100644
index 000000000..a2e0baffb
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/generated/pull_4.ma
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "basics/pts.ma".
+
+(* GENERATED LIBRARY ********************************************************)
+
+lemma pull_4 (A1:Type[0])
+             (A2:A1→Type[0])
+             (A3:∀x1.A2 x1→Type[0])
+             (A4:Type[0])
+             (A:∀x1:A1.∀x2:A2 x1.A3 x1 x2 → A4 → Type[0]):
+             (∀x4,x1,x2,x3. A x1 x2 x3 x4) →
+             (∀x1,x2,x3,x4. A x1 x2 x3 x4).
+/2 width=1 by/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/insert_eq/insert_eq_1.ma b/matita/matita/contribs/lambdadelta/ground/insert_eq/insert_eq_1.ma
deleted file mode 100644
index 4652c2e86..000000000
--- a/matita/matita/contribs/lambdadelta/ground/insert_eq/insert_eq_1.ma
+++ /dev/null
@@ -1,21 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basics/relations.ma".
-
-(* GENERATED LIBRARY ********************************************************)
-
-lemma insert_eq_1 (T1) (a1) (Q1,Q2:predicate T1):
-      (∀b1. Q1 b1 → a1 = b1 → Q2 b1) → Q1 a1 → Q2 a1.
-/2 width=1 by/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma b/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma
index 5b655e686..148cbc512 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma
@@ -15,7 +15,7 @@
 include "ground/notation/relations/doteq_4.ma".
 include "ground/lib/relations.ma".
 
-(* EXTENSIONAL EQUIVALENCE **************************************************)
+(* EXTENSIONAL EQUIVALENCE FOR FUNCTIONS ************************************)
 
 definition exteq (A,B:Type[0]): relation (A → B) ≝
            λf1,f2. ∀a. f1 a = f2 a.
@@ -44,7 +44,7 @@ lemma exteq_canc_sn (A) (B): left_cancellable … (exteq A B).
 lemma exteq_canc_dx (A) (B): right_cancellable … (exteq A B).
 /2 width=1 by exteq_repl/ qed-.
 
-(* Constructions with function composition **********************************)
+(* Constructions with compose ***********************************************)
 
 lemma compose_repl_fwd_dx (A) (B) (C) (g) (f1) (f2):
       f1 ≐{A,B} f2 → g ∘ f1 ≐{A,C} g ∘ f2.
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_eq.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_eq.ma
index ffa06ab6d..a24530890 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_eq.ma
@@ -15,7 +15,7 @@
 include "ground/notation/relations/ringeq_3.ma".
 include "ground/lib/list.ma".
 
-(* EXTENSIONAL EQUIVALENCE OF LISTS *****************************************)
+(* EXTENSIONAL EQUIVALENCE FOR LISTS ****************************************)
 
 rec definition list_eq A (l1,l2:list A) on l1 ≝
 match l1 with
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/logic.ma b/matita/matita/contribs/lambdadelta/ground/lib/logic.ma
index fc2e2ea85..1de5ee4c0 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/logic.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/logic.ma
@@ -28,7 +28,7 @@ interpretation
 
 (* LOGIC ********************************************************************)
 
-(* Constructions with And ***************************************************)
+(* Constructions with land **************************************************)
 
 lemma commutative_and: ∀A,B. A ∧ B → B ∧ A.
 #A #B * /2 width=1 by conj/
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/lstar_2a.ma b/matita/matita/contribs/lambdadelta/ground/lib/lstar_2a.ma
index ba513ae85..dc3ed1ef3 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/lstar_2a.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/lstar_2a.ma
@@ -15,7 +15,7 @@
 include "ground/lib/ltc.ma".
 include "ground/arith/nat_plus.ma".
 
-(* NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE FOR FOR λδ-2A ***************)
+(* NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE FOR λδ-2A *******************)
 
 definition lstar_aux (B) (R:relation B) (l): relation B ≝
            λb1,b2. ∨∨ (∧∧ l = 𝟎 & b1 = b2) | (∧∧ l = 𝟏  & R b1 b2).
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma b/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma
index 1d08fb15d..c0d091c3c 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma
@@ -15,7 +15,7 @@
 include "ground/insert_eq/insert_eq_1.ma".
 include "ground/lib/functions.ma".
 
-(* LABELLED TRANSITIVE CLOSURE **********************************************)
+(* LABELLED TRANSITIVE CLOSURE FOR RELATIONS ********************************)
 
 inductive ltc (A:Type[0]) (f) (B) (R:relation3 A B B): relation3 A B B ≝
 | ltc_rc   : ∀a,b1,b2. R a b1 b2 → ltc … a b1 b2
@@ -56,7 +56,7 @@ generalize in match IHb0; generalize in match Hb0; generalize in match a1; -IHb0
 elim H -a2 -b -b2 /4 width=4 by ltc_trans/
 qed-.
 
-(* Advanced elimiations with reflexivity ************************************)
+(* Advanced eliminations (with reflexivity) *********************************)
 
 lemma ltc_ind_sn_refl (A) (i) (f) (B) (R) (Q:relation2 A B) (b2):
                       associative … f → right_identity … f i → reflexive B (R i) →
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/ltc_ctc.ma b/matita/matita/contribs/lambdadelta/ground/lib/ltc_ctc.ma
index 54b1117b6..e6fcccec6 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/ltc_ctc.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/ltc_ctc.ma
@@ -15,11 +15,11 @@
 include "ground/lib/star.ma".
 include "ground/lib/ltc.ma".
 
-(* LABELLED TRANSITIVE CLOSURE **********************************************)
+(* LABELLED TRANSITIVE CLOSURE FOR RELATIONS ********************************)
 
-alias symbol "subseteq" = "relation inclusion". (**)
+alias symbol "subseteq" = "relation inclusion". (* * alias *)
 
-(* Constructions with contextual transitive closure *************************)
+(* Constructions with ctc ***************************************************)
 
 lemma ltc_CTC (C) (A) (i) (f) (B) (R:relation4 C A B B):
               left_identity … f i →
@@ -28,7 +28,7 @@ lemma ltc_CTC (C) (A) (i) (f) (B) (R:relation4 C A B B):
 #b #b2 #_ #Hb2 #IH >(Hf i) -Hf /2 width=3 by ltc_dx/
 qed.
 
-(* Inversions with contextual transitive closure ****************************)
+(* Inversions with ctc ******************************************************)
 
 lemma ltc_inv_CTC (C) (A) (i) (f) (B) (R:relation4 C A B B):
                   associative … f → annulment_2 … f i →
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/relations.ma b/matita/matita/contribs/lambdadelta/ground/lib/relations.ma
index 56f6e21f7..328e2ea5b 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/relations.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/relations.ma
@@ -17,28 +17,7 @@ include "ground/xoa/and_3.ma".
 include "ground/xoa/ex_2_2.ma".
 include "ground/lib/logic.ma".
 
-(* GENERIC RELATIONS ********************************************************)
-
-definition replace_2 (A) (B): relation3 (relation2 A B) (relation A) (relation B) ≝
-           λR,Sa,Sb. ∀a1,b1. R a1 b1 → ∀a2. Sa a1 a2 → ∀b2. Sb b1 b2 → R a2 b2.
-
-(* Inclusion ****************************************************************)
-
-definition subR2 (S1) (S2): relation (relation2 S1 S2) ≝
-           λR1,R2. (∀a1,a2. R1 a1 a2 → R2 a1 a2).
-
-interpretation
-  "2-relation inclusion"
-  'subseteq R1 R2 = (subR2 ?? R1 R2).
-
-definition subR3 (S1) (S2) (S3): relation (relation3 S1 S2 S3) ≝
-           λR1,R2. (∀a1,a2,a3. R1 a1 a2 a3 → R2 a1 a2 a3).
-
-interpretation
-  "3-relation inclusion"
-  'subseteq R1 R2 = (subR3 ??? R1 R2).
-
-(* Properties of relations **************************************************)
+(* RELATIONS ****************************************************************)
 
 definition relation5: Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] ≝
            λA,B,C,D,E.A→B→C→D→E→Prop.
@@ -46,7 +25,10 @@ definition relation5: Type[0] → Type[0] → Type[0] → Type[0] → Type[0] 
 definition relation6: Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] ≝
            λA,B,C,D,E,F.A→B→C→D→E→F→Prop.
 
-(**) (* we don't use "∀a. reflexive … (R a)" since auto seems to dislike repeatd δ-expansion *)
+definition replace_2 (A) (B): relation3 (relation2 A B) (relation A) (relation B) ≝
+           λR,Sa,Sb. ∀a1,b1. R a1 b1 → ∀a2. Sa a1 a2 → ∀b2. Sb b1 b2 → R a2 b2.
+
+(* * we don't use "∀a. reflexive … (R a)" since auto seems to dislike repeatd δ-expansion *)
 definition c_reflexive (A) (B): predicate (relation3 A B B) ≝
            λR. ∀a,b. R a b b.
 
@@ -95,15 +77,7 @@ definition is_mono (B:Type[0]): predicate (predicate B) ≝
 definition is_inj2 (A,B:Type[0]): predicate (relation2 A B) ≝
            λR. ∀a1,b. R a1 b → ∀a2. R a2 b → a1 = a2.
 
-(* Main properties of equality **********************************************)
-
-theorem canc_sn_eq (A): left_cancellable A (eq …).
-// qed-.
-
-theorem canc_dx_eq (A): right_cancellable A (eq …).
-// qed-.
-
-(* Normal form and strong normalization *************************************)
+(* NOTE: Normal form and strong normalization *******************************)
 
 definition NF (A): relation A → relation A → predicate A ≝
            λR,S,a1. ∀a2. R a1 a2 → S a1 a2.
@@ -135,13 +109,13 @@ lemma NF_to_SN_sn (A) (R) (S): ∀a. NF_sn A R S a → SN_sn A R S a.
 elim HSa12 -HSa12 /2 width=1 by/
 qed.
 
-(* Normal form and strong normalization with unboxed triples ****************)
+(* NOTE: Normal form and strong normalization with unboxed triples **********)
 
 inductive SN3 (A) (B) (C) (R,S:relation6 A B C A B C): relation3 A B C ≝
 | SN3_intro: ∀a1,b1,c1. (∀a2,b2,c2. R a1 b1 c1 a2 b2 c2 → (S a1 b1 c1 a2 b2 c2 → ⊥) → SN3 … R S a2 b2 c2) → SN3 … R S a1 b1 c1
 .
 
-(* Relations with unboxed triples *******************************************)
+(* NOTE: Reflexive closure with unboxed triples *****************************)
 
 definition tri_RC (A,B,C): tri_relation A B C → tri_relation A B C ≝
            λR,a1,b1,c1,a2,b2,c2.
@@ -150,3 +124,27 @@ definition tri_RC (A,B,C): tri_relation A B C → tri_relation A B C ≝
 
 lemma tri_RC_reflexive (A) (B) (C): ∀R. tri_reflexive A B C (tri_RC … R).
 /3 width=1 by and3_intro, or_intror/ qed.
+
+(* NOTE: Inclusion for relations ********************************************)
+
+definition subR2 (S1) (S2): relation (relation2 S1 S2) ≝
+           λR1,R2. (∀a1,a2. R1 a1 a2 → R2 a1 a2).
+
+interpretation
+  "2-relation inclusion"
+  'subseteq R1 R2 = (subR2 ?? R1 R2).
+
+definition subR3 (S1) (S2) (S3): relation (relation3 S1 S2 S3) ≝
+           λR1,R2. (∀a1,a2,a3. R1 a1 a2 a3 → R2 a1 a2 a3).
+
+interpretation
+  "3-relation inclusion"
+  'subseteq R1 R2 = (subR3 ??? R1 R2).
+
+(* Main constructions with eq ***********************************************)
+
+theorem canc_sn_eq (A): left_cancellable A (eq …).
+// qed-.
+
+theorem canc_dx_eq (A): right_cancellable A (eq …).
+// qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/star.ma b/matita/matita/contribs/lambdadelta/ground/lib/star.ma
index 5e748c5ea..ee7ff16f7 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/star.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/star.ma
@@ -15,7 +15,7 @@
 include "basics/star1.ma".
 include "ground/lib/relations.ma".
 
-(* TRANSITIVE CLOSURE *******************************************************)
+(* TRANSITIVE CLOSURE FOR RELATIONS *****************************************)
 
 definition CTC: ∀A:Type[0]. ∀B. (A→relation B) → (A→relation B) ≝
                 λA,B,R,a. TC … (R a).
@@ -139,7 +139,7 @@ elim (TC_idem … (S L2) …  T1 T2)
 #_ #H1 #H2 #_ @H2 @HSR /3 width=3 by/
 qed-.
 
-(* Normal form and strong normalization *************************************)
+(* NOTE: Normal form and strong normalization *******************************)
 
 lemma SN_to_NF: ∀A,R,S. NF_dec A R S →
                 ∀a1. SN A R S a1 →
@@ -149,7 +149,7 @@ lemma SN_to_NF: ∀A,R,S. NF_dec A R S →
 * #a0 #Ha10 #Ha01 elim (IHa1 … Ha10 Ha01) -IHa1 -Ha01 /3 width=3 by star_compl, ex2_intro/
 qed-.
 
-(* Relations with unboxed pairs *********************************************)
+(* NOTE: Relations with unboxed pairs ***************************************)
 
 lemma bi_TC_strip: ∀A,B,R. bi_confluent A B R →
                    ∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. bi_TC … R a0 b0 a2 b2 →
@@ -186,11 +186,11 @@ lemma bi_TC_decomp_l: ∀A,B. ∀R:bi_relation A B.
                       ∃∃a,b. R a1 b1 a b & bi_TC … R a b a2 b2.
 #A #B #R #a1 #a2 #b1 #b2 #H @(bi_TC_ind_dx … a1 b1 H) -a1 -b1
 [ /2 width=1 by or_introl/
-| #a1 #a #b1 #b #Hab1 #Hab2 #_ /3 width=4 by ex2_2_intro, or_intror/ (**) (* auto fails without #_ *)
+| #a1 #a #b1 #b #Hab1 #Hab2 #_ /3 width=4 by ex2_2_intro, or_intror/ (* * auto fails without #_ *)
 ]
 qed-.
 
-(* Relations with unboxed triples *******************************************)
+(* NOTE: Relations with unboxed triples *************************************)
 
 definition tri_star: ∀A,B,C,R. tri_relation A B C ≝
                      λA,B,C,R. tri_RC A B C (tri_TC … R).
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream.ma
index d0e05e17e..ff7a6c349 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream.ma
@@ -30,3 +30,11 @@ interpretation
 lemma stream_rew (A) (t:stream A): match t with [ stream_cons a u ⇒ a ⨮ u ] = t.
 #A * //
 qed.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_stream_cons_bi (A) (a1,a2:A) (u1) (u2):
+      a1 ⨮ u1 = a2 ⨮ u2 → ∧∧ a1 = a2 & u1 = u2.
+#A #a1 #a2 #u1 #u2 #H destruct
+/2 width=1 by conj/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/pull/pull_2.ma b/matita/matita/contribs/lambdadelta/ground/pull/pull_2.ma
deleted file mode 100644
index dd1411ebb..000000000
--- a/matita/matita/contribs/lambdadelta/ground/pull/pull_2.ma
+++ /dev/null
@@ -1,24 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basics/pts.ma".
-
-(* GENERATED LIBRARY ********************************************************)
-
-lemma pull_2 (A1:Type[0])
-             (A2:Type[0])
-             (A:A1→A2→Type[0]):
-             (∀x2,x1. A x1 x2) →
-             (∀x1,x2. A x1 x2).
-/2 width=1 by/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/pull/pull_4.ma b/matita/matita/contribs/lambdadelta/ground/pull/pull_4.ma
deleted file mode 100644
index a2e0baffb..000000000
--- a/matita/matita/contribs/lambdadelta/ground/pull/pull_4.ma
+++ /dev/null
@@ -1,26 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basics/pts.ma".
-
-(* GENERATED LIBRARY ********************************************************)
-
-lemma pull_4 (A1:Type[0])
-             (A2:A1→Type[0])
-             (A3:∀x1.A2 x1→Type[0])
-             (A4:Type[0])
-             (A:∀x1:A1.∀x2:A2 x1.A3 x1 x2 → A4 → Type[0]):
-             (∀x4,x1,x2,x3. A x1 x2 x3 x4) →
-             (∀x1,x2,x3,x4. A x1 x2 x3 x4).
-/2 width=1 by/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/nstream.ma b/matita/matita/contribs/lambdadelta/ground/relocation/nstream.ma
index 42c174ddc..8819cdc51 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/nstream.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/nstream.ma
@@ -88,7 +88,7 @@ lemma iota_next: ∀R,a,b,f. b f = case_type0 R a b (↑f).
 #R #a #b * //
 qed.
 
-(* Specific properties ******************************************************)
+(* Poperties with stream_tl *************************************************)
 
 lemma tl_push: ∀f. f = ⫰⫯f.
 // qed.