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

State before:
sz : ℕ
n m : FinInt (sz + 1)
⊢ 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
Tactic:
cases n
State after:
case next
sz : ℕ
m : FinInt (sz + 1)
a✝¹ : Bool
a✝ : FinInt sz
⊢ 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

State before:
sz : ℕ
m : FinInt (sz + 1)
bn : Bool
n' : FinInt sz
⊢ 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
Tactic:
case next bn n' =>
cases m; case next bm m' =>
cases bn <;> cases bm <;> simp [addfull]
case false.false =>
match h: addfull n' m' with
| .next br r =>
cases br <;> simp [toSint, ←FinInt.addfull_toUint, h]
case false.true =>
match h: addfull n' m' with
| .next br r =>
have h' := FinInt.addfull_toUint n' m'
rw [h] at h'
cases br <;> simp at h' <;> simp [toSint]
. simp [h']; sorry_arith
. sorry_arith
case true.false =>
match h: addfull n' m' with
| .next br r =>
have h' := FinInt.addfull_toUint n' m'
rw [h] at h'
cases br <;> simp at h' <;> simp [toSint]
. simp [h']; sorry_arith
. sorry_arith
case true.true =>
match h: addfull n' m' with
| .next br r =>
have h' := FinInt.addfull_toUint n' m'
rw [h] at h'
cases br <;> simp at h' <;> simp [toSint, h'] <;> sorry_arith
State after:
no goals

State before:
sz : ℕ
m : FinInt (sz + 1)
bn : Bool
n' : FinInt sz
⊢ 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
Tactic:
cases m
State after:
case next
sz : ℕ
bn : Bool
n' : FinInt sz
a✝¹ : Bool
a✝ : FinInt sz
⊢ 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✝)

State before:
sz : ℕ
bn : Bool
n' : FinInt sz
bm : Bool
m' : FinInt sz
⊢ 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')
Tactic:
case next bm m' =>
cases bn <;> cases bm <;> simp [addfull]
case false.false =>
match h: addfull n' m' with
| .next br r =>
cases br <;> simp [toSint, ←FinInt.addfull_toUint, h]
case false.true =>
match h: addfull n' m' with
| .next br r =>
have h' := FinInt.addfull_toUint n' m'
rw [h] at h'
cases br <;> simp at h' <;> simp [toSint]
. simp [h']; sorry_arith
. sorry_arith
case true.false =>
match h: addfull n' m' with
| .next br r =>
have h' := FinInt.addfull_toUint n' m'
rw [h] at h'
cases br <;> simp at h' <;> simp [toSint]
. simp [h']; sorry_arith
. sorry_arith
case true.true =>
match h: addfull n' m' with
| .next br r =>
have h' := FinInt.addfull_toUint n' m'
rw [h] at h'
cases br <;> simp at h' <;> simp [toSint, h'] <;> sorry_arith
State after:
no goals

State before:
sz : ℕ
bn : Bool
n' : FinInt sz
bm : Bool
m' : FinInt sz
⊢ 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')
Tactic:
cases bn <;> cases bm <;> simp [addfull]
State after:
case false.false
sz : ℕ
n' m' : FinInt sz
⊢ 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')

case false.true
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match addfull n' m' with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)

case true.false
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match addfull n' m' with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)

case true.true
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')

State before:
sz : ℕ
n' m' : FinInt sz
⊢ 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')
Tactic:
case false.false =>
  match h: addfull n' m' with
  | .next br r =>
    cases br <;> simp [toSint, ←FinInt.addfull_toUint, h]
State after:
no goals

State before:
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match addfull n' m' with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)
Tactic:
case false.true =>
  match h: addfull n' m' with
  | .next br r =>
    have h' := FinInt.addfull_toUint n' m'
    rw [h] at h'
    cases br <;> simp at h' <;> simp [toSint]
    . simp [h']; sorry_arith
    . sorry_arith
State after:
no goals

State before:
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match addfull n' m' with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)
Tactic:
case true.false =>
  match h: addfull n' m' with
  | .next br r =>
    have h' := FinInt.addfull_toUint n' m'
    rw [h] at h'
    cases br <;> simp at h' <;> simp [toSint]
    . simp [h']; sorry_arith
    . sorry_arith
State after:
no goals

State before:
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')
Tactic:
case true.true =>
  match h: addfull n' m' with
  | .next br r =>
    have h' := FinInt.addfull_toUint n' m'
    rw [h] at h'
    cases br <;> simp at h' <;> simp [toSint, h'] <;> sorry_arith
State after:
no goals

State before:
sz : ℕ
n' m' : FinInt sz
⊢ 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')
Tactic:
match h: addfull n' m' with
| .next br r =>
  cases br <;> simp [toSint, ←FinInt.addfull_toUint, h]
State after:
no goals

