Zulip Chat Archive

Stream: new members

Topic: Mockingbird combinator puzzles


view this post on Zulip Jordan Scales (Dec 09 2020 at 18:48):

Hey all :)

I'm hoping to get some assistance with cleaning up my proofs a bit (or overhauling them entirely!). Currently working through Smullyan's "To Mock a Mockingbird" which features some fun logic puzzles with combinators. This time, however, I'd like to solve the puzzles while I'm also learning Lean

https://github.com/jdan/mockingbird.lean/blob/ecd60d26338f7d07b46fbff36a7fc3d65031b88c/src/mockingbird.lean

In particular, I'm representing a "Combinator" as an inductive type with a single "Ap" constructor (Ap A B) = "AB." I don't love it! I'm also struggling to simplify my proofs a little but instead relying on stuff I barely know like cases and rw :) Any help would be appreciated!

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 18:59):

the proofs look fine. You can use use instead of existsi, it's a bit less fussy.

view this post on Zulip Kevin Buzzard (Dec 09 2020 at 19:00):

e.g. the last two lines of the second proof can just be use [B, Hb],

view this post on Zulip Yakov Pechersky (Dec 09 2020 at 19:10):

Here's a variant in writing it:

import tactic

namespace mockingbird

inductive Bird
| Ap : Bird -> Bird -> Bird

instance : has_mul Bird := Bird.Ap

structure forest : Prop :=
  /-
    (the composition condition)
    For any two birds A and B, there is a bird C such that
    for any bird x, Cx = A(Bx)
  -/
(comp (A B : Bird) :  (C : Bird),  (x : Bird), C * x = A * (B * x))
  /-
    (the mockingbird condition)
    The forest contains a mockingbird M
  -/
(mockingbird :  (M : Bird),  (x : Bird), M * x = x * x)

/--
  1. One rumor is that Every bird in the forest is fond of
  at least one bird
-/
theorem all_birds_fond (h : forest) (A : Bird) :
   (B : Bird), B = A * B :=
begin
  obtain M, hM := h.mockingbird,
  obtain C, hC := h.comp A M,
  use C * C,
  rw [hM, hC, hM]
end

/--
  2. A bird x is called "egocentric" if it is fond of itself.
  Prove using C₁ and C₂ that at least one bird is egocentric.
-/
theorem egocentric_bird_exists (h : forest) :
   (x : Bird), x = x * x :=
begin
  obtain M, hM := h.mockingbird,
  simp_rw hM,
  exact all_birds_fond h M
end

end mockingbird

view this post on Zulip Eric Wieser (Dec 09 2020 at 19:28):

Is inhabited (Bird) undecidable?

view this post on Zulip Mario Carneiro (Dec 09 2020 at 19:28):

it's false

view this post on Zulip Adam Topaz (Dec 09 2020 at 19:30):

Looks like Bird wants to be coinductive?

view this post on Zulip Eric Wieser (Dec 09 2020 at 19:30):

What's the proof that it's false?

view this post on Zulip Mario Carneiro (Dec 09 2020 at 19:30):

theorem no_birds : Bird  false
| (Bird.Ap b _) := no_birds b

view this post on Zulip Eric Wieser (Dec 09 2020 at 19:30):

I tried

lemma no_Bird : Bird  false
| b := begin
  cases b with b1 b2,
  exact no_Bird b2,
end

I gues it's confused by tactic mode?

view this post on Zulip Mario Carneiro (Dec 09 2020 at 19:31):

you have to actually pattern match

view this post on Zulip Adam Topaz (Dec 09 2020 at 19:32):

inductive Bird
| Ap : Bird -> Bird -> Bird

theorem no : Bird  false :=
begin
  intro x,
  induction x,
  assumption
end

view this post on Zulip Mario Carneiro (Dec 09 2020 at 19:32):

otherwise lean falls back on well founded recursion using a natural measure, which would have worked here except for the cases

