From 3c257bf84769adf162510ed86a89872e3003629a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 10 Dec 2021 16:49:53 +0100 Subject: [PATCH] update in delayed updating + WIP on dephi + some renaming + subset notation improved --- .../delayed_updating/syntax/bdd_term.ma | 131 +++++++++++++++--- .../delayed_updating/syntax/label.ma | 12 +- .../delayed_updating/syntax/path.ma | 1 - .../delayed_updating/syntax/path_dephi.ma | 30 ++++ .../syntax/{term.ma => preterm.ma} | 18 +-- ...onstructors.ma => preterm_constructors.ma} | 53 ++++--- .../delayed_updating/syntax/preterm_dephi.ma | 20 +++ .../lib/basics/core_notation/subseteq_2.ma | 5 +- 8 files changed, 211 insertions(+), 59 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_dephi.ma rename matita/matita/contribs/lambdadelta/delayed_updating/syntax/{term.ma => preterm.ma} (77%) rename matita/matita/contribs/lambdadelta/delayed_updating/syntax/{term_constructors.ma => preterm_constructors.ma} (57%) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_dephi.ma 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 5052f4cc9..e7d140231 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma @@ -17,12 +17,12 @@ 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/syntax/preterm_constructors.ma". include "delayed_updating/notation/relations/in_predicate_d_phi_1.ma". (* BY-DEPTH DELAYED (BDD) TERM **********************************************) -inductive bdd: predicate term ≝ +inductive bdd: predicate preterm ≝ | bdd_oref: ∀n. bdd #n | bdd_iref: ∀t,n. bdd t → bdd 𝛗n.t | bdd_abst: ∀t. bdd t → bdd 𝛌.t @@ -30,12 +30,12 @@ inductive bdd: predicate term ≝ . interpretation - "well-formed by-depth delayed (term)" + "well-formed by-depth delayed (preterm)" 'InPredicateDPhi t = (bdd t). -(* Basic destructions *******************************************************) +(* Basic inversions *********************************************************) -lemma bdd_inv_in_com_gen: +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 @@ -51,13 +51,13 @@ lemma bdd_inv_in_com_gen: ] qed-. -lemma bdd_inv_in_com_d: +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 #Ht #Hq -elim (bdd_inv_in_com_gen … Ht Hq) -Ht -Hq * +elim (bdd_inv_in_comp_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 @@ -66,40 +66,125 @@ elim (bdd_inv_in_com_gen … Ht Hq) -Ht -Hq * ] qed-. -lemma bdd_inv_in_ini_d: +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 #Ht * #r #Hq -elim (bdd_inv_in_com_d … Ht Hq) -Ht -Hq * +elim (bdd_inv_in_comp_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 +| #u #Hu #Hq #H0 destruct /4 width=4 by ex3_intro, ex_intro, or_intror/ ] qed-. -lemma pippo: +lemma bdd_inv_in_comp_L: + ∀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 * +[ #n0 #_ #H0 destruct +| #u0 #q0 #n0 #_ #_ #_ #H0 destruct +| #u0 #q0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=4 by ex3_intro/ +| #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct +| #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct +] +qed-. + +lemma bdd_inv_in_root_L: + ∀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 +/3 width=4 by ex3_intro, ex_intro/ +qed-. + +lemma bdd_inv_in_comp_A: + ∀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 * +[ #n0 #_ #H0 destruct +| #u0 #q0 #n0 #_ #_ #_ #H0 destruct +| #u0 #q0 #_ #_ #_ #H0 destruct +| #v0 #u0 #q0 #Hv0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=6 by ex4_2_intro/ +| #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct +] +qed-. + +lemma bdd_inv_in_root_A: + ∀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 +#v #u #Hv #Hu #Hq #H0 destruct +/3 width=6 by ex4_2_intro, ex_intro/ +qed-. + +lemma bdd_inv_in_comp_S: + ∀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 * +[ #n0 #_ #H0 destruct +| #u0 #q0 #n0 #_ #_ #_ #H0 destruct +| #u0 #q0 #_ #_ #_ #H0 destruct +| #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct +| #v0 #u0 #q0 #Hv0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=6 by ex4_2_intro/ +] +qed-. + +lemma bdd_inv_in_root_S: + ∀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 +#v #u #Hv #Hu #Hq #H0 destruct +/3 width=6 by ex4_2_intro, ex_intro/ +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 elim p -p [ #t #Ht