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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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