matita/matita/contribs/lambdadelta/basic_2/unfold/gr2_minus.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 "basic_2/unfold/gr2.ma".
  16
  17 (* GENERIC RELOCATION WITH PAIRS ********************************************)
  18
  19 inductive minuss: nat → relation (list2 nat nat) ≝
  20 | minuss_nil: ∀i. minuss i ⟠ ⟠
  21 | minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 →
  22               minuss i ({d, e} @ des1) ({d - i, e} @ des2)
  23 | minuss_ge : ∀des1,des2,d,e,i. d ≤ i → minuss (e + i) des1 des2 →
  24               minuss i ({d, e} @ des1) des2
  25 .
  26
  27 interpretation "minus (generic relocation with pairs)"
  28    'RMinus des1 i des2 = (minuss i des1 des2).
  29
  30 (* Basic inversion lemmas ***************************************************)
  31
  32 fact minuss_inv_nil1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → des1 = ⟠ → des2 = ⟠.
  33 #des1 #des2 #i * -des1 -des2 -i
  34 [ //
  35 | #des1 #des2 #d #e #i #_ #_ #H destruct
  36 | #des1 #des2 #d #e #i #_ #_ #H destruct
  37 ]
  38 qed.
  39
  40 lemma minuss_inv_nil1: ∀des2,i. ⟠ ▭ i ≡ des2 → des2 = ⟠.
  41 /2 width=4/ qed-.
  42
  43 fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 →
  44                            ∀d,e,des. des1 = {d, e} @ des →
  45                            d ≤ i ∧ des ▭ e + i ≡ des2 ∨
  46                            ∃∃des0. i < d & des ▭ i ≡ des0 &
  47                                    des2 = {d - i, e} @ des0.
  48 #des1 #des2 #i * -des1 -des2 -i
  49 [ #i #d #e #des #H destruct
  50 | #des1 #des #d1 #e1 #i1 #Hid1 #Hdes #d2 #e2 #des2 #H destruct /3 width=3/
  51 | #des1 #des #d1 #e1 #i1 #Hdi1 #Hdes #d2 #e2 #des2 #H destruct /3 width=1/
  52 ]
  53 qed.
  54
  55 lemma minuss_inv_cons1: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 →
  56                         d ≤ i ∧ des1 ▭ e + i ≡ des2 ∨
  57                         ∃∃des. i < d & des1 ▭ i ≡ des &
  58                                des2 = {d - i, e} @ des.
  59 /2 width=3/ qed-.
  60
  61 lemma minuss_inv_cons1_ge: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 →
  62                            d ≤ i → des1 ▭ e + i ≡ des2.
  63 #des1 #des2 #d #e #i #H
  64 elim (minuss_inv_cons1 … H) -H * // #des #Hid #_ #_ #Hdi
  65 lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi
  66 elim (lt_refl_false … Hi)
  67 qed-.
  68
  69 lemma minuss_inv_cons1_lt: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 →
  70                            i < d →
  71                            ∃∃des. des1 ▭ i ≡ des & des2 = {d - i, e} @ des.
  72 #des1 #des2 #d #e #i #H
  73 elim (minuss_inv_cons1 … H) -H * /2 width=3/ #Hdi #_ #Hid
  74 lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi
  75 elim (lt_refl_false … Hi)
  76 qed-.