maximum.fst

(* 
  Ported from Dafny. 
  Original version: https://github.com/dafny-lang/dafny/blob/master/Test/tutorial/maximum.dfy 
*)

module Maximum

open FStar.List
include FStar.List.Tot

val contained_in: x:int -> xs:list int -> bool
let rec contained_in x xs = 
  match xs with 
  | [] -> false
  | [y] -> x = y
  | y :: ys -> x = y || contained_in x ys

(*
method Maximum(values: seq<int>) returns (max: int)
  requires values != []
  ensures max in values
  ensures forall i | 0 <= i < |values| :: values[i] <= max
*)
val max: xs:list int -> Tot int
let rec max xs = 
  match xs with 
  | [] -> 0
  | [x] -> x
  | x :: ys -> if max ys > x then max ys else x
  
val maxSpec: xs:list int -> Lemma
  (ensures 
    (contained_in (max xs) xs) /\ 
    (for_all (fun x -> x <= max xs) xs))

(*
lemma maxIsUnique(values: seq<int>, m1: int, m2: int)
  requires m1 in values && forall i | 0 <= i < |values| :: values[i] <= m1
  requires m2 in values && forall i | 0 <= i < |values| :: values[i] <= m2
  ensures m1 == m2 
*)
assume val xs:list int
assume val m1:int
assume Pre1: ((contained_in m1 xs) /\ (for_all (fun x -> x <= m1) xs))
assume val m2:int
assume Pre2: ((contained_in m2 xs) /\ (for_all (fun x -> x <= m2) xs))
let _ = assert (m1 = m2)