internlm/Lean-Github huggingface dataset:
Theorem: FinInt.add_toUint_msb
Proof state before:
sz : ℕ
n m : FinInt sz
br : Bool
r : FinInt sz
h : addfull n m = next br r
h₁ : toUint (next br r) = toUint n + toUint m
h₂ : n + m = r
⊢ toUint (n + m) =
    match next br r with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz
Tactic:
cases br <;> simp [h₂] at *
Proof state after:
case false
sz : ℕ
n m r : FinInt sz
h : addfull n m = next false r
h₁ : toUint r = toUint n + toUint m
h₂ : True
⊢ toUint r = toUint n + toUint m

case true
sz : ℕ
n m r : FinInt sz
h : addfull n m = next true r
h₂ : True
h₁ : 2 ^ sz + toUint r = toUint n + toUint m
⊢ toUint r = toUint n + toUint m - 2 ^ sz
Theorem: FinInt.add_toUint_msb
Proof state before:
case false
sz : ℕ
n m r : FinInt sz
h : addfull n m = next false r
h₁ : toUint r = toUint n + toUint m
h₂ : True
⊢ toUint r = toUint n + toUint m

case true
sz : ℕ
n m r : FinInt sz
h : addfull n m = next true r
h₂ : True
h₁ : 2 ^ sz + toUint r = toUint n + toUint m
⊢ toUint r = toUint n + toUint m - 2 ^ sz
Tactic:
. exact h₁
Proof state after:
case true
sz : ℕ
n m r : FinInt sz
h : addfull n m = next true r
h₂ : True
h₁ : 2 ^ sz + toUint r = toUint n + toUint m
⊢ toUint r = toUint n + toUint m - 2 ^ sz
Theorem: FinInt.add_toUint_msb
Proof state before:
case true
sz : ℕ
n m r : FinInt sz
h : addfull n m = next true r
h₂ : True
h₁ : 2 ^ sz + toUint r = toUint n + toUint m
⊢ toUint r = toUint n + toUint m - 2 ^ sz
Tactic:
. sorry_arith
Proof state after:
no goals
Theorem: FinInt.add_toUint_msb
Proof state before:
sz : ℕ
n m : FinInt sz
br : Bool
r : FinInt sz
h : addfull n m = next br r
h₁ : toUint (next br r) = toUint n + toUint m
⊢ n + m = r
Tactic:
simp [HAdd.hAdd, add, h]
Proof state after:
no goals
Theorem: FinInt.add_toUint_by_lt
Proof state before:
sz : ℕ
n m : FinInt sz
⊢ toUint n + toUint m < 2 ^ sz → toUint (n + m) = toUint n + toUint m
Tactic:
intros h_bound
Proof state after:
sz : ℕ
n m : FinInt sz
h_bound : toUint n + toUint m < 2 ^ sz
⊢ toUint (n + m) = toUint n + toUint m
Theorem: FinInt.add_toUint_by_lt
Proof 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]
Proof 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)
Theorem: FinInt.add_toUint_by_lt
Proof 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
Proof 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)
Theorem: FinInt.add_toUint_by_lt
Proof 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
Proof state after:
no goals
Theorem: FinInt.add_toUint_by_lt
Proof 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₁]
Proof 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)
Theorem: FinInt.add_toUint_by_lt
Proof 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₂
Proof 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)
Theorem: FinInt.add_toUint_by_lt
Proof 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]
Proof 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)
Theorem: FinInt.add_toUint_by_lt
Proof 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
Proof state after:
no goals
Theorem: FinInt.add_toUint_by_lt
Proof 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₁]
Proof state after:
no goals
Theorem: FinInt.add_toUint_rem
Proof state before:
sz : ℕ
n m : FinInt sz
⊢ toUint (n + m) = if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz
Tactic:
simp [FinInt.add_toUint_msb]
Proof state after:
sz : ℕ
n m : FinInt sz
⊢ (match addfull n m with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz) =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz
Theorem: FinInt.add_toUint_rem
Proof state before:
sz : ℕ
n m : FinInt sz
⊢ (match addfull n m with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz) =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz
Tactic:
cases h_full: addfull n m
Proof state after:
case next
sz : ℕ
n m : FinInt sz
a✝¹ : Bool
a✝ : FinInt sz
h_full : addfull n m = next a✝¹ a✝
⊢ (match next a✝¹ a✝ with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz) =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz
Theorem: FinInt.add_toUint_rem
Proof state before:
sz : ℕ
n m : FinInt sz
br : Bool
r' : FinInt sz
h_full : addfull n m = next br r'
⊢ (match next br r' with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz) =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz
Tactic:
case next br r' =>
cases br <;> simp
. have h := O_lt r'; rw [←h_full] at h
  simp [FinInt.addfull_toUint] at h; simp [h]
. have h := I_not_lt r'; rw [←h_full] at h; sorry
Proof state after:
no goals
Theorem: FinInt.add_toUint_rem
Proof state before:
sz : ℕ
n m : FinInt sz
br : Bool
r' : FinInt sz
h_full : addfull n m = next br r'
⊢ (match next br r' with
    | next false a => toUint n + toUint m
    | next true a => toUint n + toUint m - 2 ^ sz) =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz
Tactic:
cases br <;> simp
Proof state after:
case false
sz : ℕ
n m r' : FinInt sz
h_full : addfull n m = next false r'
⊢ toUint n + toUint m = if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz

case true
sz : ℕ
n m r' : FinInt sz
h_full : addfull n m = next true r'
⊢ toUint n + toUint m - 2 ^ sz =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz
Theorem: FinInt.add_toUint_rem
Proof state before:
case false
sz : ℕ
n m r' : FinInt sz
h_full : addfull n m = next false r'
⊢ toUint n + toUint m = if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz

case true
sz : ℕ
n m r' : FinInt sz
h_full : addfull n m = next true r'
⊢ toUint n + toUint m - 2 ^ sz =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz
Tactic:
. have h := O_lt r'; rw [←h_full] at h
  simp [FinInt.addfull_toUint] at h; simp [h]
Proof state after:
case true
sz : ℕ
n m r' : FinInt sz
h_full : addfull n m = next true r'
⊢ toUint n + toUint m - 2 ^ sz =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz
Theorem: FinInt.add_toUint_rem
Proof state before:
case true
sz : ℕ
n m r' : FinInt sz
h_full : addfull n m = next true r'
⊢ toUint n + toUint m - 2 ^ sz =
    if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz
Tactic:
. have h := I_not_lt r'; rw [←h_full] at h; sorry
Proof state after:
no goals
Theorem: FinInt.add_toUint
Proof state before:
sz : ℕ
n m : FinInt sz
⊢ toUint (n + m) = mod2 (toUint n + toUint m) sz
Tactic:
rw [add_toUint_rem]
Proof state after:
sz : ℕ
n m : FinInt sz
⊢ (if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz) =
    mod2 (toUint n + toUint m) sz
Theorem: FinInt.add_toUint
Proof state before:
sz : ℕ
n m : FinInt sz
⊢ (if toUint n + toUint m < 2 ^ sz then toUint n + toUint m else toUint n + toUint m - 2 ^ sz) =
    mod2 (toUint n + toUint m) sz
Tactic:
split
Proof state after:
case inl
sz : ℕ
n m : FinInt sz
h✝ : toUint n + toUint m < 2 ^ sz
⊢ toUint n + toUint m = mod2 (toUint n + toUint m) sz

case inr
sz : ℕ
n m : FinInt sz
h✝ : ¬toUint n + toUint m < 2 ^ sz
⊢ toUint n + toUint m - 2 ^ sz = mod2 (toUint n + toUint m) sz
Theorem: FinInt.add_toUint
Proof state before:
case inl
sz : ℕ
n m : FinInt sz
h✝ : toUint n + toUint m < 2 ^ sz
⊢ toUint n + toUint m = mod2 (toUint n + toUint m) sz

case inr
sz : ℕ
n m : FinInt sz
h✝ : ¬toUint n + toUint m < 2 ^ sz
⊢ toUint n + toUint m - 2 ^ sz = mod2 (toUint n + toUint m) sz
Tactic:
. simp [mod2_idem ⟨Int.add_ge_zero _ _ toUint_ge toUint_ge, by assumption⟩]
Proof state after:
case inr
sz : ℕ
n m : FinInt sz
h✝ : ¬toUint n + toUint m < 2 ^ sz
⊢ toUint n + toUint m - 2 ^ sz = mod2 (toUint n + toUint m) sz
Theorem: FinInt.add_toUint
Proof state before:
case inr
sz : ℕ
n m : FinInt sz
h✝ : ¬toUint n + toUint m < 2 ^ sz
⊢ toUint n + toUint m - 2 ^ sz = mod2 (toUint n + toUint m) sz
Tactic:
. sorry_arith
Proof state after:
no goals
Theorem: FinInt.add_toUint
Proof state before:
sz : ℕ
n m : FinInt sz
h✝ : toUint n + toUint m < 2 ^ sz
⊢ toUint ?m.152087 + toUint ?m.152089 < 2 ^ ?m.152070
Tactic:
assumption
Proof state after:
no goals
Theorem: FinInt.add_toUint_cong2
Proof state before:
sz : ℕ
n m : FinInt sz
⊢ toUint (n + m) ≡ toUint n + toUint m [2^sz]
Tactic:
simp [cong2, toUint_mod2]
Proof state after:
sz : ℕ
n m : FinInt sz
⊢ toUint (n + m) = mod2 (toUint n + toUint m) sz
Theorem: FinInt.add_toUint_cong2
Proof state before:
sz : ℕ
n m : FinInt sz
⊢ toUint (n + m) = mod2 (toUint n + toUint m) sz
Tactic:
apply add_toUint
Proof state after:
no goals
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
n m : FinInt (sz + 1)
⊢ toSint (n + m) =
    match n, m with
    | next false n', next false m' =>
      match n + m with
      | next false a => toSint n + toSint m
      | next true a => toSint n + toSint m - 2 ^ (sz + 1)
    | next false n', next true m' => toSint n + toSint m
    | next true n', next false m' => toSint n + toSint m
    | next true n', next true m' =>
      match n + m with
      | next false a => toSint n + toSint m + 2 ^ (sz + 1)
      | next true a => toSint n + toSint m
Tactic:
have h := addfull_toSint n m
Proof state after:
sz : ℕ
n m : FinInt (sz + 1)
h :
  toSint (addfull n m) =
    match n, m with
    | next false n', next false m' => toSint n + toSint m
    | next false n', next true m' =>
      match addfull n m with
      | next false a => toSint n + toSint m + 2 ^ (sz + 1)
      | next true a => toSint n + toSint m - 2 ^ (sz + 1)
    | next true n', next false m' =>
      match addfull n m with
      | next false a => toSint n + toSint m + 2 ^ (sz + 1)
      | next true a => toSint n + toSint m - 2 ^ (sz + 1)
    | next true n', next true m' => toSint n + toSint m
⊢ toSint (n + m) =
    match n, m with
    | next false n', next false m' =>
      match n + m with
      | next false a => toSint n + toSint m
      | next true a => toSint n + toSint m - 2 ^ (sz + 1)
    | next false n', next true m' => toSint n + toSint m
    | next true n', next false m' => toSint n + toSint m
    | next true n', next true m' =>
      match n + m with
      | next false a => toSint n + toSint m + 2 ^ (sz + 1)
      | next true a => toSint n + toSint m
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
n m : FinInt (sz + 1)
h :
  toSint (addfull n m) =
    match n, m with
    | next false n', next false m' => toSint n + toSint m
    | next false n', next true m' =>
      match addfull n m with
      | next false a => toSint n + toSint m + 2 ^ (sz + 1)
      | next true a => toSint n + toSint m - 2 ^ (sz + 1)
    | next true n', next false m' =>
      match addfull n m with
      | next false a => toSint n + toSint m + 2 ^ (sz + 1)
      | next true a => toSint n + toSint m - 2 ^ (sz + 1)
    | next true n', next true m' => toSint n + toSint m
⊢ toSint (n + m) =
    match n, m with
    | next false n', next false m' =>
      match n + m with
      | next false a => toSint n + toSint m
      | next true a => toSint n + toSint m - 2 ^ (sz + 1)
    | next false n', next true m' => toSint n + toSint m
    | next true n', next false m' => toSint n + toSint m
    | next true n', next true m' =>
      match n + m with
      | next false a => toSint n + toSint m + 2 ^ (sz + 1)
      | next true a => toSint n + toSint m
Tactic:
cases n
Proof state after:
case next
sz : ℕ
m : FinInt (sz + 1)
a✝¹ : Bool
a✝ : FinInt sz
h :
  toSint (addfull (next a✝¹ a✝) m) =
    match next a✝¹ a✝, m with
    | next false n', next false m' => toSint (next a✝¹ a✝) + toSint m
    | next false n', next true m' =>
      match addfull (next a✝¹ a✝) m with
      | next false a => toSint (next a✝¹ a✝) + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next a✝¹ a✝) + toSint m - 2 ^ (sz + 1)
    | next true n', next false m' =>
      match addfull (next a✝¹ a✝) m with
      | next false a => toSint (next a✝¹ a✝) + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next a✝¹ a✝) + toSint m - 2 ^ (sz + 1)
    | next true n', next true m' => toSint (next a✝¹ a✝) + toSint m
