Theorem: FinInt.add_toUint_by_lt (MLIR/Util/FinInt.lean)

State before:
sz : ℕ
n m : FinInt sz
⊢ toUint n + toUint m < 2 ^ sz → toUint (n + m) = toUint n + toUint m
Tactic:
intros h_bound
State after:
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
⊢ toUint (n + m) = toUint n + toUint m

State before:
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
⊢ toUint (n + m) = toUint n + toUint m
Tactic:
simp [HAdd.hAdd, FinInt.add, FinInt.addfull_toUint]
State after:
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
⊢ toUint
      (match addfull n m with
      | next carry n => n) =
    Add.add (toUint n) (toUint m)

State before:
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
⊢ toUint
      (match addfull n m with
      | next carry n => n) =
    Add.add (toUint n) (toUint m)
Tactic:
cases h₁: addfull n m
State after:
case next
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
a✝¹ : Bool
a✝ : FinInt sz
h₁ : addfull n m = next a✝¹ a✝
⊢ toUint
      (match next a✝¹ a✝ with
      | next carry n => n) =
    Add.add (toUint n) (toUint m)

State before:
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
carry : Bool
r : FinInt sz
h₁ : addfull n m = next carry r
⊢ toUint
      (match next carry r with
      | next carry n => n) =
    Add.add (toUint n) (toUint m)
Tactic:
case next carry r =>
  have h₂: (addfull n m).toUint = (next carry r).toUint := by simp [h₁]
  cases carry <;> simp at h₂
  . simp [←h₂, FinInt.addfull_toUint, HAdd.hAdd]
  . simp [FinInt.addfull_toUint] at h₂
    rw [h₂] at h_bound
    sorry_arith
State after:
no goals

State before:
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
carry : Bool
r : FinInt sz
h₁ : addfull n m = next carry r
⊢ toUint
      (match next carry r with
      | next carry n => n) =
    Add.add (toUint n) (toUint m)
Tactic:
have h₂: (addfull n m).toUint = (next carry r).toUint := by simp [h₁]
State after:
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
carry : Bool
r : FinInt sz
h₁ : addfull n m = next carry r
h₂ : toUint (addfull n m) = toUint (next carry r)
⊢ toUint
      (match next carry r with
      | next carry n => n) =
    Add.add (toUint n) (toUint m)

State before:
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
carry : Bool
r : FinInt sz
h₁ : addfull n m = next carry r
h₂ : toUint (addfull n m) = toUint (next carry r)
⊢ toUint
      (match next carry r with
      | next carry n => n) =
    Add.add (toUint n) (toUint m)
Tactic:
cases carry <;> simp at h₂
State after:
case false
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
r : FinInt sz
h₁ : addfull n m = next false r
h₂ : toUint (addfull n m) = toUint r
⊢ toUint
      (match next false r with
      | next carry n => n) =
    Add.add (toUint n) (toUint m)

case true
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
r : FinInt sz
h₁ : addfull n m = next true r
h₂ : toUint (addfull n m) = 2 ^ sz + toUint r
⊢ toUint
      (match next true r with
      | next carry n => n) =
    Add.add (toUint n) (toUint m)

State before:
case false
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
r : FinInt sz
h₁ : addfull n m = next false r
h₂ : toUint (addfull n m) = toUint r
⊢ toUint
      (match next false r with
      | next carry n => n) =
    Add.add (toUint n) (toUint m)

case true
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
r : FinInt sz
h₁ : addfull n m = next true r
h₂ : toUint (addfull n m) = 2 ^ sz + toUint r
⊢ toUint
      (match next true r with
      | next carry n => n) =
    Add.add (toUint n) (toUint m)
Tactic:
. simp [←h₂, FinInt.addfull_toUint, HAdd.hAdd]
State after:
case true
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
r : FinInt sz
h₁ : addfull n m = next true r
h₂ : toUint (addfull n m) = 2 ^ sz + toUint r
⊢ toUint
      (match next true r with
      | next carry n => n) =
    Add.add (toUint n) (toUint m)

State before:
case true
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
r : FinInt sz
h₁ : addfull n m = next true r
h₂ : toUint (addfull n m) = 2 ^ sz + toUint r
⊢ toUint
      (match next true r with
      | next carry n => n) =
    Add.add (toUint n) (toUint m)
Tactic:
. simp [FinInt.addfull_toUint] at h₂
  rw [h₂] at h_bound
  sorry_arith
State after:
no goals

State before:
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
carry : Bool
r : FinInt sz
h₁ : addfull n m = next carry r
⊢ toUint (addfull n m) = toUint (next carry r)
Tactic:
simp [h₁]
State after:
no goals