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 definition copy ≝
  28  λl:list bar.make_list ? (λn.〈nth_base l (\len l - S n),〈OQ,OQ〉〉) (\len l).
  29
  30 lemma sorted_copy:
  31   ∀l:list bar.sorted q2_lt l → sorted q2_lt (copy l).
  32 intros 2; unfold copy; generalize in match (le_n (\len l));
  33 elim (\len l) in ⊢ (?%?→? ? (? ? ? %));
  34 simplify; [apply (sorted_nil q2_lt);] cases n in H1 H2;
  35 simplify; intros; [apply (sorted_one q2_lt);]
  36 apply (sorted_cons q2_lt);
  37 [2: apply H1; apply lt_to_le; apply H2;
  38 |1: elim l in H2 H; simplify; [simplify in H2; cases (not_le_Sn_O ? H2)]
  39     simplify in H3; unfold nth_base;
  40     unfold canonical_q_lt; unfold q2_trel; unfold q2_lt; simplify;
  41     change with (q2_lt (\nth (a::l1) ▭ (\len l1-S n1)) (\nth (a::l1) ▭ (\len l1-n1)));
  42     cut (∃w.w = \len l1 - S n1); [2: exists[apply (\len l1 - S n1)] reflexivity]
  43     cases Hcut; rewrite < H4; rewrite < (?:S w = \len l1 - n1);
  44     [1: apply (sorted_near q2_lt (a::l1) H2); rewrite > H4;
  45         simplify; apply le_S_S; elim (\len l1) in H3; simplify;
  46         [ cases (not_le_Sn_O ? (le_S_S_to_le ?? H3));
  47         | lapply le_S_S_to_le to H5 as H6;
  48           lapply le_S_S_to_le to H6 as H7; clear H5 H6;
  49           cases H7 in H3; intros; [rewrite < minus_n_n; apply le_S_S; apply le_O_n]
  50           simplify in H5; apply le_S_S; apply (trans_le ???? (H5 ?));
  51           [2: apply le_S_S; apply le_S_S; assumption;
  52           |1: apply (lt_minus_S_n_to_le_minus_n n1 (S m) (S (minus m n1)) ?).
  53               apply (not_le_to_lt (S (minus m n1)) (minus (S m) (S n1)) ?).
  54               apply (not_le_Sn_n (minus (S m) (S n1))).]]
  55     |2: rewrite > H4; lapply le_S_S_to_le to H3 as K;
  56         clear H4 Hcut H3 H H1 H2; generalize in match K; clear K;
  57         apply (nat_elim2 ???? n1 (\len l1)); simplify; intros;
  58         [1: rewrite < minus_n_O; cases n2 in H; [intro; cases (not_le_Sn_O ? H)]
  59             intros; cases n3; simplify; reflexivity;
  60         |2: cases (not_le_Sn_O ? H);
  61         |3: apply H; apply le_S_S_to_le; apply H1;]]]
  62 qed.
  63
  64 lemma len_copy: ∀l. \len (copy l) = \len l.
  65 intro; unfold copy; apply len_mk_list;
  66 qed.
  67
  68 lemma copy_same_bases: ∀l. same_bases l (copy l).
  69 intro; unfold copy; elim l using list_elim_with_len; [1: intro;reflexivity]
  70 simplify; rewrite < minus_n_n;
  71 simplify in ⊢ (? ? (? ? (? ? ? % ?) ?));
  72 apply same_bases_cons; [2: reflexivity]
  73 cases l1 in H; [intros 2; reflexivity]
  74 simplify in ⊢ (? ? (? ? (λ_:?.? ? ? (? ? %) ?) ?)→?);
  75 simplify in ⊢ (?→? ? (? ? (λ_:?.? ? ? (? ? (? % ?)) ?) ?));
  76 intro; rewrite > (mk_list_ext ?? (λn:nat.〈nth_base (b::l2) (\len l2-n),〈OQ,OQ〉〉));[assumption]
  77 intro; elim x; [simplify; rewrite < minus_n_O; reflexivity]
  78 simplify in ⊢ (? ? (? ? ? (? ? %) ?) ?);
  79 simplify in H2:(? ? %); rewrite > minus_lt; [reflexivity] apply le_S_S_to_le;
  80 assumption;
  81 qed.
  82
  83 lemma rewrite_ext_nth_height : ∀n,m,f,f1,g,g1. (∀t.g t = g1 t) →
  84 nth_height (\mk_list (λn.〈f n,g n〉) m) n = nth_height (\mk_list (λn.〈f1 n,g1 n〉) m) n.
  85 intros; generalize in match n; clear n; elim m; [reflexivity] simplify;
  86 cases n1; [simplify;apply H;] simplify; apply (H1 n2);
  87 qed.
  88
  89 lemma copy_OQ : ∀l,n.nth_height (copy l) n = 〈OQ,OQ〉.
  90 intro; elim l; [cases n; [reflexivity] simplify; rewrite > nth_nil; reflexivity]
  91 cases n; simplify [reflexivity]
  92 change with (nth_height (\mk_list (λn:ℕ.〈nth_base (a::l1) (\len l1-n),〈OQ,OQ〉〉) (\len l1)) n1 = 〈OQ,OQ〉);
  93 rewrite > (rewrite_ext_nth_height ??? (λ_.OQ) ? (λ_.〈OQ,OQ〉)); [2: intros; reflexivity]
  94 generalize in match n1;
  95 elim (\len l1); simplify; unfold nth_height; [rewrite > nth_nil; reflexivity]
  96 cases n3; simplify; [reflexivity] apply (H1 n4);
  97 qed.
  98
  99 lemma prepend_sorted_with_same_head:
 100  ∀r,x,l1,l2,d1,d2.
 101    sorted r (x::l1) → sorted r l2 →
 102    (r x (\nth l1 d1 O) → r x (\nth l2 d2 O)) → (l1 = [] → r x d1) →
 103    sorted r (x::l2).
 104 intros 8 (R x l1 l2 d1 d2 Sl1 Sl2);  inversion Sl1; inversion Sl2;
 105 intros; destruct; try assumption; [3: apply (sorted_one R);]
 106 [1: apply sorted_cons;[2:assumption] apply H2; apply H3; reflexivity;
 107 |2: apply sorted_cons;[2: assumption] apply H5; apply H6; reflexivity;
 108 |3: apply sorted_cons;[2: assumption] apply H5; assumption;
 109 |4: apply sorted_cons;[2: assumption] apply H8; apply H4;]
 110 qed.
 111
 112 lemma move_head_sorted: ∀x,l1,l2.
 113   sorted q2_lt (x::l1) → sorted q2_lt l2 → nth_base l2 O = nth_base l1 O →
 114     l1 ≠ [] → sorted q2_lt (x::l2).
 115 intros; apply (prepend_sorted_with_same_head q2_lt x l1 l2 ▭ ▭);
 116 try assumption; intros; unfold nth_base in H2; whd in H4;
 117 [1: rewrite < H2 in H4; assumption;
 118 |2: cases (H3 H4);]
 119 qed.
 120
 121 alias symbol "lt" = "bar lt".
 122 lemma inversion_sorted:
 123   ∀a,l. sorted q2_lt (a::l) → Or (a < \hd ▭ l) (l = []).
 124 intros 2; elim l; [right;reflexivity] left; inversion H1; intros;
 125 [1,2:destruct H2| destruct H5; assumption]
 126 qed.
 127
 128 lemma inversion_sorted2:
 129   ∀a,b,l. sorted q2_lt (a::b::l) → a < b.
 130 intros; inversion H; intros; [1,2:destruct H1] destruct H4; assumption;
 131 qed.
 132
 133 lemma sort_q2lt_same_base:
 134   ∀b,h1,h2,l. sorted q2_lt (〈b,h1〉::l) → sorted q2_lt (〈b,h2〉::l).
 135 intros; cases (inversion_sorted ?? H); [2: rewrite > H1; apply (sorted_one q2_lt)]
 136 lapply (sorted_tail q2_lt ?? H) as K; clear H; cases l in H1 K; simplify; intros;
 137 [apply (sorted_one q2_lt);|apply (sorted_cons q2_lt);[2: assumption] apply H]
 138 qed.
 139