matita/matita/contribs/lambdadelta/ground/relocation/pr_nat.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/notation/relations/ratsucc_3.ma".
  16 include "ground/arith/nat_pred_succ.ma".
  17 include "ground/relocation/pr_pat.ma".
  18
  19 (* NON-NEGATIVE APPLICATION FOR PARTIAL RELOCATION MAPS *********************)
  20
  21 definition pr_nat: relation3 pr_map nat nat ≝
  22            λf,l1,l2. @❨↑l1,f❩ ≘ ↑l2.
  23
  24 interpretation
  25   "relational non-negative application (partial relocation maps)"
  26   'RAtSucc l1 f l2 = (pr_nat f l1 l2).
  27
  28 (* Basic constructions ******************************************************)
  29
  30 lemma pr_nat_refl (f) (g) (k1) (k2):
  31       (⫯f) = g → 𝟎 = k1 → 𝟎 = k2 → @↑❨k1,g❩ ≘ k2.
  32 #f #g #k1 #k2 #H1 #H2 #H3 destruct
  33 /2 width=2 by pr_pat_refl/
  34 qed.
  35
  36 lemma pr_nat_push (f) (l1) (l2) (g) (k1) (k2):
  37       @↑❨l1,f❩ ≘ l2 → ⫯f = g → ↑l1 = k1 → ↑l2 = k2 → @↑❨k1,g❩ ≘ k2.
  38 #f #l1 #l2 #g #k1 #k2 #Hf #H1 #H2 #H3 destruct
  39 /2 width=7 by pr_pat_push/
  40 qed.
  41
  42 lemma pr_nat_next (f) (l1) (l2) (g) (k2):
  43       @↑❨l1,f❩ ≘ l2 → ↑f = g → ↑l2 = k2 → @↑❨l1,g❩ ≘ k2.
  44 #f #l1 #l2 #g #k2 #Hf #H1 #H2 destruct
  45 /2 width=5 by pr_pat_next/
  46 qed.
  47
  48 lemma pr_nat_pred_bi (f) (i1) (i2):
  49       @❨i1,f❩ ≘ i2 → @↑❨↓i1,f❩ ≘ ↓i2.
  50 #f #i1 #i2
  51 >(npsucc_pred i1) in ⊢ (%→?); >(npsucc_pred i2) in ⊢ (%→?);
  52 //
  53 qed.
  54
  55 (* Basic inversions *********************************************************)
  56
  57 (*** pr_nat_inv_ppx *)
  58 lemma pr_nat_inv_zero_push (f) (l1) (l2):
  59       @↑❨l1,f❩ ≘ l2 → ∀g. 𝟎 = l1 → ⫯g = f → 𝟎 = l2.
  60 #f #l1 #l2 #H #g #H1 #H2 destruct
  61 lapply (pr_pat_inv_unit_push … H ???) -H
  62 /2 width=2 by eq_inv_npsucc_bi/
  63 qed-.
  64
  65 (*** pr_nat_inv_npx *)
  66 lemma pr_nat_inv_succ_push (f) (l1) (l2):
  67       @↑❨l1,f❩ ≘ l2 → ∀g,k1. ↑k1 = l1 → ⫯g = f →
  68       ∃∃k2. @↑❨k1,g❩ ≘ k2 & ↑k2 = l2.
  69 #f #l1 #l2 #H #g #k1 #H1 #H2 destruct
  70 elim (pr_pat_inv_succ_push … H) -H [|*: // ] #k2 #Hg
  71 >(npsucc_pred (↑l2)) #H
  72 @(ex2_intro … (↓k2)) //
  73 qed-.
  74
  75 (*** pr_nat_inv_xnx *)
  76 lemma pr_nat_inv_next (f) (l1) (l2):
  77       @↑❨l1,f❩ ≘ l2 → ∀g. ↑g = f →
  78       ∃∃k2. @↑❨l1,g❩ ≘ k2 & ↑k2 = l2.
  79 #f #l1 #l2 #H #g #H1 destruct
  80 elim (pr_pat_inv_next … H) -H [|*: // ] #k2
  81 >(npsucc_pred (k2)) in ⊢ (%→?→?); #Hg #H
  82 @(ex2_intro … (↓k2)) //
  83 qed-.
  84
  85 (* Advanced inversions ******************************************************)
  86
  87 (*** pr_nat_inv_ppn *)
  88 lemma pr_nat_inv_zero_push_succ (f) (l1) (l2):
  89       @↑❨l1,f❩ ≘ l2 → ∀g,k2. 𝟎 = l1 → ⫯g = f → ↑k2 = l2 → ⊥.
  90 #f #l1 #l2 #Hf #g #k2 #H1 #H <(pr_nat_inv_zero_push … Hf … H1 H) -f -g -l1 -l2
  91 /2 width=3 by eq_inv_nsucc_zero/
  92 qed-.
  93
  94 (*** pr_nat_inv_npp *)
  95 lemma pr_nat_inv_succ_push_zero (f) (l1) (l2):
  96       @↑❨l1,f❩ ≘ l2 → ∀g,k1. ↑k1 = l1 → ⫯g = f → 𝟎 = l2 → ⊥.
  97 #f #l1 #l2 #Hf #g #k1 #H1 #H elim (pr_nat_inv_succ_push … Hf … H1 H) -f -l1
  98 #x2 #Hg * -l2 /2 width=3 by eq_inv_zero_nsucc/
  99 qed-.
 100
 101 (*** pr_nat_inv_npn *)
 102 lemma pr_nat_inv_succ_push_succ (f) (l1) (l2):
 103       @↑❨l1,f❩ ≘ l2 → ∀g,k1,k2. ↑k1 = l1 → ⫯g = f → ↑k2 = l2 → @↑❨k1,g❩ ≘ k2.
 104 #f #l1 #l2 #Hf #g #k1 #k2 #H1 #H elim (pr_nat_inv_succ_push … Hf … H1 H) -f -l1
 105 #x2 #Hg * -l2 #H >(eq_inv_nsucc_bi … H) -k2 //
 106 qed-.
 107
 108 (*** pr_nat_inv_xnp *)
 109 lemma pr_nat_inv_next_zero (f) (l1) (l2):
 110       @↑❨l1,f❩ ≘ l2 → ∀g. ↑g = f → 𝟎 = l2 → ⊥.
 111 #f #l1 #l2 #Hf #g #H elim (pr_nat_inv_next … Hf … H) -f
 112 #x2 #Hg * -l2 /2 width=3 by eq_inv_zero_nsucc/
 113 qed-.
 114
 115 (*** pr_nat_inv_xnn *)
 116 lemma pr_nat_inv_next_succ (f) (l1) (l2):
 117       @↑❨l1,f❩ ≘ l2 → ∀g,k2. ↑g = f → ↑k2 = l2 → @↑❨l1,g❩ ≘ k2.
 118 #f #l1 #l2 #Hf #g #k2 #H elim (pr_nat_inv_next … Hf … H) -f
 119 #x2 #Hg * -l2 #H >(eq_inv_nsucc_bi … H) -k2 //
 120 qed-.
 121
 122 (*** pr_nat_inv_pxp *)
 123 lemma pr_nat_inv_zero_bi (f) (l1) (l2):
 124       @↑❨l1,f❩ ≘ l2 → 𝟎 = l1 → 𝟎 = l2 → ∃g. ⫯g = f.
 125 #f elim (pr_map_split_tl … f) /2 width=2 by ex_intro/
 126 #H #l1 #l2 #Hf #H1 #H2 cases (pr_nat_inv_next_zero … Hf … H H2)
 127 qed-.
 128
 129 (*** pr_nat_inv_pxn *)
 130 lemma pr_nat_inv_zero_succ (f) (l1) (l2):
 131       @↑❨l1,f❩ ≘ l2 → ∀k2. 𝟎 = l1 → ↑k2 = l2 →
 132       ∃∃g. @↑❨l1,g❩ ≘ k2 & ↑g = f.
 133 #f elim (pr_map_split_tl … f)
 134 #H #l1 #l2 #Hf #k2 #H1 #H2
 135 [ elim (pr_nat_inv_zero_push_succ … Hf … H1 H H2)
 136 | /3 width=5 by pr_nat_inv_next_succ, ex2_intro/
 137 ]
 138 qed-.
 139
 140 (*** pr_nat_inv_nxp *)
 141 lemma pr_nat_inv_succ_zero (f) (l1) (l2):
 142       @↑❨l1,f❩ ≘ l2 → ∀k1. ↑k1 = l1 → 𝟎 = l2 → ⊥.
 143 #f elim (pr_map_split_tl f)
 144 #H #l1 #l2 #Hf #k1 #H1 #H2
 145 [ elim (pr_nat_inv_succ_push_zero … Hf … H1 H H2)
 146 | elim (pr_nat_inv_next_zero … Hf … H H2)
 147 ]
 148 qed-.
 149
 150 (*** pr_nat_inv_nxn *)
 151 lemma pr_nat_inv_succ_bi (f) (l1) (l2):
 152       @↑❨l1,f❩ ≘ l2 → ∀k1,k2. ↑k1 = l1 → ↑k2 = l2 →
 153       ∨∨ ∃∃g. @↑❨k1,g❩ ≘ k2 & ⫯g = f
 154        | ∃∃g. @↑❨l1,g❩ ≘ k2 & ↑g = f.
 155 #f elim (pr_map_split_tl f) *
 156 /4 width=7 by pr_nat_inv_next_succ, pr_nat_inv_succ_push_succ, ex2_intro, or_intror, or_introl/
 157 qed-.
 158
 159 (* Note: the following inversion lemmas must be checked *)
 160 (*** pr_nat_inv_xpx *)
 161 lemma pr_nat_inv_push (f) (l1) (l2):
 162       @↑❨l1,f❩ ≘ l2 → ∀g. ⫯g = f →
 163       ∨∨ ∧∧ 𝟎 = l1 & 𝟎 = l2
 164        | ∃∃k1,k2. @↑❨k1,g❩ ≘ k2 & ↑k1 = l1 & ↑k2 = l2.
 165 #f * [2: #l1 ] #l2 #Hf #g #H
 166 [ elim (pr_nat_inv_succ_push … Hf … H) -f /3 width=5 by or_intror, ex3_2_intro/
 167 | >(pr_nat_inv_zero_push … Hf … H) -f /3 width=1 by conj, or_introl/
 168 ]
 169 qed-.
 170
 171 (*** pr_nat_inv_xpp *)
 172 lemma pr_nat_inv_push_zero (f) (l1) (l2):
 173       @↑❨l1,f❩ ≘ l2 → ∀g. ⫯g = f → 𝟎 = l2 → 𝟎 = l1.
 174 #f #l1 #l2 #Hf #g #H elim (pr_nat_inv_push … Hf … H) -f * //
 175 #k1 #k2 #_ #_ * -l2 #H elim (eq_inv_zero_nsucc … H)
 176 qed-.
 177
 178 (*** pr_nat_inv_xpn *)
 179 lemma pr_nat_inv_push_succ (f) (l1) (l2):
 180       @↑❨l1,f❩ ≘ l2 → ∀g,k2. ⫯g = f → ↑k2 = l2 →
 181       ∃∃k1. @↑❨k1,g❩ ≘ k2 & ↑k1 = l1.
 182 #f #l1 #l2 #Hf #g #k2 #H elim (pr_nat_inv_push … Hf … H) -f *
 183 [ #_ * -l2 #H elim (eq_inv_nsucc_zero … H)
 184 | #x1 #x2 #Hg #H1 * -l2 #H
 185   lapply (eq_inv_nsucc_bi … H) -H #H destruct
 186   /2 width=3 by ex2_intro/
 187 ]
 188 qed-.
 189
 190 (*** pr_nat_inv_xxp *)
 191 lemma pr_nat_inv_zero_dx (f) (l1) (l2):
 192       @↑❨l1,f❩ ≘ l2 → 𝟎 = l2 → ∃∃g. 𝟎 = l1 & ⫯g = f.
 193 #f elim (pr_map_split_tl f)
 194 #H #l1 #l2 #Hf #H2
 195 [ /3 width=6 by pr_nat_inv_push_zero, ex2_intro/
 196 | elim (pr_nat_inv_next_zero … Hf … H H2)
 197 ]
 198 qed-.
 199
 200 (*** pr_nat_inv_xxn *)
 201 lemma pr_nat_inv_succ_dx (f) (l1) (l2): @↑❨l1,f❩ ≘ l2 → ∀k2.  ↑k2 = l2 →
 202       ∨∨ ∃∃g,k1. @↑❨k1,g❩ ≘ k2 & ↑k1 = l1 & ⫯g = f
 203        | ∃∃g. @↑❨l1,g❩ ≘ k2 & ↑g = f.
 204 #f elim (pr_map_split_tl f)
 205 #H #l1 #l2 #Hf #k2 #H2
 206 [ elim (pr_nat_inv_push_succ … Hf … H H2) -l2 /3 width=5 by or_introl, ex3_2_intro/
 207 | lapply (pr_nat_inv_next_succ … Hf … H H2) -l2 /3 width=3 by or_intror, ex2_intro/
 208 ]
 209 qed-.