How to eliminate dependent pattern matchings?

Stream: lean4

[Ryan Lahfa]

Given the following example:

inductive Tree (T: Type) where
| none : Tree T
| some : T → Tree T → Tree T → Tree T

#reduce Tree.some (Tree.none) (Tree.none)

def height (t: Tree T): Nat := match t with
| .none => 0
| .some _ left right => 1 + max (height left) (height right)

structure WeirdT {T U: Type} where
  left: Tree T
  right: Tree T
  c: Nat
  x: height left + height right = c
  y: Nat

def weird_fun {U: Type} (t: Tree T): Tree (@WeirdT T U) :=
  match t with
  | .none => Tree.none
  | .some _ left right => match Hbf : (height left) + (height right) with
    | 1 => Tree.some (WeirdT.mk _ _ _ Hbf 0) .none .none
    | 2 => Tree.some (WeirdT.mk _ _ _ Hbf 1) .none .none
    | 3 => Tree.some (WeirdT.mk _ _ _ Hbf 2) .none .none
    | 4 => Tree.some (WeirdT.mk _ _ _ Hbf 3) .none .none
    | _ => Tree.none

example {left right: Tree T} (Hbf: height left + height right = 0): Tree.some (WeirdT.mk left right 0 Hbf 0) t u = weird_fun (Tree.some n (Tree.none) (Tree.none)) := by
  simp [weird_fun]
  -- Here, `split` can be used, but is there a way to eliminate directly the right branch?

I know that split + rename_i / case can be used to go through a dependent pattern matching, but in my code, I have multiple nested dependent pattern matchings and split makes the proof much more verbose (slower?).

Am I missing a trick here?

[Markus Himmel]

simp and dsimp are aware of match, so you can make progress with dsimp [height] in your case. Is that what you're looking for?

[Damiano Testa]

Or simply using

@[simp] def height (t: Tree T): Nat := match t with

[Ryan Lahfa]

@Markus Himmel Not really, because in my non-MWE, all that's doing is just unfolding a mutually recursive definition and I'm not sure this creates progress, but I see why this MWE makes it appear as the solution.

[Ryan Lahfa]

Here's an updated MWE where dsimp/simp doesn't seem to work to me:

inductive Tree (T: Type) where
| mk : T → Option (Tree T) → Option (Tree T) → Tree T

#reduce Tree.mk (Option.none) (Option.none)

mutual
def height (t: Option (Tree T)): Nat := match t with
| .none => 0
| .some t => height_node t
def height_node (t: Tree T): Nat := match t with
| .mk _ left right => 1 + max (height left) (height right)
end

structure WeirdT {T U: Type} where
  left: Option (Tree T)
  right: Option (Tree T)
  c: Nat
  x: height left + height right = c
  y: Nat

def weird_fun {U: Type} (t: Option (Tree T)): Option (Tree (@WeirdT T U)) :=
  match t with
  | .none => Option.none
  | .some (Tree.mk _ left right) => match Hbf : (height left) + (height right) with
    | 1 => .some $ Tree.mk (WeirdT.mk _ _ _ Hbf 0) .none .none
    | 2 => .some $ Tree.mk (WeirdT.mk _ _ _ Hbf 1) .none .none
    | 3 => .some $ Tree.mk (WeirdT.mk _ _ _ Hbf 2) .none .none
    | 4 => .some $ Tree.mk (WeirdT.mk _ _ _ Hbf 3) .none .none
    | _ => Option.none

example {left right: Option (Tree T)} (Hbf: height left + height right = 1): Option.some (Tree.mk (WeirdT.mk left right 1 Hbf 0) t u) = weird_fun (.some $ .mk n left right) := by
  simp [weird_fun]
  dsimp [height] -- shows a mutual defn
  simp [height] -- makes no progress
  simp [Hbf]

[Jakob von Raumer]

Try split

[Ryan Lahfa]

Jakob von Raumer said:

Try split

Yes but this is what I want to avoid :P