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. ordered A le l = true → ordered A le (tail A l) = true.
 100   intros 3 (A le l).
 101   elim l
 102   [ simplify; reflexivity;
 103   | simplify;
 104     generalize in match H1;
 105     clear H1;
 106     elim l1;
 107     [ simplify; reflexivity;
 108     | cut ((le s s1 \land ordered A le (s1::l2)) = true);
 109       [ generalize in match Hcut;
 110         apply andb_elim;
 111         elim (le s s1);
 112         [ simplify;
 113           fold simplify (ordered ? le (s1::l2));
 114           intros; assumption;
 115         | simplify;
 116           intros (Habsurd);
 117           apply False_ind;
 118           apply (not_eq_true_false);
 119           symmetry;
 120           assumption
 121         ]
 122       | exact H2;
 123       ]
 124     ]
 125   ].
 126 qed.
 127
 128 lemma insert_sorted:
 129   \forall A:Set. \forall le:A\to A\to bool.
 130   (\forall a,b:A. le a b = false \to le b a = true) \to
 131   \forall l:list A. \forall x:A.
 132     ordered A le l = true \to ordered A le (insert A le x l) = true.
 133  intros 5 (A le H l x).
 134  apply (insert_ind ? ? ? (λl,il. ordered ? le l = true → ordered ? le il = true));
 135  clear l; intros; simplify; intros;
 136   [2: rewrite > H1;
 137     [ generalize in match (H ? ? H2); clear H2; intro;
 138       generalize in match H4; clear H4;
 139       elim l'; simplify;
 140       [ rewrite > H5;
 141         reflexivity
 142       | elim (le x s); simplify;
 143         [ rewrite > H5;
 144           reflexivity
 145         | simplify in H4;
 146           rewrite > (andb_true_true ? ? H4);
 147           reflexivity
 148         ]
 149       ]
 150     | apply (ordered_injective ? ? ? H4)
 151     ]
 152   | reflexivity
 153   | rewrite > H2;
 154     rewrite > H4;
 155     reflexivity
 156   ].
 157 qed.
 158
 159 theorem insertionsort_sorted:
 160   ∀A:Set.
 161   ∀le:A → A → bool.∀eq:A → A → bool.
 162   (∀a,b:A. le a b = false → le b a = true) \to
 163   ∀l:list A.
 164   ordered A le (insertionsort A le l) = true.
 165   intros 5 (A le eq le_tot l).
 166   elim l;
 167   [ simplify;
 168     reflexivity;
 169   | apply (insert_sorted ? ? le_tot (insertionsort ? le l1) s);
 170     assumption;
 171   ]
 172 qed.