Mockingbird combinator puzzles

Stream: new members

[Jordan Scales]

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!

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Yakov Pechersky]

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

[Eric Wieser]

Is inhabited (Bird) undecidable?

[Mario Carneiro]

it's false

[Adam Topaz]

Looks like Bird wants to be coinductive?

[Eric Wieser]

What's the proof that it's false?

[Mario Carneiro]

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

[Eric Wieser]

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?

[Mario Carneiro]

you have to actually pattern match

[Adam Topaz]

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

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

[Mario Carneiro]

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

[Jordan Scales]

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

[Mario Carneiro]

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

[Eric Wieser]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Eric Wieser]

Bundling Ap makes sense in your version @Yakov Pechersky

[Eric Wieser]

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

[Yakov Pechersky]

Yeah that works too