From 9a2debe5cc023de2739ebb1b72dc3f1f55fac7bc Mon Sep 17 00:00:00 2001
From: Dan Stanescu <stanescu@uwyo.edu>
Date: Tue, 23 Jun 2020 10:56:09 -0600
Subject: [PATCH 01/16] Added puzzles directory

---
 archive/logic_puzzles/knights_and_knaves.lean |  74 +++++++
 archive/logic_puzzles/lady_or_tiger.lean      | 197 ++++++++++++++++++
 2 files changed, 271 insertions(+)
 create mode 100644 archive/logic_puzzles/knights_and_knaves.lean
 create mode 100644 archive/logic_puzzles/lady_or_tiger.lean

diff --git a/archive/logic_puzzles/knights_and_knaves.lean b/archive/logic_puzzles/knights_and_knaves.lean
new file mode 100644
index 0000000000000..10f77d11d3f93
--- /dev/null
+++ b/archive/logic_puzzles/knights_and_knaves.lean
@@ -0,0 +1,74 @@
+import tactic
+
+/-
+Knights and knaves puzzles by R. Smullyan.
+There is an island where all inhabitants are either knights or knaves. 
+Knights always tell the truth. Knaves always lie.
+Jack and Bob are two inhabitants of this island.
+-/
+
+inductive person
+| knight
+| knave
+
+notation `y` := person.knight
+notation `n` := person.knave
+
+structure Q := (p₁ p₂ : person)
+
+/-
+In this first puzzle, only Jack makes a statement.
+He affirms that both our heroes (i.e. both Jack and Bob) are knaves.
+What kind of islanders are they?
+-/
+
+def Q1 := Q
+
+namespace Q1
+
+variables (q : Q1)
+
+def S1 := q.1 = n ∧ q.2 = n
+
+def H := (q.1 = y ∧ q.S1) ∨ (q.1 = n ∧ ¬ q.S1)
+
+lemma answer : q.H → q.1 = n ∧ q.2 = y :=
+begin
+    rcases q with ⟨_|_,_|_⟩;
+    { simp [H, S1], },
+    done
+end
+
+end Q1
+
+/-
+In the second puzzle, both Jack and Bob make a statement.
+Jack states that he's a knave if and only if Bob is a knave.
+Bob only states that they are different kinds. 
+Again, what kind of islanders are our protagonists?
+-/
+
+
+def Q2 := Q
+
+namespace Q2
+
+variables (q : Q2)
+
+def S1 := q.2 = n ↔ q.1 = n
+def S2 := q.1 = y ∧ q.2 = n ∨ q.1 = n ∧ q.2 = y
+
+def H1 := (q.1 = y ∧ q.S1) ∨ (q.1 = n ∧ ¬ q.S1)
+def H2 := (q.2 = y ∧ q.S2) ∨ (q.2 = n ∧ ¬ q.S2)
+def H := q.H1 ∧ q.H2
+
+lemma answer : q.H → q.1 = n ∧ q.2 = y :=
+begin
+    rcases q with ⟨_|_,_|_⟩;
+    { simp [H, H1, S1, H2, S2], },
+    done
+end
+
+
+end Q2
+
diff --git a/archive/logic_puzzles/lady_or_tiger.lean b/archive/logic_puzzles/lady_or_tiger.lean
new file mode 100644
index 0000000000000..93d3c7e521c5a
--- /dev/null
+++ b/archive/logic_puzzles/lady_or_tiger.lean
@@ -0,0 +1,197 @@
+import tactic
+
+/-
+The first three puzzles from:
+    "The Lady or the Tiger? And Other Logic Puzzles"
+        by Raymond Smullyan.
+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.
+-/
+
+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)
+
+def Q1 := Q
+
+namespace Q1
+
+variables (q : Q1)
+
+def D1 := q.1 = y ∧ q.2 = n
+
+def D2 := (q.1 = y ∨ q.2 = y) ∧ (q.1 = n ∨ q.2 = n)
+
+def H := q.D1 ∧ ¬q.D2 ∨ ¬q.D1 ∧ q.D2
+
+lemma answer_term : q.H → q.1 = n ∧ q.2 = y :=
+by rcases q with ⟨_|_,_|_⟩; simp [H, D1, D2]
+
+lemma answer_tactic : q.H → q.1 = n ∧ q.2 = y :=
+begin
+    rcases q with ⟨_|_,_|_⟩,
+    simp [H], simp [D1], simp [D2],
+    simp[H], simp [D1], simp [D2],
+    simp [H], 
+    simp [H], simp [D1], simp [D2], 
+    done
+end
+
+end Q1
+
+def Q2 := Q
+/- ∧ : \and ∨ : \or ¬ : \not -/
+
+namespace Q2
+
+variables (q : Q2)
+
+def D1 := q.1=y ∨ q.2=y
+
+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
+
+def Q3 := Q
+/- ∧ : \and ∨ : \or ¬ : \not -/
+
+namespace Q3
+
+variables (q : Q3)
+
+def D1 := q.1=n∨q.2=y
+
+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
+/- ∧ : \and ∨ : \or ¬ : \not -/
+
+namespace Q4
+
+variables (q : Q4)
+
+def D1 := q.1=y ∧ q.2=y
+
+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
+
+lemma answer1 : 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
+
+lemma answer2 : q.H → q.1 = n ∧ q.2 = y :=
+begin
+    rcases q with ⟨_|_,_|_⟩;
+    simp [H, H1, D1, H2, D2], 
+    done
+end
+
+/-
+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."
+-/
+
+end Q4
+
+def Q5 := Q
+/- ∧ : \and ∨ : \or ¬ : \not -/
+
+namespace Q5
+
+variables (q : Q5)
+
+def D1 := q.1=y ∨ q.2=y ∨ q.1 = y ∧ q.2 = y
+
+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
+/- ∧ : \and ∨ : \or ¬ : \not -/
+
+namespace Q6
+
+variables (q : Q6)
+
+def D1 := q.1 = q.2
+
+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

