Julin S (Apr 24 2023 at 17:17): 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).
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