State before:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h : addfull n' m' = next br r
⊢ toSint
      (match next br r 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')
Tactic:
cases br <;> simp [toSint, ←FinInt.addfull_toUint, h]
State after:
no goals

State before:
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match addfull n' m' with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)
Tactic:
match h: addfull n' m' with
| .next br r =>
  have h' := FinInt.addfull_toUint n' m'
  rw [h] at h'
  cases br <;> simp at h' <;> simp [toSint]
  . simp [h']; sorry_arith
  . sorry_arith
State after:
no goals

State before:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h : addfull n' m' = next br r
⊢ toSint
      (match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)
Tactic:
have h' := FinInt.addfull_toUint n' m'
State after:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h : addfull n' m' = next br r
h' : toUint (addfull n' m') = toUint n' + toUint m'
⊢ toSint
      (match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)

State before:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h : addfull n' m' = next br r
h' : toUint (addfull n' m') = toUint n' + toUint m'
⊢ toSint
      (match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)
Tactic:
rw [h] at h'
State after:
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'
⊢ toSint
      (match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)

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'
⊢ toSint
      (match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)
Tactic:
cases br <;> simp at h' <;> simp [toSint]
State after:
case false
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next false r
h' : toUint r = toUint n' + toUint m'
⊢ 2 ^ sz + toUint r = toUint n' + (toUint m' - 2 ^ sz) + 2 ^ (sz + 1)

case true
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next true r
h' : 2 ^ sz + toUint r = toUint n' + toUint m'
⊢ toUint r = toUint n' + (toUint m' - 2 ^ sz)

State before:
case false
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next false r
h' : toUint r = toUint n' + toUint m'
⊢ 2 ^ sz + toUint r = toUint n' + (toUint m' - 2 ^ sz) + 2 ^ (sz + 1)

case true
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next true r
h' : 2 ^ sz + toUint r = toUint n' + toUint m'
⊢ toUint r = toUint n' + (toUint m' - 2 ^ sz)
Tactic:
. simp [h']; sorry_arith
State after:
case true
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next true r
h' : 2 ^ sz + toUint r = toUint n' + toUint m'
⊢ toUint r = toUint n' + (toUint m' - 2 ^ sz)

State before:
case true
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next true r
h' : 2 ^ sz + toUint r = toUint n' + toUint m'
⊢ toUint r = toUint n' + (toUint m' - 2 ^ sz)
Tactic:
. sorry_arith
State after:
no goals

State before:
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match addfull n' m' with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)
Tactic:
match h: addfull n' m' with
| .next br r =>
  have h' := FinInt.addfull_toUint n' m'
  rw [h] at h'
  cases br <;> simp at h' <;> simp [toSint]
  . simp [h']; sorry_arith
  . sorry_arith
State after:
no goals

State before:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h : addfull n' m' = next br r
⊢ toSint
      (match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)
Tactic:
have h' := FinInt.addfull_toUint n' m'
State after:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h : addfull n' m' = next br r
h' : toUint (addfull n' m') = toUint n' + toUint m'
⊢ toSint
      (match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)

State before:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h : addfull n' m' = next br r
h' : toUint (addfull n' m') = toUint n' + toUint m'
⊢ toSint
      (match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)
Tactic:
rw [h] at h'
State after:
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'
⊢ toSint
      (match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)

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'
⊢ toSint
      (match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)
Tactic:
cases br <;> simp at h' <;> simp [toSint]
State after:
case false
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next false r
h' : toUint r = toUint n' + toUint m'
⊢ 2 ^ sz + toUint r = toUint n' - 2 ^ sz + toUint m' + 2 ^ (sz + 1)

case true
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next true r
h' : 2 ^ sz + toUint r = toUint n' + toUint m'
⊢ toUint r = toUint n' - 2 ^ sz + toUint m'

State before:
case false
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next false r
h' : toUint r = toUint n' + toUint m'
⊢ 2 ^ sz + toUint r = toUint n' - 2 ^ sz + toUint m' + 2 ^ (sz + 1)

case true
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next true r
h' : 2 ^ sz + toUint r = toUint n' + toUint m'
⊢ toUint r = toUint n' - 2 ^ sz + toUint m'
Tactic:
. simp [h']; sorry_arith
State after:
case true
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next true r
h' : 2 ^ sz + toUint r = toUint n' + toUint m'
⊢ toUint r = toUint n' - 2 ^ sz + toUint m'

State before:
case true
sz : ℕ
n' m' r : FinInt sz
h : addfull n' m' = next true r
h' : 2 ^ sz + toUint r = toUint n' + toUint m'
⊢ toUint r = toUint n' - 2 ^ sz + toUint m'
Tactic:
. sorry_arith
State after:
no goals

State before:
sz : ℕ
n' m' : FinInt sz
⊢ toSint
      (match addfull n' m' with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')
Tactic:
match h: addfull n' m' with
| .next br r =>
  have h' := FinInt.addfull_toUint n' m'
  rw [h] at h'
  cases br <;> simp at h' <;> simp [toSint, h'] <;> sorry_arith
State after:
no goals

State before:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h : addfull n' m' = next br r
⊢ toSint
      (match next br r with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')
Tactic:
have h' := FinInt.addfull_toUint n' m'
State after:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h : addfull n' m' = next br r
h' : toUint (addfull n' m') = toUint n' + toUint m'
⊢ toSint
      (match next br r with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')

State before:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h : addfull n' m' = next br r
h' : toUint (addfull n' m') = toUint n' + toUint m'
⊢ toSint
      (match next br r with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')
Tactic:
rw [h] at h'
State after:
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'
⊢ toSint
      (match next br r with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')

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'
⊢ toSint
      (match next br r with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')
Tactic:
cases br <;> simp at h' <;> simp [toSint, h'] <;> sorry_arith
State after:
no goals