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=0101b8d9361671cef4edcdb00f89c8fa34d70c05;hpb=f83215ca9b8d0019c85a991ec90c6c658c0aaff8;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 0101b8d93..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,38 +12,40 @@ (* *) (**************************************************************************) +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/preterm_equivalence.ma". -include "delayed_updating/syntax/preterm_constructors.ma". -include "delayed_updating/notation/functions/class_d_phi_0.ma". (* BY-DEPTH DELAYED (BDD) TERM **********************************************) -inductive bdd: 𝒫❨preterm❩ ≝ -| bdd_oref: ∀n. bdd (#n) -| bdd_iref: ∀t,n. bdd t → bdd (𝛗n.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_appl: ∀u,t. bdd u → bdd t → bdd (＠u.t) | bdd_conv: ∀t1,t2. t1 ⇔ t2 → bdd t1 → bdd t2 . interpretation - "by-depth delayed (preterm)" - 'ClassDPhi = (bdd). + "by-depth delayed (prototerm)" + 'ClassDTau = (bdd). + +(* COMMENT (* Basic inversions *********************************************************) lemma bdd_inv_in_comp_gen: - ∀t,p. t ϵ 𝐃𝛗 → p ϵ t → + ∀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 + | ∃∃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 #H elim H -H [ #n * /3 width=3 by or5_intro0, ex2_intro/ @@ -62,14 +64,15 @@ lemma bdd_inv_in_comp_gen: qed-. lemma bdd_inv_in_comp_d: - ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱n◗q ϵ t → + ∀t,q,n. t ϵ 𝐃𝛕 → 𝗱n◗q ϵ t → ∨∨ ∧∧ #n ⇔ t & 𝐞 = q - | ∃∃u. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t + | ∃∃u. u ϵ 𝐃𝛕 & q ϵ ɱ.u & 𝛕n.u ⇔ t . #t #q #n #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 @@ -77,9 +80,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 → + ∀t,q,n. t ϵ 𝐃𝛕 → 𝗱n◗q ϵ ▵t → ∨∨ ∧∧ #n ⇔ t & 𝐞 = q - | ∃∃u. u ϵ 𝐃𝛗 & q ϵ ▵u & 𝛗n.u ⇔ t + | ∃∃u. u ϵ 𝐃𝛕 & q ϵ ▵ɱ.u & 𝛕n.u ⇔ t . #t #q #n #Ht * #r #Hq elim (bdd_inv_in_comp_d … Ht Hq) -Ht -Hq * @@ -92,8 +95,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 * @@ -106,8 +109,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 @@ -115,8 +118,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 * @@ -129,8 +132,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 @@ -139,8 +142,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 * @@ -153,8 +156,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 @@ -165,18 +168,18 @@ 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