helm/software/matita/contribs/dama/dama/models/q_value_skip.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 "models/q_shift.ma".
  16
  17 lemma q_cmp2:
  18   ∀a,b:ℚ.a < b ∨ b ≤ a.
  19 intros; cases (q_cmp a b);
  20 [1: right; apply q_eq_to_le; symmetry; assumption;
  21 |2: left; assumption;
  22 |3: right; apply q_lt_to_le; assumption;]
  23 qed.
  24
  25
  26
  27 lemma value_skip:
  28  ∀f,i,b,tl. bars f = b::tl → start f + Qpos (\fst b) < i →
  29   \fst (value f i) = \fst (value (mk_q_f (start f + Qpos (\fst b)) tl) i).
  30 intros; cases (value f i); cases H2; clear H2;
  31 [1: cases (?:False); apply (q_lt_corefl (start f)); cases H3; clear H3 H4 H5;
  32     apply (q_lt_trans ???? H2);
  33 |2:
  34 simplify in ⊢ (? ? % ?);