From b6c48aa9e8e5faf7f7e53c25df7a9952eef1ccf1 Mon Sep 17 00:00:00 2001
From: Dan Stanescu <stanescu@uwyo.edu>
Date: Tue, 23 Jun 2020 12:07:01 -0600
Subject: [PATCH 02/16] Update knights_and_knaves.lean

Added copyright etc.
---
 archive/logic_puzzles/knights_and_knaves.lean | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/archive/logic_puzzles/knights_and_knaves.lean b/archive/logic_puzzles/knights_and_knaves.lean
index 10f77d11d3f93..d560d752994b5 100644
--- a/archive/logic_puzzles/knights_and_knaves.lean
+++ b/archive/logic_puzzles/knights_and_knaves.lean
@@ -1,7 +1,15 @@
+/-
+Copyright (c) 2020 Dan Stanescu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: D. Stanescu.
+-/
+
 import tactic
 
-/-
-Knights and knaves puzzles by R. Smullyan.
+/-!
+# Knights and knaves puzzles
+Two puzzles from "Knights and Knaves" by Raymond Smullyan.
+
 There is an island where all inhabitants are either knights or knaves. 
 Knights always tell the truth. Knaves always lie.
 Jack and Bob are two inhabitants of this island.

From b3e577a1940ccb20dd4488c91e1d05f925fdac13 Mon Sep 17 00:00:00 2001
From: Dan Stanescu <stanescu@uwyo.edu>
Date: Tue, 23 Jun 2020 12:14:53 -0600
Subject: [PATCH 03/16] Update lady_or_tiger.lean

---
 archive/logic_puzzles/lady_or_tiger.lean | 26 ++++++++++++++++--------
 1 file changed, 17 insertions(+), 9 deletions(-)

diff --git a/archive/logic_puzzles/lady_or_tiger.lean b/archive/logic_puzzles/lady_or_tiger.lean
index 93d3c7e521c5a..e225593e185ba 100644
--- a/archive/logic_puzzles/lady_or_tiger.lean
+++ b/archive/logic_puzzles/lady_or_tiger.lean
@@ -1,12 +1,21 @@
+/-
+Copyright (c) 2020 Dan Stanescu.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: D.Stanescu and Y. G. Kudryashov.
+-/
+
 import tactic
 
-/-
-The first three puzzles from:
+/-!
+# Six logic puzzles.
+-/
+
+/-- The first six puzzles from:
     "The Lady or the Tiger? And Other Logic Puzzles"
         by Raymond Smullyan.
-Contributed to the Lean Zulip chat by Yury G. Kudryashov
+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.
+Slightly modified in appearance (for readability) but not in content by D. Stanescu.
 -/
 
 inductive door_leads_to
@@ -81,8 +90,7 @@ by rcases q with ⟨_|_,_|_⟩; simp [H, D1, D2]
 
 end Q3
 
