helm/software/matita/contribs/dama/dama/models/list_support.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 "list/list.ma".
  16
  17 interpretation "list nth" 'nth = (nth _).
  18 interpretation "list nth" 'nth_appl l d i = (nth _ l d i).
  19 notation "\nth" with precedence 90 for @{'nth}.
  20 notation < "\nth \nbsp term 90 l \nbsp term 90 d \nbsp term 90 i"
  21 with precedence 69 for @{'nth_appl $l $d $i}.
  22
  23 definition make_list ≝
  24   λA:Type.λdef:nat→A.
  25     let rec make_list (n:nat) on n ≝
  26       match n with [ O ⇒ nil ? | S m ⇒ def m :: make_list m]
  27     in make_list.
  28
  29 interpretation "\mk_list appl" 'mk_list_appl f n = (make_list _ f n).
  30 interpretation "\mk_list" 'mk_list = (make_list _).
  31 notation "\mk_list" with precedence 90 for @{'mk_list}.
  32 notation < "\mk_list \nbsp term 90 f \nbsp term 90 n"
  33 with precedence 69 for @{'mk_list_appl $f $n}.
  34
  35 notation "\len" with precedence 90 for @{'len}.
  36 interpretation "len" 'len = (length _).
  37 notation < "\len \nbsp term 90 l" with precedence 69 for @{'len_appl $l}.
  38 interpretation "len appl" 'len_appl l = (length _ l).
  39
  40 lemma len_mk_list : ∀T:Type.∀f:nat→T.∀n.\len (\mk_list f n) = n.
  41 intros; elim n; [reflexivity] simplify; rewrite > H; reflexivity;
  42 qed.
  43
  44 record rel : Type ≝ {
  45   rel_T :> Type;
  46   rel_op :2> rel_T → rel_T → Prop
  47 }.
  48
  49 record trans_rel : Type ≝ {
  50   o_rel :> rel;
  51   o_tra : ∀x,y,z: o_rel.o_rel x y → o_rel y z → o_rel x z
  52 }.
  53
  54 lemma trans: ∀r:trans_rel.∀x,y,z:r.r x y → r y z → r x z.
  55 apply o_tra;
  56 qed.
  57
  58 inductive sorted (lt : trans_rel): list (rel_T lt) → Prop ≝
  59 | sorted_nil : sorted lt []
  60 | sorted_one : ∀x. sorted lt [x]
  61 | sorted_cons : ∀x,y,tl. lt x y → sorted lt (y::tl) → sorted lt (x::y::tl).
  62
  63 lemma nth_nil: ∀T,i.∀def:T. \nth [] def i = def.
  64 intros; elim i; simplify; [reflexivity;] assumption; qed.
  65
  66 lemma len_append: ∀T:Type.∀l1,l2:list T. \len (l1@l2) = \len l1 + \len l2.
  67 intros; elim l1; [reflexivity] simplify; rewrite < H; reflexivity;
  68 qed.
  69
  70 inductive non_empty_list (A:Type) : list A → Type :=
  71 | show_head: ∀x,l. non_empty_list A (x::l).
  72
  73 lemma len_gt_non_empty :
  74   ∀T.∀l:list T.O < \len l → non_empty_list T l.
  75 intros; cases l in H; [intros; cases (not_le_Sn_O ? H);] intros; constructor 1;
  76 qed.
  77
  78 lemma sorted_tail: ∀r,x,l.sorted r (x::l) → sorted r l.
  79 intros; inversion H; intros; [destruct H1;|destruct H1;constructor 1;]
  80 destruct H4; assumption;
  81 qed.
  82
  83 lemma sorted_skip: ∀r,x,y,l. sorted r (x::y::l) → sorted r (x::l).
  84 intros (r x y l H1); inversion H1; intros; [1,2: destruct H]
  85 destruct H4; inversion H2; intros; [destruct H4]
  86 [1: destruct H4; constructor 2;
  87 |2: destruct H7; constructor 3; [ apply (o_tra ? ??? H H4);]
  88     apply (sorted_tail ??? H2);]
  89 qed.
  90
  91 lemma sorted_tail_bigger : ∀r,x,l,d.sorted r (x::l) → ∀i. i < \len l → r x (\nth l d i).
  92 intros 4; elim l; [ cases (not_le_Sn_O i H1);]
  93 cases i in H2;
  94 [2: intros; apply (H ? n);[apply (sorted_skip ???? H1)|apply le_S_S_to_le; apply H2]
  95 |1: intros; inversion H1; intros; [1,2: destruct H3]
  96     destruct H6; simplify; assumption;]
  97 qed.
  98
  99 lemma all_bases_positive : ∀f:q_f.∀i. OQ < nth_base (bars f) (S i).
 100 intro f; generalize in match (bars_begin_OQ f); generalize in match (bars_sorted f);
 101 cases (bars_not_nil f); intros;
 102 cases (cmp_nat i (len l));
 103 [1: lapply (sorted_tail_bigger ?? H ? H2) as K; simplify in H1;
 104     rewrite > H1 in K; apply K;
 105 |2: rewrite > H2; simplify; elim l; simplify; [apply (q_pos_OQ one)]
 106     assumption;
 107 |3: simplify; elim l in i H2;[simplify; rewrite > nth_nil; apply (q_pos_OQ one)]
 108     cases n in H3; intros; [cases (not_le_Sn_O ? H3)] apply (H2 n1);
 109     apply (le_S_S_to_le ?? H3);]
 110 qed.
 111
 112 lemma lt_n_plus_n_Sm : ∀n,m:nat.n < n + S m.
 113 intros; rewrite > sym_plus; apply (le_S_S n (m+n)); apply (le_plus_n m n); qed.
 114
 115 lemma nth_concat_lt_len:
 116   ∀T:Type.∀l1,l2:list T.∀def.∀i.i < len l1 → nth (l1@l2) def i = nth l1 def i.
 117 intros 4; elim l1; [cases (not_le_Sn_O ? H)] cases i in H H1; simplify; intros;
 118 [reflexivity| rewrite < H;[reflexivity] apply le_S_S_to_le; apply H1]
 119 qed.
 120
 121 lemma nth_concat_ge_len:
 122   ∀T:Type.∀l1,l2:list T.∀def.∀i.
 123     len l1 ≤ i → nth (l1@l2) def i = nth l2 def (i - len l1).
 124 intros 4; elim l1; [ rewrite < minus_n_O; reflexivity]
 125 cases i in H1; simplify; intros; [cases (not_le_Sn_O ? H1)]
 126 apply H; apply le_S_S_to_le; apply H1;
 127 qed.
 128
 129 lemma nth_len:
 130   ∀T:Type.∀l1,l2:list T.∀def,x.
 131     nth (l1@x::l2) def (len l1) = x.
 132 intros 2; elim l1;[reflexivity] simplify; apply H; qed.
 133
 134 lemma all_bigger_can_concat_bigger:
 135    ∀l1,l2,start,b,x,n.
 136     (∀i.i< len l1 → nth_base l1 i < \fst b) →
 137     (∀i.i< len l2 → \fst b ≤ nth_base l2 i) →
 138     (∀i.i< len l1 → start ≤ i → x ≤ nth_base l1 i) →
 139     start ≤ n → n < len (l1@b::l2) → x ≤ \fst b → x ≤ nth_base (l1@b::l2) n.
 140 intros; cases (cmp_nat n (len l1));
 141 [1: unfold nth_base;  rewrite > (nth_concat_lt_len ????? H6);
 142     apply (H2 n); assumption;
 143 |2: rewrite > H6; unfold nth_base; rewrite > nth_len; assumption;
 144 |3: unfold nth_base; rewrite > nth_concat_ge_len; [2: apply lt_to_le; assumption]
 145     rewrite > len_concat in H4; simplify in H4; rewrite < plus_n_Sm in H4;
 146     lapply linear le_S_S_to_le to H4 as K; rewrite > sym_plus in K;
 147     lapply linear le_plus_to_minus to K as X;
 148     generalize in match X; generalize in match (n - len l1); intro W; cases W; clear W X;
 149     [intros; assumption] intros;
 150     apply (q_le_trans ??? H5); apply (H1 n1); assumption;]
 151 qed.
 152
 153 lemma sorted_head_smaller:
 154   ∀l,p. sorted (p::l) → ∀i.i < len l → \fst p < nth_base l i.
 155 intro l; elim l; intros; [cases (not_le_Sn_O ? H1)] cases i in H2; simplify; intros;
 156 [1: inversion H1; [1,2: simplify; intros; destruct H3] intros; destruct H6; assumption;
 157 |2: apply (H p ? n ?); [apply (sorted_skip ??? H1)] apply le_S_S_to_le; apply H2]
 158 qed.