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 (* Basic inversions *********************************************************)
  39
  40 lemma bdd_inv_in_comp_gen:
  41       ∀t,p. t ϵ 𝐃𝛗 → p ϵ t →
  42       ∨∨ ∃∃n. #n ⇔ t & 𝗱n◗𝐞 = p
  43        | ∃∃u,q,n. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t & 𝗱n◗q = p
  44        | ∃∃u,q. u ϵ 𝐃𝛗 & q ϵ u & 𝛌.u ⇔ t & 𝗟◗q = p
  45        | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ u & @v.u ⇔ t & 𝗔◗q = p
  46        | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ v & @v.u ⇔ t & 𝗦◗q = p
  47 .
  48 #t #p #H elim H -H
  49 [ #n * /3 width=3 by or5_intro0, ex2_intro/
  50 | #u #n #Hu #_ * #q #Hq #Hp /3 width=7 by ex4_3_intro, or5_intro1/
  51 | #u #Hu #_ * #q #Hq #Hp /3 width=6 by or5_intro2, ex4_2_intro/
  52 | #v #u #Hv #Hu #_ #_ * * #q #Hq #Hp /3 width=8 by ex5_3_intro, or5_intro3, or5_intro4/
  53 | #t1 #t2 #Ht12 #_ #IH #Ht2
  54   elim IH -IH [6: /2 width=3 by subset_in_eq_repl_fwd/ ] *
  55   [ /4 width=3 by subset_eq_trans, or5_intro0, ex2_intro/
  56   | /4 width=7 by subset_eq_trans, ex4_3_intro, or5_intro1/
  57   | /4 width=6 by subset_eq_trans, or5_intro2, ex4_2_intro/
  58   | /4 width=8 by subset_eq_trans, ex5_3_intro, or5_intro3/
  59   | /4 width=8 by subset_eq_trans, ex5_3_intro, or5_intro4/
  60   ]
  61 ]
  62 qed-.
  63
  64 lemma bdd_inv_in_comp_d:
  65       ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱n◗q ϵ t →
  66       ∨∨ ∧∧ #n ⇔ t & 𝐞 = q
  67        | ∃∃u. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t
  68 .
  69 #t #q #n #Ht #Hq
  70 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
  71 [ #n0 #H1 #H2 destruct /3 width=1 by or_introl, conj/
  72 | #u0 #q0 #n0 #Hu0 #Hq0 #H1 #H2 destruct /3 width=4 by ex3_intro, or_intror/
  73 | #u0 #q0 #_ #_ #_ #H0 destruct
  74 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
  75 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
  76 ]
  77 qed-.
  78
  79 lemma bdd_inv_in_root_d:
  80       ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱n◗q ϵ ▵t →
  81       ∨∨ ∧∧ #n ⇔ t & 𝐞 = q
  82        | ∃∃u. u ϵ 𝐃𝛗 & q ϵ ▵u & 𝛗n.u ⇔ t
  83 .
  84 #t #q #n #Ht * #r #Hq
  85 elim (bdd_inv_in_comp_d … Ht Hq) -Ht -Hq *
  86 [ #H1 #H2
  87   elim (eq_inv_list_empty_append … H2) -H2 #H2 #_ destruct
  88   /3 width=1 by or_introl, conj/
  89 | #u #Hu #Hq #H0 destruct
  90   /4 width=4 by ex3_intro, ex_intro, or_intror/
  91 ]
  92 qed-.
  93
  94 lemma bdd_inv_in_comp_L:
  95       ∀t,q. t ϵ 𝐃𝛗 → 𝗟◗q ϵ t →
  96       ∃∃u. u ϵ 𝐃𝛗 & q ϵ u & 𝛌.u ⇔ t
  97 .
  98 #t #q #Ht #Hq
  99 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
 100 [ #n0 #_ #H0 destruct
 101 | #u0 #q0 #n0 #_ #_ #_ #H0 destruct
 102 | #u0 #q0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=4 by ex3_intro/
 103 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
 104 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
 105 ]
 106 qed-.
 107
 108 lemma bdd_inv_in_root_L:
 109       ∀t,q. t ϵ 𝐃𝛗 → 𝗟◗q ϵ ▵t →
 110       ∃∃u. u ϵ 𝐃𝛗 & q ϵ ▵u & 𝛌.u ⇔ t.
 111 #t #q #Ht * #r #Hq
 112 elim (bdd_inv_in_comp_L … Ht Hq) -Ht -Hq
 113 #u #Hu #Hq #H0 destruct
 114 /3 width=4 by ex3_intro, ex_intro/
 115 qed-.
 116
 117 lemma bdd_inv_in_comp_A:
 118       ∀t,q. t ϵ 𝐃𝛗 → 𝗔◗q ϵ t →
 119       ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ u & @v.u ⇔ t
 120 .
 121 #t #q #Ht #Hq
 122 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
 123 [ #n0 #_ #H0 destruct
 124 | #u0 #q0 #n0 #_ #_ #_ #H0 destruct
 125 | #u0 #q0 #_ #_ #_ #H0 destruct
 126 | #v0 #u0 #q0 #Hv0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=6 by ex4_2_intro/
 127 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
 128 ]
 129 qed-.
 130
 131 lemma bdd_inv_in_root_A:
 132       ∀t,q. t ϵ 𝐃𝛗 → 𝗔◗q ϵ ▵t →
 133       ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ ▵u & @v.u ⇔ t
 134 .
 135 #t #q #Ht * #r #Hq
 136 elim (bdd_inv_in_comp_A … Ht Hq) -Ht -Hq
 137 #v #u #Hv #Hu #Hq #H0 destruct
 138 /3 width=6 by ex4_2_intro, ex_intro/
 139 qed-.
 140
 141 lemma bdd_inv_in_comp_S:
 142       ∀t,q. t ϵ 𝐃𝛗 → 𝗦◗q ϵ t →
 143       ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ v & @v.u ⇔ t
 144 .
 145 #t #q #Ht #Hq
 146 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
 147 [ #n0 #_ #H0 destruct
 148 | #u0 #q0 #n0 #_ #_ #_ #H0 destruct
 149 | #u0 #q0 #_ #_ #_ #H0 destruct
 150 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
 151 | #v0 #u0 #q0 #Hv0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=6 by ex4_2_intro/
 152 ]
 153 qed-.
 154
 155 lemma bdd_inv_in_root_S:
 156       ∀t,q. t ϵ 𝐃𝛗 → 𝗦◗q ϵ ▵t →
 157       ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ ▵v & @v.u ⇔ t
 158 .
 159 #t #q #Ht * #r #Hq
 160 elim (bdd_inv_in_comp_S … Ht Hq) -Ht -Hq
 161 #v #u #Hv #Hu #Hq #H0 destruct
 162 /3 width=6 by ex4_2_intro, ex_intro/
 163 qed-.
 164
 165 (* Advanced inversions ******************************************************)
 166
 167 lemma bbd_mono_in_root_d:
 168       ∀l,n,p,t. t ϵ 𝐃𝛗 → p◖𝗱n ϵ ▵t → p◖l ϵ ▵t → 𝗱n = l.
 169 #l #n #p elim p -p
 170 [ #t #Ht <list_cons_comm <list_cons_comm #Hn #Hl
 171   elim (bdd_inv_in_root_d … Ht Hn) -Ht -Hn *
 172   [ #H0 #_
 173     lapply (prototerm_root_eq_repl … H0) -H0 #H0
 174     lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
 175     elim (prototerm_in_root_inv_lcons_oref … Hl) -Hl //
 176   | #u #_ #_ #H0
 177     lapply (prototerm_root_eq_repl … H0) -H0 #H0
 178     lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
 179     elim (prototerm_in_root_inv_lcons_iref … Hl) -Hl //
 180   ]
 181 | * [ #m ] #p #IH #t #Ht
 182   <list_cons_shift <list_cons_shift #Hn #Hl
 183   [ elim (bdd_inv_in_root_d … Ht Hn) -Ht -Hn *
 184     [ #_ #H0
 185       elim (eq_inv_list_empty_rcons ??? H0)
 186     | #u #Hu #Hp #H0
 187       lapply (prototerm_root_eq_repl … H0) -H0 #H0
 188       lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
 189       elim (prototerm_in_root_inv_lcons_iref … Hl) -Hl #_ #Hl
 190       /2 width=4 by/
 191     ]
 192   | elim (bdd_inv_in_root_L … Ht Hn) -Ht -Hn
 193     #u #Hu #Hp #H0
 194     lapply (prototerm_root_eq_repl … H0) -H0 #H0
 195     lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
 196     elim (prototerm_in_root_inv_lcons_abst … Hl) -Hl #_ #Hl
 197     /2 width=4 by/
 198   | elim (bdd_inv_in_root_A … Ht Hn) -Ht -Hn
 199     #v #u #_ #Hu #Hp #H0
 200     lapply (prototerm_root_eq_repl … H0) -H0 #H0
 201     lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
 202     elim (prototerm_in_root_inv_lcons_appl … Hl) -Hl * #H0 #Hl destruct
 203     /2 width=4 by/
 204   | elim (bdd_inv_in_root_S … Ht Hn) -Ht -Hn
 205     #v #u #Hv #_ #Hp #H0
 206     lapply (prototerm_root_eq_repl … H0) -H0 #H0
 207     lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
 208     elim (prototerm_in_root_inv_lcons_appl … Hl) -Hl * #H0 #Hl destruct
 209     /2 width=4 by/
 210   ]
 211 ]
 212 qed-.