Why does this prolog rule using include/3 evaluate to false, but not when exploding it into individual comparisons?

Question

I have a prolog rule position_that_is_equals_to_two that sets X to the position at which the number 2 was found in the provided list of three elements [X, Y, Z]:

position_that_is_equals_to_two([X, Y, Z], X) :-
    include(==(2), [X, Y, Z], AllElementsWhichHaveAValueOfTwo),
    nth0(0, AllElementsWhichHaveAValueOfTwo, X).

When querying it, I immediately get false:

?- position_that_is_equals_to_two([X, _, _], X)
false

However, when I replace include/3 with individual comparisons, prolog gives three possible values for X, which is the output I would expect:

position_that_is_equals_to_two([X, Y, Z], X) :-
    (
        (   X == 2 ; X #= 1)
    ;   (   Y == 2 ; X #= 2)
    ;   (   Z == 2 ; X #= 3)
    ).

Querying it:

?- position_that_is_equals_to_two([X, _, _], X)
X = 1
X = 2
X = 3

Why is the first variant returning false? How can it me modified to (1) still use include and (2) list possible values for X, like the second variant does?

Answer 1

How can it be modified to still use include?

It can't. Include shrinks the original list and throws away information you need to answer the question. With AllElementsWhichHaveAValueOfTwo = [2] what is the index of that two? Was it 0, 1, 2 or 50,000? You can't know.

Worse, include/3 has the signature include(:Goal, +List1, ?List2) and the + means the List1 must be provided, you can't give it unground variables like [X,Y,Z] and have it fill them in. So it can't be used for that reason also.

---

Take this query:

?- position_that_is_equals_to_two([X, _, _], X)

What you expect out of it is that X in the list has value two and X as the index has value zero. You want 2 = 0. That can't work.

---

Your other code is giving the right answer for the wrong reasons; the code (X == 2 ; X #= 1) says "variable X must be two OR variable X must be one" which is allowed but for your indexing you need them both at the same time, not either/or. What you want it to say is "first list item must be two AND the index must be one".

Change the code to (X = 2, X = 1) which is logically how it should be and you're back to asking for 2 = 1 which can't work.

Answer 2

In your example code, X is being used for 2 different purposes and values - that's a conflict.

== is not clpfd.

Looks like this would be sufficient (without using clpfd):

pos_2(Pos, L) :-
    length(L, 3),
    nth1(Pos, L, 2).

Result in swi-prolog:

?- pos_2(Pos, L).
Pos = 1,
L = [2, _, _] ;
Pos = 2,
L = [_, 2, _] ;
Pos = 3,
L = [_, _, 2].