## Stream: Lean for teaching

### Topic: The lady and the tiger

#### Yury G. Kudryashov (Jun 16 2020 at 01:25):

The first three questions from "The Lady or the Tiger? And Other Logic Puzzles" in Lean:

import tactic

inductive door_state
| tiger

notation y := door_state.lady
notation n := door_state.tiger

structure Q := (d₁ d₂ : door_state)

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 : q.H → q.1 = n ∧ q.2 = y :=
by rcases q with ⟨_|_,_|_⟩; simp [H, D1, D2]

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


Q2 and Q3 are written by my 7-year-old son. As you can see, we concentrated on correctly stating the problems, not on translating "human" solutions.

#### Kevin Buzzard (Jun 16 2020 at 01:31):

Where can I see the original puzzles?

#### Jeremy Avigad (Jun 16 2020 at 01:35):

Coincidentally, they are here: http://www.andrew.cmu.edu/user/avigad/summer_school/2020/. I just used them last week. (It's the first of the two PDF files.)

#### Dan Stanescu (Jun 19 2020 at 19:52):

It would be nice to have a good collection of such puzzles in a repository somewhere. These tend to attract students. I remember when showing the barber paradox from TPiL in a department talk, students all across the spectrum seemed to very much enjoy it. Puzzles will make for great bait!

#### Patrick Massot (Jun 19 2020 at 20:39):

https://xenaproject.wordpress.com/2018/11/17/blue-eyed-islanders-guest-post/

#### Dan Stanescu (Jun 21 2020 at 14:19):

Here's a solution to the fourth puzzle in the same framework:

import tactic

| tiger

notation y := door_leads_to.lady
notation n := door_leads_to.tiger

structure Q := (d₁ d₂ : door_leads_to)

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 answer : q.H → q.1 = n ∧ q.2 = y :=
begin
rcases q with ⟨_|_,_|_⟩;
simp [H, H1, D1, H2, D2],
done
end

end Q4


#### Dan Stanescu (Jun 21 2020 at 14:22):

This is an incipient repository for logic puzzles in Lean that I will try to grow and maintain:
https://github.com/stanescuUW/LeanPuzzles

#### Dan Stanescu (Jun 21 2020 at 14:24):

@Yury G. Kudryashov I hope you don't mind me citing your son's work.

#### Dan Stanescu (Jun 21 2020 at 14:29):

Some of these puzzles may make for good introduction to Lean. After all, Logic and proof has a motivational example:
https://leanprover.github.io/logic_and_proof/propositional_logic.html

#### Dan Stanescu (Jun 21 2020 at 14:32):

Mentioning @Jeremy Avigad and @Chris Hughes here in case they want to contribute their solutions to :up:

#### Patrick Massot (Jun 21 2020 at 14:37):

I wouldn't mind seeing such things in https://github.com/leanprover-community/mathlib/tree/master/archive

#### Kevin Buzzard (Jun 21 2020 at 14:38):

The advantage of putting them in the archive is that they don't bitrot

#### Patrick Massot (Jun 21 2020 at 14:41):

Yes, that's the point.

#### Dan Stanescu (Jun 21 2020 at 14:41):

Patrick Massot said:

I wouldn't mind seeing such things in https://github.com/leanprover-community/mathlib/tree/master/archive

No problem. Let me just have a good starting point. The only problem I've been thinking about: avoiding copyright issues. For now, my plan is to write down puzzle descriptions in the Lean files.

#### Patrick Massot (Jun 21 2020 at 14:41):

Of course this kind of things will be very stable anyway.

#### Dan Stanescu (Jun 23 2020 at 17:02):

@Patrick Massot This PR is active now (with 8 puzzles so far):

https://github.com/leanprover-community/mathlib/pull/3153

#### Alexandre Rademaker (Sep 06 2020 at 19:58):

I have also made some common sense problems in Lean. Maybe unnecessary but I started from SUMO Ontology specification of some classes and relations, https://github.com/own-pt/common-sense-lean/blob/master/misc/bs.lean. Many more puzzles and CS problems may be borrowed from http://tptp.org/cgi-bin/SeeTPTP?Category=Problems.

#### Alexandre Rademaker (Sep 06 2020 at 21:32):

Another amazing example that I found recently http://www.andrew.cmu.edu/user/avigad/Papers/mutilated.pd

#### Alexandre Rademaker (Sep 06 2020 at 21:33):

Unfortunately it is not working in the current mathlib

#### Alexandre Rademaker (Sep 06 2020 at 22:04):

Hi @Yury G. Kudryashov, I am trying to understand your approach. If Q is a structure with two fields. It stands for a possible configuration, right? A state of affairs. So q.1 and q.2 extract each door configuration. But what is q.D1? D1 type is Q1 → Prop? So q.D1 is the same as D1 q and ¬q.D2 is ¬(D2 q)...

#### Yury G. Kudryashov (Sep 06 2020 at 22:14):

Note that my code was optimized to save my son a few keystrokes, not to improve readability. AFAIR, q.D1 is "door 1 says"

#### Alexandre Rademaker (Sep 06 2020 at 22:16):

Hum, I see. If we can think of fields of structures as shortcuts for functions from the type of the structure to the types of the values of its fields, we can also use the dot notation in the other way around, every function from a structure to a value can use the dot notation... What confused me is that the point example in https://leanprover.github.io/theorem_proving_in_lean/structures_and_records.html, have a namespace with the same name of the structure, but in your code, the namespace name is Q1 which is the type the variable q. But the sentence makes it clear for me:

More generally, given an expression p.foo x y z, Lean will insert p at the first non-implicit argument to foo of type point.

#### Alexandre Rademaker (Sep 06 2020 at 22:23):

Yury G. Kudryashov said:

Note that my code was optimized to save my son a few keystrokes, not to improve readability. AFAIR, q.D1 is "door 1 says"

I see, so ¬q.D2 would mean that what door 2 says ... is false.

Last updated: Dec 20 2023 at 11:08 UTC