list sorting (to be completed ...)

diff --git a/helm/matita/library/list/sort.ma b/helm/matita/library/list/sort.ma
new file mode 100644 (file)
index 0000000..2d60662
--- /dev/null
+++ b/helm/matita/library/list/sort.ma
@@ -0,0 +1,178 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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')
+       ]
+  ].
+
+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
+  \to 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);
+        [ change with (ordered A le (s1::l2) = true \to ordered A le (s1::l2) = true).
+          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).
+  elim l;
+  [ 2: change with (ordered A le (match le x s with
+         [ true ⇒ x::(s::l1) | false ⇒ s::(insert A le x l1) ]) = true).
+       apply (bool_elim ? (le x s));
+       [ intros;
+         change with ((le x s \land ordered A le (s::l1)) = true);
+         apply andb_elim;
+         rewrite > H3;
+         assumption;
+       | generalize in match H2;
+         clear H1; clear H2;
+         generalize in match s;
+         clear s;
+         elim l1
+         [ simplify;
+           rewrite > (H x a H2);
+           reflexivity;
+         | change with ((ordered A le (a::match le x s with
+              [ true ⇒ x::s::l2 | false ⇒ s::(insert A le x l2) ])) = true).
+            apply (bool_elim ? (le x s));
+            [ intros;
+              change with ((le a x \land (le x s \land ordered A le (s::l2))) = true).
+              apply andb_elim;
+              rewrite > (H x a H3);
+              change with ((le x s \land ordered A le (s::l2)) = true).
+              apply andb_elim;
+              rewrite > H4;
+              apply (ordered_injective A le (a::s::l2));
+              assumption;
+            | intros;
+              change with ((le a s \land ordered A le (s::(insert A le x l2))) = true);
+              apply andb_elim;
+              change in H2 with ((le a s \land ordered A le (s::l2)) = true); 
+              generalize in match H2;
+              apply (andb_elim (le a s));
+              elim (le a s);
+              [ change with (ordered A le (s::l2) = true \to ordered A le (s::insert A le x l2) = true);
+                intros;
+                apply (H1 s);
+                assumption;
+              | simplify; intros; assumption
+              ]
+           ]
+         ]
+      ]
+   | simplify; 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 A le le_tot (insertionsort A le l1) s);
+    assumption;
+  ]
+qed.
+
+(*
+theorem insertionsort_correct:
+  ∀A:Set.
+  ∀le:A → A → bool.∀eq:A → A → bool.
+  (∀a,b:A. le a b = false → le b a = true) \to
+  ∀l,l':list A.
+  l' = insertionsort A le l
+  \to ordered A le l' = true
+    ∧ ((\forall x:A. mem A eq x l = true \to mem A eq x l' = true)
+        ∧ (\forall x:A. mem A eq x l = true \to mem A eq x l' = true)).
+  intros;
+  split;
+  [ rewrite > H1; 
+    apply (insertionsort_sorted A le eq H);
+  | split;
+    [ TO BE CONTINUED ...
+*)