-/-
-Puzzles 4-7 from the same book:
+/-- 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. 
@@ -91,7 +99,7 @@ is in in that room and is false if a tiger is in that room. The opposite is true
 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.
@@ -130,7 +138,7 @@ begin
     done
 end
 
-/-
+/--
 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."
@@ -163,7 +171,7 @@ 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.

From 7ef8a0820b7a74c72823809feda4347663bb1736 Mon Sep 17 00:00:00 2001
From: Dan Stanescu <stanescu@uwyo.edu>
Date: Tue, 23 Jun 2020 12:15:33 -0600
Subject: [PATCH 04/16] Update knights_and_knaves.lean

---
 archive/logic_puzzles/knights_and_knaves.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/archive/logic_puzzles/knights_and_knaves.lean b/archive/logic_puzzles/knights_and_knaves.lean
index d560d752994b5..89cd5b29a46f4 100644
--- a/archive/logic_puzzles/knights_and_knaves.lean
+++ b/archive/logic_puzzles/knights_and_knaves.lean
@@ -24,7 +24,7 @@ notation `n` := person.knave
 
 structure Q := (p₁ p₂ : person)
 
-/-
+/--
 In this first puzzle, only Jack makes a statement.
 He affirms that both our heroes (i.e. both Jack and Bob) are knaves.
 What kind of islanders are they?
@@ -49,7 +49,7 @@ end
 
 end Q1
 
-/-
+/--
 In the second puzzle, both Jack and Bob make a statement.
 Jack states that he's a knave if and only if Bob is a knave.
 Bob only states that they are different kinds. 

From 23c51d983979fc13a5211b254f14caa9e8afbe6c Mon Sep 17 00:00:00 2001
From: Dan Stanescu <stanescu@uwyo.edu>
Date: Wed, 24 Jun 2020 09:14:56 -0600
Subject: [PATCH 05/16] Update archive/logic_puzzles/lady_or_tiger.lean

Co-authored-by: Scott Morrison <scott@tqft.net>
---
 archive/logic_puzzles/lady_or_tiger.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/archive/logic_puzzles/lady_or_tiger.lean b/archive/logic_puzzles/lady_or_tiger.lean
index e225593e185ba..ccac2f3b72784 100644
--- a/archive/logic_puzzles/lady_or_tiger.lean
+++ b/archive/logic_puzzles/lady_or_tiger.lean
@@ -90,7 +90,7 @@ by rcases q with ⟨_|_,_|_⟩; simp [H, D1, D2]
 
 end Q3
 
-/-- Puzzles 4-7 from the same book:
+/-! 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. 

From 036fa03a697506b9fbaa045e87d197e55676f8b9 Mon Sep 17 00:00:00 2001
From: Dan Stanescu <stanescu@uwyo.edu>
Date: Wed, 24 Jun 2020 09:16:10 -0600
Subject: [PATCH 06/16] Update archive/logic_puzzles/knights_and_knaves.lean

Co-authored-by: Scott Morrison <scott@tqft.net>
---
 archive/logic_puzzles/knights_and_knaves.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/archive/logic_puzzles/knights_and_knaves.lean b/archive/logic_puzzles/knights_and_knaves.lean
index 89cd5b29a46f4..b9abde36ec278 100644
--- a/archive/logic_puzzles/knights_and_knaves.lean
+++ b/archive/logic_puzzles/knights_and_knaves.lean
@@ -63,7 +63,7 @@ namespace Q2
 
 variables (q : Q2)
 
-def S1 := q.2 = n ↔ q.1 = n
+def S1 := q.1 = n ↔ q.2 = n
 def S2 := q.1 = y ∧ q.2 = n ∨ q.1 = n ∧ q.2 = y
 
 def H1 := (q.1 = y ∧ q.S1) ∨ (q.1 = n ∧ ¬ q.S1)
@@ -79,4 +79,3 @@ end
 
 
 end Q2
-

From 559469cac7eabea22b4283d4d3383ab4c99cb2d7 Mon Sep 17 00:00:00 2001
From: Dan Stanescu <stanescu@uwyo.edu>
Date: Thu, 25 Jun 2020 07:38:19 -0600
Subject: [PATCH 07/16] Update knights_and_knaves.lean

---
 archive/logic_puzzles/knights_and_knaves.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/archive/logic_puzzles/knights_and_knaves.lean b/archive/logic_puzzles/knights_and_knaves.lean
