From: Ferruccio Guidi Date: Sat, 11 Dec 2021 21:17:15 +0000 (+0100) Subject: update in delayed_updating X-Git-Tag: make_still_working~124^2 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=ec5739f16f3d23d26dd2528bf20df21919580e0f update in delayed_updating + terms are defined modulo logical equivalence --- diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_phi_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_phi_0.ma new file mode 100644 index 000000000..2e2651dbf --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_phi_0.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR DELAYED UPDATING ********************************************) + +notation "hvbox( 𝐃𝛗 )" + non associative with precedence 75 + for @{ 'ClassDPhi }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uptriangle_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uptriangle_1.ma new file mode 100644 index 000000000..09ceac1e5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uptriangle_1.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR DELAYED UPDATING ********************************************) + +notation "hvbox( ▵ term 75 t )" + non associative with precedence 75 + for @{ 'UpTriangle $t }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/in_predicate_d_phi_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/in_predicate_d_phi_1.ma deleted file mode 100644 index 7942fed3c..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/in_predicate_d_phi_1.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR DELAYED UPDATING ********************************************) - -notation "hvbox( t ϵ break 𝐃𝛗 )" - non associative with precedence 45 - for @{ 'InPredicateDPhi $t }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_arrow_epsilon_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_arrow_epsilon_2.ma deleted file mode 100644 index 1c4f842fe..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_arrow_epsilon_2.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR DELAYED UPDATING ********************************************) - -notation "hvbox( p ϵ▵ break term 46 t )" - non associative with precedence 45 - for @{ 'UpArrowEpsilon $p $t }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma index e7d140231..26fb80e56 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma @@ -17,44 +17,54 @@ include "ground/xoa/ex_3_1.ma". include "ground/xoa/ex_4_2.ma". include "ground/xoa/ex_4_3.ma". include "ground/xoa/ex_5_3.ma". +include "delayed_updating/syntax/preterm_equivalence.ma". include "delayed_updating/syntax/preterm_constructors.ma". -include "delayed_updating/notation/relations/in_predicate_d_phi_1.ma". +include "delayed_updating/notation/functions/class_d_phi_0.ma". (* BY-DEPTH DELAYED (BDD) TERM **********************************************) -inductive bdd: predicate preterm ≝ +inductive bdd: 𝒫❨preterm❩ ≝ | bdd_oref: ∀n. bdd #n | bdd_iref: ∀t,n. bdd t → bdd 𝛗n.t | bdd_abst: ∀t. bdd t → bdd 𝛌.t | bdd_appl: ∀u,t. bdd u → bdd t → bdd @u.t +| bdd_conv: ∀t1,t2. t1 ⇔ t2 → bdd t1 → bdd t2 . interpretation - "well-formed by-depth delayed (preterm)" - 'InPredicateDPhi t = (bdd t). + "by-depth delayed (preterm)" + 'ClassDPhi = (bdd). (* Basic inversions *********************************************************) lemma bdd_inv_in_comp_gen: - ∀t,p. t ϵ 𝐃𝛗 → p ϵ⬦ t → - ∨∨ ∃∃n. #n = t & 𝗱❨n❩;𝐞 = p - | ∃∃u,q,n. u ϵ 𝐃𝛗 & q ϵ⬦ u & 𝛗n.u = t & 𝗱❨n❩;q = p - | ∃∃u,q. u ϵ 𝐃𝛗 & q ϵ⬦ u & 𝛌.u = t & 𝗟;q = p - | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ⬦ u & @v.u = t & 𝗔;q = p - | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ⬦ v & @v.u = t & 𝗦;q = p + ∀t,p. t ϵ 𝐃𝛗 → p ϵ t → + ∨∨ ∃∃n. #n ⇔ t & 𝗱❨n❩;𝐞 = p + | ∃∃u,q,n. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t & 𝗱❨n❩;q = p + | ∃∃u,q. u ϵ 𝐃𝛗 & q ϵ u & 𝛌.u ⇔ t & 𝗟;q = p + | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ u & @v.u ⇔ t & 𝗔;q = p + | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ v & @v.u ⇔ t & 𝗦;q = p . -#t #p * +#t #p #H elim H -H [ #n * /3 width=3 by or5_intro0, ex2_intro/ -| #u #n #Hu * #q #Hq #Hp /3 width=7 by ex4_3_intro, or5_intro1/ -| #u #Hu * #q #Hq #Hp /3 width=6 by or5_intro2, ex4_2_intro/ -| #v #u #Hv #Hu * * #q #Hq #Hp /3 width=8 by ex5_3_intro, or5_intro3, or5_intro4/ +| #u #n #Hu #_ * #q #Hq #Hp /3 width=7 by ex4_3_intro, or5_intro1/ +| #u #Hu #_ * #q #Hq #Hp /3 width=6 by or5_intro2, ex4_2_intro/ +| #v #u #Hv #Hu #_ #_ * * #q #Hq #Hp /3 width=8 by ex5_3_intro, or5_intro3, or5_intro4/ +| #t1 #t2 #Ht12 #_ #IH #Ht2 + elim IH -IH [6: /2 width=3 by subset_in_eq_repl_fwd/ ] * + [ /4 width=3 by subset_eq_trans, or5_intro0, ex2_intro/ + | /4 width=7 by subset_eq_trans, ex4_3_intro, or5_intro1/ + | /4 width=6 by subset_eq_trans, or5_intro2, ex4_2_intro/ + | /4 width=8 by subset_eq_trans, ex5_3_intro, or5_intro3/ + | /4 width=8 by subset_eq_trans, ex5_3_intro, or5_intro4/ + ] ] qed-. lemma bdd_inv_in_comp_d: - ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩;q ϵ⬦ t → - ∨∨ ∧∧ #n = t & 𝐞 = q - | ∃∃u. u ϵ 𝐃𝛗 & q ϵ⬦ u & 𝛗n.u = t + ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩;q ϵ t → + ∨∨ ∧∧ #n ⇔ t & 𝐞 = q + | ∃∃u. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t . #t #q #n #Ht #Hq elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq * @@ -67,9 +77,9 @@ elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq * qed-. lemma bdd_inv_in_root_d: - ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩;q ϵ▵ t → - ∨∨ ∧∧ #n = t & 𝐞 = q - | ∃∃u. u ϵ 𝐃𝛗 & q ϵ▵ u & 𝛗n.u = t + ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩;q ϵ ▵t → + ∨∨ ∧∧ #n ⇔ t & 𝐞 = q + | ∃∃u. u ϵ 𝐃𝛗 & q ϵ ▵u & 𝛗n.u ⇔ t . #t #q #n #Ht * #r #Hq elim (bdd_inv_in_comp_d … Ht Hq) -Ht -Hq * @@ -82,8 +92,8 @@ elim (bdd_inv_in_comp_d … Ht Hq) -Ht -Hq * qed-. lemma bdd_inv_in_comp_L: - ∀t,q. t ϵ 𝐃𝛗 → 𝗟;q ϵ⬦ t → - ∃∃u. u ϵ 𝐃𝛗 & q ϵ⬦ u & 𝛌.u = t + ∀t,q. t ϵ 𝐃𝛗 → 𝗟;q ϵ t → + ∃∃u. u ϵ 𝐃𝛗 & q ϵ u & 𝛌.u ⇔ t . #t #q #Ht #Hq elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq * @@ -96,8 +106,8 @@ elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq * qed-. lemma bdd_inv_in_root_L: - ∀t,q. t ϵ 𝐃𝛗 → 𝗟;q ϵ▵ t → - ∃∃u. u ϵ 𝐃𝛗 & q ϵ▵ u & 𝛌.u = t. + ∀t,q. t ϵ 𝐃𝛗 → 𝗟;q ϵ ▵t → + ∃∃u. u ϵ 𝐃𝛗 & q ϵ ▵u & 𝛌.u ⇔ t. #t #q #Ht * #r #Hq elim (bdd_inv_in_comp_L … Ht Hq) -Ht -Hq #u #Hu #Hq #H0 destruct @@ -105,8 +115,8 @@ elim (bdd_inv_in_comp_L … Ht Hq) -Ht -Hq qed-. lemma bdd_inv_in_comp_A: - ∀t,q. t ϵ 𝐃𝛗 → 𝗔;q ϵ⬦ t → - ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ⬦ u & @v.u = t + ∀t,q. t ϵ 𝐃𝛗 → 𝗔;q ϵ t → + ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ u & @v.u ⇔ t . #t #q #Ht #Hq elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq * @@ -119,8 +129,8 @@ elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq * qed-. lemma bdd_inv_in_root_A: - ∀t,q. t ϵ 𝐃𝛗 → 𝗔;q ϵ▵ t → - ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ▵ u & @v.u = t + ∀t,q. t ϵ 𝐃𝛗 → 𝗔;q ϵ ▵t → + ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ ▵u & @v.u ⇔ t . #t #q #Ht * #r #Hq elim (bdd_inv_in_comp_A … Ht Hq) -Ht -Hq @@ -129,8 +139,8 @@ elim (bdd_inv_in_comp_A … Ht Hq) -Ht -Hq qed-. lemma bdd_inv_in_comp_S: - ∀t,q. t ϵ 𝐃𝛗 → 𝗦;q ϵ⬦ t → - ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ⬦ v & @v.u = t + ∀t,q. t ϵ 𝐃𝛗 → 𝗦;q ϵ t → + ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ v & @v.u ⇔ t . #t #q #Ht #Hq elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq * @@ -143,8 +153,8 @@ elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq * qed-. lemma bdd_inv_in_root_S: - ∀t,q. t ϵ 𝐃𝛗 → 𝗦;q ϵ▵ t → - ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ▵ v & @v.u = t + ∀t,q. t ϵ 𝐃𝛗 → 𝗦;q ϵ ▵t → + ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ ▵v & @v.u ⇔ t . #t #q #Ht * #r #Hq elim (bdd_inv_in_comp_S … Ht Hq) -Ht -Hq @@ -155,13 +165,17 @@ qed-. (* Advanced inversions ******************************************************) lemma bbd_mono_in_root_d: - ∀l,n,p,t. t ϵ 𝐃𝛗 → p,𝗱❨n❩ ϵ▵ t → p,l ϵ▵ t → 𝗱❨n❩ = l. + ∀l,n,p,t. t ϵ 𝐃𝛗 → p,𝗱❨n❩ ϵ ▵t → p,l ϵ ▵t → 𝗱❨n❩ = l. #l #n #p elim p -p [ #t #Ht