fail to show termination for apparently smaller argument

Stream: lean4

[Xiaoning Bian]

The following code won't typecheck in Lean4:

def is_even (a : Nat) : Prop := ∃ b, a = 2 * b

inductive Evenℕ : Nat -> Type where
  | zeroEven : Evenℕ 0
  | add2Even : (n : Nat) -> Evenℕ n -> Evenℕ (Nat.succ (Nat.succ n))

theorem EE (n : Nat) (en : Evenℕ n) : is_even n := by
  induction en with
  | zeroEven => exact (Exists.intro 0
        (calc 0
         _ = 2 * 0 := by simp))
  | add2Even a en2 => exact (have aa : is_even a := EE a en2
             let ⟨w, hw⟩ := aa
             Exists.intro (w + 1)
             (calc a + 2
              _ = 2 * (w + 1) := by simp_arith ; rw[hw]))

EE fails termination check.

[Henrik Böving]

def isEven (a : Nat) : Prop := ∃ b, a = 2 * b

inductive IsEven : Nat → Prop where
| zero : IsEven 0
| add2 : IsEven n → IsEven (n + 2)

theorem EE (n : Nat) (en : IsEven n) : isEven n := by
  induction en with
  | zero => exists 0
  | add2 _ ih =>
    rcases ih with ⟨b, hb⟩
    exists b + 1
    omega

you can do it like this.

[Henrik Böving]

Or like this if you really want pattern matching:

def isEven (a : Nat) : Prop := ∃ b, a = 2 * b

inductive IsEven : Nat → Prop where
| zero : IsEven 0
| add2 : IsEven n → IsEven (n + 2)

theorem EE (n : Nat) (en : IsEven n) : isEven n := by
  match en with
  | .zero => exists 0
  | .add2 h =>
    have ih := EE _ h
    rcases ih with ⟨b, hb⟩
    exists b + 1
    omega

[Xiaoning Bian]

Thanks! it also works with "omega" replaced by "simp_arith; rw[hb]".