(** Coincidence count Exercise proposed by Rustan Leino at Dagstuhl seminar 16131, March 2016 You are given two sequences of integers, sorted in increasing order and without duplicate elements, and you count the number of elements that appear in both sequences (in linear time and constant space). See also coincidence_count.mlw for a version using arrays. Authors: Jean-Christophe FilliĆ¢tre (CNRS) *) module CoincidenceCount use list.List use set.SetAppInt use list.Elements use list.Mem as L use int.Int clone export list.Sorted with type t = int, predicate le = (<), goal Transitive.Trans let rec coincidence_count (a b: list int) : set requires { sorted a } requires { sorted b } ensures { result == inter (elements a) (elements b) } variant { a, b } = match a, b with | Cons ha ta, Cons hb tb -> if ha = hb then add ha (coincidence_count ta tb) else if ha < hb then coincidence_count ta b else coincidence_count a tb | _ -> empty () end end (* the same, with elements of any type *) module CoincidenceCountAnyType use list.List use list.Elements use list.Mem as L use int.Int type t val predicate eq (x y : t) ensures { result <-> x = y } clone set.SetApp with type elt = t, val eq = eq val predicate rel (x y : t) clone relations.TotalStrictOrder with type t, predicate rel, axiom . clone export list.Sorted with type t = t, predicate le = rel, goal Transitive.Trans let rec coincidence_count (a b: list t) : set requires { sorted a } requires { sorted b } ensures { result == inter (elements a) (elements b) } variant { a, b } = match a, b with | Cons ha ta, Cons hb tb -> if eq ha hb then add ha (coincidence_count ta tb) else if rel ha hb then coincidence_count ta b else coincidence_count a tb | _ -> empty () end end (* the same, using only lists *) module CoincidenceCountList use list.List use list.Mem use int.Int clone export list.Sorted with type t = int, predicate le = (<), goal Transitive.Trans let rec coincidence_count (a b: list int) : list int requires { sorted a } requires { sorted b } ensures { forall x. mem x result <-> mem x a /\ mem x b } variant { a, b } = match a, b with | Cons ha ta, Cons hb tb -> if ha = hb then Cons ha (coincidence_count ta tb) else if ha < hb then coincidence_count ta b else coincidence_count a tb | _ -> Nil end end