matita/matita/contribs/lambdadelta/ground/relocation/fr2_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/rat_3.ma".
  16 include "ground/arith/nat_plus.ma".
  17 include "ground/arith/nat_lt.ma".
  18 include "ground/relocation/fr2_map.ma".
  19
  20 (* NON-NEGATIVE APPLICATION FOR FINITE RELOCATION MAPS WITH PAIRS ***********)
  21
  22 (*** at *)
  23 inductive fr2_nat: fr2_map → relation nat ≝
  24 (*** at_nil *)
  25 | fr2_nat_nil (l):
  26   fr2_nat (◊) l l
  27 (*** at_lt *)
  28 | fr2_nat_lt (f) (d) (h) (l1) (l2):
  29   l1 < d → fr2_nat f l1 l2 → fr2_nat (❨d,h❩;f) l1 l2
  30 (*** at_ge *)
  31 | fr2_nat_ge (f) (d) (h) (l1) (l2):
  32   d ≤ l1 → fr2_nat f (l1 + h) l2 → fr2_nat (❨d,h❩;f) l1 l2
  33 .
  34
  35 interpretation
  36   "non-negative relational application (finite relocation maps with pairs)"
  37   'RAt l1 f l2 = (fr2_nat f l1 l2).
  38
  39 (* Basic inversions *********************************************************)
  40
  41 (*** at_inv_nil *)
  42 lemma fr2_nat_inv_nil (l1) (l2):
  43       @❪l1, ◊❫ ≘ l2 → l1 = l2.
  44 #l1 #l2 @(insert_eq_1 … (◊))
  45 #f * -f -l1 -l2
  46 [ //
  47 | #f #d #h #l1 #l2 #_ #_ #H destruct
  48 | #f #d #h #l1 #l2 #_ #_ #H destruct
  49 ]
  50 qed-.
  51
  52 (*** at_inv_cons *)
  53 lemma fr2_nat_inv_cons (f) (d) (h) (l1) (l2):
  54       @❪l1, ❨d,h❩;f❫ ≘ l2 →
  55       ∨∨ ∧∧ l1 < d & @❪l1, f❫ ≘ l2
  56        | ∧∧ d ≤ l1 & @❪l1+h, f❫ ≘ l2.
  57 #g #d #h #l1 #l2 @(insert_eq_1 … (❨d, h❩;g))
  58 #f * -f -l1 -l2
  59 [ #l #H destruct
  60 | #f1 #d1 #h1 #l1 #l2 #Hld1 #Hl12 #H destruct /3 width=1 by or_introl, conj/
  61 | #f1 #d1 #h1 #l1 #l2 #Hdl1 #Hl12 #H destruct /3 width=1 by or_intror, conj/
  62 ]
  63 qed-.
  64
  65 (*** at_inv_cons *)
  66 lemma fr2_nat_inv_cons_lt (f) (d) (h) (l1) (l2):
  67       @❪l1, ❨d,h❩;f❫ ≘ l2 → l1 < d → @❪l1, f❫ ≘ l2.
  68 #f #d #h #l1 #h2 #H
  69 elim (fr2_nat_inv_cons … H) -H * // #Hdl1 #_ #Hl1d
  70 elim (nlt_ge_false … Hl1d Hdl1)
  71 qed-.
  72
  73 (*** at_inv_cons *)
  74 lemma fr2_nat_inv_cons_ge (f) (d) (h) (l1) (l2):
  75       @❪l1, ❨d,h❩;f❫ ≘ l2 → d ≤ l1 → @❪l1+h, f❫ ≘ l2.
  76 #f #d #h #l1 #h2 #H
  77 elim (fr2_nat_inv_cons … H) -H * // #Hl1d #_ #Hdl1
  78 elim (nlt_ge_false … Hl1d Hdl1)
  79 qed-.