view this post on Zulip Jordan Scales (Dec 09 2020 at 19:32):

I love the has_mul trick and also TIL structure - thanks, this is great

view this post on Zulip Mario Carneiro (Dec 09 2020 at 19:34):

lemma no_Bird : Bird  false
| b := begin
  have IH :  b':Bird, b'.sizeof < b.sizeof  false :=
    λ b' h, no_Bird b',
  cases b with b1 b2,
  exact IH b2 (by well_founded_tactics.default_dec_tac),
end

view this post on Zulip Eric Wieser (Dec 09 2020 at 19:36):

So the golfed proofs are:

namespace mockingbird

inductive Bird
| Ap : Bird -> Bird -> Bird

instance : has_mul Bird := Bird.Ap

/-- A bird cannot exist -/
lemma no_Bird : Bird  false
| (Bird.Ap a b) := no_Bird b

structure forest : Prop :=
(comp (A B : Bird) :  (C : Bird),  (x : Bird), C * x = A * (B * x))
(mockingbird :  (M : Bird),  (x : Bird), M * x = x * x)

/-- A forest cannot exist -/
lemma no_forest : forest  false
| _, b, _ := no_Bird b

theorem all_birds_fond (h : forest) (A : Bird) :
   (B : Bird), B = A * B :=
false.elim (no_Bird A)

theorem egocentric_bird_exists (h : forest) :
   (x : Bird), x = x * x :=
false.elim (no_forest h)

end mockingbird

Which is probably an indication that your theorem statement is wrong

view this post on Zulip Mario Carneiro (Dec 09 2020 at 19:37):

I haven't looked at the problem statement too carefully but I would guess you can just use a constant instead of an inductive

view this post on Zulip Mario Carneiro (Dec 09 2020 at 19:38):

constant Bird : Type
constant Bird.Ap : Bird -> Bird -> Bird

view this post on Zulip Mario Carneiro (Dec 09 2020 at 19:39):

you can also have them be variables in addition to C1 and C2 to the theorems

view this post on Zulip Yakov Pechersky (Dec 09 2020 at 19:53):

import tactic

namespace mockingbird

inductive Bird | Bird

structure forest (K : Type) :=
(Ap : K  K  K)
  /-
    (the composition condition)
    For any two birds A and B, there is a bird C such that
    for any bird x, Cx = A(Bx)
  -/
(comp (A B : K) :  (C : K),  (x : K), Ap C x = Ap A (Ap B x))
  /-
    (the mockingbird condition)
    The forest contains a mockingbird M
  -/
(mockingbird :  (M : K),  (x : K), Ap M x = Ap x x)

variables {h : forest Bird}

local infixl `*` := h.Ap

/--
  1. One rumor is that Every bird in the forest is fond of
  at least one bird
-/
theorem all_birds_fond (A : Bird) :
   (B : Bird), B = A * B :=
begin
  obtain M, hM := h.mockingbird,
  obtain C, hC := h.comp A M,
  use C * C,
  rw [hM, hC, hM]
end

/--
  2. A bird x is called "egocentric" if it is fond of itself.
  Prove using C₁ and C₂ that at least one bird is egocentric.
-/
theorem egocentric_bird_exists :
   (x : Bird), x = x * x :=
begin
  obtain M, hM := h.mockingbird,
  simp_rw hM,
  exact all_birds_fond M,
end

end mockingbird

view this post on Zulip Yakov Pechersky (Dec 09 2020 at 19:55):

Of course that's all valid because there is only one Bird. So I like Mario's constant version more.

view this post on Zulip Eric Wieser (Dec 09 2020 at 19:58):

Bundling Ap makes sense in your version @Yakov Pechersky

view this post on Zulip Eric Wieser (Dec 09 2020 at 19:58):

Just add variables {Bird : Type*} instead of the inductive?

view this post on Zulip Yakov Pechersky (Dec 09 2020 at 19:59):

Yeah that works too


Last updated: May 06 2021 at 21:09 UTC