index b9abde36ec278..c305c36ef562b 100644
--- a/archive/logic_puzzles/knights_and_knaves.lean
+++ b/archive/logic_puzzles/knights_and_knaves.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Dan Stanescu. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: D. Stanescu.
+Authors: Dan Stanescu.
 -/
 
 import tactic

From 2b6997e70cca3d2f295ca6735cb52c2692ac95a5 Mon Sep 17 00:00:00 2001
From: Dan Stanescu <stanescu@uwyo.edu>
Date: Thu, 25 Jun 2020 07:41:30 -0600
Subject: [PATCH 08/16] Update knights_and_knaves.lean

---
 archive/logic_puzzles/knights_and_knaves.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/archive/logic_puzzles/knights_and_knaves.lean b/archive/logic_puzzles/knights_and_knaves.lean
index c305c36ef562b..8e359431ca297 100644
--- a/archive/logic_puzzles/knights_and_knaves.lean
+++ b/archive/logic_puzzles/knights_and_knaves.lean
@@ -42,9 +42,9 @@ def H := (q.1 = y ∧ q.S1) ∨ (q.1 = n ∧ ¬ q.S1)
 
 lemma answer : q.H → q.1 = n ∧ q.2 = y :=
 begin
-    rcases q with ⟨_|_,_|_⟩;
-    { simp [H, S1], },
-    done
+   rcases q with ⟨_|_,_|_⟩;
+   { simp [H, S1], },
+   done
 end
 
 end Q1
@@ -72,9 +72,9 @@ def H := q.H1 ∧ q.H2
 
 lemma answer : q.H → q.1 = n ∧ q.2 = y :=
 begin
-    rcases q with ⟨_|_,_|_⟩;
-    { simp [H, H1, S1, H2, S2], },
-    done
+   rcases q with ⟨_|_,_|_⟩;
+   { simp [H, H1, S1, H2, S2], },
+   done
 end
 
 

From 39538ece05631e362f617be82eb20a884cb22399 Mon Sep 17 00:00:00 2001
From: Dan Stanescu <stanescu@uwyo.edu>
Date: Thu, 25 Jun 2020 07:57:04 -0600
Subject: [PATCH 09/16] Update lady_or_tiger.lean

---
 archive/logic_puzzles/lady_or_tiger.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/archive/logic_puzzles/lady_or_tiger.lean b/archive/logic_puzzles/lady_or_tiger.lean
index ccac2f3b72784..8131f64d3cfa6 100644
--- a/archive/logic_puzzles/lady_or_tiger.lean
+++ b/archive/logic_puzzles/lady_or_tiger.lean
@@ -138,13 +138,14 @@ begin
     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."
 -/
 
-end Q4
 
 def Q5 := Q
 /- ∧ : \and ∨ : \or ¬ : \not -/

From d5a08b76c038ea4f16fc2aaf38e049c11c884a41 Mon Sep 17 00:00:00 2001
From: Dan Stanescu <stanescu@uwyo.edu>
Date: Thu, 25 Jun 2020 08:11:52 -0600
Subject: [PATCH 10/16] Update knights_and_knaves.lean

Improved puzzle descriptions, added links.
---
 archive/logic_puzzles/knights_and_knaves.lean | 31 +++++++++++--------
 1 file changed, 18 insertions(+), 13 deletions(-)

diff --git a/archive/logic_puzzles/knights_and_knaves.lean b/archive/logic_puzzles/knights_and_knaves.lean
index 8e359431ca297..e9ec0cce0fcdd 100644
--- a/archive/logic_puzzles/knights_and_knaves.lean
+++ b/archive/logic_puzzles/knights_and_knaves.lean
@@ -9,25 +9,27 @@ 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.
-Jack and Bob are two inhabitants of this island.
+Joe and Bob are two inhabitants of this island.
 -/
 
-inductive person
+inductive islander
 | knight
 | knave
 
-notation `y` := person.knight
-notation `n` := person.knave
+notation `y` := islander.knight
+notation `n` := islander.knave
 
-structure Q := (p₁ p₂ : person)
+structure Q := (Joe Bob : islander)
 
 /--
-In this first puzzle, only Jack makes a statement.
-He affirms that both our heroes (i.e. both Jack and Bob) are knaves.
-What kind of islanders are they?
+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
@@ -36,8 +38,9 @@ namespace Q1
 
 variables (q : Q1)
 
+-- Joe's statement; Joe is the first member of q
 def S1 := q.1 = n ∧ q.2 = n
