## 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!

Last updated: Oct 04 2023 at 20:01 UTC