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_nsucc_zero/
 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 (* Main inversions **********************************************************)
 121
 122 theorem ppc_mono (q) (n1):
 123         q ϵ 𝐂❨n1❩ → ∀n2. q ϵ 𝐂❨n2❩ → n1 = n2.
 124 #q1 #n1 #Hn1 elim Hn1 -q1 -n1
 125 [|*: #q1 #n1 [ #k1 ] #_ #IH ] #n2 #Hn2
 126 [ <(pcc_inv_empty … Hn2) -n2 //
 127 | lapply (pcc_inv_d_dx … Hn2) -Hn2 #Hn2
 128   lapply (IH … Hn2) -q1 #H0
 129   /2 width=2 by eq_inv_nplus_bi_dx/
 130 | lapply (pcc_inv_m_dx … Hn2) -Hn2 #Hn2
 131   <(IH … Hn2) -q1 -n2 //
 132 | elim (pcc_inv_L_dx … Hn2) -Hn2 #Hn2 #H0
 133   >(IH … Hn2) -q1 //
 134 | lapply (pcc_inv_A_dx … Hn2) -Hn2 #Hn2
 135   <(IH … Hn2) -q1 -n2 //
 136 | lapply (pcc_inv_S_dx … Hn2) -Hn2 #Hn2
 137   <(IH … Hn2) -q1 -n2 //
 138 ]
 139 qed-.
 140
 141 theorem pcc_inj_L_sn (p1) (p2) (q1) (n):
 142         q1 ϵ 𝐂❨n❩ → ∀q2. q2 ϵ 𝐂❨n❩ →
 143         p1●𝗟◗q1 = p2●𝗟◗q2 → q1 = q2.
 144 #p1 #p2 #q1 #n #Hq1 elim Hq1 -q1 -n
 145 [|*: #q1 #n1 [ #k1 ] #_ #IH ] * //
 146 [1,3,5,7,9,11: #l2 #q2 ] #Hq2
 147 <list_append_lcons_sn <list_append_lcons_sn #H0
 148 elim (eq_inv_list_lcons_bi ????? H0) -H0 #H0 #H1 destruct
 149 [ elim (pcc_inv_L_dx_zero … Hq2)
 150 | lapply (pcc_inv_d_dx … Hq2) -Hq2 #Hq2
 151   <(IH … Hq2) //
 152 | lapply (pcc_inv_m_dx … Hq2) -Hq2 #Hq2
 153   <(IH … Hq2) //
 154 | lapply (pcc_inv_L_dx_succ … Hq2) -Hq2 #Hq2
 155   <(IH … Hq2) //
 156 | lapply (pcc_inv_A_dx … Hq2) -Hq2 #Hq2
 157   <(IH … Hq2) //
 158 | lapply (pcc_inv_S_dx … Hq2) -Hq2 #Hq2
 159   <(IH … Hq2) //
 160 | elim (pcc_inv_empty_succ … Hq2)
 161 ]
 162 qed-.