New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(archive/logic_puzzles): add "Knights and knaves" and "Lady or the tiger?" #3153
Closed
Closed
Changes from all commits
Commits
Show all changes
16 commits
Select commit
Hold shift + click to select a range
9a2debe
Added puzzles directory
stanescuUW b6c48aa
Update knights_and_knaves.lean
stanescuUW b3e577a
Update lady_or_tiger.lean
stanescuUW 7ef8a08
Update knights_and_knaves.lean
stanescuUW 23c51d9
Update archive/logic_puzzles/lady_or_tiger.lean
stanescuUW 036fa03
Update archive/logic_puzzles/knights_and_knaves.lean
stanescuUW 559469c
Update knights_and_knaves.lean
stanescuUW 2b6997e
Update knights_and_knaves.lean
stanescuUW 39538ec
Update lady_or_tiger.lean
stanescuUW d5a08b7
Update knights_and_knaves.lean
stanescuUW 88f84e2
Update lady_or_tiger.lean
stanescuUW 3436338
Update archive/logic_puzzles/lady_or_tiger.lean
stanescuUW c99bf2a
Update knights_and_knaves.lean
stanescuUW 568ebd8
Update lady_or_tiger.lean
stanescuUW 478168f
Update knights_and_knaves.lean
stanescuUW a921f2c
Update lady_or_tiger.lean
stanescuUW File filter
Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,87 @@ | ||
/- | ||
Copyright (c) 2020 Dan Stanescu. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Dan Stanescu. | ||
-/ | ||
|
||
import tactic | ||
|
||
/-! | ||
# Knights and knaves puzzles | ||
Two puzzles from "Knights and Knaves" by Raymond Smullyan. | ||
For an online description of these puzzles, see: http://mesosyn.com/mental1-6.html | ||
More information on R. Smullyan: https://en.wikipedia.org/wiki/Raymond_Smullyan | ||
|
||
There is an island where all inhabitants are either knights or knaves. | ||
Knights always tell the truth. Knaves always lie. | ||
Joe and Bob are two inhabitants of this island. | ||
-/ | ||
|
||
inductive islander | ||
| knight | ||
| knave | ||
|
||
notation `y` := islander.knight | ||
notation `n` := islander.knave | ||
|
||
structure Q := (Joe Bob : islander) | ||
|
||
/-- | ||
In this first puzzle, only Joe makes a statement. | ||
He affirms that both protagonist (i.e. both Joe and Bob) are knaves. | ||
Question: what kind of islanders are they in fact? | ||
-/ | ||
|
||
def Q1 := Q | ||
|
||
namespace Q1 | ||
|
||
variables (q : Q1) | ||
|
||
-- Joe's statement | ||
def S1 := q.Joe = n ∧ q.Bob = n | ||
-- Stating that Joe can be a knight or a knave | ||
def H := (q.Joe = y ∧ q.S1) ∨ (q.Joe = n ∧ ¬ q.S1) | ||
|
||
lemma answer : q.H → q.Joe = n ∧ q.Bob = y := | ||
begin | ||
rcases q with ⟨_|_,_|_⟩; | ||
{ simp [H, S1], }, | ||
done | ||
end | ||
|
||
end Q1 | ||
|
||
/-- | ||
In the second puzzle, both Joe and Bob make a statement. | ||
Joe states that he's a knave if and only if Bob is a knave. | ||
Bob only states that they are different kinds. | ||
Question: again, what kind of islanders are our protagonists? | ||
-/ | ||
|
||
|
||
def Q2 := Q | ||
|
||
namespace Q2 | ||
|
||
variables (q : Q2) | ||
|
||
-- Joe's statement | ||
def S1 := q.Joe = n ↔ q.Bob = n | ||
-- Bob's statement | ||
def S2 := q.Joe ≠ q.Bob | ||
-- Stating that either one can be a knight or a knave | ||
def H1 := (q.Joe = y ∧ q.S1) ∨ (q.Joe = n ∧ ¬ q.S1) | ||
def H2 := (q.Bob = y ∧ q.S2) ∨ (q.Bob = n ∧ ¬ q.S2) | ||
-- Again two forms here: | ||
def H := q.H1 ∧ q.H2 | ||
|
||
lemma answer : q.H → q.Joe = n ∧ q.Bob = y := | ||
begin | ||
rcases q with ⟨_|_,_|_⟩; | ||
{ simp [H, H1, S1, H2, S2], }, | ||
done | ||
end | ||
|
||
|
||
end Q2 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,238 @@ | ||
/- | ||
Copyright (c) 2020 Dan Stanescu. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Dan Stanescu and Yuri G. Kudryashov. | ||
-/ | ||
|
||
import tactic | ||
|
||
/-! | ||
# Six logic puzzles. | ||
-/ | ||
|
||
/-- | ||
The first six puzzles from: | ||
"The Lady or the Tiger? And Other Logic Puzzles" | ||
by Raymond Smullyan. | ||
First three contributed to the Lean Zulip chat by Yury G. Kudryashov | ||
but apparently set up by his seven-years-old son. | ||
Slightly modified in appearance (for readability) but not in content by D. Stanescu. | ||
|
||
A king has prisoners choose between two rooms. The signs on the room doors offer enough information | ||
to allow them to make the right choice between rooms with ladies (i.e. presumably happiness) | ||
and rooms with tigers (i.e. presumably death). | ||
In the first three puzzles, the king explains that it is always the case that one of the door | ||
signs is true while the other one is false. | ||
-/ | ||
|
||
|
||
inductive door_leads_to | ||
| lady | ||
| tiger | ||
|
||
notation `y` := door_leads_to.lady | ||
notation `n` := door_leads_to.tiger | ||
|
||
structure Q := (d₁ d₂ : door_leads_to) | ||
|
||
/-- | ||
First puzzle: | ||
Sign on the first door indicates that there's a lady in this room and a tiger in the other room. | ||
Sign on second door indicates that in one of the rooms there's a lady and in one room a tiger. | ||
-/ | ||
|
||
def Q1 := Q | ||
stanescuUW marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
||
namespace Q1 | ||
|
||
variables (q : Q1) | ||
|
||
-- Sign on first door | ||
def D1 := q.1 = y ∧ q.2 = n | ||
-- Sign on second door | ||
def D2 := (q.1 = y ∨ q.2 = y) ∧ (q.1 = n ∨ q.2 = n) | ||
|
||
def H := q.D1 ∧ ¬q.D2 ∨ ¬q.D1 ∧ q.D2 | ||
|
||
-- Terse proof. | ||
lemma answer_t : q.H → q.1 = n ∧ q.2 = y := | ||
by rcases q with ⟨_|_,_|_⟩; simp [H, D1, D2] | ||
|
||
-- Verbose proof. State changes can be seen by clicking after each comma. | ||
lemma answer_v : q.H → q.1 = n ∧ q.2 = y := | ||
begin | ||
rcases q with ⟨_|_,_|_⟩, | ||
simp [H], simp [D1], simp [D2], | ||
simp[H], simp [D1], simp [D2], | ||
stanescuUW marked this conversation as resolved.
Show resolved
Hide resolved
|
||
simp [H], | ||
simp [H], simp [D1], simp [D2], | ||
done | ||
end | ||
|
||
end Q1 | ||
|
||
/-- | ||
Second puzzle: | ||
Sign on the first door indicates that at least one room contains a lady. | ||
Sign on second door indicates there's a tiger in the other room. | ||
-/ | ||
|
||
def Q2 := Q | ||
|
||
namespace Q2 | ||
|
||
variables (q : Q2) | ||
|
||
-- Sign on first door | ||
def D1 := q.1 = y ∨ q.2 = y | ||
-- Sign on second door | ||
def D2 := q.1 = n | ||
|
||
def H := q.D1 ∧ q.D2 ∨ ¬q.D1 ∧ ¬q.D2 | ||
|
||
lemma answer : q.H → q.1 = n ∧ q.2 = y := | ||
by rcases q with ⟨_|_,_|_⟩; simp [H, D1, D2] | ||
|
||
end Q2 | ||
|
||
/-- | ||
Third puzzle: | ||
Sign on the first door indicates that there's either a tiger in this room or a lady in the other. | ||
Sign on second door indicates there's a lady in the other room. | ||
-/ | ||
|
||
|
||
def Q3 := Q | ||
|
||
namespace Q3 | ||
|
||
variables (q : Q3) | ||
|
||
-- Sign on first door | ||
def D1 := q.1 = n ∨ q.2 = y | ||
-- Sign on second door | ||
def D2 := q.1 = y | ||
|
||
def H := q.D1 ∧ q.D2 ∨ ¬q.D1 ∧ ¬q.D2 | ||
|
||
lemma answer : q.H → q.1 = y ∧ q.2 = y := | ||
by rcases q with ⟨_|_,_|_⟩; simp [H, D1, D2] | ||
|
||
end Q3 | ||
|
||
/-! Puzzles 4-7 from the same book: | ||
"The Lady or the Tiger? And Other Logic Puzzles" | ||
by Raymond Smullyan. | ||
Solutions written by D. Stanescu in the same framework as above. | ||
In these puzzles, the king explains that the sign on the first door (D1) is true if a lady | ||
is in in that room and is false if a tiger is in that room. The opposite is true for the sign on | ||
the second door (D2), which is true if a tiger is hidden behind it but false otherwise. | ||
-/ | ||
|
||
/-- | ||
Puzzle number four: | ||
First door sign says that both rooms contain ladies. | ||
Second door sign is identical. | ||
-/ | ||
|
||
def Q4 := Q | ||
|
||
namespace Q4 | ||
|
||
variables (q : Q4) | ||
|
||
-- Sign on first door | ||
def D1 := q.1 = y ∧ q.2 = y | ||
-- Sign on second door | ||
def D2 := q.1 = y ∧ q.2 = y | ||
|
||
-- one way to set up this problem | ||
def H1 := q.1 = y ∧ q.D1 ∨ q.1 = n ∧ ¬ q.D1 | ||
def H2 := q.2 = y ∧ ¬ q.D2 ∨ q.2 = n ∧ q.D2 | ||
def H := q.H1 ∧ q.H2 | ||
|
||
-- Verbose proof | ||
lemma answer_v : q.H → q.1 = n ∧ q.2 = y := | ||
begin | ||
rcases q with ⟨_|_,_|_⟩, | ||
simp [H], simp [H1], simp [D1], simp [H2], simp [D2], | ||
simp [H], simp [H1], simp [D1], | ||
simp [H], simp [H1], | ||
simp [H], simp [H1], simp [D1], simp [H2], simp [D2], | ||
done | ||
end | ||
|
||
-- Terse proof | ||
lemma answer_t : q.H → q.1 = n ∧ q.2 = y := | ||
begin | ||
rcases q with ⟨_|_,_|_⟩; | ||
simp [H, H1, D1, H2, D2], | ||
done | ||
end | ||
|
||
end Q4 | ||
|
||
/-- | ||
Puzzle number five: | ||
First door sign says that at least one room contains a lady. | ||
Second door sign says : "In the other room there is a lady." | ||
-/ | ||
stanescuUW marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
||
|
||
def Q5 := Q | ||
|
||
namespace Q5 | ||
|
||
variables (q : Q5) | ||
|
||
-- Sign on first door | ||
def D1 := q.1 = y ∨ q.2 = y ∨ q.1 = y ∧ q.2 = y | ||
-- Sign on second door | ||
def D2 := q.1 = y | ||
|
||
-- same setup as Q4 above | ||
def H1 := q.1 = y ∧ q.D1 ∨ q.1 = n ∧ ¬ q.D1 | ||
def H2 := q.2 = y ∧ ¬ q.D2 ∨ q.2 = n ∧ q.D2 | ||
def H := q.H1 ∧ q.H2 | ||
|
||
lemma answer : q.H → q.1 = y ∧ q.2 = n := | ||
begin | ||
rcases q with ⟨_|_,_|_⟩; | ||
simp [H, H1, D1, H2, D2], | ||
done | ||
end | ||
|
||
end Q5 | ||
|
||
/-- | ||
Puzzle number six: | ||
First door sign says that it makes no difference which room the prisoner picks. | ||
Second door sign is the same as in the previous puzzle. | ||
Apparently the king is particularly fond of this puzzle. | ||
-/ | ||
|
||
def Q6 := Q | ||
|
||
namespace Q6 | ||
|
||
variables (q : Q6) | ||
|
||
-- Sign on first door | ||
def D1 := q.1 = q.2 | ||
-- Sign on second door | ||
def D2 := q.1 = y | ||
|
||
-- same setup as Q4 above | ||
def H1 := q.1 = y ∧ q.D1 ∨ q.1 = n ∧ ¬ q.D1 | ||
def H2 := q.2 = y ∧ ¬ q.D2 ∨ q.2 = n ∧ q.D2 | ||
def H := q.H1 ∧ q.H2 | ||
|
||
lemma answer : q.H → q.1 = n ∧ q.2 = y := | ||
begin | ||
rcases q with ⟨_|_,_|_⟩; | ||
simp [H, H1, D1, H2, D2], | ||
done | ||
end | ||
|
||
|
||
end Q6 |
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why introduce
q : Q1
at all? You could just havevariables (Joe Bob : islander)
in each namespace, I think.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is somehow the same question as before. I'd say it's just a matter of choice.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Okay, but I think this may be part of what @robertylewis meant when he said "I'd love to see this in idiomatic Lean,". Perhaps we can see what he thinks?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
When I introduced
structure Q
and(q : Q1)
in my son's file, my goal was to useq.S1
instead ofS1 Joe Bob
, and I wanted this in order to save him some keystrokes (he can't type fast yet).In case of knights and knaves I think that we should have something like
islander.says (i : islander) (p : Prop) := cond (i = knight) p (not p)
, then useJoe.says
andBob.says
.I wonder whether we can use some
fintype
magic to ask Lean to list all possible answers.