TPIL4 problem 8.5

Stream: new members

[Ryan McCorvie]

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]

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]

( aesop also works after the rw[simpColor]. I got the idea to use split from aesop?.)

[David Renshaw]

simpler:

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

[Ryan McCorvie]

very tricky, thank you

[Gabin Kolly]

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]

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?