From: Ferruccio Guidi Date: Mon, 6 Dec 2021 19:45:59 +0000 (+0100) Subject: update in delayed_updating X-Git-Tag: make_still_working~127 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=160b7f7385763d872b5f2632696d02fd540c4eae;p=helm.git update in delayed_updating + wip on predicate for bdd terms + updated notation + additions to lists --- diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.ma new file mode 100644 index 000000000..e08c4ea27 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.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( @ break term 76 u. break term 75 t )" + non associative with precedence 75 + for @{ 'At $u $t }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/comma_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/comma_2.ma new file mode 100644 index 000000000..f2f318da5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/comma_2.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( hd , break tl )" + right associative with precedence 50 + for @{ 'Comma $hd $tl }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/hash_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/hash_1.ma new file mode 100644 index 000000000..8d85b354a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/hash_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( # break term 90 n )" + non associative with precedence 75 + for @{ 'Hash $n }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/lamda_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/lamda_1.ma new file mode 100644 index 000000000..379a9092d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/lamda_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( 𝛌 . break term 75 t )" + non associative with precedence 75 + for @{ 'Lamda $t }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_1.ma index 8412e58e4..919edaa64 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_1.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_1.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* GROUND NOTATION **********************************************************) +(* NOTATION FOR DELAYED UPDATING ********************************************) notation "hvbox( 𝗱❨ break term 46 a ❩ )" non associative with precedence 75 diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/phi_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/phi_2.ma new file mode 100644 index 000000000..7d04cc37a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/phi_2.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( 𝛗 break term 76 n. break term 75 t )" + non associative with precedence 75 + for @{ 'Phi $n $t }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/semicolon_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/semicolon_2.ma new file mode 100644 index 000000000..81c475923 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/semicolon_2.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( hd ; break tl )" + right associative with precedence 47 + for @{ 'Semicolon $hd $tl }. 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 new file mode 100644 index 000000000..7942fed3c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/in_predicate_d_phi_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( 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 new file mode 100644 index 000000000..1c4f842fe --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_arrow_epsilon_2.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( p ϵ▵ break term 46 t )" + non associative with precedence 45 + for @{ 'UpArrowEpsilon $p $t }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_down_arrow_epsilon_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_down_arrow_epsilon_2.ma new file mode 100644 index 000000000..ffef611a4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_down_arrow_epsilon_2.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( p ϵ⬦ break term 46 t )" + non associative with precedence 45 + for @{ 'UpDownArrowEpsilon $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 new file mode 100644 index 000000000..5052f4cc9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma @@ -0,0 +1,105 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground/xoa/or_5.ma". +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/term_constructors.ma". +include "delayed_updating/notation/relations/in_predicate_d_phi_1.ma". + +(* BY-DEPTH DELAYED (BDD) TERM **********************************************) + +inductive bdd: predicate term ≝ +| 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 +. + +interpretation + "well-formed by-depth delayed (term)" + 'InPredicateDPhi t = (bdd t). + +(* Basic destructions *******************************************************) + +lemma bdd_inv_in_com_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 * +[ #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/ +] +qed-. + +lemma bdd_inv_in_com_d: + ∀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_com_gen … Ht Hq) -Ht -Hq * +[ #n0 #H1 #H2 destruct /3 width=1 by or_introl, conj/ +| #u0 #q0 #n0 #Hu0 #Hq0 #H1 #H2 destruct /3 width=4 by ex3_intro, or_intror/ +| #u0 #q0 #_ #_ #_ #H0 destruct +| #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct +| #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct +] +qed-. + +lemma bdd_inv_in_ini_d: + ∀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_com_d … Ht Hq) -Ht -Hq * +[ #H1 #H2 + elim (eq_inv_list_empty_append … H2) -H2 #H2 #_ destruct + /3 width=1 by or_introl, conj/ +| #u #Hu #Hq #H1 destruct + /4 width=4 by ex3_intro, ex_intro, or_intror/ +] +qed-. + +lemma pippo: + ∀l,n,p,t. t ϵ 𝐃𝛗 → p,𝗱❨n❩ ϵ▵ t → p,l ϵ▵ t → 𝗱❨n❩ = l. +#l #n #p elim p -p +[ #t #Ht "; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; "⊃"; "⊐"; ] ; ["≥"; "⪀"; "≽"; "⪴"; "⥸"; "⊒"; ]; ["∨"; "⩖"; "∪"; "∩"; "⋓"; "⋒" ] ; @@ -1544,7 +1544,7 @@ let predefined_classes = [ ["D"; "Δ"; "𝔻"; "ⅅ"; "𝐃"; "𝚫"; "Ⓓ"; "𝗗"; ] ; ["e"; "ɛ"; "ε"; "ϵ"; "Є"; "ℯ"; "𝕖"; "ⅇ"; "𝐞"; "𝛆"; "𝛜"; "ⓔ"; ] ; ["E"; "ℰ"; "𝔼"; "𝐄"; "Ⓔ"; ] ; - ["f"; "φ"; "ψ"; "ϕ"; "⨍"; "𝕗"; "𝐟"; "𝛟"; "𝛙"; "ⓕ"; ] ; + ["f"; "φ"; "ψ"; "ϕ"; "⨍"; "𝕗"; "𝐟"; "𝛗"; "𝛟"; "𝛙"; "ⓕ"; ] ; ["F"; "Φ"; "Ψ"; "ℱ"; "𝔽"; "𝐅"; "𝚽"; "𝚿"; "Ⓕ"; "𝗙"; ] ; ["g"; "γ"; "ℊ"; "𝕘"; "𝐠"; "𝛄"; "ⓖ"; ] ; ["G"; "Γ"; "𝔾"; "𝐆"; "𝚪"; "Ⓖ"; ] ;