How to implement a not_all_equal/1 predicate

How would one implement a not_all_equal/1 predicate, which succeeds if the given list contains at least 2 different elements and fails otherwise?

Here is my attempt (a not very pure one):

not_all_equal(L) :-
    (   member(H1, L), member(H2, L), H1 \= H2 -> true
    ;   list_to_set(L, S),
        not_all_equal_(S)
    ).

not_all_equal_([H|T]) :-
    (   member(H1, T), dif(H, H1)
    ;   not_all_equal_(T)
    ).

This however does not always have the best behaviour:

?- not_all_equal([A,B,C]), A = a, B = b.
A = a,
B = b ;
A = a,
B = b,
dif(a, C) ;
A = a,
B = b,
dif(b, C) ;
false.

In this example, only the first answer should come out, the two other ones are superfluous.

Here's a straightforward way you can do it and preserve logical-purity!

not_all_equal([E|Es]) :-
   some_dif(Es, E).

some_dif([X|Xs], E) :-
   (  dif(X, E)
   ;  X = E, some_dif(Xs, E)
   ).

Here are some sample queries using SWI-Prolog 7.7.2.

First, the most general query:

?- not_all_equal(Es).
   dif(_A,_B), Es = [_A,_B|_C]
;  dif(_A,_B), Es = [_A,_A,_B|_C]
;  dif(_A,_B), Es = [_A,_A,_A,_B|_C]
;  dif(_A,_B), Es = [_A,_A,_A,_A,_B|_C]
;  dif(_A,_B), Es = [_A,_A,_A,_A,_A,_B|_C]
...

Next, the query the OP gave in the question:

?- not_all_equal([A,B,C]), A=a, B=b.
   A = a, B = b
;  false.                          % <- the toplevel hints at non-determinism

Last, let's put the subgoal A=a, B=b upfront:

?- A=a, B=b, not_all_equal([A,B,C]).
   A = a, B = b
;  false.                          % <- (non-deterministic, like above)

Good, but ideally the last query should have succeeded deterministically!

---

Enter library(reif)

First argument indexing takes the principal functor of the first predicate argument (plus a few simple built-in tests) into account to improve the determinism of sufficiently instantiated goals.

This, by itself, does not cover dif/2 satisfactorily.

What can we do? Work with reified term equality/inequality—effectively indexing dif/2!

some_dif([X|Xs], E) :-                     % some_dif([X|Xs], E) :-
   if_(dif(X,E), true,                     %    (  dif(X,E), true
       (X = E, some_dif(Xs,E))             %    ;  X = E, some_dif(Xs,E)
      ).                                   %    ).

Notice the similarities of the new and the old implementation!

Above, the goal X = E is redundant on the left-hand side. Let's remove it!

some_dif([X|Xs], E) :-
   if_(dif(X,E), true, some_dif(Xs,E)).

Sweet! But, alas, we're not quite done (yet)!

?- not_all_equal(Xs).
DOES NOT TERMINATE

What's going on?

It turns out that the implementation of dif/3 prevents us from getting a nice answer sequence for the most general query. To do so—without using additional goals forcing fair enumeration—we need a tweaked implementation of dif/3, which I call diffirst/3:

diffirst(X, Y, T) :-
   (  X == Y -> T = false
   ;  X \= Y -> T = true
   ;  T = true,  dif(X, Y)
   ;  T = false, X = Y
   ).

Let's use diffirst/3 instead of dif/3 in the definition of predicate some_dif/2:

some_dif([X|Xs], E) :-
   if_(diffirst(X,E), true, some_dif(Xs,E)).

So, at long last, here are above queries with the new some_dif/2:

?- not_all_equal(Es).                     % query #1
   dif(_A,_B), Es = [_A,_B|_C]
;  dif(_A,_B), Es = [_A,_A,_B|_C]
;  dif(_A,_B), Es = [_A,_A,_A,_B|_C]
...

?- not_all_equal([A,B,C]), A=a, B=b.      % query #2
   A = a, B = b
;  false.

?- A=a, B=b, not_all_equal([A,B,C]).      % query #3
A = a, B = b.

Query #1 does not terminate, but has the same nice compact answer sequence. Good!

Query #2 is still non-determinstic. Okay. To me this is as good as it gets.

Query #3 has become deterministic: Better now!

---

The bottom line:

1. Use library(reif) to tame excess non-determinism while preserving logical purity!
2. diffirst/3 should find its way into library(reif) :)

---

---

---

EDIT: more general using a meta-predicate (suggested by a comment; thx!)

Let's generalize some_dif/2 like so:

:- meta_predicate some(2,?).
some(P_2, [X|Xs]) :-
   if_(call(P_2,X), true, some(P_2,Xs)).

some/2 can be used with reified predicates other than diffirst/3.

Here an update to not_all_equal/1 which now uses some/2 instead of some_dif/2:

not_all_equal([X|Xs]) :-
   some(diffirst(X), Xs).

Above sample queries still give the same answers, so I won't show these here.