matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed.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/path.ma".
  16 include "delayed_updating/notation/functions/class_c_3.ma".
  17 include "ground/arith/nat_plus_pred.ma".
  18 include "ground/lib/subset.ma".
  19 include "ground/lib/bool_and.ma".
  20 include "ground/generated/insert_eq_1.ma".
  21 include "ground/xoa/ex_3_2.ma".
  22
  23 (* CLOSED CONDITION FOR PATH ************************************************)
  24
  25 inductive pcc (o) (e): relation2 nat path ≝
  26 | pcc_empty:
  27   pcc o e e (𝐞)
  28 | pcc_d_dx (p) (n) (k):
  29   (Ⓣ = o → n = ↑↓n) →
  30   pcc o e (n+ninj k) p → pcc o e n (p◖𝗱k)
  31 | pcc_m_dx (p) (n):
  32   pcc o e n p → pcc o e n (p◖𝗺)
  33 | pcc_L_dx (p) (n):
  34   pcc o e n p → pcc o e (↑n) (p◖𝗟)
  35 | pcc_A_dx (p) (n):
  36   pcc o e n p → pcc o e n (p◖𝗔)
  37 | pcc_S_dx (p) (n):
  38   pcc o e n p → pcc o e n (p◖𝗦)
  39 .
  40
  41 interpretation
  42   "closed condition (path)"
  43   'ClassC o n e = (pcc o e n).
  44
  45 (* Advanced constructions ***************************************************)
  46
  47 lemma pcc_false_d_dx (e) (p) (n) (k:pnat):
  48       p ϵ 𝐂❨Ⓕ,n+k,e❩ → p◖𝗱k ϵ 𝐂❨Ⓕ,n,e❩.
  49 #e #p #n #k #H0
  50 @pcc_d_dx [| // ]
  51 #H0 destruct
  52 qed.
  53
  54 lemma pcc_true_d_dx (e) (p) (n:pnat) (k:pnat):
  55       p ϵ 𝐂❨Ⓣ,n+k,e❩ → p◖𝗱k ϵ 𝐂❨Ⓣ,n,e❩.
  56 /2 width=1 by pcc_d_dx/
  57 qed.
  58
  59 lemma pcc_plus_bi_dx (o) (e) (p) (n):
  60       p ϵ 𝐂❨o,n,e❩ →
  61       ∀m. p ϵ 𝐂❨o,n+m,e+m❩.
  62 #o #e #p #n #H0 elim H0 -p -n //
  63 #p #n [ #k #Ho ] #_ #IH #m
  64 [|*: /2 width=1 by pcc_m_dx, pcc_L_dx, pcc_A_dx, pcc_S_dx/ ]
  65 @pcc_d_dx // -IH #H0
  66 >Ho -Ho // <nplus_succ_sn //
  67 qed.
  68
  69 (* Basic inversions ********************************************************)
  70
  71 lemma pcc_inv_empty (o) (e) (n):
  72       (𝐞) ϵ 𝐂❨o,n,e❩ → e = n.
  73 #o #e #n @(insert_eq_1 … (𝐞))
  74 #x * -n //
  75 #p #n [ #k #_ ] #_ #H0 destruct
  76 qed-.
  77
  78 (**) (* alias *)
  79 alias symbol "DownArrow" (instance 4) = "predecessor (non-negative integers)".
  80 alias symbol "UpArrow" (instance 3) = "successor (non-negative integers)".
  81 alias symbol "and" (instance 1) = "logical and".
  82
  83 lemma pcc_inv_d_dx (o) (e) (p) (n) (k):
  84       p◖𝗱k ϵ 𝐂❨o,n,e❩ →
  85       ∧∧ (Ⓣ = o → n = ↑↓n)
  86        & p ϵ 𝐂❨o,n+k,e❩.
  87 #o #e #p #n #h @(insert_eq_1 … (p◖𝗱h))
  88 #x * -x -n
  89 [|*: #x #n [ #k #Ho ] #Hx ] #H0 destruct
  90 /3 width=1 by conj/
  91 qed-.
  92
  93 lemma pcc_inv_m_dx (o) (e) (p) (n):
  94       p◖𝗺 ϵ 𝐂❨o,n,e❩ → p ϵ 𝐂❨o,n,e❩.
  95 #o #e #p #n @(insert_eq_1 … (p◖𝗺))
  96 #x * -x -n
  97 [|*: #x #n [ #k #_ ] #Hx ] #H0 destruct //
  98 qed-.
  99
 100 lemma pcc_inv_L_dx (o) (e) (p) (n):
 101       p◖𝗟 ϵ 𝐂❨o,n,e❩ →
 102       ∧∧ p ϵ 𝐂❨o,↓n,e❩ & n = ↑↓n.
 103 #o #e #p #n @(insert_eq_1 … (p◖𝗟))
 104 #x * -x -n
 105 [|*: #x #n [ #k #_ ] #Hx ] #H0 destruct
 106 <npred_succ /2 width=1 by conj/
 107 qed-.
 108
 109 lemma pcc_inv_A_dx (o) (e) (p) (n):
 110       p◖𝗔 ϵ 𝐂❨o,n,e❩ → p ϵ 𝐂❨o,n,e❩.
 111 #o #e #p #n @(insert_eq_1 … (p◖𝗔))
 112 #x * -x -n
 113 [|*: #x #n [ #k #_ ] #Hx ] #H0 destruct //
 114 qed-.
 115
 116 lemma pcc_inv_S_dx (o) (e) (p) (n):
 117       p◖𝗦 ϵ 𝐂❨o,n,e❩ → p ϵ 𝐂❨o,n,e❩.
 118 #o #e #p #n @(insert_eq_1 … (p◖𝗦))
 119 #x * -x -n
 120 [|*: #x #n [ #k #_ ] #Hx ] #H0 destruct //
 121 qed-.
 122
 123 (* Advanced destructions ****************************************************)
 124
 125 lemma pcc_des_d_dx (o) (e) (p) (n) (k):
 126       p◖𝗱k ϵ 𝐂❨o,n,e❩ → p ϵ 𝐂❨o,n+k,e❩.
 127 #o #e #p #n #k #H0
 128 elim (pcc_inv_d_dx … H0) -H0 #H1 #H2 //
 129 qed-.
 130
 131 lemma pcc_des_gen (o) (e) (p) (n):
 132       p ϵ 𝐂❨o,n,e❩ → p ϵ 𝐂❨Ⓕ,n,e❩.
 133 #o #e #p #n #H0 elim H0 -p -n //
 134 #p #n [ #k #Ho ] #_ #IH
 135 /2 width=1 by pcc_m_dx, pcc_L_dx, pcc_A_dx, pcc_S_dx, pcc_false_d_dx/
 136 qed-.
 137
 138 (* Advanced inversions ******************************************************)
 139
 140 lemma pcc_inv_empty_succ_zero (o) (n):
 141       (𝐞) ϵ 𝐂❨o,↑n,𝟎❩ → ⊥.
 142 #o #n #H0
 143 lapply (pcc_inv_empty … H0) -H0 #H0
 144 /2 width=7 by eq_inv_zero_nsucc/
 145 qed-.
 146
 147 lemma pcc_true_inv_d_dx_zero_sn (e) (p) (k):
 148       p◖𝗱k ϵ 𝐂❨Ⓣ,𝟎, e❩ → ⊥.
 149 #e #p #k #H0
 150 elim (pcc_inv_d_dx … H0) -H0 #H0 #_
 151 elim (eq_inv_zero_nsucc … (H0 ?)) -H0 //
 152 qed-.
 153
 154 lemma pcc_inv_L_dx_zero_sn (o) (e) (p):
 155       p◖𝗟 ϵ 𝐂❨o,𝟎,e❩ → ⊥.
 156 #o #e #p #H0
 157 elim (pcc_inv_L_dx … H0) -H0 #_ #H0
 158 /2 width=7 by eq_inv_zero_nsucc/
 159 qed-.
 160
 161 lemma pcc_inv_L_dx_succ (o) (e) (p) (n):
 162       p◖𝗟 ϵ 𝐂❨o,↑n,e❩ → p ϵ 𝐂❨o,n,e❩.
 163 #o #e #p #n #H0
 164 elim (pcc_inv_L_dx … H0) -H0 //
 165 qed-.
 166
 167 (* Constructions with land **************************************************)
 168
 169 lemma pcc_land_dx (o1) (o2) (e) (p) (n):
 170       p ϵ 𝐂❨o1,n,e❩ → p ϵ 𝐂❨o1∧o2,n,e❩.
 171 #o1 * /2 width=2 by pcc_des_gen/
 172 qed.
 173
 174 lemma pcc_land_sn (o1) (o2) (e) (p) (n):
 175       p ϵ 𝐂❨o2,n,e❩ → p ϵ 𝐂❨o1∧o2,n,e❩.
 176 * /2 width=2 by pcc_des_gen/
 177 qed.
 178
 179 (* Main constructions with path_append **************************************)
 180
 181 theorem pcc_append_bi (o1) (o2) (e1) (e2) (p) (q) (m) (n):
 182         p ϵ 𝐂❨o1,m,e1❩ → q ϵ 𝐂❨o2,n,e2❩ → p●q ϵ 𝐂❨o1∧o2,m+n,e1+e2❩.
 183 #o1 #o2 #e1 #e2 #p #q #m #n #Hm #Hn elim Hn -q -n
 184 /3 width=1 by pcc_land_dx, pcc_m_dx, pcc_A_dx, pcc_S_dx, pcc_plus_bi_dx/
 185 #q #n [ #k #Ho2 ] #_ #IH
 186 [ @pcc_d_dx // #H0
 187   elim (andb_inv_true_sn … H0) -H0 #_ #H0 >Ho2 //
 188   <nplus_succ_dx <npred_succ //
 189 | <nplus_succ_dx /2 width=1 by pcc_L_dx/
 190 ]
 191 qed.
 192
 193 (* Inversions with path_append **********************************************)
 194
 195 lemma pcc_false_zero_dx_inv_append_bi (x) (m) (n):
 196       x ϵ 𝐂❨Ⓕ,m+n,𝟎❩ →
 197       ∃∃p,q. p ϵ 𝐂❨Ⓕ,m,𝟎❩ & q ϵ 𝐂❨Ⓕ,n,𝟎❩ & p●q = x.
 198 #x #m #n #Hx
 199 @(insert_eq_1 … (m+n) … Hx) -Hx #y #Hy
 200 generalize in match n; -n
 201 generalize in match m; -m
 202 elim Hy -x -y [|*: #x #y [ #k #_ ] #Hx #IH ] #m #n #Hy destruct
 203 [ elim (eq_inv_nplus_zero … Hy) -Hy #H1 #H2 destruct
 204   /2 width=5 by pcc_empty, ex3_2_intro/
 205 | elim (IH m (n+k)) -IH // #p #q #Hp #Hq #H0 destruct -Hx
 206   /3 width=5 by pcc_false_d_dx, ex3_2_intro/
 207 | elim (IH m n) -IH // #p #q #Hp #Hq #H0 destruct -Hx
 208   /3 width=5 by pcc_m_dx, ex3_2_intro/
 209 | elim (eq_inv_succ_nplus_dx … (sym_eq … Hy)) -Hy * #H1 #H2 (**) (* sym_eq *)
 210   [ destruct -IH
 211     /3 width=5 by pcc_empty, pcc_L_dx, ex3_2_intro/
 212   | elim (IH m (↓n)) -IH // #p #q #Hp #Hq #H0 destruct -Hx
 213     /3 width=5 by pcc_L_dx, ex3_2_intro/
 214   ]
 215 | elim (IH m n) -IH // #p #q #Hp #Hq #H0 destruct -Hx
 216   /3 width=5 by pcc_A_dx, ex3_2_intro/
 217 | elim (IH m n) -IH // #p #q #Hp #Hq #H0 destruct -Hx
 218   /3 width=5 by pcc_S_dx, ex3_2_intro/
 219 ]
 220 qed-.
 221
 222
 223 (* Constructions with path_lcons ********************************************)
 224
 225 lemma pcc_m_sn (o) (e) (q) (n):
 226       q ϵ 𝐂❨o,n,e❩ → (𝗺◗q) ϵ 𝐂❨o,n,e❩.
 227 #o #e #q #n #Hq
 228 lapply (pcc_append_bi (Ⓣ) … (𝟎) e … (𝐞◖𝗺) … Hq) -Hq
 229 /2 width=3 by pcc_m_dx/
 230 qed.
 231
 232 lemma pcc_L_sn (o) (e) (q) (n):
 233       q ϵ 𝐂❨o,n,e❩ → (𝗟◗q) ϵ 𝐂❨o,↑n,e❩.
 234 #o #e #q #n #Hq
 235 lapply (pcc_append_bi (Ⓣ) … (𝟎) e … (𝐞◖𝗟) … Hq) -Hq
 236 /2 width=3 by pcc_L_dx/
 237 qed.
 238
 239 lemma pcc_A_sn (o) (e) (q) (n):
 240       q ϵ 𝐂❨o,n,e❩ → (𝗔◗q) ϵ 𝐂❨o,n,e❩.
 241 #o #e #q #n #Hq
 242 lapply (pcc_append_bi (Ⓣ) … (𝟎) e … (𝐞◖𝗔) … Hq) -Hq
 243 /2 width=3 by pcc_A_dx/
 244 qed.
 245
 246 lemma pcc_S_sn (o) (e) (q) (n):
 247       q ϵ 𝐂❨o,n,e❩ → (𝗦◗q) ϵ 𝐂❨o,n,e❩.
 248 #o #e #q #n #Hq
 249 lapply (pcc_append_bi (Ⓣ) … (𝟎) e … (𝐞◖𝗦) … Hq) -Hq
 250 /2 width=3 by pcc_S_dx/
 251 qed.
 252
 253 (* Main inversions **********************************************************)
 254
 255 theorem pcc_mono (o1) (o2) (e) (q) (n1):
 256         q ϵ 𝐂❨o1,n1,e❩ → ∀n2. q ϵ 𝐂❨o2,n2,e❩ → n1 = n2.
 257 #o1 #o2 #e #q1 #n1 #Hn1 elim Hn1 -q1 -n1
 258 [|*: #q1 #n1 [ #k1 #_ ] #_ #IH ] #n2 #Hn2
 259 [ <(pcc_inv_empty … Hn2) -n2 //
 260 | lapply (pcc_des_d_dx … Hn2) -Hn2 #Hn2
 261   lapply (IH … Hn2) -q1 #H0
 262   /2 width=2 by eq_inv_nplus_bi_dx/
 263 | lapply (pcc_inv_m_dx … Hn2) -Hn2 #Hn2
 264   <(IH … Hn2) -q1 -n2 //
 265 | elim (pcc_inv_L_dx … Hn2) -Hn2 #Hn2 #H0
 266   >(IH … Hn2) -q1 //
 267 | lapply (pcc_inv_A_dx … Hn2) -Hn2 #Hn2
 268   <(IH … Hn2) -q1 -n2 //
 269 | lapply (pcc_inv_S_dx … Hn2) -Hn2 #Hn2
 270   <(IH … Hn2) -q1 -n2 //
 271 ]
 272 qed-.
 273
 274 theorem pcc_zero_dx_inj_L_sn (o1) (o2) (p1) (p2) (q1) (n):
 275         q1 ϵ 𝐂❨o1,n,𝟎❩ → ∀q2. q2 ϵ 𝐂❨o2,n,𝟎❩ →
 276         p1●𝗟◗q1 = p2●𝗟◗q2 → q1 = q2.
 277 #o1 #o2 #p1 #p2 #q1 #n #Hq1 elim Hq1 -q1 -n
 278 [|*: #q1 #n1 [ #k1 #_ ] #_ #IH ] * //
 279 [1,3,5,7,9,11: #l2 #q2 ] #Hq2
 280 <list_append_lcons_sn <list_append_lcons_sn #H0
 281 elim (eq_inv_list_lcons_bi ????? H0) -H0 #H0 #H1 destruct
 282 [ elim (pcc_inv_L_dx_zero_sn … Hq2)
 283 | lapply (pcc_des_d_dx … Hq2) -Hq2 #Hq2
 284   <(IH … Hq2) //
 285 | lapply (pcc_inv_m_dx … Hq2) -Hq2 #Hq2
 286   <(IH … Hq2) //
 287 | lapply (pcc_inv_L_dx_succ … Hq2) -Hq2 #Hq2
 288   <(IH … Hq2) //
 289 | lapply (pcc_inv_A_dx … Hq2) -Hq2 #Hq2
 290   <(IH … Hq2) //
 291 | lapply (pcc_inv_S_dx … Hq2) -Hq2 #Hq2
 292   <(IH … Hq2) //
 293 | elim (pcc_inv_empty_succ_zero … Hq2)
 294 ]
 295 qed-.
 296
 297 theorem pcc_inv_L_sn (o) (e) (q) (n) (m):
 298         (𝗟◗q) ϵ 𝐂❨o,n,e❩ → q ϵ 𝐂❨o,m,e❩ →
 299         ∧∧ ↓n = m & n = ↑↓n.
 300 #o #e #q #n #m #H1q #H2q
 301 lapply (pcc_L_sn … H2q) -H2q #H2q
 302 <(pcc_mono … H2q … H1q) -q -n
 303 /2 width=1 by conj/
 304 qed-.