matita/matita/contribs/lambdadelta/apps_2/etc/models/model_lower.etc

   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 "apps_2/notation/models/fdrop_4.ma".
  16 include "apps_2/models/model_veq.ma".
  17 include "apps_2/models/model_raise.ma".
  18
  19 (* MODEL ********************************************************************)
  20
  21 definition lower: ∀M. nat → nat → evaluation M → evaluation M ≝
  22                   λM,l,m,lv,i. tri … i l (lv i) (lv (i+m)) (lv (i+m)).
  23
  24 interpretation "evaluation lower (models)"
  25    'FDrop M l m lv = (lower M l m lv).
  26
  27 (* Basic properties *********************************************************)
  28
  29 lemma lower_lt: ∀M,lv,l,m,i. i < l → (↓[l, m]⦋M⦌ lv) i = lv i.
  30 /2 width=1 by tri_lt/ qed-.
  31
  32 lemma lower_ge: ∀M,lv,l,m,i. l ≤ i → (↓[l, m]⦋M⦌ lv) i = lv (i+m).
  33 #M #lv #l #m #i #Hli elim (le_to_or_lt_eq … Hli) -Hli #Hli destruct
  34 [ /2 width=1 by tri_gt/
  35 | /2 width=1 by tri_eq/
  36 ]
  37 qed-.
  38
  39 lemma lower_veq: ∀M,v1,v2. v1 ≐⦋M⦌ v2 → ∀l,m. ↓[l, m] v1 ≐ ↓[l, m] v2.
  40 #m #v1 #v2 #Hv12 #l #m #i elim (lt_or_ge i l) #Hli
  41 [ >lower_lt // >lower_lt //
  42 | >lower_ge // >lower_ge //
  43 ]
  44 qed.
  45
  46 lemma lower_refl: ∀M,v,l. ↓[l, 0] v ≐⦋M⦌ v.
  47 #M #v #l #i elim (lt_or_ge … i l) #Hil
  48 [ >lower_lt //
  49 | >lower_ge //
  50 ]
  51 qed.
  52
  53 (* Main properties **********************************************************)
  54
  55 theorem lower_lower_le_sym: ∀M,v,l1,l2,m1,m2. l1 ≤ l2 →
  56                             ↓[l1, m1] ↓[l2+m1, m2] v ≐⦋M⦌ ↓[l2, m2] ↓[l1, m1] v.
  57 #M #v #l1 #l2 #m1 #m2 #Hl12 #j elim (lt_or_ge … j l1) #Hjl1
  58 [ lapply (lt_to_le_to_lt … Hjl1 Hl12) -Hl12 #Hjl2
  59   >lower_lt // >lower_lt /2 width=3 by lt_to_le_to_lt/
  60   >lower_lt // >lower_lt //
  61 | >lower_ge // elim (lt_or_ge … j l2) #Hjl2 -Hl12
  62   [ >lower_lt /2 width=1 by lt_minus_to_plus/
  63     >lower_lt // >lower_ge //
  64   | >lower_ge /2 width=1 by monotonic_le_plus_l/
  65     >lower_ge // >lower_ge /2 width=1 by le_plus/
  66   ]
  67 ]
  68 qed.
  69
  70 lemma lower_lower_le: ∀M,v,l1,l2,m1,m2. l1 ≤ l2 →
  71                       ↓[l2, m2] ↓[l1, m1] v ≐⦋M⦌ ↓[l1, m1] ↓[l2+m1, m2] v.
  72 /3 width=1 by lower_lower_le_sym, veq_sym/ qed-.
  73
  74 (* Properties on raise ******************************************************)
  75
  76 lemma lower_raise_lt: ∀M,v,d,l,m,i. i ≤ l → ↓[l+1, m] [i⬐d] v ≐⦋M⦌ [i⬐d] ↓[l, m] v.
  77 #M #v #d #l #m #i #Hil #j elim (lt_or_eq_or_gt … j i) #Hij destruct
  78 [ lapply (lt_to_le_to_lt … Hij Hil) -Hil #Hjl
  79   >lower_lt /2 width=1 by le_S/ >raise_lt // >raise_lt // >lower_lt //
  80 | >lower_lt /2 width=1 by le_S_S/ >raise_eq >raise_eq //
  81 | lapply (ltn_to_ltO … Hij) #Hj
  82   >raise_gt // elim (lt_or_ge … j (l+1)) #Hlj
  83   [ -Hil >lower_lt // >lower_lt /2 width=2 by lt_plus_to_minus/ >raise_gt //
  84   | >lower_ge // >lower_ge /2 width=1 by le_plus_to_minus_r/
  85     >raise_gt /2 width=1 by le_plus/ >plus_minus //
  86   ]
  87 ]
  88 qed.
  89
  90 lemma raise_lower_lt: ∀M,v,d,l,m,i. i ≤ l → [i⬐d] ↓[l, m] v ≐⦋M⦌ ↓[l+1, m] [i⬐d] v.
  91 /3 width=1 by lower_raise_lt, veq_sym/ qed.
  92
  93 lemma lower_raise_be: ∀M,v,d,l,m,i. l ≤ i → i ≤ l + m → ↓[l, m+1] [i⬐d] v ≐⦋M⦌ ↓[l, m] v.
  94 #M #v #d #l #m #i #Hli #Hilm #j elim (lt_or_ge … j l) #Hlj
  95 [ lapply (lt_to_le_to_lt … Hlj Hli) -Hli -Hilm #Hij
  96   >lower_lt // >lower_lt // >raise_lt //
  97 | lapply (transitive_le … (j+m) Hilm ?) -Hli -Hilm /2 width=1 by monotonic_le_plus_l/ #Hijm
  98   >lower_ge // >lower_ge // >raise_gt /2 width=1 by le_S_S/
  99 ]
 100 qed.
 101
 102 lemma lower_raise_be_sym: ∀M,v,d,l,m,i. l ≤ i → i ≤ l + m → ↓[l, m] v ≐⦋M⦌  ↓[l, m+1] [i⬐d] v.
 103 /3 width=1 by lower_raise_be, veq_sym/ qed.
 104
 105 lemma lower_raise: ∀M,v,d,l. ↓[l, 1] [l⬐d] v ≐⦋M⦌ v.
 106 /3 width=3 by lower_raise_be, veq_trans/ qed.
 107
 108 lemma lower_raise_sym: ∀M,v,d,l. v ≐⦋M⦌ ↓[l, 1] [l⬐d] v.
 109 /2 width=1 by veq_sym/ qed.
 110
 111 lemma raise_lower: ∀M,v,i. [i⬐v i] ↓[i,1] v ≐⦋M⦌ v.
 112 #M #V #i #j elim (lt_or_eq_or_gt j i) #Hij destruct
 113 [ >raise_lt // >lower_lt //
 114 | >raise_eq //
 115 | >raise_gt // >lower_ge /2 width=1 by monotonic_pred/
 116   <plus_minus_m_m /2 width=2 by ltn_to_ltO/
 117 ]
 118 qed.
 119
 120 lemma raise_lower_sym: ∀M,v,i. v ≐⦋M⦌ [i⬐v i] ↓[i,1] v.
 121 /3 width=1 by raise_lower, veq_sym/ qed.
 122
 123 lemma raise_lower_be: ∀M,v,l,m. ↓[l, m] v ≐⦋M⦌ [l⬐v (l+m)] ↓[l, m+1] v.
 124 #M #v #l #m #j elim (lt_or_eq_or_gt j l) #Hlj destruct
 125 [ >lower_lt // >raise_lt // >lower_lt //
 126 | >lower_ge // >raise_eq //
 127 | lapply (ltn_to_ltO … Hlj) #Hj
 128   >lower_ge /2 width=1 by lt_to_le/ >raise_gt //
 129   >lower_ge /4 width=1 by plus_minus, monotonic_pred, eq_f/
 130 ]
 131 qed.
 132
 133 lemma raise_lower_be_sym: ∀M,v,l,m. [l⬐v (l+m)] ↓[l, m+1] v ≐⦋M⦌ ↓[l, m] v.
 134 /3 width=1 by raise_lower_be, veq_sym/ qed.
 135
 136 (* Forward lemmas on raise **************************************************)
 137
 138 lemma lower_fwd_raise_be_S: ∀M,v1,v2,d,l,m. ↓[l, m] v1 ≐⦋M⦌ [l⬐d] v2 →
 139                             ↓[l, m+1] v1 ≐ v2.
 140 #M #v1 #v2 #d #l #m #Hv12 #j elim (lt_or_ge j l) #Hlj
 141 [ lapply (Hv12 j) -Hv12
 142   >lower_lt // >lower_lt // >raise_lt //
 143 | lapply (Hv12 (j+1))
 144   >lower_ge /2 width=1 by le_S/ >lower_ge // >raise_gt /2 width=1 by le_S_S/
 145 ]
 146 qed-.
 147
 148 lemma raise_fwd_lower_be_S: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 →
 149                             v2 ≐ ↓[l, m+1] v1.
 150 /3 width=2 by lower_fwd_raise_be_S, veq_sym/ qed-.
 151
 152 lemma lower_fwd_raise_be_O: ∀M,v1,v2,d,l,m. ↓[l, m] v1 ≐⦋M⦌ [l⬐d] v2 → v1 (l+m) = d.
 153 #M #v1 #v2 #d #l #m #Hv12 lapply (Hv12 l)
 154 >lower_ge // >raise_eq //
 155 qed-.
 156
 157 lemma raise_fwd_lower_be_O: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 → d = v1 (l+m).
 158 /4 width=7 by lower_fwd_raise_be_O, veq_sym, sym_eq/ qed-.
 159
 160 (* Inversion lemmas on raise ************************************************)
 161
 162 lemma raise_inv_lower_lt: ∀M,v1,v2,d,l,m,i. i ≤ l → [i⬐d] v1 ≐⦋M⦌ ↓[l+1, m] v2 →
 163                           ∃∃v. v1 ≐ ↓[l, m] v & v2 ≐ [i⬐d] v.
 164 #M #v1 #v2 #d #l #m #i #Hil #Hv12
 165 lapply (Hv12 i) >raise_eq >lower_lt /2 width=1 by le_S_S/ #H destruct
 166 @(ex2_intro … (↓[i, 1] v2)) //
 167 @(veq_trans … (↓[i, 1] ↓[l+1, m] v2))
 168 /3 width=3 by lower_lower_le_sym, lower_veq, veq_trans/
 169 qed-.
 170
 171 lemma lower_inv_raise_lt: ∀M,v1,v2,d,l,m,i. i ≤ l → ↓[l+1, m] v2 ≐⦋M⦌ [i⬐d] v1 →
 172                           ∃∃v. v1 ≐ ↓[l, m] v & v2 ≐ [i⬐d] v.
 173 /3 width=1 by raise_inv_lower_lt, veq_sym/ qed-.
 174
 175 lemma lower_inv_raise_be: ∀M,v1,v2,d,l,m. ↓[l, m] v1 ≐⦋M⦌ [l⬐d] v2 →
 176                           v1 (l+m) = d ∧ ↓[l, m+1] v1 ≐ v2.
 177 /3 width=2 by lower_fwd_raise_be_O, lower_fwd_raise_be_S, conj/ qed-.
 178
 179 lemma raise_inv_lower_be: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 →
 180                           d = v1 (l+m) ∧ v2 ≐ ↓[l, m+1] v1.
 181 /3 width=2 by raise_fwd_lower_be_O, raise_fwd_lower_be_S, conj/ qed-.