pattern matching default

Stream: lean4

[Lev Stambler]

I am working on the Induction and Recursion exercises. I am stuck on concisely proving simpConst_eq. Specifically, I want the pattern match (where I have sorry right now) to be proved with a simple refl considering that the plus and times case has already been pattern matched.

def simpConst : Expr → Expr
  | plus (const n₁) (const n₂)  => const (n₁ + n₂)
  | times (const n₁) (const n₂) => const (n₁ * n₂)
  | e                           => e

theorem simpConst_eq (v : Nat → Nat)
        : ∀ e : Expr, eval v (simpConst e) = eval v e := by
    intro e
    -- apply simpConst_eq_exp
    simp [simpConst, eval]
    match e with
    | plus (const n₁) (const n₂)  => rfl
    | times (const n₁) (const n₂) => rfl
    | e => sorry

[Sebastian Ullrich]

There is nothing in the type theory to directly express that e is of any shape but the first two cases, especially not one that would make the match reduce. So you have to exhaustively list all cases, though if you want tactics to do that for you, you could try something like unfold simpConst; split instead of the match

[Lev Stambler]

Sebastian Ullrich said:

There is nothing in the type theory to directly express that e is of any shape but the first two cases, especially not one that would make the match reduce. So you have to exhaustively list all cases, though if you want tactics to do that for you, you could try something like unfold simpConst; split instead of the match

Thank you! This was exactly what I was looking for.