-
+-- Stating that Joe can be a knight or a knave
 def H := (q.1 = y ∧ q.S1) ∨ (q.1 = n ∧ ¬ q.S1)
 
 lemma answer : q.H → q.1 = n ∧ q.2 = y :=
@@ -50,10 +53,10 @@ end
 end Q1
 
 /--
-In the second puzzle, both Jack and Bob make a statement.
-Jack states that he's a knave if and only if Bob is a knave.
+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. 
-Again, what kind of islanders are our protagonists?
+Question: again, what kind of islanders are our protagonists?
 -/
 
 
@@ -63,9 +66,11 @@ namespace Q2
 
 variables (q : Q2)
 
+-- Joe's statement; Joe is the first member of q
 def S1 := q.1 = n ↔ q.2 = n
+-- Bob's statement; Bob is the second member of q
 def S2 := q.1 = y ∧ q.2 = n ∨ q.1 = n ∧ q.2 = y
-
+-- Stating that either one can be a knight or a knave
 def H1 := (q.1 = y ∧ q.S1) ∨ (q.1 = n ∧ ¬ q.S1)
 def H2 := (q.2 = y ∧ q.S2) ∨ (q.2 = n ∧ ¬ q.S2)
 def H := q.H1 ∧ q.H2

From 88f84e2b26115b0c0dab40f00af55f0e329d2ea1 Mon Sep 17 00:00:00 2001
From: Dan Stanescu <stanescu@uwyo.edu>
Date: Thu, 25 Jun 2020 08:41:01 -0600
Subject: [PATCH 11/16] Update lady_or_tiger.lean

Added puzzle descriptions, changes spacing etc.
---
 archive/logic_puzzles/lady_or_tiger.lean | 125 ++++++++++++++---------
 1 file changed, 77 insertions(+), 48 deletions(-)

diff --git a/archive/logic_puzzles/lady_or_tiger.lean b/archive/logic_puzzles/lady_or_tiger.lean
index 8131f64d3cfa6..018d8367c5cbd 100644
--- a/archive/logic_puzzles/lady_or_tiger.lean
+++ b/archive/logic_puzzles/lady_or_tiger.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Dan Stanescu.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: D.Stanescu and Y. G. Kudryashov.
+Authors: Dan Stanescu and Yuri G. Kudryashov.
 -/
 
 import tactic
@@ -10,14 +10,22 @@ import tactic
 # Six logic puzzles.
 -/
 
-/-- The first six puzzles from:
+/-- 
+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
@@ -27,66 +35,87 @@ 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
 
 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
 
 lemma answer_term : q.H → q.1 = n ∧ q.2 = y :=
-by rcases q with ⟨_|_,_|_⟩; simp [H, D1, D2]
+  by rcases q with ⟨_|_,_|_⟩; simp [H, D1, D2]
 
+-- Tactics mode proof. State changes can be seen by clicking after each comma.
 lemma answer_tactic : q.H → q.1 = n ∧ q.2 = y :=
 begin
-    rcases q with ⟨_|_,_|_⟩,
-    simp [H], simp [D1], simp [D2],
-    simp[H], simp [D1], simp [D2],
-    simp [H], 
-    simp [H], simp [D1], simp [D2], 
-    done
+  rcases q with ⟨_|_,_|_⟩,
+  simp [H], simp [D1], simp [D2],
+  simp[H], simp [D1], simp [D2],
+  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
-/- ∧ : \and ∨ : \or ¬ : \not -/
 
 namespace Q2
 
 variables (q : Q2)
 
-def D1 := q.1=y ∨ q.2=y
+-- Sign on first door
+def D1 := q.1 = y ∨ q.2 = y
+-- Sign on second door
+def D2 := q.1 = n
 
-def D2 := q.1=n
-
-def H := q.D1∧q.D2 ∨ ¬q.D1∧¬q.D2
+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]
+  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
-/- ∧ : \and ∨ : \or ¬ : \not -/
 
 namespace Q3
 
 variables (q : Q3)
 
-def D1 := q.1=n∨q.2=y
+-- Sign on first door
+def D1 := q.1 = n ∨ q.2 = y
+-- Sign on second door
+def D2 := q.1 = y
 
-def D2 := q.1=y
-
-def H := q.D1∧q.D2 ∨ ¬q.D1∧¬q.D2
+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]
+  by rcases q with ⟨_|_,_|_⟩; simp [H, D1, D2]
 
 end Q3
 
@@ -106,15 +135,15 @@ Second door sign is identical.
 -/
 
 def Q4 := Q
