## Stream: new members

### Topic: Mockingbird combinator puzzles

#### 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!

#### 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.

#### Kevin Buzzard (Dec 09 2020 at 19:00):

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

#### 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


#### Eric Wieser (Dec 09 2020 at 19:28):

Is inhabited (Bird) undecidable?

it's false

#### Adam Topaz (Dec 09 2020 at 19:30):

Looks like Bird wants to be coinductive?

#### Eric Wieser (Dec 09 2020 at 19:30):

What's the proof that it's false?

#### Mario Carneiro (Dec 09 2020 at 19:30):

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


#### 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?

#### Mario Carneiro (Dec 09 2020 at 19:31):

you have to actually pattern match

#### 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


#### 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

#### Jordan Scales (Dec 09 2020 at 19:32):

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

#### 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


#### 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

#### 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

#### Mario Carneiro (Dec 09 2020 at 19:38):

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


#### Mario Carneiro (Dec 09 2020 at 19:39):

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

#### 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


#### 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.

#### Eric Wieser (Dec 09 2020 at 19:58):

Bundling Ap makes sense in your version @Yakov Pechersky

#### Eric Wieser (Dec 09 2020 at 19:58):

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

#### Yakov Pechersky (Dec 09 2020 at 19:59):

Yeah that works too

Last updated: May 06 2021 at 21:09 UTC