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