Matching a conditional in a theorem

Stream: lean4

[Brandon Brown]

Related to the discussion in the other Lean4 topic "Alternative Int Hierarchy," I took the following custom int type:

inductive int : Type where
| zero : int
| pos_succ : Nat → int
| neg_succ : Nat → int

And "embedded" it into the natural numbers type, or rather, I made a bijective map between this integer type and the natural number type, and defined an addition function over these integers-as-naturals such that the integers become well-ordered as 0,-1,1,-2,2,-3,3 ...
This way I do not have to deal with the 3 constructors causing case-explosion and can write functions using the two constructor natural number type and map back into my int type representation. (This is totally not for anything practical and just for intellectual curiosity and learning lean.)

So my question is, my add function involves a conditional and I realize I don't know how to deal with these when proving theorems about a function with a conditional. The blah1 theorem should be true by definition if the number is_even. Here's a MWE with the theorem I'd like to prove at the bottom.

open Nat

inductive int : Type where
| zero : int
| pos_succ : Nat → int
| neg_succ : Nat → int

open int

def double (n : Nat) : Nat := 2 * n
def halve (n : Nat) : Nat := n / 2
def is_even (n : Nat) : Bool := do
  let y := Nat.mod n 2
  return if y = 0 then true else false

def int_to_Nat' (j : int) : Nat :=
  match j with
  | int.zero => 0
  | pos_succ j =>
    match j with
    | 0 => 2
    | succ j =>
      double (j+2)
  | neg_succ j =>
    match j with
    | 0 => 1
    | succ j => (double (j+2)) - 1
-- 0  1 2  3 4  5 6  7 8
-- 0,-1,1,-2,2,-3,3,-4,4 ...
/-
the even numbers are positive integers
the odd numbers are negative integers
-/
def Nat_to_int' (n : Nat) : int :=
  match n with
  | 0 => int.zero
  | (n+1) => do
    if is_even n then
      let x := (halve n)
      return neg_succ (x)
    else
      let x := (halve (n + 1)) - 1
      return pos_succ (x)

#reduce Nat_to_int' 6

def int_as_Nat_incr (n : Nat) : Nat :=
  match n with
  | 0 => 2
  | (n+1) =>
    if is_even n then -- if negative
      return n - 1
    else -- if positive
      return (n+3)

#reduce int_as_Nat_incr 5

def int_as_Nat_decr (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | (n + 1) =>
    if is_even n then -- if negative
      return (n + 3)
    else -- if positive
      return (n - 1)

#reduce int_as_Nat_decr 1

def add_ian (n m : Nat) : Nat :=
  match n with
  | 0 => m
  | 1 => int_as_Nat_decr m
  | succ (succ n) =>
    if is_even n then -- `n` is positive
      int_as_Nat_incr (add_ian n m)
    else -- `n` is negative
      int_as_Nat_decr (add_ian n m)

-- 0,-1,1,-2,2,-3,3
-- (1 : Nat) = (-1 : int)
#reduce add_ian 2 3 -- 1

def add'' (j k : int) : int :=
  Nat_to_int' (add_ian (int_to_Nat' j) (int_to_Nat' k))

instance : Add int where
  add := add''

def i1 : int := neg_succ 2 -- -3
def i2 : int := pos_succ 3 -- +4

#reduce i1 + i2 -- pos_succ 0

infixl:65 " +₁ " => add_ian

-- How do I match the `is_even n` case?
theorem blah1 : ∀ n m : Nat, is_even n → ((n+2) +₁ m) = int_as_Nat_incr (n +₁ m) := sorry

[Chris B]

It looks like that syntax of passing a bool elaborates to (b = true) by default.

theorem blah1 : ∀ n m : Nat, is_even n → ((n+2) +₁ m) = int_as_Nat_incr (n +₁ m) := by
intro n m h_even
cases m
simp [h_even, Nat.add, add_ian]
simp [h_even, Nat.add, add_ian]

[Brandon Brown]

Oh thanks! - I definitely tried starting out with intros and cases not sure where I went wrong; I did a lot of refactoring so might've just messed up something along the way

[Brandon Brown]

Actually that was the wrong question, I was actually having issues proving this because I don't know how to do cases on is_even

theorem add_zero : ∀ n : Nat, n +₁ 0 = n :=
  fun n =>
    match n with
    | 0 => rfl
    | 1 => rfl
    | (n+2) =>
      if is_even n then -- is positive
        sorry
      else
        sorry

I don't know how to get access to the proof is_even n in each branch

[Chris B]

There might be a cool new lean4 way of doing it, but the lean3 way still works, you have to name the hypothesis in the if case, and the negated one is then available under the same name in the else case.

theorem add_zero : ∀ n : Nat, n +₁ 0 = n :=
  fun n =>
    match n with
    | 0 => rfl
    | 1 => rfl
    | (n+2) =>
      if h_even : is_even n then
      _
      else
      _

[Brandon Brown]

Hmm I swear I tried that, but thanks again. Why doesn't this seem to work in tactic mode?

[Chris B]

I know very little about Lean 4's tactic mode, but I would assume just because it's not directly a tactic; you would have to preface it with exact or something. In tactic mode it looks like byCases h_ev: is_even n and cases h_ev: is_even n will both get you into a similar position. Lean 4 is also whitespace sensitive in some places, so you may have run afoul of that somewhere.