Stream: Coq users

Topic: Knights and Knaves puzzle

Julin S (Apr 24 2023 at 17:17):

I was looking at a 'knight and knave' problem from one of Smullyan's puzzle books and found this:

There are 3 persons: A,B,C

• At least one is a Knight.
• At least one is a Knave.
• One of them has a prize.

Each has a statement to say:

• A says: B doesn't have the prize
• B says: I don't have the prize
• C says: I have the prize

Who has the prize?

Would it be possible to solve this with coq?

What could be the goal? Goal is an assignment from {Knight, Knave} to variables A,B,C.
How can that even be stated?

(And how can we reduce this to SAT problem? Is that possible?)

I started like:

``````Inductive type : Set := K | V.

Inductive person : type -> Type :=
| Person: forall t:type, person t.

Axiom hasP: forall {t:type}, person t -> Prop.

Definition isK {t:type} (p:person t): Prop :=
match t with
| K => true
| _ => false
end = true.

Goal
exists (t1 t2 t3:type),
forall (a:person t1) (b:person t2) (c:person t3),
(t1=K \/ t2=K \/ t3=K) /\
(t1=V \/ t2=V \/ t3=V) /\
(hasP a \/ hasP b \/ hasP c) /\
(isK a -> ~hasP b) /\
(isK b -> ~hasP b) /\
(isK c -> hasP c).
``````

Paolo Giarrusso (Apr 24 2023 at 21:27):

`Inductive person := a | b | c.` and `assignment : person -> type` might be effective

Paolo Giarrusso (Apr 24 2023 at 21:29):

Also: your formalization only requires knights to be honest. Are knaves not expected to lie?

Paolo Giarrusso (Apr 24 2023 at 21:32):

Using person := a | b | c also lets you avoid forall. And since type is isomorphic to boolean, then that's basically already a SAT problem!

Julin Shaji (Dec 08 2023 at 06:34):

Paolo Giarrusso said:

`Inductive person := a | b | c.` and `assignment : person -> type` might be effective

Sorry for a reply to an old post, but in this case, does `assignment` would have to be an axiom, right? Or should it be made a `Definition` giving a `Prop`?

Paolo Giarrusso (Dec 08 2023 at 11:36):

I think neither? `Section with_assignment. Context (assignment : person -> type).`

Paolo Giarrusso (Dec 08 2023 at 11:38):

Sorry, misread. Your overall goal seems `exists assignment ...`

Julin Shaji (Dec 08 2023 at 17:26):

Yeah, like `exists t1 t2: type, assignment a = t1 /\ assignment b = t2 /\ ...` kind of thing is what I was looking it.

Evan Marzion (Dec 08 2023 at 19:45):

I gave your puzzle a try and found a set-up like this fairly simple to use:

``````Inductive Person :=
A | B | C.

Section KnightAndKnave.

Variable knight : Person.
Variable knave : Person.
Variable prize_holder : Person.

Definition statement (p : Person) : Prop :=
match p with
| A => prize_holder <> B
| B => prize_holder <> B
| C => prize_holder = C
end.

Hypothesis knight_tells_truth :
statement knight.

Hypothesis knave_tells_lie :
~ statement knave.

(* replace X with who you think has prize *)
Theorem X_has_prize : prize_holder = X.
Proof.

End KnightAndKnave.
``````

A tiny issue I have with the `assignment : person -> type` model of the problem is that it forbids by fiat a person from being both knight and knave (or neither, I suppose). Of course, the fact that one cannot be both is an easy logical consequence, but then you should prove it if necessary instead of pushing it into your axioms.

Karl Palmskog (Dec 08 2023 at 20:34):

is there a reason there can't there be several knights or several knaves?

Paolo Giarrusso (Dec 08 2023 at 21:39):

Hm, the problem statement is incomplete — I'm used to "everybody is either a knight or a knave, knights are always truthful, knaves always lie" always being part of these problems.

Paolo Giarrusso (Dec 08 2023 at 21:40):

If not, you should have predicates `knight, knave : person -> bool` (using `Prop` might force you to use classical logic unnecessarily).

Karl Palmskog (Dec 08 2023 at 21:55):

bonus: prove directly from the characteristics of a knight and a knave that a person can't be both. But probably one wants to keep the possibility to be neither.

Karl Palmskog (Dec 08 2023 at 21:57):

I would argue that making (the property of being) `knight` and `knave` decidable is against the spirit of the puzzle setup, though

Karl Palmskog (Dec 08 2023 at 21:58):

and in some sense it gives information about the nature of the puzzle if one finds oneself in the situation of needing to use classical logic

Last updated: Jun 18 2024 at 09:02 UTC