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 theorem insert_ind:
  53  ∀A:Set. ∀le: A → A → bool. ∀x:A.
  54   ∀P: list A → Prop.
  55    ∀l:list A. P (insert A le x l).
  56  intros (A le x P H l).
  57  apply (
  58  let rec insert_ind (l: list A) ≝
  59   match l in list return λl.P (insert A le x l) with
  60    [ nil ⇒ (? : P [x])
  61    | (cons he l') ⇒
  62        match le x he return λb.P (match b with [ true ⇒ x::he::l' | false ⇒ he::(insert A le x l') ]) with
  63         [ true ⇒ (H2 : P (x::he::l'))
  64         | false ⇒ (? : P (he::(insert A le x l')))
  65         ]
  66    ]
  67  in
  68   insert_ind l).
  69 qed.
  70 *)
  71
  72 let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝
  73  match l with
  74   [ nil ⇒ []
  75   | (cons he l') ⇒
  76       let l'' ≝ insertionsort A le l' in
  77        insert A le he l''
  78   ].
  79
  80 lemma ordered_injective:
  81   ∀ A:Set. ∀ le:A → A → bool.
  82   ∀ l:list A.
  83   ordered A le l = true
  84   \to ordered A le (tail A l) = true.
  85   intros 3 (A le l).
  86   elim l
  87   [ simplify; reflexivity;
  88   | simplify;
  89     generalize in match H1;
  90     clear H1;
  91     elim l1;
  92     [ simplify; reflexivity;
  93     | cut ((le s s1 \land ordered A le (s1::l2)) = true);
  94       [ generalize in match Hcut;
  95         apply andb_elim;
  96         elim (le s s1);
  97         [ simplify;
  98           fold simplify (ordered ? le (s1::l2));
  99           intros; assumption;
 100         | simplify;
 101           intros (Habsurd);
 102           apply False_ind;
 103           apply (not_eq_true_false);
 104           symmetry;
 105           assumption
 106         ]
 107       | exact H2;
 108       ]
 109     ]
 110   ].
 111 qed.
 112
 113 (*
 114 lemma insert_sorted:
 115   \forall A:Set. \forall le:A\to A\to bool.
 116   (\forall a,b:A. le a b = false \to le b a = true) \to
 117   \forall l:list A. \forall x:A.
 118     ordered A le l = true \to ordered A le (insert A le x l) = true.
 119  intros (A le H l x K).
 120  letin P ≝ (\lambda ll. ordered A le ll = true).
 121  fold simplify (P (insert A le x l)).
 122  apply (
 123   let rec insert_ind (l: list A) \def
 124   match l in list return λli. l = li → P (insert A le x li) with
 125    [ nil ⇒ (? : l = [] → P [x])
 126    | (cons he l') ⇒
 127        match le x he
 128        return
 129         λb. le x he = b → l = he::l' → P (match b with
 130              [ true ⇒ x::he::l'
 131              | false ⇒ he::(insert A le x l') ])
 132        with
 133         [ true ⇒ (? : le x he = true → l = he::l' → P (x::he::l'))
 134         | false ⇒
 135             (? : \forall lrec. P (insert A le x lrec) \to
 136                   le x he = false → l = he::l' → P (he::(insert A le x l')))
 137             l' (insert_ind l')
 138         ]
 139        (refl_eq ? (le x he))
 140    ] (refl_eq ? l) in insert_ind l);
 141
 142   intros; simplify;
 143   [ rewrite > H1;
 144     apply andb_elim; simplify;
 145     generalize in match K; clear K;
 146     rewrite > H2; intro;
 147     apply H3
 148   |
 149   | reflexivity
 150   ].
 151
 152
 153
 154
 155
 156
 157   [ rewrite > H1; simplify;
 158     generalize in match (ordered_injective A le l K);
 159     rewrite > H2; simplify; intro; change with (ordered A le l' = true).
 160     elim l'; simplify;
 161      [ reflexivity
 162      |
 163
 164
 165   rewrite > H1; simplify.
 166     elim l'; [ reflexivity | simplify;
 167   | simplify.
 168   | reflexivity.
 169   ].
 170 *)
 171
 172 lemma insert_sorted:
 173   \forall A:Set. \forall le:A\to A\to bool.
 174   (\forall a,b:A. le a b = false \to le b a = true) \to
 175   \forall l:list A. \forall x:A.
 176     ordered A le l = true \to ordered A le (insert A le x l) = true.
 177   intros 5 (A le H l x).
 178   elim l;
 179   [ 2: simplify;
 180        apply (bool_elim ? (le x s));
 181        [ intros;
 182          simplify;
 183          fold simplify (ordered ? le (s::l1));
 184          apply andb_elim;
 185          rewrite > H3;
 186          assumption;
 187        | change with (le x s = false → ordered ? le (s::insert A le x l1) = true);
 188          generalize in match H2;
 189          clear H1; clear H2;
 190          generalize in match s;
 191          clear s;
 192          elim l1
 193          [ simplify;
 194            rewrite > (H x a H2);
 195            reflexivity;
 196          | simplify in \vdash (? ? (? ? ? %) ?);
 197             change with (ordered A le (a::(insert A le x (s::l2))) = true);
 198             simplify;
 199             apply (bool_elim ? (le x s));
 200             [ intros;
 201               simplify;
 202               fold simplify (ordered A le (s::l2));
 203               apply andb_elim;
 204               rewrite > (H x a H3);
 205               simplify;
 206               fold simplify (ordered A le (s::l2));
 207               apply andb_elim;
 208               rewrite > H4;
 209               apply (ordered_injective A le (a::s::l2));
 210               assumption;
 211             | intros;
 212               simplify;
 213               fold simplify (ordered A le (s::(insert A le x l2)));
 214               apply andb_elim;
 215               simplify in H2;
 216               fold simplify (ordered A le (s::l2)) in H2;
 217               generalize in match H2;
 218               apply (andb_elim (le a s));
 219               elim (le a s);
 220               [ change with (ordered A le (s::l2) = true \to ordered A le (s::insert A le x l2) = true);
 221                 intros;
 222                 apply (H1 s);
 223                 assumption;
 224               | simplify; intros; assumption
 225               ]
 226            ]
 227          ]
 228       ]
 229    | simplify; reflexivity;
 230    ]
 231 qed.
 232
 233 theorem insertionsort_sorted:
 234   ∀A:Set.
 235   ∀le:A → A → bool.∀eq:A → A → bool.
 236   (∀a,b:A. le a b = false → le b a = true) \to
 237   ∀l:list A.
 238   ordered A le (insertionsort A le l) = true.
 239   intros 5 (A le eq le_tot l).
 240   elim l;
 241   [ simplify;
 242     reflexivity;
 243   | apply (insert_sorted A le le_tot (insertionsort A le l1) s);
 244     assumption;
 245   ]
 246 qed.