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
Kenny Lau (Jan 22 2019 at 20:58):
@Patrick Massot you should
derive decidable_eq (can we derive fintype?) and then just
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
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:= 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 (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):
%% 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