2
$\begingroup$

I'm trying to formalize in Coq the following riddle and its solution

Alice, Bob and Charlie are one of each role:

  • a truth teller (always tells the truth)
  • a liar (always lies)
  • and a spy (can lie or tell the truth)

They make the following statements:

  • Alice: I am not a truth teller.
  • Bob: I am not a spy.
  • Charlie: I am not a liar.

What role is Charlie?
A. Truth teller
B. Liar
C. Spy
D. There is not enough information

I could progress alone , up to a point reached in the following file, because I cannot introduce the fact that two distinct roles are not equal to each other.

I tried a rewrite S in L as last step but I do not know which tactic to use next.I'm pretty sure there is something basic I'm missing.

Can anyone help?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

The tactic discriminate(https://coq.inria.fr/refman/proofs/writing-proofs/reasoning-inductives.html?highlight=discriminate#coq:tacn.discriminate ) is made to handle the cases such as L: spy = liar

Improve this answer
$\endgroup$
1
  • $\begingroup$ In this case congruence also works, and you don't need to use the rewrite command beforehand. $\endgroup$
    – djao
    Commented Jun 5, 2023 at 12:14

Not the answer you're looking for? Browse other questions tagged or ask your own question.