The lady and the tiger

Stream: Lean for teaching

[Yury G. Kudryashov]

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

import tactic

inductive door_state
| lady
| 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]

Where can I see the original puzzles?

[Jeremy Avigad]

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]

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]

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

[Dan Stanescu]

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

import tactic

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

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]

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

[Dan Stanescu]

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]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Patrick Massot]

Yes, that's the point.

[Dan Stanescu]

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]

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

[Dan Stanescu]

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

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

[Alexandre Rademaker]

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]

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

[Alexandre Rademaker]

Unfortunately it is not working in the current mathlib

[Alexandre Rademaker]

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]

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]

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]

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.