(* The 2nd Verified Software Competition (VSTTE 2012) https://sites.google.com/site/vstte2012/compet Problem 2: Combinators S and K *) module Combinators type term = S | K | App term term let rec predicate eq (x y : term) ensures { result <-> x = y } = match x, y with | S, S -> True | K, K -> True | App x1 x2, App y1 y2 -> eq x1 y1 && eq x2 y2 | _, _ -> False end (* specification of the CBV reduction *) predicate is_value (t: term) = match t with | K | S -> true | App K v | App S v -> is_value v | App (App S v1) v2 -> is_value v1 /\ is_value v2 | _ -> false end (* contexts *) type context = Hole | Left context term | Right term context predicate is_context (c: context) = match c with | Hole -> true | Left c _ -> is_context c | Right v c -> is_value v && is_context c end function subst (c: context) (t: term) : term = match c with | Hole -> t | Left c1 t2 -> App (subst c1 t) t2 | Right v1 c2 -> App v1 (subst c2 t) end (* one step reduction (the notion of context is inlined in the following definition) *) inductive (-->) (t1 t2: term) = | red_K: forall c: context. is_context c -> forall v1 v2: term. is_value v1 -> is_value v2 -> subst c (App (App K v1) v2) --> subst c v1 | red_S: forall c: context. is_context c -> forall v1 v2 v3: term. is_value v1 -> is_value v2 -> is_value v3 -> subst c (App (App (App S v1) v2) v3) --> subst c (App (App v1 v3) (App v2 v3)) clone import relations.ReflTransClosure with type t = term, predicate rel = (-->) predicate (-->*) (t1 t2: term) = relTR t1 t2 type zipper = ZHole | ZLeft context term | ZRight term context let rec function subst_c (c ct:context) : context ensures { is_context c /\ is_context ct -> is_context result } = match c with | Hole -> ct | Left c1 t2 -> Left (subst_c c1 ct) t2 | Right v1 c2 -> Right v1 (subst_c c2 ct) end lemma subst_c_commute : forall c [@induction] ct t. subst c (subst ct t) = subst (subst_c c ct) t (* task 1: implement CBV reduction *) let rec reduction (ghost c:context) (t: term) : term diverges (* there are non-normalizable terms... *) requires { is_context c } ensures { subst c t -->* subst c result } ensures { is_value result } = match t with | S -> S | K -> K | App t1 t2 -> let v1 = reduction (subst_c c (Left Hole t2)) t1 in let v2 = reduction (subst_c c (Right v1 Hole)) t2 in match v1 with | K | S | App S _ -> App v1 v2 | App K v3 -> v3 | App (App S v3) v4 -> reduction c (App (App v3 v2) (App v4 v2)) | _ -> absurd end end exception BenchFailure let constant i = App (App S K) K let test_SKK () diverges (* would be hard to prove terminating *) raises { BenchFailure -> true } = let t1 = reduction Hole (App i i) in if not (eq t1 i) then raise BenchFailure; let t2 = reduction Hole (App (App (App (App K K) K) K) K) in if not (eq t2 K) then raise BenchFailure; t1, t2 (* an irreducible term is a value *) predicate irreducible (t: term) = forall t': term. not (t-->t') exception Fail let rec ghost reduce_step (c:context) (t:term) : term requires { is_context c } ensures { subst c t --> subst c result } raises { Fail -> is_value t } variant { t } = match t with | App t1 t2 -> try App (reduce_step (subst_c c (Left Hole t2)) t1) t2 with Fail -> try App t1 (reduce_step (subst_c c (Right t1 Hole)) t2) with Fail -> match t1 with | App K v -> v | App (App S v1) v2 -> App (App v1 t2) (App v2 t2) | _ -> raise Fail end end end | _ -> raise Fail end let rec lemma value_in_context (c:context) (t:term) : unit requires { is_value (subst c t) } ensures { is_value t } variant { c } = match c with | Hole -> () | Left cl _ -> value_in_context cl t | Right _ cr -> value_in_context cr t end let lemma irreducible_is_value (t:term) : unit ensures { irreducible t <-> is_value t } = try let _ = reduce_step Hole t in () with Fail -> () end (* task 2 *) use import int.Int inductive only_K (t: term) = | only_K_K: only_K K | only_K_App: forall t1 t2: term. only_K t1 -> only_K t2 -> only_K (App t1 t2) let rec reduction2 (ghost c:context) (t: term) : term requires { only_K t /\ is_context c } ensures { only_K result /\ is_value result } ensures { subst c t -->* subst c result } variant { t } = match t with | K -> K | App t1 t2 -> let v1 = reduction2 (subst_c c (Left Hole t2)) t1 in let v2 = reduction2 (subst_c c (Right v1 Hole)) t2 in match v1 with | K -> App v1 v2 | App K v3 -> v3 | _ -> absurd end | _ -> absurd end (* task 3 *) let rec function ks (n: int) : term requires { n >= 0 } ensures { only_K result } variant { n } = if n = 0 then K else App (ks (n-1)) K use import number.Parity let rec reduction3 (ghost c:context) (ghost n:int) (t: term) : term requires { n >= 0 /\ t = ks n /\ is_context c } variant { n } ensures { subst c t -->* subst c result } ensures { is_value result } ensures { even n -> result = K } ensures { odd n -> result = App K K } = match t with | K -> K | App t1 t2 -> let v1 = reduction3 (subst_c c (Left Hole t2)) (n-1) t1 in let v2 = reduction3 (subst_c c (Right v1 Hole)) 0 t2 in match v1 with | K -> App v1 v2 | App K v3 -> v3 | _ -> absurd end | _ -> absurd end let lemma ks_even_odd (n:int) : unit requires { n >= 0 } ensures { ks (2*n) -->* K } ensures { ks (2*n+1) -->* App K K } = let _ = reduction3 Hole (2*n) (ks (2*n)) in let _ = reduction3 Hole (2*n+1) (ks (2*n+1)) in () end