Minimum excludant, aka mex

Author: Jean-Christophe Filliâtre (CNRS)

Given a finite set of integers, find the smallest nonnegative integer that does not belong to this set.

In the following, the set is given as an array A. If N is the size of this array, it is clear that we have 0 <= mex <= N for we cannot have the N+1 first natural numbers in the N cells of array A (pigeon hole principle).

module MexArray

  use int.Int
  use map.Map
  use array.Array
  use ref.Refint
  use pigeon.Pigeonhole

  predicate mem (x: int) (a: array int) =
    exists i. 0 <= i < length a && a[i] = x

  let mex (a: array int) : int
    ensures { 0 <= result <= length a }
    ensures { not (mem result a) }
    ensures { forall x. 0 <= x < result -> mem x a }
  = let n = length a in
    let used = make n false in
    let ghost idx = ref (fun i -> i) in (* the position of each marked value *)
    for i = 0 to n - 1 do
      invariant { forall x. 0 <= x < n -> used[x] ->
                    mem x a && 0 <= !idx x < n && a[!idx x] = x }
      invariant { forall j. 0 <= j < i -> 0 <= a[j] < n ->
                    used[a[j]] && 0 <= !idx a[j] < n && a[!idx a[j]] = a[j] }
      let x = a[i] in
      if 0 <= x && x < n then begin used[x] <- true; idx := set !idx x i end
    done;
    let r = ref 0 in
    let ghost posn = ref (-1) in
    while !r < n && used[!r] do
      invariant { 0 <= !r <= n }
      invariant { forall j. 0 <= j < !r -> used[j] && 0 <= !idx j < n }
      invariant { if !posn >= 0 then 0 <= !posn < n && a[!posn] = n
                                else forall j. 0 <= j < !r -> a[j] <> n }
      variant   { n - !r }
      if a[!r] = n then posn := !r;
      incr r
    done;
    (* we cannot have !r=n (all values marked) and !posn>=0 at the same time *)
    if !r = n && !posn >= 0 then pigeonhole (n+1) n (set !idx n !posn);
    !r

end

module MexArrayInPlace

  use int.Int
  use int.NumOf
  use array.Array
  use array.ArraySwap
  use ref.Refint

  predicate mem (x: int) (a: array int) =
    exists i. 0 <= i < length a && a[i] = x

  function placed (a: array int) : int -> bool =
    fun i -> a[i] = i

  let mex (a: array int) : int
    ensures { 0 <= result <= length a }
    ensures { not (mem result (old a)) }
    ensures { forall x. 0 <= x < result -> mem x (old a) }
  = let n = length a in
    let i = ref 0 in
    while !i < n do
      invariant { 0 <= !i <= n }
      invariant { forall x. mem x a <-> mem x (old a) }
      invariant { forall j. 0 <= j < !i -> 0 <= a[j] < n -> a[a[j]] = a[j] }
      variant   { n - !i, n - numof (placed a) 0 n }
      let x = a[!i] in
      if x < 0 || x >= n then
        incr i
      else if x < !i then begin
        swap a !i x; incr i
      end else if a[x] = x then
        incr i
      else
        swap a !i x
    done;
    assert { forall j. 0 <= j < n -> let x = (old a)[j] in
             0 <= x < n -> a[x] = x };
    for i = 0 to n - 1 do
      invariant { forall j. 0 <= j < i -> a[j] = j }
      if a[i] <> i then return i
    done;
    n

end