helm/software/matita/contribs/dama/dama/models/q_copy.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_bars.ma".
  16
  17 (* move in nat/minus *)
  18 lemma minus_lt : ∀i,j. i < j → j - i = S (j - S i).
  19 intros 2;
  20 apply (nat_elim2 ???? i j); simplify; intros;
  21 [1: cases n in H; intros; rewrite < minus_n_O; [cases (not_le_Sn_O ? H);]
  22     simplify; rewrite < minus_n_O; reflexivity;
  23 |2: cases (not_le_Sn_O ? H);
  24 |3: apply H; apply le_S_S_to_le; assumption;]
  25 qed.
  26
  27 alias symbol "lt" = "bar lt".
  28 lemma inversion_sorted:
  29   ∀a,l. sorted q2_lt (a::l) → Or (a < \hd ▭ l) (l = []).
  30 intros 2; elim l; [right;reflexivity] left; inversion H1; intros;
  31 [1,2:destruct H2| destruct H5; assumption]
  32 qed.
  33
  34 lemma inversion_sorted2:
  35   ∀a,b,l. sorted q2_lt (a::b::l) → a < b.
  36 intros; inversion H; intros; [1,2:destruct H1] destruct H4; assumption;
  37 qed.
  38
  39 let rec copy (l : list bar) on l : list bar ≝
  40   match l with
  41   [ nil ⇒ []
  42   | cons x tl ⇒ 〈\fst x, 〈OQ,OQ〉〉 :: copy tl].
  43
  44 lemma sorted_copy:
  45   ∀l:list bar.sorted q2_lt l → sorted q2_lt (copy l).
  46 intro l; elim l; [apply (sorted_nil q2_lt)] simplify;
  47 cases l1 in H H1; simplify; intros; [apply (sorted_one q2_lt)]
  48 apply (sorted_cons q2_lt); [2: apply H; apply (sorted_tail q2_lt ?? H1);]
  49 apply (inversion_sorted2 ??? H1);
  50 qed.
  51
  52 lemma len_copy: ∀l. \len (copy l) = \len l.
  53 intro; elim l; [reflexivity] simplify; apply eq_f; assumption;
  54 qed.
  55
  56 lemma copy_same_bases: ∀l. same_bases l (copy l).
  57 intros; elim l; [intro; reflexivity] intro; simplify; cases i; [reflexivity]
  58 simplify; apply (H n);
  59 qed.
  60
  61 lemma copy_OQ : ∀l,n.nth_height (copy l) n = 〈OQ,OQ〉.
  62 intro; elim l; [elim n;[reflexivity] simplify; assumption]
  63 simplify; cases n; [reflexivity] simplify; apply (H n1);
  64 qed.
  65
  66 lemma prepend_sorted_with_same_head:
  67  ∀r,x,l1,l2,d1,d2.
  68    sorted r (x::l1) → sorted r l2 →
  69    (r x (\nth l1 d1 O) → r x (\nth l2 d2 O)) → (l1 = [] → r x d1) →
  70    sorted r (x::l2).
  71 intros 8 (R x l1 l2 d1 d2 Sl1 Sl2);  inversion Sl1; inversion Sl2;
  72 intros; destruct; try assumption; [3: apply (sorted_one R);]
  73 [1: apply sorted_cons;[2:assumption] apply H2; apply H3; reflexivity;
  74 |2: apply sorted_cons;[2: assumption] apply H5; apply H6; reflexivity;
  75 |3: apply sorted_cons;[2: assumption] apply H5; assumption;
  76 |4: apply sorted_cons;[2: assumption] apply H8; apply H4;]
  77 qed.
  78
  79 lemma move_head_sorted: ∀x,l1,l2.
  80   sorted q2_lt (x::l1) → sorted q2_lt l2 → nth_base l2 O = nth_base l1 O →
  81     l1 ≠ [] → sorted q2_lt (x::l2).
  82 intros; apply (prepend_sorted_with_same_head q2_lt x l1 l2 ▭ ▭);
  83 try assumption; intros; unfold nth_base in H2; whd in H4;
  84 [1: rewrite < H2 in H4; assumption;
  85 |2: cases (H3 H4);]
  86 qed.
  87
  88
  89 lemma sort_q2lt_same_base:
  90   ∀b,h1,h2,l. sorted q2_lt (〈b,h1〉::l) → sorted q2_lt (〈b,h2〉::l).
  91 intros; cases (inversion_sorted ?? H); [2: rewrite > H1; apply (sorted_one q2_lt)]
  92 lapply (sorted_tail q2_lt ?? H) as K; clear H; cases l in H1 K; simplify; intros;
  93 [apply (sorted_one q2_lt);|apply (sorted_cons q2_lt);[2: assumption] apply H]
  94 qed.
  95
  96
  97 lemma value_copy :
  98   ∀l,h1,h2,i,h3.
  99   value_simpl (copy l) h1 h2 i h3 = 〈OQ,OQ〉.
 100 intros; elim l in h1 h2 h3; [cases (not_le_Sn_O ? H1);]
 101 cases l1 in H H1 H2 H3;
 102 [1: intros; simplify in ⊢ (? ? (? % ? ? ? ?) ?);
 103     rewrite > (value_unit 〈\fst a,〈OQ,OQ〉〉); reflexivity;
 104 |2: intros; simplify in H2 H3 H4 ⊢ (? ? (? % ? ? ? ?) ?);
 105     cases (q_cmp (Qpos i)  (\fst b));
 106     [2: rewrite > (value_tail ??? H2 H3 ? H4 H1); apply H;
 107     |1: rewrite > (value_head ??? H2 H3 ? H4 H1); reflexivity]]
 108 qed.
 109