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