From 0d3aa91e49270813033f7b6f390c21d575ff6560 Mon Sep 17 00:00:00 2001
From: Karen Palacio <karen.palacio.1994@gmail.com>
Date: Fri, 4 Oct 2019 19:31:13 -0300
Subject: [PATCH] Added selection sort implementation in FStar

---
 selection-sort/SelSort.fst       | 35 ++++++++++++++++++++++++
 selection-sort/SelectionSort.fst | 47 ++++++++++++++++++++++++++++++++
 2 files changed, 82 insertions(+)
 create mode 100644 selection-sort/SelSort.fst
 create mode 100644 selection-sort/SelectionSort.fst

diff --git a/selection-sort/SelSort.fst b/selection-sort/SelSort.fst
new file mode 100644
index 0000000..07f2735
--- /dev/null
+++ b/selection-sort/SelSort.fst
@@ -0,0 +1,35 @@
+module SelSort
+open FStar.List.Tot
+
+(* Check that a list is sorted *)
+val sorted: list int -> Tot bool
+let rec sorted l = match l with
+    | [] | [_] -> true
+    | x::y::xs -> (x <= y) && (sorted (y::xs))
+
+val test_sorted: x:int -> l:list int ->
+      Lemma ((sorted (x::l) /\ Cons? l) ==> x <= Cons?.hd l)
+let test_sorted x l = ()
+
+val test_sorted2: unit -> Tot (m:list int{sorted m})
+let test_sorted2 () = Nil
+
+
+(* Fact about sorted *)
+val sorted_smaller: x:int
+                ->  y:int
+                ->  l:list int
+                ->  Lemma (requires (sorted (x::l) /\ mem y l))
+                          (ensures (x <= y))
+                          [SMTPat (sorted (x::l)); SMTPat (mem y l)]
+let rec sorted_smaller x y l = match l with
+    | [] -> ()
+    | z::zs -> if z=y then () else sorted_smaller x y zs
+
+
+type permutation (l1:list int) (l2:list int) =
+    length l1 = length l2 /\ (forall n. count n l1 = count n l2)
+
+type permutation_2 (l:list int) (l1:list int) (l2:list int) =
+    (forall n. mem n l = (mem n l1 || mem n l2)) /\
+    length l = length l1 + length l2
diff --git a/selection-sort/SelectionSort.fst b/selection-sort/SelectionSort.fst
new file mode 100644
index 0000000..8f15bbb
--- /dev/null
+++ b/selection-sort/SelectionSort.fst
@@ -0,0 +1,47 @@
+(*
+Made by: Karen A. Palacio, 2019.
+*)
+module SelectionSort
+open FStar.List.Tot
+open SelSort
+
+(*The minimum of a list*)
+val minimum : l1 : list int{length l1 >= 1} -> Pure int (requires True) (ensures (fun r ->(forall x. (mem x l1) ==> r<=x) /\ mem r l1))
+(decreases (length l1))
+let rec minimum l1 = match l1 with
+                  | [x] -> x
+                  | x::y::xs -> if x<y then minimum (x::xs)
+                              else minimum (y::xs)
+
+(*Erase an element of a list.
+Since erase will be called with the minimum of a given list as i, i will always belong to l1 and the length of the resulting list will be strictly less than the length of the original.
+Also it will not be called with l1 = [] *)
+
+val erase : i:int -> l1: list int -> Pure (list int)
+ (requires mem i l1)
+ (ensures (fun r -> permutation l1 (i::r)))
+let rec erase m l = match l with
+                 |[x] -> []
+                 |x::xs ->
+                   if m=x then xs
+                   else x::erase m xs
+
+val memcountLemma: y:int -> xs: list int -> 
+  Lemma (ensures mem y xs <==> count y xs > 0)
+        [SMTPat (mem y xs); SMTPat (count y xs) ]
+
+let rec memcountLemma y xs =
+  match xs with
+    | [] -> ()
+    | x::xs' -> memcountLemma y xs'
+
+(*The selection sort algorithm*)
+val selsort : l:list int -> Pure (list int) (requires True) 
+            (ensures (fun r -> sorted r /\ permutation l r)) (decreases (length l))
+
+let rec selsort l = match l with
+    |[] -> []
+    |x::xs -> let list = x::xs in
+      let min = minimum list in
+      let rest = erase min list in
+      min::selsort rest