X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Flist%2Fsort.ma;fp=helm%2Fmatita%2Flibrary%2Flist%2Fsort.ma;h=939cecedec6486a27274a4ce6ac834888f7c58ce;hb=792b5d29ebae8f917043d9dd226692919b5d6ca1;hp=0000000000000000000000000000000000000000;hpb=a14a8c7637fd0b95e9d4deccb20c6abc98e8f953;p=helm.git

diff --git a/helm/matita/library/list/sort.ma b/helm/matita/library/list/sort.ma
new file mode 100644
index 000000000..939cecede
--- /dev/null
+++ b/helm/matita/library/list/sort.ma
@@ -0,0 +1,172 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/list/sort/".
+
+include "datatypes/bool.ma".
+include "datatypes/constructors.ma".
+include "list/list.ma".
+
+let rec mem (A:Set) (eq: A → A → bool) x (l: list A) on l ≝
+ match l with
+  [ nil ⇒ false
+  | (cons a l') ⇒
+    match eq x a with
+     [ true ⇒ true
+     | false ⇒ mem A eq x l'
+     ]
+  ].
+  
+let rec ordered (A:Set) (le: A → A → bool) (l: list A) on l ≝
+ match l with
+  [ nil ⇒ true
+  | (cons x l') ⇒
+     match l' with
+      [ nil ⇒ true
+      | (cons y l'') ⇒
+          le x y \land ordered A le l'
+      ]
+  ].
+  
+let rec insert (A:Set) (le: A → A → bool) x (l: list A) on l ≝
+ match l with
+  [ nil ⇒ [x]
+  | (cons he l') ⇒
+      match le x he with
+       [ true ⇒ x::l
+       | false ⇒ he::(insert A le x l')
+       ]
+  ].
+
+lemma insert_ind :
+ ∀A:Set. ∀le: A → A → bool. ∀x.
+  ∀P:(list A → list A → Prop).
+   ∀H:(∀l: list A. l=[] → P [] [x]).
+    ∀H2:
+    (∀l: list A. ∀he. ∀l'. P l' (insert ? le x l') →
+      le x he = false → l=he::l' → P (he::l') (he::(insert ? le x l'))).
+     ∀H3:
+     (∀l: list A. ∀he. ∀l'. P l' (insert ? le x l') →
+       le x he = true → l=he::l' → P (he::l') (x::he::l')).
+    ∀l:list A. P l (insert ? le x l).
+  intros.
+  apply (
+    let rec insert_ind (l: list A) \def
+    match l in list
+    return
+      λli.
+       l = li → P li (insert ? le x li)
+    with
+     [ nil ⇒ H l
+     | (cons he l') ⇒
+         match le x he
+         return
+          λb. le x he = b → l = he::l' →
+           P (he::l')
+            (match b with 
+              [ true ⇒ x::he::l'
+              | false ⇒ he::(insert ? le x l') ])
+         with
+          [ true ⇒ H2 l he l' (insert_ind l')
+          | false ⇒ H1 l he l' (insert_ind l')
+          ]
+         (refl_eq ? (le x he))
+     ] (refl_eq ? l) in insert_ind l).
+qed.
+
+
+let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝
+ match l with
+  [ nil ⇒ []
+  | (cons he l') ⇒
+      let l'' ≝ insertionsort A le l' in
+       insert A le he l''
+  ].
+
+lemma ordered_injective:
+  ∀A:Set. ∀le:A → A → bool.
+   ∀l:list A. ordered A le l = true → ordered A le (tail A l) = true.
+  intros 3 (A le l).
+  elim l
+  [ simplify; reflexivity;
+  | simplify;
+    generalize in match H1;
+    clear H1;
+    elim l1;
+    [ simplify; reflexivity;
+    | cut ((le s s1 \land ordered A le (s1::l2)) = true);
+      [ generalize in match Hcut; 
+        apply andb_elim;
+        elim (le s s1);
+        [ simplify;
+          fold simplify (ordered ? le (s1::l2));
+          intros; assumption;
+        | simplify;
+          intros (Habsurd);
+          apply False_ind;
+          apply (not_eq_true_false);
+          symmetry;
+          assumption
+        ]
+      | exact H2;
+      ]
+    ]
+  ].
+qed.
+
+lemma insert_sorted:
+  \forall A:Set. \forall le:A\to A\to bool.
+  (\forall a,b:A. le a b = false \to le b a = true) \to
+  \forall l:list A. \forall x:A.
+    ordered A le l = true \to ordered A le (insert A le x l) = true.
+ intros 5 (A le H l x).
+ apply (insert_ind ? ? ? (λl,il. ordered ? le l = true → ordered ? le il = true));
+ clear l; intros; simplify; intros;
+  [2: rewrite > H1;
+    [ generalize in match (H ? ? H2); clear H2; intro;
+      generalize in match H4; clear H4;
+      elim l'; simplify;
+      [ rewrite > H5;
+        reflexivity
+      | elim (le x s); simplify;
+        [ rewrite > H5;
+          reflexivity
+        | simplify in H4;
+          rewrite > (andb_true_true ? ? H4);
+          reflexivity
+        ]
+      ]
+    | apply (ordered_injective ? ? ? H4)
+    ]
+  | reflexivity
+  | rewrite > H2;
+    rewrite > H4;
+    reflexivity
+  ].
+qed.
+  
+theorem insertionsort_sorted:
+  ∀A:Set.
+  ∀le:A → A → bool.∀eq:A → A → bool.
+  (∀a,b:A. le a b = false → le b a = true) \to
+  ∀l:list A.
+  ordered A le (insertionsort A le l) = true.
+  intros 5 (A le eq le_tot l).
+  elim l;
+  [ simplify;
+    reflexivity;
+  | apply (insert_sorted ? ? le_tot (insertionsort ? le l1) s);
+    assumption;
+  ]
+qed.
\ No newline at end of file