matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "delayed_updating/syntax/prototerm_constructors.ma".
  16 include "delayed_updating/syntax/prototerm_equivalence.ma".
  17 include "delayed_updating/notation/functions/class_d_phi_0.ma".
  18 include "ground/xoa/or_5.ma".
  19 include "ground/xoa/ex_3_1.ma".
  20 include "ground/xoa/ex_4_2.ma".
  21 include "ground/xoa/ex_4_3.ma".
  22 include "ground/xoa/ex_5_3.ma".
  23
  24 (* BY-DEPTH DELAYED (BDD) TERM **********************************************)
  25
  26 inductive bdd: 𝒫❨prototerm❩ ≝
  27 | bdd_oref: ∀n. bdd (#n)
  28 | bdd_iref: ∀t,n. bdd t → bdd (𝛗n.t)
  29 | bdd_abst: ∀t. bdd t → bdd (𝛌.t)
  30 | bdd_appl: ∀u,t. bdd u → bdd t → bdd (@u.t)
  31 | bdd_conv: ∀t1,t2. t1 ⇔ t2 → bdd t1 → bdd t2
  32 .
  33
  34 interpretation
  35   "by-depth delayed (prototerm)"
  36   'ClassDPhi = (bdd).
  37
  38 (*
  39
  40 (* Basic inversions *********************************************************)
  41
  42 lemma bdd_inv_in_comp_gen:
  43       ∀t,p. t ϵ 𝐃𝛗 → p ϵ t →
  44       ∨∨ ∃∃n. #n ⇔ t & 𝗱n◗𝐞 = p
  45        | ∃∃u,q,n. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t & 𝗱n◗𝗺◗q = p
  46        | ∃∃u,q. u ϵ 𝐃𝛗 & q ϵ u & 𝛌.u ⇔ t & 𝗟◗q = p
  47        | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ u & @v.u ⇔ t & 𝗔◗q = p
  48        | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ v & @v.u ⇔ t & 𝗦◗q = p
  49 .
  50 #t #p #H elim H -H
  51 [ #n * /3 width=3 by or5_intro0, ex2_intro/
  52 | #u #n #Hu #_ * #q #Hq #Hp /3 width=7 by ex4_3_intro, or5_intro1/
  53 | #u #Hu #_ * #q #Hq #Hp /3 width=6 by or5_intro2, ex4_2_intro/
  54 | #v #u #Hv #Hu #_ #_ * * #q #Hq #Hp /3 width=8 by ex5_3_intro, or5_intro3, or5_intro4/
  55 | #t1 #t2 #Ht12 #_ #IH #Ht2
  56   elim IH -IH [6: /2 width=3 by subset_in_eq_repl_fwd/ ] *
  57   [ /4 width=3 by subset_eq_trans, or5_intro0, ex2_intro/
  58   | /4 width=7 by subset_eq_trans, ex4_3_intro, or5_intro1/
  59   | /4 width=6 by subset_eq_trans, or5_intro2, ex4_2_intro/
  60   | /4 width=8 by subset_eq_trans, ex5_3_intro, or5_intro3/
  61   | /4 width=8 by subset_eq_trans, ex5_3_intro, or5_intro4/
  62   ]
  63 ]
  64 qed-.
  65
  66 lemma bdd_inv_in_comp_d:
  67       ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱n◗q ϵ t →
  68       ∨∨ ∧∧ #n ⇔ t & 𝐞 = q
  69        | ∃∃u. u ϵ 𝐃𝛗 & q ϵ ɱ.u & 𝛗n.u ⇔ t
  70 .
  71 #t #q #n #Ht #Hq
  72 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
  73 [ #n0 #H1 #H2 destruct /3 width=1 by or_introl, conj/
  74 | #u0 #q0 #n0 #Hu0 #Hq0 #H1 #H2 destruct
  75  /4 width=4 by ex3_intro, ex2_intro, or_intror/
  76 | #u0 #q0 #_ #_ #_ #H0 destruct
  77 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
  78 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
  79 ]
  80 qed-.
  81
  82 lemma bdd_inv_in_root_d:
  83       ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱n◗q ϵ ▵t →
  84       ∨∨ ∧∧ #n ⇔ t & 𝐞 = q
  85        | ∃∃u. u ϵ 𝐃𝛗 & q ϵ ▵ɱ.u & 𝛗n.u ⇔ t
  86 .
  87 #t #q #n #Ht * #r #Hq
  88 elim (bdd_inv_in_comp_d … Ht Hq) -Ht -Hq *
  89 [ #H1 #H2
  90   elim (eq_inv_list_empty_append … H2) -H2 #H2 #_ destruct
  91   /3 width=1 by or_introl, conj/
  92 | #u #Hu #Hq #H0 destruct
  93   /4 width=4 by ex3_intro, ex_intro, or_intror/
  94 ]
  95 qed-.
  96
  97 lemma bdd_inv_in_comp_L:
  98       ∀t,q. t ϵ 𝐃𝛗 → 𝗟◗q ϵ t →
  99       ∃∃u. u ϵ 𝐃𝛗 & q ϵ u & 𝛌.u ⇔ t
 100 .
 101 #t #q #Ht #Hq
 102 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
 103 [ #n0 #_ #H0 destruct
 104 | #u0 #q0 #n0 #_ #_ #_ #H0 destruct
 105 | #u0 #q0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=4 by ex3_intro/
 106 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
 107 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
 108 ]
 109 qed-.
 110
 111 lemma bdd_inv_in_root_L:
 112       ∀t,q. t ϵ 𝐃𝛗 → 𝗟◗q ϵ ▵t →
 113       ∃∃u. u ϵ 𝐃𝛗 & q ϵ ▵u & 𝛌.u ⇔ t.
 114 #t #q #Ht * #r #Hq
 115 elim (bdd_inv_in_comp_L … Ht Hq) -Ht -Hq
 116 #u #Hu #Hq #H0 destruct
 117 /3 width=4 by ex3_intro, ex_intro/
 118 qed-.
 119
 120 lemma bdd_inv_in_comp_A:
 121       ∀t,q. t ϵ 𝐃𝛗 → 𝗔◗q ϵ t →
 122       ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ u & @v.u ⇔ t
 123 .
 124 #t #q #Ht #Hq
 125 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
 126 [ #n0 #_ #H0 destruct
 127 | #u0 #q0 #n0 #_ #_ #_ #H0 destruct
 128 | #u0 #q0 #_ #_ #_ #H0 destruct
 129 | #v0 #u0 #q0 #Hv0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=6 by ex4_2_intro/
 130 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
 131 ]
 132 qed-.
 133
 134 lemma bdd_inv_in_root_A:
 135       ∀t,q. t ϵ 𝐃𝛗 → 𝗔◗q ϵ ▵t →
 136       ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ ▵u & @v.u ⇔ t
 137 .
 138 #t #q #Ht * #r #Hq
 139 elim (bdd_inv_in_comp_A … Ht Hq) -Ht -Hq
 140 #v #u #Hv #Hu #Hq #H0 destruct
 141 /3 width=6 by ex4_2_intro, ex_intro/
 142 qed-.
 143
 144 lemma bdd_inv_in_comp_S:
 145       ∀t,q. t ϵ 𝐃𝛗 → 𝗦◗q ϵ t →
 146       ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ v & @v.u ⇔ t
 147 .
 148 #t #q #Ht #Hq
 149 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
 150 [ #n0 #_ #H0 destruct
 151 | #u0 #q0 #n0 #_ #_ #_ #H0 destruct
 152 | #u0 #q0 #_ #_ #_ #H0 destruct
 153 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
 154 | #v0 #u0 #q0 #Hv0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=6 by ex4_2_intro/
 155 ]
 156 qed-.
 157
 158 lemma bdd_inv_in_root_S:
 159       ∀t,q. t ϵ 𝐃𝛗 → 𝗦◗q ϵ ▵t →
 160       ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ ▵v & @v.u ⇔ t
 161 .
 162 #t #q #Ht * #r #Hq
 163 elim (bdd_inv_in_comp_S … Ht Hq) -Ht -Hq
 164 #v #u #Hv #Hu #Hq #H0 destruct
 165 /3 width=6 by ex4_2_intro, ex_intro/
 166 qed-.
 167
 168 (* Advanced inversions ******************************************************)
 169
 170 lemma bbd_mono_in_root_d:
 171       ∀l,n,p,t. t ϵ 𝐃𝛗 → p◖𝗱n ϵ ▵t → p◖l ϵ ▵t → 𝗱n = l.
 172 #l #n #p elim p -p
 173 [ #t #Ht <list_cons_comm <list_cons_comm #Hn #Hl
 174   elim (bdd_inv_in_root_d … Ht Hn) -Ht -Hn *
 175   [ #H0 #_
 176     lapply (prototerm_root_eq_repl … H0) -H0 #H0
 177     lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
 178     elim (prototerm_in_root_inv_lcons_oref … Hl) -Hl //
 179   | #u #_ #_ #H0
 180     lapply (prototerm_root_eq_repl … H0) -H0 #H0
 181     lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
 182     elim (prototerm_in_root_inv_lcons_iref … Hl) -Hl //
 183   ]
 184 | * [ #m ] #p #IH #t #Ht
 185   <list_cons_shift <list_cons_shift #Hn #Hl
 186   [ elim (bdd_inv_in_root_d … Ht Hn) -Ht -Hn *
 187     [ #_ #H0
 188       elim (eq_inv_list_empty_rcons ??? H0)
 189     | #u #Hu #Hp #H0
 190       lapply (prototerm_root_eq_repl … H0) -H0 #H0
 191       lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
 192       elim (prototerm_in_root_inv_lcons_iref … Hl) -Hl #_ #Hl
 193       /2 width=4 by/
 194     ]
 195   | elim (bdd_inv_in_root_L … Ht Hn) -Ht -Hn
 196     #u #Hu #Hp #H0
 197     lapply (prototerm_root_eq_repl … H0) -H0 #H0
 198     lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
 199     elim (prototerm_in_root_inv_lcons_abst … Hl) -Hl #_ #Hl
 200     /2 width=4 by/
 201   | elim (bdd_inv_in_root_A … Ht Hn) -Ht -Hn
 202     #v #u #_ #Hu #Hp #H0
 203     lapply (prototerm_root_eq_repl … H0) -H0 #H0
 204     lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
 205     elim (prototerm_in_root_inv_lcons_appl … Hl) -Hl * #H0 #Hl destruct
 206     /2 width=4 by/
 207   | elim (bdd_inv_in_root_S … Ht Hn) -Ht -Hn
 208     #v #u #Hv #_ #Hp #H0
 209     lapply (prototerm_root_eq_repl … H0) -H0 #H0
 210     lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
 211     elim (prototerm_in_root_inv_lcons_appl … Hl) -Hl * #H0 #Hl destruct
 212     /2 width=4 by/
 213   ]
 214 ]
 215 qed-.
 216 *)