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 let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝
  53  match l with
  54   [ nil ⇒ []
  55   | (cons he l') ⇒
  56       let l'' ≝ insertionsort A le l' in
  57        insert A le he l''
  58   ].
  59
  60 lemma ordered_injective:
  61   ∀ A:Set. ∀ le:A → A → bool.
  62   ∀ l:list A.
  63   ordered A le l = true
  64   \to ordered A le (tail A l) = true.
  65   intros 3 (A le l).
  66   elim l
  67   [ simplify; reflexivity;
  68   | simplify;
  69     generalize in match H1;
  70     clear H1;
  71     elim l1;
  72     [ simplify; reflexivity;
  73     | cut ((le s s1 \land ordered A le (s1::l2)) = true);
  74       [ generalize in match Hcut;
  75         apply andb_elim;
  76         elim (le s s1);
  77         [ change with (ordered A le (s1::l2) = true \to ordered A le (s1::l2) = true).
  78           intros; assumption;
  79         | simplify;
  80           intros (Habsurd);
  81           apply False_ind;
  82           apply (not_eq_true_false);
  83           symmetry;
  84           assumption
  85         ]
  86       | exact H2;
  87       ]
  88     ]
  89   ].
  90 qed.
  91
  92 lemma insert_sorted:
  93   \forall A:Set. \forall le:A\to A\to bool.
  94   (\forall a,b:A. le a b = false \to le b a = true) \to
  95   \forall l:list A. \forall x:A.
  96     ordered A le l = true \to ordered A le (insert A le x l) = true.
  97   intros 5 (A le H l x).
  98   elim l;
  99   [ 2: change with (ordered A le (match le x s with
 100          [ true ⇒ x::(s::l1) | false ⇒ s::(insert A le x l1) ]) = true).
 101        apply (bool_elim ? (le x s));
 102        [ intros;
 103          change with ((le x s \land ordered A le (s::l1)) = true);
 104          apply andb_elim;
 105          rewrite > H3;
 106          assumption;
 107        | generalize in match H2;
 108          clear H1; clear H2;
 109          generalize in match s;
 110          clear s;
 111          elim l1
 112          [ simplify;
 113            rewrite > (H x a H2);
 114            reflexivity;
 115          | change with ((ordered A le (a::match le x s with
 116               [ true ⇒ x::s::l2 | false ⇒ s::(insert A le x l2) ])) = true).
 117             apply (bool_elim ? (le x s));
 118             [ intros;
 119               change with ((le a x \land (le x s \land ordered A le (s::l2))) = true).
 120               apply andb_elim;
 121               rewrite > (H x a H3);
 122               change with ((le x s \land ordered A le (s::l2)) = true).
 123               apply andb_elim;
 124               rewrite > H4;
 125               apply (ordered_injective A le (a::s::l2));
 126               assumption;
 127             | intros;
 128               change with ((le a s \land ordered A le (s::(insert A le x l2))) = true);
 129               apply andb_elim;
 130               change in H2 with ((le a s \land ordered A le (s::l2)) = true);
 131               generalize in match H2;
 132               apply (andb_elim (le a s));
 133               elim (le a s);
 134               [ change with (ordered A le (s::l2) = true \to ordered A le (s::insert A le x l2) = true);
 135                 intros;
 136                 apply (H1 s);
 137                 assumption;
 138               | simplify; intros; assumption
 139               ]
 140            ]
 141          ]
 142       ]
 143    | simplify; reflexivity;
 144    ]
 145 qed.
 146
 147 theorem insertionsort_sorted:
 148   ∀A:Set.
 149   ∀le:A → A → bool.∀eq:A → A → bool.
 150   (∀a,b:A. le a b = false → le b a = true) \to
 151   ∀l:list A.
 152   ordered A le (insertionsort A le l) = true.
 153   intros 5 (A le eq le_tot l).
 154   elim l;
 155   [ simplify;
 156     reflexivity;
 157   | apply (insert_sorted A le le_tot (insertionsort A le l1) s);
 158     assumption;
 159   ]
 160 qed.
 161
 162 (*
 163 theorem insertionsort_correct:
 164   ∀A:Set.
 165   ∀le:A → A → bool.∀eq:A → A → bool.
 166   (∀a,b:A. le a b = false → le b a = true) \to
 167   ∀l,l':list A.
 168   l' = insertionsort A le l
 169   \to ordered A le l' = true
 170     ∧ ((\forall x:A. mem A eq x l = true \to mem A eq x l' = true)
 171         ∧ (\forall x:A. mem A eq x l = true \to mem A eq x l' = true)).
 172   intros;
 173   split;
 174   [ rewrite > H1;
 175     apply (insertionsort_sorted A le eq H);
 176   | split;
 177     [ TO BE CONTINUED ...
 178 *)