-/- ∧ : \and ∨ : \or ¬ : \not -/
 
 namespace Q4
 
 variables (q : Q4)
 
-def D1 := q.1=y ∧ q.2=y
-
-def D2 := q.1=y ∧ q.2=y
+-- 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
@@ -123,19 +152,19 @@ def H := q.H1 ∧ q.H2
 
 lemma answer1 : 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
+  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
 
 lemma answer2 : q.H → q.1 = n ∧ q.2 = y :=
 begin
-    rcases q with ⟨_|_,_|_⟩;
-    simp [H, H1, D1, H2, D2], 
-    done
+  rcases q with ⟨_|_,_|_⟩;
+  simp [H, H1, D1, H2, D2], 
+  done
 end
 
 end Q4
@@ -148,15 +177,15 @@ Second door sign says : "In the other room there is a lady."
 
 
 def Q5 := Q
-/- ∧ : \and ∨ : \or ¬ : \not -/
 
 namespace Q5
 
 variables (q : Q5)
 
-def D1 := q.1=y ∨ q.2=y ∨ q.1 = y ∧ q.2 = y
-
-def D2 := q.1=y
+-- 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
@@ -165,9 +194,9 @@ 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
+  rcases q with ⟨_|_,_|_⟩;
+  simp [H, H1, D1, H2, D2], 
+  done
 end
 
 end Q5
@@ -180,15 +209,15 @@ Apparently the king is particularly fond of this puzzle.
 -/
 
 def Q6 := Q
-/- ∧ : \and ∨ : \or ¬ : \not -/
 
 namespace Q6
 
 variables (q : Q6)
 
+-- Sign on first door
 def D1 := q.1 = q.2
-
-def D2 := q.1=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
@@ -197,9 +226,9 @@ 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
+  rcases q with ⟨_|_,_|_⟩;
+  simp [H, H1, D1, H2, D2], 
+  done
 end
 
 

From 3436338a517ae36102bf08ff1ae5cd94150b61ce Mon Sep 17 00:00:00 2001
From: Dan Stanescu <stanescu@uwyo.edu>
Date: Thu, 25 Jun 2020 16:56:02 -0600
Subject: [PATCH 12/16] Update archive/logic_puzzles/lady_or_tiger.lean

Co-authored-by: Scott Morrison <scott@tqft.net>
---
 archive/logic_puzzles/lady_or_tiger.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/archive/logic_puzzles/lady_or_tiger.lean b/archive/logic_puzzles/lady_or_tiger.lean
index 018d8367c5cbd..afcc662c67260 100644
--- a/archive/logic_puzzles/lady_or_tiger.lean
+++ b/archive/logic_puzzles/lady_or_tiger.lean
@@ -62,7 +62,7 @@ lemma answer_tactic : q.H → q.1 = n ∧ q.2 = y :=
 begin
   rcases q with ⟨_|_,_|_⟩,
   simp [H], simp [D1], simp [D2],
-  simp[H], simp [D1], simp [D2],
+  simp [H], simp [D1], simp [D2],
   simp [H], 
   simp [H], simp [D1], simp [D2], 
   done

From c99bf2a328e4831bb3ab263be84b324aa371e16c Mon Sep 17 00:00:00 2001
From: Dan Stanescu <stanescu@uwyo.edu>
Date: Thu, 25 Jun 2020 17:34:18 -0600
Subject: [PATCH 13/16] Update knights_and_knaves.lean

Changed as per SM's requests.
---
 archive/logic_puzzles/knights_and_knaves.lean | 41 +++++++++++++------
 1 file changed, 28 insertions(+), 13 deletions(-)

diff --git a/archive/logic_puzzles/knights_and_knaves.lean b/archive/logic_puzzles/knights_and_knaves.lean
index e9ec0cce0fcdd..36117b01b177a 100644
--- a/archive/logic_puzzles/knights_and_knaves.lean
+++ b/archive/logic_puzzles/knights_and_knaves.lean
@@ -38,12 +38,12 @@ namespace Q1
 
 variables (q : Q1)
 
--- Joe's statement; Joe is the first member of q
-def S1 := q.1 = n ∧ q.2 = n
+-- Joe's statement
+def S1 := q.Joe = n ∧ q.Bob = n
 -- Stating that Joe can be a knight or a knave
-def H := (q.1 = y ∧ q.S1) ∨ (q.1 = n ∧ ¬ q.S1)
+def H := (q.Joe = y ∧ q.S1) ∨ (q.Joe = n ∧ ¬ q.S1)
 
