From: Ferruccio Guidi 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 ( ∃∃ ) ( ∨∨ ) ( ∧∧ )" * ] } ]