# Zulip Chat Archive

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

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?

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

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