Stream: Coq users

Topic: Knights and Knaves puzzle


view this post on Zulip 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

Each has a statement to say:

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).

view this post on Zulip Paolo Giarrusso (Apr 24 2023 at 21:27):

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

view this post on Zulip Paolo Giarrusso (Apr 24 2023 at 21:29):

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

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Dec 08 2023 at 11:36):

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

view this post on Zulip Paolo Giarrusso (Dec 08 2023 at 11:38):

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

view this post on Zulip 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.

view this post on Zulip Julin Shaji (Dec 08 2023 at 17:26):

Am trying to read this now: https://www.cs.ru.nl/bachelors-theses/2022/Kimberley_Frings___1027103___Formalizing_and_proving_knights_and_knaves_puzzles_in_three_valued_logic_in_Coq.pdf

view this post on Zulip 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.
Admitted.

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.

view this post on Zulip Karl Palmskog (Dec 08 2023 at 20:34):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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