Don't pattern match on composed constructors?

Stream: lean4

[Brandon Brown]

I've written an integer type as a subtype of a "pre-integer" base type based on whether the base int is in an acceptable normal form.
Now I'm trying to prove things about my is_norm function, e.g. that a base int of the form succ^n pred is in normal form according to is_norm. I've defined two versions of the is_norm predicate, the first was what first came to mind, but it was seemingly impossible to prove that is_norm (succ^n pred) = true whereas redefining the function using nested functions made it straightforward. Is the lesson here that I should always avoid defining functions that use pattern matching on composed constructors, e.g. succ (pred a) because the resulting proofs are extremely difficult or is there an equally easy proof using my first is_norm function that's just not obvious to me?

MWE:

inductive b_int : Type
| zero : b_int
| succ : b_int → b_int
| pred : b_int → b_int

open b_int

-- Initial version, very straightforward definition
def is_norm (a : b_int) : Bool :=
match a with
| zero => true
| succ (pred a) => false
| pred (succ a) => false
| succ a => is_norm a
| pred a => is_norm a

-- More elaborate, but ends up making proof way easier?
def is_norm'' (a : b_int) : Bool :=
match a with
| zero => true
| succ a => isSucc a
| pred a => isPred a
  where
  isSucc (b : b_int) : Bool :=
  match b with
  | pred b => false
  | zero => true
  | succ b => isSucc b
  isPred (c : b_int) : Bool :=
  match c with
  | succ c => false
  | zero => true
  | pred c => isPred c

def int := {x : b_int // is_norm x}

-- This is to define a b_int that only uses either succ or pred repeatedly
def fun_pow {α : Type _} (f : α → α) (n : Nat) (a : α) : α :=
  match n with
  | 0 => a
  | (n+1) => f (fun_pow f n a)

#reduce fun_pow b_int.succ 5 zero -- succ (succ (succ (succ (succ zero))))

example : is_norm (zero.pred.succ.succ) = false := by rfl

theorem fun_pow_succ_n {n : Nat} : fun_pow succ n.succ zero = succ (fun_pow succ n zero) := rfl

-- Fairly easy to prove with is_norm''
theorem succ_n_is_norm {n : Nat} : is_norm'' (fun_pow succ n zero) = true := by
  induction n with
  | zero => rfl
  | succ n c =>
    rw [fun_pow_succ_n]
    have z₁ : is_norm'' (succ (fun_pow succ n zero)) = is_norm''.isSucc (fun_pow succ n zero) from rfl
    rw [z₁]
    induction n with
    | zero => rfl
    | succ l m =>
      rw [fun_pow_succ_n]
      have z₂ : is_norm''.isSucc (succ (fun_pow succ l zero)) = is_norm''.isSucc (fun_pow succ l zero) from rfl
      rw [z₂];
      assumption

-- I have no idea how to prove with the first is_norm:
theorem succ_n_is_norm2 {n : Nat} : is_norm (fun_pow succ n zero) = true := sorry

[Sebastian Ullrich]

You just have to do sufficient case splits until the is_norm case is uniquely determined

theorem succ_n_is_norm2 {n : Nat} : is_norm (fun_pow succ n zero) = true := by
  induction n with
  | zero => rfl
  | succ n ih =>
    cases n with
    | zero => rfl
    | succ n => exact ih

[Brandon Brown]

Thank you!