How to automatically find counterexample

[jariji]

I'm trying to write a spec for map, starting with the proposition that map preserves length. map(Set, Data.Vectors()) doesn't find a counterexample but I can specify one myself: map(abs, Set([-1, 1])).

Is there some way I could have defined the Set generator that would have enabled it to find that example, without having to specify it explicitly?

using Supposition
Base.map(f, x::Set) = Set(Iterators.map(f, x))
length_map(f, x) = length(map(f, x)) == length(x)
@check false_negative(f=Data.Just(abs), x=map(Set, Data.Vectors(Data.Integers{Int}(); max_size=8))) = length_map(f, x) 
@check counterexample(f=Data.Just(abs), x=Data.Just(Set([-1,1]))) = length_map(f, x)

[Seelengrab]

On a 64-bit system, Int has $2^\mathrm{64}$ distinct values. The likelihood that two numbers with the same absolute value are picked is pretty small, about $1/2^\mathrm{63}$ if my Math is right (both 0 and typemin already map to themselves, so are not relevant). Therefore, the easiest way to increase the likelihood of finding a collision is to use a smaller datatype, e.g. Int8:

julia> data = map(Set, Data.Vectors(Data.Integers{Int8}(); max_size=8))

julia> @check false_negative(f=Data.Just(abs), x=data) = length_map(f, x)
Found counterexample
  Context: false_negative

  Arguments:
      f::typeof(abs) = abs
      x::Set{Int8} = Set(Int8[-127, 127])

This works because abs behaves the same for Int8 as it does for Int.

An alternative is to use a mapping that forces more collisions by tightening the result domain (i.e. one that is not injective):

julia> data = map(Set, Data.Vectors(Data.Integers{Int}(); max_size=8));

julia> @check function false_negative(r=Data.Integers(1,500), x=data)
           length_map(x) do s
               rem(s, r)
           end
       end
Found counterexample
  Context: false_negative

  Arguments:
      r::Int64 = 1
      x::Set{Int64} = Set([-9223372036854775807, -9223372036854775808])

This has the effect that more initial values end up in the sets of possible collisions with each other, increasing the likelihood that Supposition.jl is able to find a collision.

Note that both of these didn't find the final collision with typemin initially/as their first counterexample! This is only what Supposition.jl ended up reducing it to. To find a collision, it truly did have to find at least two numbers that are mapped to the same result. I'd like to improve the UX around this at some point, showing how many reductions it took to find this, storing the initial counter example (or perhaps even a complete reduction log on request?) and some other niceties that make this more clear.

[jariji]

That's a great answer, thanks @Seelengrab.