-lemma answer : q.H → q.1 = n ∧ q.2 = y :=
+lemma answer : q.H → q.Joe = n ∧ q.Bob = y :=
 begin
    rcases q with ⟨_|_,_|_⟩;
    { simp [H, S1], },
@@ -66,19 +66,34 @@ namespace Q2
 
 variables (q : Q2)
 
--- Joe's statement; Joe is the first member of q
-def S1 := q.1 = n ↔ q.2 = n
--- Bob's statement; Bob is the second member of q
-def S2 := q.1 = y ∧ q.2 = n ∨ q.1 = n ∧ q.2 = y
+-- Joe's statement
+def S1 := q.Joe = n ↔ q.Bob = n
+-- Bob's statement in its original form (variant v1)
+def S2_v1 := q.Joe ≠ q.Bob
+-- Bob's statement written in a different form (variant v2)
+def S2_v2 := q.Joe = y ∧ q.Bob = n ∨ q.Joe = n ∧ q.Bob = y
 -- Stating that either one can be a knight or a knave
-def H1 := (q.1 = y ∧ q.S1) ∨ (q.1 = n ∧ ¬ q.S1)
-def H2 := (q.2 = y ∧ q.S2) ∨ (q.2 = n ∧ ¬ q.S2)
-def H := q.H1 ∧ q.H2
+def H1 := (q.Joe = y ∧ q.S1) ∨ (q.Joe = n ∧ ¬ q.S1)
+-- For Bob we need two forms:
+def H2_v1 := (q.Bob = y ∧ q.S2_v1) ∨ (q.Bob = n ∧ ¬ q.S2_v1)
+def H2_v2 := (q.Bob = y ∧ q.S2_v2) ∨ (q.Bob = n ∧ ¬ q.S2_v2)
+-- Again two forms here:
+def H_v1 := q.H1 ∧ q.H2_v1
+def H_v2 := q.H1 ∧ q.H2_v2
+
+-- Result using the original form of Bob's statement
+lemma answer_v1 : q.H_v1 → q.Joe = n ∧ q.Bob = y :=
+begin
+   rcases q with ⟨_|_,_|_⟩;
+   { simp [H_v1, H1, S1, H2_v1, S2_v1], },
+   done
+end
 
-lemma answer : q.H → q.1 = n ∧ q.2 = y :=
+-- Result using the second form of Bob's statement
+lemma answer_v2 : q.H_v2 → q.Joe = n ∧ q.Bob = y :=
 begin
    rcases q with ⟨_|_,_|_⟩;
-   { simp [H, H1, S1, H2, S2], },
+   { simp [H_v2, H1, S1, H2_v2, S2_v2], },
    done
 end
 

From 568ebd84c74ef5679380b49116bbfc22435db4da Mon Sep 17 00:00:00 2001
From: Dan Stanescu <stanescu@uwyo.edu>
Date: Thu, 25 Jun 2020 17:37:21 -0600
Subject: [PATCH 14/16] Update lady_or_tiger.lean

Changed as per SM's suggestions.
---
 archive/logic_puzzles/lady_or_tiger.lean | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/archive/logic_puzzles/lady_or_tiger.lean b/archive/logic_puzzles/lady_or_tiger.lean
index afcc662c67260..f234e6feafc1c 100644
--- a/archive/logic_puzzles/lady_or_tiger.lean
+++ b/archive/logic_puzzles/lady_or_tiger.lean
@@ -54,15 +54,16 @@ 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_term : q.H → q.1 = n ∧ q.2 = y :=
   by rcases q with ⟨_|_,_|_⟩; simp [H, D1, D2]
 
--- Tactics mode proof. State changes can be seen by clicking after each comma.
+-- Verbose proof. State changes can be seen by clicking after each comma.
 lemma answer_tactic : q.H → q.1 = n ∧ q.2 = y :=
 begin
   rcases q with ⟨_|_,_|_⟩,
   simp [H], simp [D1], simp [D2],
-  simp [H], simp [D1], simp [D2],
+  simp[H], simp [D1], simp [D2],
   simp [H], 
   simp [H], simp [D1], simp [D2], 
   done
@@ -150,6 +151,7 @@ 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 answer1 : q.H → q.1 = n ∧ q.2 = y :=
 begin
   rcases q with ⟨_|_,_|_⟩,
@@ -160,6 +162,7 @@ begin
   done
 end
 
+-- Terse proof
 lemma answer2 : q.H → q.1 = n ∧ q.2 = y :=
 begin
   rcases q with ⟨_|_,_|_⟩;

