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
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?