Zulip Chat Archive

Stream: general

Topic: Logic puzzles in Lean

Patrick Massot (Jan 22 2019 at 20:20):

I'm considering include a couple of small logic puzzles in my Lean exercises. But I realize I don't know how to do that. Probably I should have paid more attention to some of Kevin's messages. Say I want to formalize the solution to the first question in http://www.johnpratt.com/items/puzzles/logic_puzzles.html Say I define inductive people : Type | Brown | Jones | Smith. I'd like to do case disjunctions according to whether some term of type people is Brown, Jones or Smith. But cases is very disappointing. It replaces only in the current goal. What is the workflow here?

Kevin Buzzard (Jan 22 2019 at 20:56):

Answer to second one: https://xkcd.com/1134/ . For the first one, Chris would prove it using dec_trivial somehow.

Kenny Lau (Jan 22 2019 at 20:58):

@Patrick Massot you should derive decidable_eq (can we derive fintype?) and then just dec_trivial everything

Patrick Massot (Jan 22 2019 at 21:12):

I don't want a nice hi-tech proof. The question is whether I could do a logic exercise using those questions, not a dec_trivial exercise.

Rob Lewis (Jan 22 2019 at 21:33):

I'm not sure exactly what you're trying to do, could you post some code where cases doesn't do quite what you want?

Patrick Massot (Jan 22 2019 at 22:02):

Rob, say I start with:

attribute [instance] classical.prop_decidable

inductive people : Type | Brown | Jones | Smith

variables (only_child : people  Prop) (salary : people  )

inductive job : Type | doctor | lawyer | teacher
variable (P : job  people)
variable (J : people  job)
variable (PJ :  x, P (J x) = x)
variable (JP :  x, J (P x) = x)
include PJ JP

open people job

example (h₁ : only_child (P teacher))
 (h₂ : salary (P teacher) < salary (P lawyer))
 (h₃ : salary (P teacher) < salary (P doctor))
 (h₄ : ¬ only_child Brown)
 (h₅ : salary Smith > salary (P lawyer))
: J Smith = doctor  J Brown = lawyer  J Jones = teacher:=

I'd like to say: let's examine in turn all three possibilities for J Smith, derive contradictions in two cases, deduce the value of J Smith and move on. But cases J Smith does not do that. It does spawn 3 cases, but with no extra assumption, simply replacing J Smith in the goal.

Patrick Massot (Jan 22 2019 at 22:05):

Of course I can use by_cases H : J Smith = doctor, but this gives me two goals, not three, and only the first goal has the shape I'd like to see

Rob Lewis (Jan 22 2019 at 22:05):

cases h : J Smith?

Rob Lewis (Jan 22 2019 at 22:06):

That will give you the three goals, each with an additional hypothesis h : J Smith = ...

Patrick Massot (Jan 22 2019 at 22:06):


Kenny Lau (Jan 22 2019 at 22:07):


@[derive decidable_eq]
inductive people : Type | Brown | Jones | Smith

@[derive decidable_eq]
inductive job : Type | doctor | lawyer | teacher

Patrick Massot (Jan 25 2019 at 09:42):

I think I manage to turn that logic puzzle into something that could be an exercise in my "proof by case analysis" lecture. Remember the context: I'm trying to get a usable exercise from the first item in http://www.johnpratt.com/items/puzzles/logic_puzzles.html. My attempt lives at https://gist.github.com/PatrickMassot/232210a83f193ea4a2caafb9b0e4245c you should scroll down to line 38 before reading the beginning if curious

Kevin Buzzard (Jan 25 2019 at 09:48):

+1 for use of linarith. @Rob Lewis can mention this application in his next grant proposal.

Patrick Massot (Jan 25 2019 at 10:02):

By the way, @Abhimanyu Pallavi Sudhir you should have a look at the tactic I created in this gist, in case you are still stuck on yesterday's question.

Abhimanyu Pallavi Sudhir (Jan 25 2019 at 10:28):

Thanks -- I'm guessing the %% is the key? I'll try it out.

Patrick Massot (Jan 25 2019 at 10:49):

Yes, this is explained in the tactic tutorial I referred to

Rob Lewis (Jan 25 2019 at 11:40):

Using %% is called "antiquotation." AFAIK you can't antiquote identifiers, so you won't be able to write something like `[simp at %%a].

Last updated: Aug 03 2023 at 10:10 UTC