# Zulip Chat Archive

## Stream: new members

### Topic: TPIL4 problem 8.5

#### Ryan McCorvie (May 11 2023 at 21:00):

I am really stuck on problem 5 in chapter 8 of Theorem Proving in Lean 4, and I would be grateful for any suggestions or hints.

Here's a simplifed example of how I get stuck. Let a `CTree`

be a binary tree where the leaf nodes are either black or red, and each leaf is associated with a `Nat`

. Let `sum`

be the sum over all the leaves. Let `simpColor`

replace a tree which consists of two red leaves or two black leaves with a single colored leaf whose value is the sum.

I want to prove that `sum simpColor t = sum t`

for all `t : CTree`

.

```
inductive CTree where
| black : Nat → CTree
| red : Nat → CTree
| branch : CTree → CTree → CTree
open CTree
def sum : CTree → Nat
| black n => n
| red n => n
| branch t₁ t₂ => sum t₁ + sum t₂
def simpColor : CTree → CTree
| branch (red n₁) (red n₂) => red (n₁ + n₂)
| branch (black n₁) (black n₂) => black (n₁ + n₂)
| t => t
```

I think I can just match the tree according to the cases in `simpColor`

and verify this holds for each part.

```
theorem simpColor_eq : ∀ t : CTree, sum (simpColor t) = sum t := by
intro t
match t with
| branch (red m) (red n) => rfl
| branch (black m) (black n) => rfl
| t1 => rfl --- this case fails
```

However, the last case fails. I assume this is becuase the last case overmatches, and when we get to that branch, lean doesn't know we aren't in the first two branches. That is, it tries to prove `simpColor t1 = t1`

for a generic `t1 : CTree`

, not for the specific `t1`

which is known not to be in the first two cases. Is there some way to match on the cases in a function definition rather than the cases in an inductive type?

Alternatively, instead of doing a match on `t `

, I can `rw [simpColor]`

, and this puts a big match statement in my equality. If there was some tactic which enabled me to rewrite

```
f ( match x with
| x1 => t1
...
| xn => tn )
```

as

```
match x with
| x1 => f t1
...
| xn => f tn
```

then I could make progress. Is there something like that?

My last idea is to tediously enumerate the refinement of all the cases invovled in the definition of `sum`

and `simpColor`

. I get something like this

```
theorem simpColor_eq2
: ∀ t : CTree, sum (simpColor t) = sum t := by
intro t
match t with
| branch t₁ t₂ =>
match t₁, t₂ with
| s1, branch s2 s3 => rfl --- Weirdly this case fails
| branch _ _, _ => rfl
| red n₁, red n₂ => rfl
| black n₁, black n₂ => rfl
| red n₁, black n₂ => rfl
| black n₁, red n₂ => rfl
| red n => rfl
| black n => rfl
-- Weirdly this case fails
variable (t1 t2 t3 : CTree)
example : simpColor (branch t1 (branch t2 t3)) = branch t1 (branch t2 t3) := by rfl
```

However, there is one case which doesn't work. I can't tell why, to my eye the matcher should easily resolve this case. So maybe my hypothesis about why the previous version doesn't work is wrong, and this points to the real problem.

I appreciate any insights you can give. Thank you

#### David Renshaw (May 11 2023 at 21:36):

This works:

```
theorem simpColor_eq : ∀ t : CTree, sum (simpColor t) = sum t := by
intro t
match t with
| branch (red m) (red n) => rfl
| branch (black m) (black n) => rfl
| t1 => rw[simpColor]; split <;> rfl
```

#### David Renshaw (May 11 2023 at 21:37):

( `aesop`

also works after the `rw[simpColor]`

. I got the idea to use `split`

from `aesop?`

.)

#### David Renshaw (May 11 2023 at 21:41):

simpler:

```
theorem simpColor_eq : ∀ t : CTree, sum (simpColor t) = sum t := by
intro t
rw[simpColor]
split <;> rfl
```

#### Ryan McCorvie (May 11 2023 at 23:15):

very tricky, thank you

#### Gabin Kolly (May 12 2023 at 13:18):

It is still mysterious that we have

```
| branch _ (branch _ _) => rfl --- not accepted
| branch (branch _ _) _ => rfl --- accepted
```

Does anybody have an explanation? By the way, `| branch _ (branch _ _) => simp only [simpColor]`

works.

#### Ryan McCorvie (May 18 2023 at 07:52):

Yes, I also noticed the mysterious case works with `simp [simpColor]`

. The actual problem 8.5 has some more details, where we are evaluating over an expression tree

```
inductive Expr where
| const : Nat → Expr
| var : Nat → Expr
| plus : Expr → Expr → Expr
| times : Expr → Expr → Expr
deriving Repr
```

and the `eval`

function also takes a function `v`

which assigns values to variables. In that case, the analogous theorem looks like this:

```
theorem simpConst_eq (v : Nat → Nat)
: ∀ e : Expr, eval v (simpConst e) = eval v e := by
intro e
match e with
| const n => rfl
| var n => rfl
| plus t1 t2 => match t1, t2 with
| const _, const _ => rfl
| var n, _ => rfl
| _, var n => simp[simpConst]
| plus _ _, _ => rfl
| times _ _, _ => rfl
| _, plus _ _ => simp[simpConst]
| _, times _ _ => simp[simpConst]
| times t1 t2 => match t1, t2 with
| const _, const _ => rfl
| var n, _ => rfl
| _, var n => simp[simpConst]
| plus _ _, _ => rfl
| times _ _, _ => rfl
| _, plus _ _ => simp[simpConst]
| _, times _ _ => simp[simpConst]
```

All the lines with a `simp`

didn't work with a `rfl`

and all of those lines involving matching the right expression. So I guess there is some limitation of `rfl`

in this setup which prevents noticing the patterns on the right term?

Last updated: Dec 20 2023 at 11:08 UTC