X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fbdd_term.ma;h=1eb11fc030bc8c9f0676f2d82b52b9450ad371aa;hb=306205b6853874cf485152222593b57249c6e7fa;hp=5052f4cc9776ac2013be96b7bef2322af98cdfbb;hpb=160b7f7385763d872b5f2632696d02fd540c4eae;p=helm.git 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..1eb11fc03 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma @@ -12,94 +12,205 @@ (* *) (**************************************************************************) +include "delayed_updating/syntax/prototerm_constructors.ma". +include "delayed_updating/syntax/prototerm_eq.ma". +include "delayed_updating/notation/functions/class_d_tau_0.ma". 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 +inductive bdd: 𝒫❨prototerm❩ ≝ +| bdd_oref: ∀k. bdd (⧣k) +| bdd_iref: ∀t,k. bdd t → bdd (𝛕k.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 (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 + "by-depth delayed (prototerm)" + 'ClassDTau = (bdd). + +(* COMMENT + +(* 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 #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_com_d: - ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩;q ϵ⬦ t → - ∨∨ ∧∧ #n = t & 𝐞 = q - | ∃∃u. u ϵ 𝐃𝛗 & q ϵ⬦ u & 𝛗n.u = t +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 #n0 #Hu0 #Hq0 #H1 #H2 destruct + /4 width=4 by ex3_intro, ex2_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 +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: - ∀l,n,p,t. t ϵ 𝐃𝛗 → p,𝗱❨n❩ ϵ▵ t → p,l ϵ▵ t → 𝗱❨n❩ = l. +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