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 "ground/xoa/or_5.ma".
  16 include "ground/xoa/ex_3_1.ma".
  17 include "ground/xoa/ex_4_2.ma".
  18 include "ground/xoa/ex_4_3.ma".
  19 include "ground/xoa/ex_5_3.ma".
  20 include "delayed_updating/syntax/preterm_constructors.ma".
  21 include "delayed_updating/notation/relations/in_predicate_d_phi_1.ma".
  22
  23 (* BY-DEPTH DELAYED (BDD) TERM **********************************************)
  24
  25 inductive bdd: predicate preterm ≝
  26 | bdd_oref: ∀n. bdd #n
  27 | bdd_iref: ∀t,n. bdd t → bdd 𝛗n.t
  28 | bdd_abst: ∀t. bdd t → bdd 𝛌.t
  29 | bdd_appl: ∀u,t. bdd u → bdd t → bdd @u.t
  30 .
  31
  32 interpretation
  33   "well-formed by-depth delayed (preterm)"
  34   'InPredicateDPhi t = (bdd t).
  35
  36 (* Basic inversions *********************************************************)
  37
  38 lemma bdd_inv_in_comp_gen:
  39       ∀t,p. t ϵ 𝐃𝛗 → p ϵ⬦ t →
  40       ∨∨ ∃∃n. #n = t & 𝗱❨n❩;𝐞 = p
  41        | ∃∃u,q,n. u ϵ 𝐃𝛗 & q ϵ⬦ u & 𝛗n.u = t & 𝗱❨n❩;q = p
  42        | ∃∃u,q. u ϵ 𝐃𝛗 & q ϵ⬦ u & 𝛌.u = t & 𝗟;q = p
  43        | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ⬦ u & @v.u = t & 𝗔;q = p
  44        | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ⬦ v & @v.u = t & 𝗦;q = p
  45 .
  46 #t #p *
  47 [ #n * /3 width=3 by or5_intro0, ex2_intro/
  48 | #u #n #Hu * #q #Hq #Hp /3 width=7 by ex4_3_intro, or5_intro1/
  49 | #u #Hu * #q #Hq #Hp /3 width=6 by or5_intro2, ex4_2_intro/
  50 | #v #u #Hv #Hu * * #q #Hq #Hp /3 width=8 by ex5_3_intro, or5_intro3, or5_intro4/
  51 ]
  52 qed-.
  53
  54 lemma bdd_inv_in_comp_d:
  55       ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩;q ϵ⬦ t →
  56       ∨∨ ∧∧ #n = t & 𝐞 = q
  57        | ∃∃u. u ϵ 𝐃𝛗 & q ϵ⬦ u & 𝛗n.u = t
  58 .
  59 #t #q #n #Ht #Hq
  60 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
  61 [ #n0 #H1 #H2 destruct /3 width=1 by or_introl, conj/
  62 | #u0 #q0 #n0 #Hu0 #Hq0 #H1 #H2 destruct /3 width=4 by ex3_intro, or_intror/
  63 | #u0 #q0 #_ #_ #_ #H0 destruct
  64 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
  65 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
  66 ]
  67 qed-.
  68
  69 lemma bdd_inv_in_root_d:
  70       ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩;q ϵ▵ t →
  71       ∨∨ ∧∧ #n = t & 𝐞 = q
  72        | ∃∃u. u ϵ 𝐃𝛗 & q ϵ▵ u & 𝛗n.u = t
  73 .
  74 #t #q #n #Ht * #r #Hq
  75 elim (bdd_inv_in_comp_d … Ht Hq) -Ht -Hq *
  76 [ #H1 #H2
  77   elim (eq_inv_list_empty_append … H2) -H2 #H2 #_ destruct
  78   /3 width=1 by or_introl, conj/
  79 | #u #Hu #Hq #H0 destruct
  80   /4 width=4 by ex3_intro, ex_intro, or_intror/
  81 ]
  82 qed-.
  83
  84 lemma bdd_inv_in_comp_L:
  85       ∀t,q. t ϵ 𝐃𝛗 → 𝗟;q ϵ⬦ t →
  86       ∃∃u. u ϵ 𝐃𝛗 & q ϵ⬦ u & 𝛌.u = t
  87 .
  88 #t #q #Ht #Hq
  89 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
  90 [ #n0 #_ #H0 destruct
  91 | #u0 #q0 #n0 #_ #_ #_ #H0 destruct
  92 | #u0 #q0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=4 by ex3_intro/
  93 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
  94 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
  95 ]
  96 qed-.
  97
  98 lemma bdd_inv_in_root_L:
  99       ∀t,q. t ϵ 𝐃𝛗 → 𝗟;q ϵ▵ t →
 100       ∃∃u. u ϵ 𝐃𝛗 & q ϵ▵ u & 𝛌.u = t.
 101 #t #q #Ht * #r #Hq
 102 elim (bdd_inv_in_comp_L … Ht Hq) -Ht -Hq
 103 #u #Hu #Hq #H0 destruct
 104 /3 width=4 by ex3_intro, ex_intro/
 105 qed-.
 106
 107 lemma bdd_inv_in_comp_A:
 108       ∀t,q. t ϵ 𝐃𝛗 → 𝗔;q ϵ⬦ t →
 109       ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ⬦ u & @v.u = t
 110 .
 111 #t #q #Ht #Hq
 112 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
 113 [ #n0 #_ #H0 destruct
 114 | #u0 #q0 #n0 #_ #_ #_ #H0 destruct
 115 | #u0 #q0 #_ #_ #_ #H0 destruct
 116 | #v0 #u0 #q0 #Hv0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=6 by ex4_2_intro/
 117 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
 118 ]
 119 qed-.
 120
 121 lemma bdd_inv_in_root_A:
 122       ∀t,q. t ϵ 𝐃𝛗 → 𝗔;q ϵ▵ t →
 123       ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ▵ u & @v.u = t
 124 .
 125 #t #q #Ht * #r #Hq
 126 elim (bdd_inv_in_comp_A … Ht Hq) -Ht -Hq
 127 #v #u #Hv #Hu #Hq #H0 destruct
 128 /3 width=6 by ex4_2_intro, ex_intro/
 129 qed-.
 130
 131 lemma bdd_inv_in_comp_S:
 132       ∀t,q. t ϵ 𝐃𝛗 → 𝗦;q ϵ⬦ t →
 133       ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ⬦ v & @v.u = t
 134 .
 135 #t #q #Ht #Hq
 136 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
 137 [ #n0 #_ #H0 destruct
 138 | #u0 #q0 #n0 #_ #_ #_ #H0 destruct
 139 | #u0 #q0 #_ #_ #_ #H0 destruct
 140 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
 141 | #v0 #u0 #q0 #Hv0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=6 by ex4_2_intro/
 142 ]
 143 qed-.
 144
 145 lemma bdd_inv_in_root_S:
 146       ∀t,q. t ϵ 𝐃𝛗 → 𝗦;q ϵ▵ t →
 147       ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ▵ v & @v.u = t
 148 .
 149 #t #q #Ht * #r #Hq
 150 elim (bdd_inv_in_comp_S … Ht Hq) -Ht -Hq
 151 #v #u #Hv #Hu #Hq #H0 destruct
 152 /3 width=6 by ex4_2_intro, ex_intro/
 153 qed-.
 154
 155 (* Advanced inversions ******************************************************)
 156
 157 lemma bbd_mono_in_root_d:
 158       ∀l,n,p,t. t ϵ 𝐃𝛗 → p,𝗱❨n❩ ϵ▵ t → p,l ϵ▵ t → 𝗱❨n❩ = l.
 159 #l #n #p elim p -p
 160 [ #t #Ht <list_cons_comm <list_cons_comm #Hn #Hl
 161   elim (bdd_inv_in_root_d … Ht Hn) -Ht -Hn *
 162   [ #H0 #_ destruct
 163     elim (preterm_in_root_inv_lcons_oref … Hl) -Hl //
 164   | #u #_ #_ #H0 destruct
 165     elim (preterm_in_root_inv_lcons_iref … Hl) -Hl //
 166   ]
 167 | * [ #m ] #p #IH #t #Ht
 168   <list_cons_shift <list_cons_shift #Hn #Hl
 169   [ elim (bdd_inv_in_root_d … Ht Hn) -Ht -Hn *
 170     [ #_ #H0
 171       elim (eq_inv_list_empty_rcons ??? H0)
 172     | #u #Hu #Hp #H0 destruct
 173       elim (preterm_in_root_inv_lcons_iref … Hl) -Hl #_ #Hl
 174       /2 width=4 by/
 175     ]
 176   | elim (bdd_inv_in_root_L … Ht Hn) -Ht -Hn
 177     #u #Hu #Hp #H0 destruct
 178     elim (preterm_in_root_inv_lcons_abst … Hl) -Hl #_ #Hl
 179     /2 width=4 by/
 180   | elim (bdd_inv_in_root_A … Ht Hn) -Ht -Hn
 181     #v #u #_ #Hu #Hp #H0 destruct
 182     elim (preterm_in_root_inv_lcons_appl … Hl) -Hl * #H0 #Hl destruct
 183     /2 width=4 by/
 184   | elim (bdd_inv_in_root_S … Ht Hn) -Ht -Hn
 185     #v #u #Hv #_ #Hp #H0 destruct
 186     elim (preterm_in_root_inv_lcons_appl … Hl) -Hl * #H0 #Hl destruct
 187     /2 width=4 by/
 188   ]
 189 ]
 190 qed-.