From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Thu, 10 May 2018 10:27:14 +0000 (+0200)
Subject: update in ground_2
X-Git-Tag: make_still_working~325
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d9a1ff8259a7882caa0ffd27282838c00a34cab5;p=helm.git

update in ground_2

set up for equality insertion lemmas
---

diff --git a/matita/matita/contribs/lambdadelta/ground_2/insert_eq/insert_eq_0.ma b/matita/matita/contribs/lambdadelta/ground_2/insert_eq/insert_eq_0.ma
new file mode 100644
index 000000000..6a3788e7d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/insert_eq/insert_eq_0.ma
@@ -0,0 +1,20 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_0: ∀A,a. ∀Q1,Q2:predicate A. (∀a0. Q1 a0 → a = a0 → Q2 a0) → Q1 a → Q2 a.
+/2 width=1 by/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma
index 27ef34de4..4bfd5c7c7 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/insert_eq/insert_eq_0.ma".
 include "ground_2/lib/functions.ma".
 
 (* LABELLED TRANSITIVE CLOSURE **********************************************)
@@ -37,7 +38,7 @@ lemma ltc_ind_sn (A) (f) (B) (R) (Q:relation2 A B) (b2): associative … f →
                  (∀a,b1. R a b1 b2 → Q a b1) →
                  (∀a1,a2,b1,b. R a1 b1 b → ltc … f … R a2 b b2 → Q a2 b → Q (f a1 a2) b1) →
                  ∀a,b1. ltc … f … R a b1 b2 → Q a b1.
-#A #f #B #R #Q #b2 #Hf #IH1 #IH2 #a #b1 @(insert_eq … b2)
+#A #f #B #R #Q #b2 #Hf #IH1 #IH2 #a #b1 @(insert_eq_0 … b2)
 #b0 #H elim H -a -b1 -b0 /2 width=2 by/
 #a1 #a2 #b1 #b #b0 #H #Hb2 #_
 generalize in match Hb2; generalize in match a2; -Hb2 -a2
@@ -48,7 +49,7 @@ lemma ltc_ind_dx (A) (f) (B) (R) (Q:A→predicate B) (b1): associative … f →
                  (∀a,b2. R a b1 b2 → Q a b2) →
                  (∀a1,a2,b,b2. ltc … f … R a1 b1 b → Q a1 b → R a2 b b2 → Q (f a1 a2) b2) →
                  ∀a,b2. ltc … f … R a b1 b2 → Q a b2.
-#A #f #B #R #Q #b1 #Hf #IH1 #IH2 #a #b2 @(insert_eq … b1)
+#A #f #B #R #Q #b1 #Hf #IH1 #IH2 #a #b2 @(insert_eq_0 … b1)
 #b0 #H elim H -a -b0 -b2 /2 width=2 by/
 #a1 #a2 #b0 #b #b2 #Hb0 #H #IHb0 #_
 generalize in match IHb0; generalize in match Hb0; generalize in match a1; -IHb0 -Hb0 -a1
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma
index 7c63b469f..fa8bae343 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma
@@ -17,9 +17,6 @@ include "ground_2/lib/logic.ma".
 
 (* GENERIC RELATIONS ********************************************************)
 
-lemma insert_eq: ∀A,a. ∀Q1,Q2:predicate A. (∀a0. Q1 a0 → a = a0 → Q2 a0) → Q1 a → Q2 a.
-/2 width=1 by/ qed-.
-
 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.
 
diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
index 06ff4be72..77174d94b 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
@@ -62,8 +62,12 @@ table {
      }
    ]
    class "orange"
-   [ { "generated logical decomposables" * } {
-        [ { "" * } {
+   [ { "generated library" * } {
+        [ { "equality insertion" * } {
+             [ "insert_eq" * ]
+          }
+        ]
+        [ { "logical decomposables" * } {
              [ "xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )" * ]
           }
         ]