From 478168ff58ed4369567e9a35bad205f992ad0893 Mon Sep 17 00:00:00 2001
From: Dan Stanescu <stanescu@uwyo.edu>
Date: Fri, 26 Jun 2020 01:37:56 -0600
Subject: [PATCH 15/16] Update knights_and_knaves.lean

---
 archive/logic_puzzles/knights_and_knaves.lean | 26 +++++--------------
 1 file changed, 6 insertions(+), 20 deletions(-)

diff --git a/archive/logic_puzzles/knights_and_knaves.lean b/archive/logic_puzzles/knights_and_knaves.lean
index 36117b01b177a..42c9c739e6605 100644
--- a/archive/logic_puzzles/knights_and_knaves.lean
+++ b/archive/logic_puzzles/knights_and_knaves.lean
@@ -68,32 +68,18 @@ variables (q : Q2)
 
 -- Joe's statement
 def S1 := q.Joe = n ↔ q.Bob = n
--- Bob's statement in its original form (variant v1)
-def S2_v1 := q.Joe ≠ q.Bob
--- Bob's statement written in a different form (variant v2)
-def S2_v2 := q.Joe = y ∧ q.Bob = n ∨ q.Joe = n ∧ q.Bob = y
+-- 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)
--- For Bob we need two forms:
-def H2_v1 := (q.Bob = y ∧ q.S2_v1) ∨ (q.Bob = n ∧ ¬ q.S2_v1)
-def H2_v2 := (q.Bob = y ∧ q.S2_v2) ∨ (q.Bob = n ∧ ¬ q.S2_v2)
+def H2 := (q.Bob = y ∧ q.S2) ∨ (q.Bob = n ∧ ¬ q.S2)
 -- Again two forms here:
-def H_v1 := q.H1 ∧ q.H2_v1
-def H_v2 := q.H1 ∧ q.H2_v2
+def H := q.H1 ∧ q.H2
 
--- Result using the original form of Bob's statement
-lemma answer_v1 : q.H_v1 → q.Joe = n ∧ q.Bob = y :=
-begin
-   rcases q with ⟨_|_,_|_⟩;
-   { simp [H_v1, H1, S1, H2_v1, S2_v1], },
-   done
-end
-
--- Result using the second form of Bob's statement
-lemma answer_v2 : q.H_v2 → q.Joe = n ∧ q.Bob = y :=
+lemma answer : q.H → q.Joe = n ∧ q.Bob = y :=
 begin
    rcases q with ⟨_|_,_|_⟩;
-   { simp [H_v2, H1, S1, H2_v2, S2_v2], },
+   { simp [H, H1, S1, H2, S2], },
    done
 end
 

From a921f2c96e5fa7c60e1350917911e261d86d939d Mon Sep 17 00:00:00 2001
From: Dan Stanescu <stanescu@uwyo.edu>
Date: Fri, 26 Jun 2020 01:41:21 -0600
Subject: [PATCH 16/16] Update lady_or_tiger.lean

---
 archive/logic_puzzles/lady_or_tiger.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/archive/logic_puzzles/lady_or_tiger.lean b/archive/logic_puzzles/lady_or_tiger.lean
index f234e6feafc1c..3b7a5af1b136c 100644
--- a/archive/logic_puzzles/lady_or_tiger.lean
+++ b/archive/logic_puzzles/lady_or_tiger.lean
@@ -55,11 +55,11 @@ 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_term : q.H → q.1 = n ∧ q.2 = y :=
+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_tactic : q.H → q.1 = n ∧ q.2 = y :=
+lemma answer_v : q.H → q.1 = n ∧ q.2 = y :=
 begin
   rcases q with ⟨_|_,_|_⟩,
   simp [H], simp [D1], simp [D2],
@@ -152,7 +152,7 @@ def H2 := q.2 = y ∧ ¬ q.D2 ∨ q.2 = n ∧ q.D2
 def H := q.H1 ∧ q.H2
 
 -- Verbose proof
-lemma answer1 : q.H → q.1 = n ∧ q.2 = y :=
+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], 
@@ -163,7 +163,7 @@ begin
 end
 
 -- Terse proof
-lemma answer2 : q.H → q.1 = n ∧ q.2 = y :=
+lemma answer_t : q.H → q.1 = n ∧ q.2 = y :=
 begin
   rcases q with ⟨_|_,_|_⟩;
   simp [H, H1, D1, H2, D2],