Tricking elm-test into solving a river-crossing puzzle

[Janiczek]

It’s a mini-blogpost in an Ellie. Written in a “literate programming” style - my comments-to-code ratio has never been so high, I imagine

https://ellie-app.com/nHNx6brVja1/0

[dmy]

Brilliant! And a nice read
Got it on the second try, you saved my saturday night

[G4BB3R]

Great post, I have never thought about using test for this purpose! I tried another approach enumerating all possible game states only, and generating all valid paths instead of fuzz testing, but it was harder to develop and too easy to make a mistake because there are 15 states, and obviously in a real case like a webapp this would not be possible in complex cases. But very funny puzzle!

https://ellie-app.com/8RkX2Krgsa1/0

[gampleman]

In many quick test implementations this trick is built in.

A lot of them have a forAll function which corresponds to elm test’s fuzz function and corresponds to a ∀ in logic.

They also have an exists function (which doesn’t exist in elm (pun not intended)) and corresponds to an ∃ in logic. It’s implementation follows logic:

∃x.f(x) = !∀x.!f(x)

Which is essentially what OP’s post does.

[dmy]

They also have an exists function (which doesn’t exist in elm (pun not intended)) and corresponds to an ∃ in logic.

Well, we are not alone:

Is there a "there exists" quantifier in QuickCheck?

It seems more common for those that use testing by enumeration (vs random generation), right?

[Janiczek]

I didn’t immediately follow your post, so let me go at it from a different angle, try to “braindump” what I think is happening in the Ellie and hopefully arrive at the same conclusion

there doesn't exist a list of Msgs x such that update(x, allLeft) == allRight
!∃x: update(x, allLeft) == allRight

which can be said as

for all lists of Msgs x: update(x, allLeft) /= allRight
∀x: update(x, allLeft) /= allRight

If we extract the update(x, allLeft) == allRight into predicate p(x), then:

!∃x: p(x)
∀x: !p(x)

which are the same. (Cool!)
Alright, so that agrees with your post. I had trouble reading the logic statement, but now I think I can translate it into English for myself:

exists x such that f(x) MEANS THAT not for all x is it true that not f(x)

[gampleman]

Exactly.
…