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

   1 lemma pippo: ∀M,v1,v2,d,i. [i⬐d] v1 ≐⦋M⦌ v2 → v1 ≐⦋M⦌ ↓[i,1] v2.
   2 #M #v1 #v2 #d #i #H #j elim (lt_or_ge … j i) #Hij
   3 [ >lower_lt // <(H j) >raise_lt //
   4 | >lower_ge // <(H (j+1)) >raise_gt /2 width=1 by le_S_S/
   5 ]
   6 qed-.
   7
   8 lemma vdrop_refl: ∀M,v,l. ↓[l, 0] v ≐⦋M⦌ v.
   9 #M #v #l #i elim (lt_or_ge … i l) #Hil
  10 [ >vdrop_lt //
  11 | >vdrop_ge //
  12 ]
  13 qed.
  14
  15 (* Main properties **********************************************************)
  16
  17 theorem vdrop_vdrop_le_sym: ∀M,v,l1,l2,m1,m2. l1 ≤ l2 →
  18                             ↓[l1, m1] ↓[l2+m1, m2] v ≐⦋M⦌ ↓[l2, m2] ↓[l1, m1] v.
  19 #M #v #l1 #l2 #m1 #m2 #Hl12 #j elim (lt_or_ge … j l1) #Hjl1
  20 [ lapply (lt_to_le_to_lt … Hjl1 Hl12) -Hl12 #Hjl2
  21   >vdrop_lt // >vdrop_lt /2 width=3 by lt_to_le_to_lt/
  22   >vdrop_lt // >vdrop_lt //
  23 | >vdrop_ge // elim (lt_or_ge … j l2) #Hjl2 -Hl12
  24   [ >vdrop_lt /2 width=1 by lt_minus_to_plus/
  25     >vdrop_lt // >vdrop_ge //
  26   | >vdrop_ge /2 width=1 by monotonic_le_plus_l/
  27     >vdrop_ge // >vdrop_ge /2 width=1 by le_plus/
  28   ]
  29 ]
  30 qed.
  31
  32 lemma vdrop_vdrop_le: ∀M,v,l1,l2,m1,m2. l1 ≤ l2 →
  33                       ↓[l2, m2] ↓[l1, m1] v ≐⦋M⦌ ↓[l1, m1] ↓[l2+m1, m2] v.
  34 /3 width=1 by vdrop_vdrop_le_sym, veq_sym/ qed-.
  35
  36 (* Properties on raise ******************************************************)
  37
  38 lemma vdrop_raise_lt: ∀M,v,d,l,m,i. i ≤ l → ↓[l+1, m] [i⬐d] v ≐⦋M⦌ [i⬐d] ↓[l, m] v.
  39 #M #v #d #l #m #i #Hil #j elim (lt_or_eq_or_gt … j i) #Hij destruct
  40 [ lapply (lt_to_le_to_lt … Hij Hil) -Hil #Hjl
  41   >vdrop_lt /2 width=1 by le_S/ >raise_lt // >raise_lt // >vdrop_lt //
  42 | >vdrop_lt /2 width=1 by le_S_S/ >raise_eq >raise_eq //
  43 | lapply (ltn_to_ltO … Hij) #Hj
  44   >raise_gt // elim (lt_or_ge … j (l+1)) #Hlj
  45   [ -Hil >vdrop_lt // >vdrop_lt /2 width=2 by lt_plus_to_minus/ >raise_gt //
  46   | >vdrop_ge // >vdrop_ge /2 width=1 by le_plus_to_minus_r/
  47     >raise_gt /2 width=1 by le_plus/ >plus_minus //
  48   ]
  49 ]
  50 qed.
  51
  52 lemma raise_vdrop_lt: ∀M,v,d,l,m,i. i ≤ l → [i⬐d] ↓[l, m] v ≐⦋M⦌ ↓[l+1, m] [i⬐d] v.
  53 /3 width=1 by vdrop_raise_lt, veq_sym/ qed.
  54
  55 lemma vdrop_raise_be: ∀M,v,d,l,m,i. l ≤ i → i ≤ l + m → ↓[l, m+1] [i⬐d] v ≐⦋M⦌ ↓[l, m] v.
  56 #M #v #d #l #m #i #Hli #Hilm #j elim (lt_or_ge … j l) #Hlj
  57 [ lapply (lt_to_le_to_lt … Hlj Hli) -Hli -Hilm #Hij
  58   >vdrop_lt // >vdrop_lt // >raise_lt //
  59 | lapply (transitive_le … (j+m) Hilm ?) -Hli -Hilm /2 width=1 by monotonic_le_plus_l/ #Hijm
  60   >vdrop_ge // >vdrop_ge // >raise_gt /2 width=1 by le_S_S/
  61 ]
  62 qed.
  63
  64 lemma vdrop_raise_be_sym: ∀M,v,d,l,m,i. l ≤ i → i ≤ l + m → ↓[l, m] v ≐⦋M⦌  ↓[l, m+1] [i⬐d] v.
  65 /3 width=1 by vdrop_raise_be, veq_sym/ qed.
  66
  67 lemma vdrop_raise: ∀M,v,d,l. ↓[l, 1] [l⬐d] v ≐⦋M⦌ v.
  68 /3 width=3 by vdrop_raise_be, veq_trans/ qed.
  69
  70 lemma vdrop_raise_sym: ∀M,v,d,l. v ≐⦋M⦌ ↓[l, 1] [l⬐d] v.
  71 /2 width=1 by veq_sym/ qed.
  72
  73 lemma raise_vdrop: ∀M,v,i. [i⬐v i] ↓[i,1] v ≐⦋M⦌ v.
  74 #M #V #i #j elim (lt_or_eq_or_gt j i) #Hij destruct
  75 [ >raise_lt // >vdrop_lt //
  76 | >raise_eq //
  77 | >raise_gt // >vdrop_ge /2 width=1 by monotonic_pred/
  78   <plus_minus_m_m /2 width=2 by ltn_to_ltO/
  79 ]
  80 qed.
  81
  82 lemma raise_vdrop_sym: ∀M,v,i. v ≐⦋M⦌ [i⬐v i] ↓[i,1] v.
  83 /3 width=1 by raise_vdrop, veq_sym/ qed.
  84
  85 lemma raise_vdrop_be: ∀M,v,l,m. ↓[l, m] v ≐⦋M⦌ [l⬐v (l+m)] ↓[l, m+1] v.
  86 #M #v #l #m #j elim (lt_or_eq_or_gt j l) #Hlj destruct
  87 [ >vdrop_lt // >raise_lt // >vdrop_lt //
  88 | >vdrop_ge // >raise_eq //
  89 | lapply (ltn_to_ltO … Hlj) #Hj
  90   >vdrop_ge /2 width=1 by lt_to_le/ >raise_gt //
  91   >vdrop_ge /4 width=1 by plus_minus, monotonic_pred, eq_f/
  92 ]
  93 qed.
  94
  95 lemma raise_vdrop_be_sym: ∀M,v,l,m. [l⬐v (l+m)] ↓[l, m+1] v ≐⦋M⦌ ↓[l, m] v.
  96 /3 width=1 by raise_vdrop_be, veq_sym/ qed.
  97
  98 (* Forward lemmas on raise **************************************************)
  99
 100 lemma vdrop_fwd_raise_be_S: ∀M,v1,v2,d,l,m. ↓[l, m] v1 ≐⦋M⦌ [l⬐d] v2 →
 101                             ↓[l, m+1] v1 ≐ v2.
 102 #M #v1 #v2 #d #l #m #Hv12 #j elim (lt_or_ge j l) #Hlj
 103 [ lapply (Hv12 j) -Hv12
 104   >vdrop_lt // >vdrop_lt // >raise_lt //
 105 | lapply (Hv12 (j+1))
 106   >vdrop_ge /2 width=1 by le_S/ >vdrop_ge // >raise_gt /2 width=1 by le_S_S/
 107 ]
 108 qed-.
 109
 110 lemma raise_fwd_vdrop_be_S: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 →
 111                             v2 ≐ ↓[l, m+1] v1.
 112 /3 width=2 by vdrop_fwd_raise_be_S, veq_sym/ qed-.
 113
 114 lemma vdrop_fwd_raise_be_O: ∀M,v1,v2,d,l,m. ↓[l, m] v1 ≐⦋M⦌ [l⬐d] v2 → v1 (l+m) = d.
 115 #M #v1 #v2 #d #l #m #Hv12 lapply (Hv12 l)
 116 >vdrop_ge // >raise_eq //
 117 qed-.
 118
 119 lemma raise_fwd_vdrop_be_O: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 → d = v1 (l+m).
 120 /4 width=7 by vdrop_fwd_raise_be_O, veq_sym, sym_eq/ qed-.
 121
 122 (* Inversion lemmas on raise ************************************************)
 123
 124 lemma raise_inv_vdrop_lt: ∀M,v1,v2,d,l,m,i. i ≤ l → [i⬐d] v1 ≐⦋M⦌ ↓[l+1, m] v2 →
 125                           ∃∃v. v1 ≐ ↓[l, m] v & v2 ≐ [i⬐d] v.
 126 #M #v1 #v2 #d #l #m #i #Hil #Hv12
 127 lapply (Hv12 i) >raise_eq >vdrop_lt /2 width=1 by le_S_S/ #H destruct
 128 @(ex2_intro … (↓[i, 1] v2)) //
 129 @(veq_trans … (↓[i, 1] ↓[l+1, m] v2))
 130 /3 width=3 by vdrop_vdrop_le_sym, vdrop_veq, veq_trans/
 131 qed-.
 132
 133 lemma vdrop_inv_raise_lt: ∀M,v1,v2,d,l,m,i. i ≤ l → ↓[l+1, m] v2 ≐⦋M⦌ [i⬐d] v1 →
 134                           ∃∃v. v1 ≐ ↓[l, m] v & v2 ≐ [i⬐d] v.
 135 /3 width=1 by raise_inv_vdrop_lt, veq_sym/ qed-.
 136
 137 lemma vdrop_inv_raise_be: ∀M,v1,v2,d,l,m. ↓[l, m] v1 ≐⦋M⦌ [l⬐d] v2 →
 138                           v1 (l+m) = d ∧ ↓[l, m+1] v1 ≐ v2.
 139 /3 width=2 by vdrop_fwd_raise_be_O, vdrop_fwd_raise_be_S, conj/ qed-.
 140
 141 lemma raise_inv_vdrop_be: ∀M,v1,v2,d,l,m. [l⬐d] v2 ≐⦋M⦌ ↓[l, m] v1 →
 142                           d = v1 (l+m) ∧ v2 ≐ ↓[l, m+1] v1.
 143 /3 width=2 by raise_fwd_vdrop_be_O, raise_fwd_vdrop_be_S, conj/ qed-.