From 005d5a6a7989ce78e668dd0d241e11ced23249e4 Mon Sep 17 00:00:00 2001 From: Santiago Zanella-Beguelin Date: Thu, 14 Jul 2016 15:13:23 +0100 Subject: [PATCH] Simplified QuickSort.List example --- examples/algorithms/QuickSort.List.fst | 135 ++++++++++++------------- 1 file changed, 66 insertions(+), 69 deletions(-) diff --git a/examples/algorithms/QuickSort.List.fst b/examples/algorithms/QuickSort.List.fst index e6e90066e55..58b681de1d0 100644 --- a/examples/algorithms/QuickSort.List.fst +++ b/examples/algorithms/QuickSort.List.fst @@ -1,92 +1,89 @@ module QuickSort.List +#set-options "--initial_ifuel 1 --initial_fuel 1 --max_ifuel 1 --max_fuel 1" + open FStar.List.Tot -#set-options "--initial_ifuel 2 --initial_fuel 1 --max_ifuel 2 --max_fuel 1" -(* Specification of sortedness according to some comparison function f *) +(* Specification of sorted according to a comparison function f *) val sorted: ('a -> 'a -> Tot bool) -> list 'a -> Tot bool -let rec sorted f l = match l with - | [] -> true - | [x] -> true - | x::y::xs -> f x y && sorted f (y::xs) - - -type total_order (a:Type) (f: (a -> a -> Tot bool)) = - (forall a. f a a) (* reflexivity *) - /\ (forall a1 a2. (f a1 a2 /\ f a2 a1) ==> a1 == a2) (* anti-symmetry *) - /\ (forall a1 a2 a3. f a1 a2 /\ f a2 a3 ==> f a1 a3) (* transitivity *) - /\ (forall a1 a2. f a1 a2 \/ f a2 a1) (* totality *) - - -val count : 'a -> list 'a -> Tot nat -let rec count (x:'a) (l:list 'a) = match l with - | hd::tl -> (if hd=x then 1 else 0) + count x tl +let rec sorted f = function + | x::y::xs -> f x y && sorted f (y::xs) + | _ -> true + +type total_order (a:Type) = + f:(a -> a -> Tot bool) { + (forall a. f a a) // reflexive + /\ (forall a1 a2. f a1 a2 /\ f a2 a1 ==> a1 = a2) // anti-symmetric + /\ (forall a1 a2 a3. f a1 a2 /\ f a2 a3 ==> f a1 a3) // transitive + /\ (forall a1 a2. f a1 a2 \/ f a2 a1) // total + } + +val count: 'a -> list 'a -> Tot nat +let rec count x = function + | hd::tl -> (if hd = x then 1 else 0) + count x tl | [] -> 0 -val mem_count : x:'a -> l:list 'a -> - Lemma (requires True) (ensures (mem x l == (count x l > 0))) - [SMTPat (mem x l)] (decreases l) -let rec mem_count x l = match l with +val mem_count: x:'a -> l:list 'a -> + Lemma (requires True) + (ensures (mem x l = (count x l > 0))) + (decreases l) + [SMTPat (mem x l)] +let rec mem_count x = function | [] -> () | _::tl -> mem_count x tl -val append_count: l:list 'a -> m:list 'a -> x:'a - -> Lemma (requires True) - (ensures (count x (append l m) = (count x l + count x m))) - [SMTPat (count x (append l m))] -let rec append_count l m x = match l with +val append_count: l:list 'a -> m:list 'a -> x:'a -> + Lemma (requires True) + (ensures (count x (l @ m) = (count x l + count x m))) + [SMTPat (count x (l @ m))] +let rec append_count l m x = + match l with | [] -> () | hd::tl -> append_count tl m x val partition: ('a -> Tot bool) -> list 'a -> Tot (list 'a * list 'a) -let rec partition p = function +let rec partition f = function | [] -> [], [] | hd::tl -> - let l1, l2 = partition p tl in - if p hd - then hd::l1, l2 - else l1, hd::l2 - -(* this is used only to speed things up *) -type trigger (#a:Type) (x:a) = True - -val partition_lemma: f:('a -> Tot bool) -> l:list 'a -> Lemma (requires True) - (ensures (forall hi lo. (hi, lo) = partition f l - ==> (length l = length hi + length lo - /\ (forall x.{:pattern (trigger x)} - trigger x ==> - (mem x hi ==> f x) - /\ (mem x lo ==> not (f x)) - /\ (count x l = count x hi + count x lo))))) - [SMTPat (partition f l)] + let l1, l2 = partition f tl in + if f hd then (hd::l1, l2) else (l1, hd::l2) + + +val partition_lemma: f:('a -> Tot bool) -> l:list 'a -> + Lemma (requires True) + (ensures (let (hi, lo) = partition f l in + length l = length hi + length lo + /\ (forall x. (mem x hi ==> f x) + /\ (mem x lo ==> ~(f x)) + /\ (count x l = count x hi + count x lo)))) + [SMTPat (partition f l)] let rec partition_lemma f l = match l with - | [] -> () - | hd::tl -> cut (trigger hd); partition_lemma f tl - - -val sorted_app_lemma: #a:Type - -> f:(a -> a -> Tot bool){total_order a f} - -> l1:list a{sorted f l1} - -> l2:list a{sorted f l2} - -> pivot:a - -> Lemma (requires ((forall y.{:pattern (trigger y)} trigger y ==> - ((mem y l1 ==> not (f pivot y)) - /\ (mem y l2 ==> f pivot y))))) - (ensures (sorted f (append l1 (pivot::l2)))) - [SMTPat (sorted f (append l1 (pivot::l2)))] -let rec sorted_app_lemma #a f l1 l2 pivot = match l1 with - | [] -> if is_Cons l2 then cut (trigger (Cons.hd l2)) else () - | hd::tl -> cut (trigger hd); sorted_app_lemma f tl l2 pivot - -val sort: f:('a -> 'a -> Tot bool){total_order 'a f} - -> l:list 'a - -> Tot (m:list 'a{sorted f m /\ (forall i.{:pattern trigger i} trigger i ==> (count i l = count i m))}) - (decreases (length l)) -let rec sort f = function + | [] -> () + | hd::tl -> partition_lemma f tl + + +val sorted_app_lemma: f:total_order 'a + -> l1:list 'a{sorted f l1} -> l2:list 'a{sorted f l2} -> pivot:'a + -> Lemma (requires (forall y. (mem y l1 ==> ~(f pivot y)) + /\ (mem y l2 ==> f pivot y))) + (ensures (sorted f (l1 @ pivot :: l2))) + [SMTPat (sorted f (l1 @ pivot::l2))] +let rec sorted_app_lemma #a f l1 l2 pivot = + match l1 with + | hd::tl -> sorted_app_lemma f tl l2 pivot + | _ -> () + +type is_permutation (a:Type) (l:list a) (m:list a) = + forall x. count x l = count x m + +val quicksort: f:total_order 'a -> l:list 'a -> + Tot (m:list 'a{sorted f m /\ is_permutation 'a l m}) + (decreases (length l)) +let rec quicksort f = function | [] -> [] | pivot::tl -> let hi, lo = partition (f pivot) tl in - append (sort f lo) (pivot::(sort f hi)) + (quicksort f lo) @ pivot :: quicksort f hi