## Coincidence count, using lists

Authors: Jean-Christophe Filliâtre

Topics: List Data Structure

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

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).

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
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
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
```

# Why3 Proof Results for Project "coincidence_count_list"

## Theory "coincidence_count_list.CoincidenceCount": fully verified

 Obligations Alt-Ergo 2.1.0 Alt-Ergo 2.2.0 CVC4 1.6 Transitive.Trans 0.00 --- --- VC for coincidence_count --- --- --- split_vc variant decrease --- --- 0.05 precondition --- --- 0.04 precondition --- --- 0.05 variant decrease --- --- 0.05 precondition --- --- 0.04 precondition --- --- 0.02 variant decrease --- --- 0.04 precondition --- --- 0.02 precondition --- --- 0.04 postcondition --- --- --- split_all_full postcondition --- --- --- split_all_full postcondition --- 2.13 ---

## Theory "coincidence_count_list.CoincidenceCountAnyType": fully verified

 Obligations Alt-Ergo 2.1.0 CVC4 1.6 VC for eq'refn --- 0.02 Transitive.Trans 0.00 --- VC for coincidence_count 1.57 ---

## Theory "coincidence_count_list.CoincidenceCountList": fully verified

 Obligations Alt-Ergo 2.1.0 Transitive.Trans 0.00 VC for coincidence_count 0.29