⊢ toSint (next a✝¹ a✝ + m) =
    match next a✝¹ a✝, m with
    | next false n', next false m' =>
      match next a✝¹ a✝ + m with
      | next false a => toSint (next a✝¹ a✝) + toSint m
      | next true a => toSint (next a✝¹ a✝) + toSint m - 2 ^ (sz + 1)
    | next false n', next true m' => toSint (next a✝¹ a✝) + toSint m
    | next true n', next false m' => toSint (next a✝¹ a✝) + toSint m
    | next true n', next true m' =>
      match next a✝¹ a✝ + m with
      | next false a => toSint (next a✝¹ a✝) + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next a✝¹ a✝) + toSint m
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
m : FinInt (sz + 1)
bn : Bool
n' : FinInt sz
h :
  toSint (addfull (next bn n') m) =
    match next bn n', m with
    | next false n'_1, next false m' => toSint (next bn n') + toSint m
    | next false n'_1, next true m' =>
      match addfull (next bn n') m with
      | next false a => toSint (next bn n') + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint m - 2 ^ (sz + 1)
    | next true n'_1, next false m' =>
      match addfull (next bn n') m with
      | next false a => toSint (next bn n') + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint m - 2 ^ (sz + 1)
    | next true n'_1, next true m' => toSint (next bn n') + toSint m
⊢ toSint (next bn n' + m) =
    match next bn n', m with
    | next false n'_1, next false m' =>
      match next bn n' + m with
      | next false a => toSint (next bn n') + toSint m
      | next true a => toSint (next bn n') + toSint m - 2 ^ (sz + 1)
    | next false n'_1, next true m' => toSint (next bn n') + toSint m
    | next true n'_1, next false m' => toSint (next bn n') + toSint m
    | next true n'_1, next true m' =>
      match next bn n' + m with
      | next false a => toSint (next bn n') + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint m
Tactic:
case next bn n' =>
cases m; case next bm m' =>
cases bn <;> cases bm <;> simp [addfull] at *
case false.false =>
match h': addfull n' m' with
| .next br r =>
rw [h'] at h
cases br <;> simp [bne, toSint] at * <;> sorry_arith
case false.true =>
match h': addfull n' m' with
| .next br r =>
rw [h'] at h
cases br <;> simp [bne, BEq.beq, toSint] at * <;> sorry_arith
case true.false =>
match h': addfull n' m' with
| .next br r =>
rw [h'] at h
cases br <;> simp [bne, BEq.beq, toSint] at * <;> sorry_arith
case true.true =>
match h': addfull n' m' with
| .next br r =>
rw [h'] at h
cases br <;> simp [bne, toSint] at * <;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
m : FinInt (sz + 1)
bn : Bool
n' : FinInt sz
h :
  toSint (addfull (next bn n') m) =
    match next bn n', m with
    | next false n'_1, next false m' => toSint (next bn n') + toSint m
    | next false n'_1, next true m' =>
      match addfull (next bn n') m with
      | next false a => toSint (next bn n') + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint m - 2 ^ (sz + 1)
    | next true n'_1, next false m' =>
      match addfull (next bn n') m with
      | next false a => toSint (next bn n') + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint m - 2 ^ (sz + 1)
    | next true n'_1, next true m' => toSint (next bn n') + toSint m
⊢ toSint (next bn n' + m) =
    match next bn n', m with
    | next false n'_1, next false m' =>
      match next bn n' + m with
      | next false a => toSint (next bn n') + toSint m
      | next true a => toSint (next bn n') + toSint m - 2 ^ (sz + 1)
    | next false n'_1, next true m' => toSint (next bn n') + toSint m
    | next true n'_1, next false m' => toSint (next bn n') + toSint m
    | next true n'_1, next true m' =>
      match next bn n' + m with
      | next false a => toSint (next bn n') + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint m
Tactic:
cases m
Proof state after:
case next
sz : ℕ
bn : Bool
n' : FinInt sz
a✝¹ : Bool
a✝ : FinInt sz
h :
  toSint (addfull (next bn n') (next a✝¹ a✝)) =
    match next bn n', next a✝¹ a✝ with
    | next false n'_1, next false m' => toSint (next bn n') + toSint (next a✝¹ a✝)
    | next false n'_1, next true m' =>
      match addfull (next bn n') (next a✝¹ a✝) with
      | next false a => toSint (next bn n') + toSint (next a✝¹ a✝) + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint (next a✝¹ a✝) - 2 ^ (sz + 1)
    | next true n'_1, next false m' =>
      match addfull (next bn n') (next a✝¹ a✝) with
      | next false a => toSint (next bn n') + toSint (next a✝¹ a✝) + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint (next a✝¹ a✝) - 2 ^ (sz + 1)
    | next true n'_1, next true m' => toSint (next bn n') + toSint (next a✝¹ a✝)
⊢ toSint (next bn n' + next a✝¹ a✝) =
    match next bn n', next a✝¹ a✝ with
    | next false n'_1, next false m' =>
      match next bn n' + next a✝¹ a✝ with
      | next false a => toSint (next bn n') + toSint (next a✝¹ a✝)
      | next true a => toSint (next bn n') + toSint (next a✝¹ a✝) - 2 ^ (sz + 1)
    | next false n'_1, next true m' => toSint (next bn n') + toSint (next a✝¹ a✝)
    | next true n'_1, next false m' => toSint (next bn n') + toSint (next a✝¹ a✝)
    | next true n'_1, next true m' =>
      match next bn n' + next a✝¹ a✝ with
      | next false a => toSint (next bn n') + toSint (next a✝¹ a✝) + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint (next a✝¹ a✝)
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
bn : Bool
n' : FinInt sz
bm : Bool
m' : FinInt sz
h :
  toSint (addfull (next bn n') (next bm m')) =
    match next bn n', next bm m' with
    | next false n'_1, next false m'_1 => toSint (next bn n') + toSint (next bm m')
    | next false n'_1, next true m'_1 =>
      match addfull (next bn n') (next bm m') with
      | next false a => toSint (next bn n') + toSint (next bm m') + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint (next bm m') - 2 ^ (sz + 1)
    | next true n'_1, next false m'_1 =>
      match addfull (next bn n') (next bm m') with
      | next false a => toSint (next bn n') + toSint (next bm m') + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint (next bm m') - 2 ^ (sz + 1)
    | next true n'_1, next true m'_1 => toSint (next bn n') + toSint (next bm m')
⊢ toSint (next bn n' + next bm m') =
    match next bn n', next bm m' with
    | next false n'_1, next false m'_1 =>
      match next bn n' + next bm m' with
      | next false a => toSint (next bn n') + toSint (next bm m')
      | next true a => toSint (next bn n') + toSint (next bm m') - 2 ^ (sz + 1)
    | next false n'_1, next true m'_1 => toSint (next bn n') + toSint (next bm m')
    | next true n'_1, next false m'_1 => toSint (next bn n') + toSint (next bm m')
    | next true n'_1, next true m'_1 =>
      match next bn n' + next bm m' with
      | next false a => toSint (next bn n') + toSint (next bm m') + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint (next bm m')
Tactic:
case next bm m' =>
cases bn <;> cases bm <;> simp [addfull] at *
case false.false =>
match h': addfull n' m' with
| .next br r =>
rw [h'] at h
cases br <;> simp [bne, toSint] at * <;> sorry_arith
case false.true =>
match h': addfull n' m' with
| .next br r =>
rw [h'] at h
cases br <;> simp [bne, BEq.beq, toSint] at * <;> sorry_arith
case true.false =>
match h': addfull n' m' with
| .next br r =>
rw [h'] at h
cases br <;> simp [bne, BEq.beq, toSint] at * <;> sorry_arith
case true.true =>
match h': addfull n' m' with
| .next br r =>
rw [h'] at h
cases br <;> simp [bne, toSint] at * <;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
n' m' : FinInt sz
h :
  toSint
      (match addfull n' m' with
      | next false r => next false (next false r)
      | next true r => next false (next true r)) =
    toSint (next false n') + toSint (next false m')
⊢ toSint (next false n' + next false m') =
    match next false n' + next false m' with
    | next false a => toSint (next false n') + toSint (next false m')
    | next true a => toSint (next false n') + toSint (next false m') - 2 ^ (sz + 1)
Tactic:
case false.false =>
  match h': addfull n' m' with
  | .next br r =>
    rw [h'] at h
    cases br <;> simp [bne, toSint] at * <;> sorry_arith
Proof state after:
no goals