Skip to content

Instantly share code, notes, and snippets.

@PatrickMassot
Created January 25, 2019 09:42
Show Gist options
  • Save PatrickMassot/232210a83f193ea4a2caafb9b0e4245c to your computer and use it in GitHub Desktop.
Save PatrickMassot/232210a83f193ea4a2caafb9b0e4245c to your computer and use it in GitHub Desktop.
Logic puzzle from John P. Pratt in Lean (starts at line 38)
import tactic.interactive
import tactic.linarith
@[derive decidable_eq]
inductive people : Type | Brown | Jones | Smith
constant only_child : people → Prop
constant salary : people → ℕ
@[derive decidable_eq]
inductive job : Type | doctor | lawyer | teacher
constant P : job → people
constant J : people → job
axiom JP : ∀ (p : people) (j : job) , J p = j ↔ P j = p
lemma contradicts {p p' j}
(hp : J p = j) (hp' : J p' = j) (H : (p ≠ p') . tactic.interactive.trivial) : false :=
begin
apply H,
rw JP at hp,
rwa [JP, hp] at hp'
end
namespace tactic.interactive
open tactic
open interactive (parse)
open lean.parser (ident)
meta def absurd_from (h1 : parse ident) (h2 : parse ident) : tactic unit :=
do H1 ← get_local h1,
H2 ← get_local h2,
exfalso,
`[exact contradicts %%H1 %%H2]
end tactic.interactive
open people job
/- The exercise starts here.
Objects of type job are either teacher, lawyer or doctor
Objects of type people are either Smith, Brown or Jones
J : people → job
P : job → people
satisfy the following axiom which ensures that every people has only one job :
JP : ∀ (p : people) (j : job) , J p = j ↔ P j = p
If your context contains assumptions
H : J p = j
H' : J p' = j
with p ≠ p' then you can use tactic
absurd_from H H'
to close any goal
For every people p, the tactic
cases H : J p
will open three new goals under all three possible assumptions H for the value of J p
Remember tactics:
* trivial will close trivial goals ;
* exfalso will replace any goal with false. This is a good move when the
current assumptions are inconsistent ;
* linarith will handle easy inequality arguments.
-/
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
cases H : J Smith,
{ split, trivial,
cases H' : J Brown,
{ absurd_from H H' },
{ split, trivial,
cases H'' : J Jones,
{ absurd_from H H'' },
{ absurd_from H' H'' },
{ trivial } },
{ exfalso,
rw JP at H',
rw ← H' at h₄,
exact h₄ h₁ } },
{ exfalso,
rw JP at H,
rw H at h₅,
linarith },
{ exfalso,
rw JP at H,
rw H at h₂,
linarith }
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment