helm/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 set "baseuri" "cic:/matita/list/sort/".
  16
  17 include "datatypes/bool.ma".
  18 include "datatypes/constructors.ma".
  19 include "list/list.ma".
  20
  21 let rec mem (A:Set) (eq: A → A → bool) x (l: list A) on l ≝
  22  match l with
  23   [ nil ⇒ false
  24   | (cons a l') ⇒
  25     match eq x a with
  26      [ true ⇒ true
  27      | false ⇒ mem A eq x l'
  28      ]
  29   ].
  30
  31 let rec ordered (A:Set) (le: A → A → bool) (l: list A) on l ≝
  32  match l with
  33   [ nil ⇒ true
  34   | (cons x l') ⇒
  35      match l' with
  36       [ nil ⇒ true
  37       | (cons y l'') ⇒
  38           le x y \land ordered A le l'
  39       ]
  40   ].
  41
  42 let rec insert (A:Set) (le: A → A → bool) x (l: list A) on l ≝
  43  match l with
  44   [ nil ⇒ [x]
  45   | (cons he l') ⇒
  46       match le x he with
  47        [ true ⇒ x::l
  48        | false ⇒ he::(insert A le x l')
  49        ]
  50   ].
  51
  52 lemma insert_ind :
  53  ∀A:Set. ∀le: A → A → bool. ∀x.
  54   ∀P:(list A → list A → Prop).
  55    ∀H:(∀l: list A. l=[] → P [] [x]).
  56     ∀H2:
  57     (∀l: list A. ∀he. ∀l'. P l' (insert ? le x l') →
  58       le x he = false → l=he::l' → P (he::l') (he::(insert ? le x l'))).
  59      ∀H3:
  60      (∀l: list A. ∀he. ∀l'. P l' (insert ? le x l') →
  61        le x he = true → l=he::l' → P (he::l') (x::he::l')).
  62     ∀l:list A. P l (insert ? le x l).
  63   intros.
  64   apply (
  65     let rec insert_ind (l: list A) \def
  66     match l in list
  67     return
  68       λli.
  69        l = li → P li (insert ? le x li)
  70     with
  71      [ nil ⇒ H l
  72      | (cons he l') ⇒
  73          match le x he
  74          return
  75           λb. le x he = b → l = he::l' →
  76            P (he::l')
  77             (match b with
  78               [ true ⇒ x::he::l'
  79               | false ⇒ he::(insert ? le x l') ])
  80          with
  81           [ true ⇒ H2 l he l' (insert_ind l')
  82           | false ⇒ H1 l he l' (insert_ind l')
  83           ]
  84          (refl_eq ? (le x he))
  85      ] (refl_eq ? l) in insert_ind l).
  86 qed.
  87
  88
  89 let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝
  90  match l with
  91   [ nil ⇒ []
  92   | (cons he l') ⇒
  93       let l'' ≝ insertionsort A le l' in
  94        insert A le he l''
  95   ].
  96
  97 lemma ordered_injective:
  98   ∀ A:Set. ∀ le:A → A → bool.
  99   ∀ l:list A.
 100   ordered A le l = true
 101   \to ordered A le (tail A l) = true.
 102   intros 3 (A le l).
 103   elim l
 104   [ simplify; reflexivity;
 105   | simplify;
 106     generalize in match H1;
 107     clear H1;
 108     elim l1;
 109     [ simplify; reflexivity;
 110     | cut ((le s s1 \land ordered A le (s1::l2)) = true);
 111       [ generalize in match Hcut;
 112         apply andb_elim;
 113         elim (le s s1);
 114         [ simplify;
 115           fold simplify (ordered ? le (s1::l2));
 116           intros; assumption;
 117         | simplify;
 118           intros (Habsurd);
 119           apply False_ind;
 120           apply (not_eq_true_false);
 121           symmetry;
 122           assumption
 123         ]
 124       | exact H2;
 125       ]
 126     ]
 127   ].
 128 qed.
 129
 130 lemma insert_sorted:
 131   \forall A:Set. \forall le:A\to A\to bool.
 132   (\forall a,b:A. le a b = false \to le b a = true) \to
 133   \forall l:list A. \forall x:A.
 134     ordered A le l = true \to ordered A le (insert A le x l) = true.
 135  intros 5 (A le H l x).
 136  apply (insert_ind ? ? ? (λl,il. ordered ? le l = true → ordered ? le il = true));
 137  intros; simplify; intros;
 138   [2: rewrite > H1;
 139     [ generalize in match (H ? ? H2); clear H2; intro;
 140       generalize in match H4; clear H4;
 141       elim l'; simplify;
 142       [ rewrite > H5;
 143         reflexivity
 144       | elim (le x s); simplify;
 145         [ rewrite > H5;
 146           reflexivity
 147         | simplify in H4;
 148           rewrite > (andb_true_true ? ? H4);
 149           reflexivity
 150         ]
 151       ]
 152     | apply (ordered_injective ? ? ? H4)
 153     ]
 154   | reflexivity
 155   | rewrite > H2;
 156     rewrite > H4;
 157     reflexivity
 158   ].
 159 qed.
 160
 161 theorem insertionsort_sorted:
 162   ∀A:Set.
 163   ∀le:A → A → bool.∀eq:A → A → bool.
 164   (∀a,b:A. le a b = false → le b a = true) \to
 165   ∀l:list A.
 166   ordered A le (insertionsort A le l) = true.
 167   intros 5 (A le eq le_tot l).
 168   elim l;
 169   [ simplify;
 170     reflexivity;
 171   | apply (insert_sorted A le le_tot (insertionsort A le l1) s);
 172     assumption;
 173   ]
 174 qed.