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_1.ma".
  17 include "ground/arith/nat_plus.ma".
  18 include "ground/arith/nat_pred_succ.ma".
  19 include "ground/lib/subset.ma".
  20 include "ground/generated/insert_eq_1.ma".
  21
  22 (* CLOSED CONDITION FOR PATH ************************************************)
  23
  24 inductive pcc: relation2 nat path ≝
  25 | pcc_empty:
  26   pcc (𝟎) (𝐞)
  27 | pcc_d_dx (p) (n) (k):
  28   pcc (n+ninj k) p → pcc n (p◖𝗱k)
  29 | pcc_m_dx (p) (n):
  30   pcc n p → pcc n (p◖𝗺)
  31 | pcc_L_dx (p) (n):
  32   pcc n p → pcc (↑n) (p◖𝗟)
  33 | pcc_A_dx (p) (n):
  34   pcc n p → pcc n (p◖𝗔)
  35 | pcc_S_dx (p) (n):
  36   pcc n p → pcc n (p◖𝗦)
  37 .
  38
  39 interpretation
  40   "closed condition (path)"
  41   'ClassC n = (pcc n).
  42
  43 (* Basic inversions ********************************************************)
  44
  45 lemma pcc_inv_empty (n):
  46       (𝐞) ϵ 𝐂❨n❩ → 𝟎 = n.
  47 #n @(insert_eq_1 … (𝐞))
  48 #x * -n //
  49 #p #n [ #k ] #_ #H0 destruct
  50 qed-.
  51
  52 lemma pcc_inv_d_dx (p) (n) (k):
  53       p◖𝗱k ϵ 𝐂❨n❩ → p ϵ 𝐂❨n+k❩.
  54 #p #n #h @(insert_eq_1 … (p◖𝗱h))
  55 #x * -x -n
  56 [|*: #x #n [ #k ] #Hx ] #H0 destruct //
  57 qed-.
  58
  59 lemma pcc_inv_m_dx (p) (n):
  60       p◖𝗺 ϵ 𝐂❨n❩ → p ϵ 𝐂❨n❩.
  61 #p #n @(insert_eq_1 … (p◖𝗺))
  62 #x * -x -n
  63 [|*: #x #n [ #k ] #Hx ] #H0 destruct //
  64 qed-.
  65
  66 lemma pcc_inv_L_dx (p) (n):
  67       p◖𝗟 ϵ 𝐂❨n❩ →
  68       ∧∧ p ϵ 𝐂❨↓n❩ & n = ↑↓n.
  69 #p #n @(insert_eq_1 … (p◖𝗟))
  70 #x * -x -n
  71 [|*: #x #n [ #k ] #Hx ] #H0 destruct
  72 <npred_succ /2 width=1 by conj/
  73 qed-.
  74
  75 lemma pcc_inv_A_dx (p) (n):
  76       p◖𝗔 ϵ 𝐂❨n❩ → p ϵ 𝐂❨n❩.
  77 #p #n @(insert_eq_1 … (p◖𝗔))
  78 #x * -x -n
  79 [|*: #x #n [ #k ] #Hx ] #H0 destruct //
  80 qed-.
  81
  82 lemma pcc_inv_S_dx (p) (n):
  83       p◖𝗦 ϵ 𝐂❨n❩ → p ϵ 𝐂❨n❩.
  84 #p #n @(insert_eq_1 … (p◖𝗦))
  85 #x * -x -n
  86 [|*: #x #n [ #k ] #Hx ] #H0 destruct //
  87 qed-.
  88
  89 (* Advanced inversions ******************************************************)
  90
  91 lemma pcc_inv_empty_succ (n):
  92       (𝐞) ϵ 𝐂❨↑n❩ → ⊥.
  93 #n #H0
  94 lapply (pcc_inv_empty … H0) -H0 #H0
  95 /2 width=7 by eq_inv_zero_nsucc/
  96 qed-.
  97
  98 lemma pcc_inv_L_dx_zero (p):
  99       p◖𝗟 ϵ 𝐂❨𝟎❩ → ⊥.
 100 #p #H0
 101 elim (pcc_inv_L_dx … H0) -H0 #_ #H0
 102 /2 width=7 by eq_inv_zero_nsucc/
 103 qed-.
 104
 105 lemma pcc_inv_L_dx_succ (p) (n):
 106       p◖𝗟 ϵ 𝐂❨↑n❩ → p ϵ 𝐂❨n❩.
 107 #p #n #H0
 108 elim (pcc_inv_L_dx … H0) -H0 //
 109 qed-.
 110
 111 (* Main constructions with path_append **************************************)
 112
 113 theorem pcc_append_bi (p) (q) (m) (n):
 114         p ϵ 𝐂❨m❩ → q ϵ 𝐂❨n❩ → p●q ϵ 𝐂❨m+n❩.
 115 #p #q #m #n #Hm #Hm elim Hm -Hm // -Hm
 116 #p #n [ #k ] #_ #IH [3: <nplus_succ_dx ]
 117 /2 width=1 by pcc_d_dx, pcc_m_dx, pcc_L_dx, pcc_A_dx, pcc_S_dx/
 118 qed.
 119
 120 (* Constructions with path_lcons ********************************************)
 121
 122 lemma pcc_m_sn (q) (n):
 123       q ϵ 𝐂❨n❩ → (𝗺◗q) ϵ 𝐂❨n❩.
 124 #q #n #Hq
 125 lapply (pcc_append_bi (𝐞◖𝗺) … Hq) -Hq
 126 /2 width=3 by pcc_m_dx/
 127 qed.
 128
 129 lemma pcc_L_sn (q) (n):
 130       q ϵ 𝐂❨n❩ → (𝗟◗q) ϵ 𝐂❨↑n❩.
 131 #q #n #Hq
 132 lapply (pcc_append_bi (𝐞◖𝗟) … Hq) -Hq
 133 /2 width=3 by pcc_L_dx/
 134 qed.
 135
 136 lemma pcc_A_sn (q) (n):
 137       q ϵ 𝐂❨n❩ → (𝗔◗q) ϵ 𝐂❨n❩.
 138 #q #n #Hq
 139 lapply (pcc_append_bi (𝐞◖𝗔) … Hq) -Hq
 140 /2 width=3 by pcc_A_dx/
 141 qed.
 142
 143 lemma pcc_S_sn (q) (n):
 144       q ϵ 𝐂❨n❩ → (𝗦◗q) ϵ 𝐂❨n❩.
 145 #q #n #Hq
 146 lapply (pcc_append_bi (𝐞◖𝗦) … Hq) -Hq
 147 /2 width=3 by pcc_S_dx/
 148 qed.
 149
 150 (* Main inversions **********************************************************)
 151
 152 theorem pcc_mono (q) (n1):
 153         q ϵ 𝐂❨n1❩ → ∀n2. q ϵ 𝐂❨n2❩ → n1 = n2.
 154 #q1 #n1 #Hn1 elim Hn1 -q1 -n1
 155 [|*: #q1 #n1 [ #k1 ] #_ #IH ] #n2 #Hn2
 156 [ <(pcc_inv_empty … Hn2) -n2 //
 157 | lapply (pcc_inv_d_dx … Hn2) -Hn2 #Hn2
 158   lapply (IH … Hn2) -q1 #H0
 159   /2 width=2 by eq_inv_nplus_bi_dx/
 160 | lapply (pcc_inv_m_dx … Hn2) -Hn2 #Hn2
 161   <(IH … Hn2) -q1 -n2 //
 162 | elim (pcc_inv_L_dx … Hn2) -Hn2 #Hn2 #H0
 163   >(IH … Hn2) -q1 //
 164 | lapply (pcc_inv_A_dx … Hn2) -Hn2 #Hn2
 165   <(IH … Hn2) -q1 -n2 //
 166 | lapply (pcc_inv_S_dx … Hn2) -Hn2 #Hn2
 167   <(IH … Hn2) -q1 -n2 //
 168 ]
 169 qed-.
 170
 171 theorem pcc_inj_L_sn (p1) (p2) (q1) (n):
 172         q1 ϵ 𝐂❨n❩ → ∀q2. q2 ϵ 𝐂❨n❩ →
 173         p1●𝗟◗q1 = p2●𝗟◗q2 → q1 = q2.
 174 #p1 #p2 #q1 #n #Hq1 elim Hq1 -q1 -n
 175 [|*: #q1 #n1 [ #k1 ] #_ #IH ] * //
 176 [1,3,5,7,9,11: #l2 #q2 ] #Hq2
 177 <list_append_lcons_sn <list_append_lcons_sn #H0
 178 elim (eq_inv_list_lcons_bi ????? H0) -H0 #H0 #H1 destruct
 179 [ elim (pcc_inv_L_dx_zero … Hq2)
 180 | lapply (pcc_inv_d_dx … Hq2) -Hq2 #Hq2
 181   <(IH … Hq2) //
 182 | lapply (pcc_inv_m_dx … Hq2) -Hq2 #Hq2
 183   <(IH … Hq2) //
 184 | lapply (pcc_inv_L_dx_succ … Hq2) -Hq2 #Hq2
 185   <(IH … Hq2) //
 186 | lapply (pcc_inv_A_dx … Hq2) -Hq2 #Hq2
 187   <(IH … Hq2) //
 188 | lapply (pcc_inv_S_dx … Hq2) -Hq2 #Hq2
 189   <(IH … Hq2) //
 190 | elim (pcc_inv_empty_succ … Hq2)
 191 ]
 192 qed-.
 193
 194 theorem pcc_inv_L_sn (q) (n) (m):
 195         (𝗟◗q) ϵ 𝐂❨n❩ → q ϵ 𝐂❨m❩ →
 196         ∧∧ ↓n = m & n = ↑↓n.
 197 #q #n #m #H1q #H2q
 198 lapply (pcc_L_sn … H2q) -H2q #H2q
 199 <(pcc_mono … H2q … H1q) -q -n
 200 /2 width=1 by conj/
 201 qed-.