matita/library/list/sort.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 "datatypes/bool.ma".
  16 include "datatypes/constructors.ma".
  17 include "list/in.ma".
  18
  19 inductive sorted (A:Type) (P:A \to A \to Prop): list A \to Prop \def
  20 | sort_nil : sorted A P []
  21 | sort_cons : \forall x,l.sorted A P l \to (\forall y.in_list ? y l \to P x y)
  22               \to sorted A P (x::l).
  23
  24 lemma sorted_cons_to_sorted : \forall A,P,x,l.sorted A P (x::l) \to sorted A P l.
  25 intros;inversion H;intros
  26   [destruct H1
  27   |destruct H4;assumption]
  28 qed.
  29
  30 lemma sorted_to_minimum : \forall A,P,x,l.sorted A P (x::l) \to
  31                           \forall y.in_list ? y l \to P x y.
  32 intros;inversion H;intros;
  33   [destruct H2
  34   |destruct H5;apply H4;assumption]
  35 qed.
  36
  37
  38 let rec ordered (A:Type) (le: A → A → bool) (l: list A) on l ≝
  39  match l with
  40   [ nil ⇒ true
  41   | (cons x l') ⇒
  42      match l' with
  43       [ nil ⇒ true
  44       | (cons y l'') ⇒
  45           le x y \land ordered A le l'
  46       ]
  47   ].
  48
  49 lemma sorted_to_eq_sorted_b_true :
  50       \forall A,ord,ordb.
  51       (\forall x,y.ord x y \to ordb x y = true) \to
  52       \forall l.sorted A ord l \to ordered A ordb l = true.
  53 intros 5;elim l
  54   [reflexivity
  55   |simplify;rewrite > H1;generalize in match H2;cases l1;intros
  56      [reflexivity
  57      |simplify;rewrite > H
  58         [reflexivity
  59         |apply (sorted_to_minimum ? ? ? ? H3);apply in_list_head]
  60      |apply sort_nil
  61      |apply (sorted_cons_to_sorted ? ? ? ? H3)]]
  62 qed.
  63
  64 (*
  65    TODO
  66    per far funzionare questa dimostrazione bisogna appoggiarsi a un
  67    eqb (e utilizzare quindi in_list <-> mem), oppure modificare la definizione
  68    di sorted in modo che non si appoggi più a in_list:
  69    sorted []
  70    sorted [x] per ogni x
  71    sorted x::y::l se ord x y e sorted y::l
  72
  73 lemma eq_sorted_b_true_to_sorted :
  74       \forall A,ord,ordb.
  75       (\forall x,y.ordb x y = true \to ord x y) \to
  76       \forall l.ordered A ordb l = true \to sorted A ord l.
  77 intros 5;elim l
  78   [apply sort_nil
  79   |apply sort_cons
  80      [apply H1;simplify in H2;generalize in match H2;cases l1;intros
  81         [reflexivity
  82         |simplify in H3;simplify;apply (andb_true_true_r ? ? H3)]
  83      |intros;apply H;generalize in match H2;
  84       generalize in match (in_list_to_mem_true ? ? ? ? H
  85         [
  86 *)
  87
  88 let rec insert (A:Type) (le: A → A → bool) x (l: list A) on l ≝
  89  match l with
  90   [ nil ⇒ [x]
  91   | (cons he l') ⇒
  92       match le x he with
  93        [ true ⇒ x::l
  94        | false ⇒ he::(insert A le x l')
  95        ]
  96   ].
  97
  98 lemma insert_ind :
  99  ∀A:Type. ∀le: A → A → bool. ∀x.
 100   ∀P:(list A → list A → Prop).
 101    ∀H:(∀l: list A. l=[] → P [] [x]).
 102     ∀H2:
 103     (∀l: list A. ∀he. ∀l'. P l' (insert ? le x l') →
 104       le x he = false → l=he::l' → P (he::l') (he::(insert ? le x l'))).
 105      ∀H3:
 106      (∀l: list A. ∀he. ∀l'. P l' (insert ? le x l') →
 107        le x he = true → l=he::l' → P (he::l') (x::he::l')).
 108     ∀l:list A. P l (insert ? le x l).
 109   intros.
 110   apply (
 111     let rec insert_ind (l: list A) \def
 112     match l in list
 113     return
 114       λli.
 115        l = li → P li (insert ? le x li)
 116     with
 117      [ nil ⇒ H l
 118      | (cons he l') ⇒
 119          match le x he
 120          return
 121           λb. le x he = b → l = he::l' →
 122            P (he::l')
 123             (match b with
 124               [ true ⇒ x::he::l'
 125               | false ⇒ he::(insert ? le x l') ])
 126          with
 127           [ true ⇒ H2 l he l' (insert_ind l')
 128           | false ⇒ H1 l he l' (insert_ind l')
 129           ]
 130          (refl_eq ? (le x he))
 131      ] (refl_eq ? l) in insert_ind l).
 132 qed.
 133
 134
 135 let rec insertionsort (A:Type) (le: A → A → bool) (l: list A) on l ≝
 136  match l with
 137   [ nil ⇒ []
 138   | (cons he l') ⇒
 139       let l'' ≝ insertionsort A le l' in
 140        insert A le he l''
 141   ].
 142
 143 lemma ordered_injective:
 144   ∀A:Type. ∀le:A → A → bool.
 145    ∀l:list A. ordered A le l = true → ordered A le (tail A l) = true.
 146   intros 3 (A le l).
 147   elim l
 148   [ simplify; reflexivity;
 149   | simplify;
 150     generalize in match H1;
 151     clear H1;
 152     elim l1;
 153     [ simplify; reflexivity;
 154     | cut ((le t t1 \land ordered A le (t1::l2)) = true);
 155       [ generalize in match Hcut;
 156         apply andb_elim;
 157         elim (le t t1);
 158         [ simplify;
 159           fold simplify (ordered ? le (t1::l2));
 160           intros; assumption;
 161         | simplify;
 162           intros (Habsurd);
 163           apply False_ind;
 164           apply (not_eq_true_false);
 165           symmetry;
 166           assumption
 167         ]
 168       | exact H2;
 169       ]
 170     ]
 171   ].
 172 qed.
 173
 174 lemma insert_sorted:
 175   \forall A:Type. \forall le:A\to A\to bool.
 176   (\forall a,b:A. le a b = false \to le b a = true) \to
 177   \forall l:list A. \forall x:A.
 178     ordered A le l = true \to ordered A le (insert A le x l) = true.
 179  intros 5 (A le H l x).
 180  apply (insert_ind ? ? ? (λl,il. ordered ? le l = true → ordered ? le il = true));
 181  clear l; intros; simplify; intros;
 182   [2: rewrite > H1;
 183     [ generalize in match (H ? ? H2); clear H2; intro;
 184       generalize in match H4; clear H4;
 185       elim l'; simplify;
 186       [ rewrite > H5;
 187         reflexivity
 188       | elim (le x t); simplify;
 189         [ rewrite > H5;
 190           reflexivity
 191         | simplify in H4;
 192           rewrite > (andb_true_true ? ? H4);
 193           reflexivity
 194         ]
 195       ]
 196     | apply (ordered_injective ? ? ? H4)
 197     ]
 198   | reflexivity
 199   | rewrite > H2;
 200     rewrite > H4;
 201     reflexivity
 202   ].
 203 qed.
 204
 205 theorem insertionsort_sorted:
 206   ∀A:Type.
 207   ∀le:A → A → bool.∀eq:A → A → bool.
 208   (∀a,b:A. le a b = false → le b a = true) \to
 209   ∀l:list A.
 210   ordered A le (insertionsort A le l) = true.
 211   intros 5 (A le eq le_tot l).
 212   elim l;
 213   [ simplify;
 214     reflexivity;
 215   | apply (insert_sorted ? ? le_tot (insertionsort ? le l1) t);
 216     assumption;
 217   ]
 218 qed.