Logic puzzles in Lean

Stream: general

[Patrick Massot]

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]

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

[Kenny Lau]

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

[Patrick Massot]

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]

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]

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:=
begin
   sorry
end

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]

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]

cases h : J Smith?

[Rob Lewis]

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

[Patrick Massot]

Thanks!

[Kenny Lau]

btw

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

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

[Patrick Massot]

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]

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

[Patrick Massot]

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]

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

[Patrick Massot]

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

[Rob Lewis]

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