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

State before:
sz : ℕ
n m : FinInt (sz + 1)
⊢ (addv n m).snd = false → toSint (addv n m).fst = toSint n + toSint m
Tactic:
intros h_nov
State after:
sz : ℕ
n m : FinInt (sz + 1)
h_nov : (addv n m).snd = false
⊢ toSint (addv n m).fst = toSint n + toSint m

State before:
sz : ℕ
n m : FinInt (sz + 1)
h_nov : (addv n m).snd = false
⊢ toSint (addv n m).fst = toSint n + toSint m
Tactic:
simp [addv] at *
State after:
sz : ℕ
n m : FinInt (sz + 1)
h_nov :
  (match n, m with
      | next false n', next false m' =>
        match n + m with
        | next msb r' => (next msb r', msb)
      | next true n', next true m' =>
        match n + m with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (n + m, false)).snd =
    false
⊢ toSint
      (match n, m with
        | next false n', next false m' =>
          match n + m with
          | next msb r' => (next msb r', msb)
        | next true n', next true m' =>
          match n + m with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (n + m, false)).fst =
    toSint n + toSint m

State before:
sz : ℕ
n m : FinInt (sz + 1)
h_nov :
  (match n, m with
      | next false n', next false m' =>
        match n + m with
        | next msb r' => (next msb r', msb)
      | next true n', next true m' =>
        match n + m with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (n + m, false)).snd =
    false
⊢ toSint
      (match n, m with
        | next false n', next false m' =>
          match n + m with
          | next msb r' => (next msb r', msb)
        | next true n', next true m' =>
          match n + m with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (n + m, false)).fst =
    toSint n + toSint m
Tactic:
have h := add_toSint_msb n m
State after:
sz : ℕ
n m : FinInt (sz + 1)
h_nov :
  (match n, m with
      | next false n', next false m' =>
        match n + m with
        | next msb r' => (next msb r', msb)
      | next true n', next true m' =>
        match n + m with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (n + m, false)).snd =
    false
h :
  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
⊢ toSint
      (match n, m with
        | next false n', next false m' =>
          match n + m with
          | next msb r' => (next msb r', msb)
        | next true n', next true m' =>
          match n + m with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (n + m, false)).fst =
    toSint n + toSint m

State before:
sz : ℕ
n m : FinInt (sz + 1)
h_nov :
  (match n, m with
      | next false n', next false m' =>
        match n + m with
        | next msb r' => (next msb r', msb)
      | next true n', next true m' =>
        match n + m with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (n + m, false)).snd =
    false
h :
  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
⊢ toSint
      (match n, m with
        | next false n', next false m' =>
          match n + m with
          | next msb r' => (next msb r', msb)
        | next true n', next true m' =>
          match n + m with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (n + m, false)).fst =
    toSint n + toSint m
Tactic:
cases n
State after:
case next
sz : ℕ
m : FinInt (sz + 1)
a✝¹ : Bool
a✝ : FinInt sz
h_nov :
  (match next a✝¹ a✝, m with
      | next false n', next false m' =>
        match next a✝¹ a✝ + m with
        | next msb r' => (next msb r', msb)
      | next true n', next true m' =>
        match next a✝¹ a✝ + m with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (next a✝¹ a✝ + m, false)).snd =
    false
h :
  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
⊢ toSint
      (match next a✝¹ a✝, m with
        | next false n', next false m' =>
          match next a✝¹ a✝ + m with
          | next msb r' => (next msb r', msb)
        | next true n', next true m' =>
          match next a✝¹ a✝ + m with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (next a✝¹ a✝ + m, false)).fst =
    toSint (next a✝¹ a✝) + toSint m

State before:
sz : ℕ
m : FinInt (sz + 1)
dn : Bool
n' : FinInt sz
h_nov :
  (match next dn n', m with
      | next false n'_1, next false m' =>
        match next dn n' + m with
        | next msb r' => (next msb r', msb)
      | next true n'_1, next true m' =>
        match next dn n' + m with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (next dn n' + m, false)).snd =
    false
h :
  toSint (next dn n' + m) =
    match next dn n', m with
    | next false n'_1, next false m' =>
      match next dn n' + m with
      | next false a => toSint (next dn n') + toSint m
      | next true a => toSint (next dn n') + toSint m - 2 ^ (sz + 1)
    | next false n'_1, next true m' => toSint (next dn n') + toSint m
    | next true n'_1, next false m' => toSint (next dn n') + toSint m
    | next true n'_1, next true m' =>
      match next dn n' + m with
      | next false a => toSint (next dn n') + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next dn n') + toSint m
⊢ toSint
      (match next dn n', m with
        | next false n'_1, next false m' =>
          match next dn n' + m with
          | next msb r' => (next msb r', msb)
        | next true n'_1, next true m' =>
          match next dn n' + m with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (next dn n' + m, false)).fst =
    toSint (next dn n') + toSint m
Tactic:
case next dn n' =>
cases m; case next dm m' =>
cases dn <;> cases dm <;> simp [h] at *
case false.false =>
match h: next false n' + next false m' with
| .next br r =>
rw [h] at h_nov
cases br <;> simp at *
rw [←h]; simp [add_toSint_msb]; simp [h]
case true.true =>
match h: next true n' + next true m' with
| .next br r =>
rw [h] at h_nov
cases br <;> simp at *
rw [←h]; simp [add_toSint_msb]; simp [h]
State after:
no goals

State before:
sz : ℕ
m : FinInt (sz + 1)
dn : Bool
n' : FinInt sz
h_nov :
  (match next dn n', m with
      | next false n'_1, next false m' =>
        match next dn n' + m with
        | next msb r' => (next msb r', msb)
      | next true n'_1, next true m' =>
        match next dn n' + m with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (next dn n' + m, false)).snd =
    false
h :
  toSint (next dn n' + m) =
    match next dn n', m with
    | next false n'_1, next false m' =>
      match next dn n' + m with
      | next false a => toSint (next dn n') + toSint m
      | next true a => toSint (next dn n') + toSint m - 2 ^ (sz + 1)
    | next false n'_1, next true m' => toSint (next dn n') + toSint m
    | next true n'_1, next false m' => toSint (next dn n') + toSint m
    | next true n'_1, next true m' =>
      match next dn n' + m with
      | next false a => toSint (next dn n') + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next dn n') + toSint m
⊢ toSint
      (match next dn n', m with
        | next false n'_1, next false m' =>
          match next dn n' + m with
          | next msb r' => (next msb r', msb)
        | next true n'_1, next true m' =>
          match next dn n' + m with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (next dn n' + m, false)).fst =
    toSint (next dn n') + toSint m
Tactic:
cases m
State after:
case next
sz : ℕ
dn : Bool
n' : FinInt sz
a✝¹ : Bool
a✝ : FinInt sz
h_nov :
  (match next dn n', next a✝¹ a✝ with
      | next false n'_1, next false m' =>
        match next dn n' + next a✝¹ a✝ with
        | next msb r' => (next msb r', msb)
      | next true n'_1, next true m' =>
        match next dn n' + next a✝¹ a✝ with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (next dn n' + next a✝¹ a✝, false)).snd =
    false
h :
  toSint (next dn n' + next a✝¹ a✝) =
    match next dn n', next a✝¹ a✝ with
    | next false n'_1, next false m' =>
      match next dn n' + next a✝¹ a✝ with
      | next false a => toSint (next dn n') + toSint (next a✝¹ a✝)
      | next true a => toSint (next dn n') + toSint (next a✝¹ a✝) - 2 ^ (sz + 1)
    | next false n'_1, next true m' => toSint (next dn n') + toSint (next a✝¹ a✝)
    | next true n'_1, next false m' => toSint (next dn n') + toSint (next a✝¹ a✝)
    | next true n'_1, next true m' =>
      match next dn n' + next a✝¹ a✝ with
      | next false a => toSint (next dn n') + toSint (next a✝¹ a✝) + 2 ^ (sz + 1)
      | next true a => toSint (next dn n') + toSint (next a✝¹ a✝)
⊢ toSint
      (match next dn n', next a✝¹ a✝ with
        | next false n'_1, next false m' =>
          match next dn n' + next a✝¹ a✝ with
          | next msb r' => (next msb r', msb)
        | next true n'_1, next true m' =>
          match next dn n' + next a✝¹ a✝ with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (next dn n' + next a✝¹ a✝, false)).fst =
    toSint (next dn n') + toSint (next a✝¹ a✝)

State before:
sz : ℕ
dn : Bool
n' : FinInt sz
dm : Bool
m' : FinInt sz
h_nov :
  (match next dn n', next dm m' with
      | next false n'_1, next false m'_1 =>
        match next dn n' + next dm m' with
        | next msb r' => (next msb r', msb)
      | next true n'_1, next true m'_1 =>
        match next dn n' + next dm m' with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (next dn n' + next dm m', false)).snd =
    false
h :
  toSint (next dn n' + next dm m') =
    match next dn n', next dm m' with
    | next false n'_1, next false m'_1 =>
      match next dn n' + next dm m' with
      | next false a => toSint (next dn n') + toSint (next dm m')
      | next true a => toSint (next dn n') + toSint (next dm m') - 2 ^ (sz + 1)
    | next false n'_1, next true m'_1 => toSint (next dn n') + toSint (next dm m')
    | next true n'_1, next false m'_1 => toSint (next dn n') + toSint (next dm m')
    | next true n'_1, next true m'_1 =>
      match next dn n' + next dm m' with
      | next false a => toSint (next dn n') + toSint (next dm m') + 2 ^ (sz + 1)
      | next true a => toSint (next dn n') + toSint (next dm m')
⊢ toSint
      (match next dn n', next dm m' with
        | next false n'_1, next false m'_1 =>
          match next dn n' + next dm m' with
          | next msb r' => (next msb r', msb)
        | next true n'_1, next true m'_1 =>
          match next dn n' + next dm m' with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (next dn n' + next dm m', false)).fst =
    toSint (next dn n') + toSint (next dm m')
Tactic:
case next dm m' =>
cases dn <;> cases dm <;> simp [h] at *
case false.false =>
match h: next false n' + next false m' with
| .next br r =>
rw [h] at h_nov
cases br <;> simp at *
rw [←h]; simp [add_toSint_msb]; simp [h]
case true.true =>
match h: next true n' + next true m' with
| .next br r =>
rw [h] at h_nov
cases br <;> simp at *
rw [←h]; simp [add_toSint_msb]; simp [h]
State after:
no goals

State before:
sz : ℕ
dn : Bool
n' : FinInt sz
dm : Bool
m' : FinInt sz
h_nov :
  (match next dn n', next dm m' with
      | next false n'_1, next false m'_1 =>
        match next dn n' + next dm m' with
        | next msb r' => (next msb r', msb)
      | next true n'_1, next true m'_1 =>
        match next dn n' + next dm m' with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (next dn n' + next dm m', false)).snd =
    false
h :
  toSint (next dn n' + next dm m') =
    match next dn n', next dm m' with
    | next false n'_1, next false m'_1 =>
      match next dn n' + next dm m' with
      | next false a => toSint (next dn n') + toSint (next dm m')
      | next true a => toSint (next dn n') + toSint (next dm m') - 2 ^ (sz + 1)
    | next false n'_1, next true m'_1 => toSint (next dn n') + toSint (next dm m')
    | next true n'_1, next false m'_1 => toSint (next dn n') + toSint (next dm m')
    | next true n'_1, next true m'_1 =>
      match next dn n' + next dm m' with
      | next false a => toSint (next dn n') + toSint (next dm m') + 2 ^ (sz + 1)
      | next true a => toSint (next dn n') + toSint (next dm m')
⊢ toSint
      (match next dn n', next dm m' with
        | next false n'_1, next false m'_1 =>
          match next dn n' + next dm m' with
          | next msb r' => (next msb r', msb)
        | next true n'_1, next true m'_1 =>
          match next dn n' + next dm m' with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (next dn n' + next dm m', false)).fst =
    toSint (next dn n') + toSint (next dm m')
Tactic:
cases dn <;> cases dm <;> simp [h] at *
State after:
case false.false
sz : ℕ
n' m' : FinInt sz
h_nov :
  (match next false n' + next false m' with
      | next msb r' => (next msb r', msb)).snd =
    false
h : True
⊢ toSint
      (match next false n' + next false m' with
        | next msb r' => (next msb r', msb)).fst =
    toSint (next false n') + toSint (next false m')

case true.true
sz : ℕ
n' m' : FinInt sz
h_nov :
  (match next true n' + next true m' with
      | next msb r' => (next msb r', !msb)).snd =
    false
h : True
⊢ toSint
      (match next true n' + next true m' with
        | next msb r' => (next msb r', !msb)).fst =
    toSint (next true n') + toSint (next true m')

State before:
sz : ℕ
n' m' : FinInt sz
h_nov :
  (match next false n' + next false m' with
      | next msb r' => (next msb r', msb)).snd =
    false
h : True
⊢ toSint
      (match next false n' + next false m' with
        | next msb r' => (next msb r', msb)).fst =
    toSint (next false n') + toSint (next false m')
Tactic:
case false.false =>
  match h: next false n' + next false m' with
  | .next br r =>
    rw [h] at h_nov
    cases br <;> simp at *
    rw [←h]; simp [add_toSint_msb]; simp [h]
State after:
no goals

State before:
sz : ℕ
n' m' : FinInt sz
h_nov :
  (match next true n' + next true m' with
      | next msb r' => (next msb r', !msb)).snd =
    false
h : True
⊢ toSint
      (match next true n' + next true m' with
        | next msb r' => (next msb r', !msb)).fst =
    toSint (next true n') + toSint (next true m')
Tactic:
case true.true =>
  match h: next true n' + next true m' with
  | .next br r =>
    rw [h] at h_nov
    cases br <;> simp at *
    rw [←h]; simp [add_toSint_msb]; simp [h]
State after:
no goals

State before:
sz : ℕ
n' m' : FinInt sz
h_nov :
  (match next false n' + next false m' with
      | next msb r' => (next msb r', msb)).snd =
    false
h : True
⊢ toSint
      (match next false n' + next false m' with
        | next msb r' => (next msb r', msb)).fst =
    toSint (next false n') + toSint (next false m')
Tactic:
match h: next false n' + next false m' with
| .next br r =>
  rw [h] at h_nov
  cases br <;> simp at *
  rw [←h]; simp [add_toSint_msb]; simp [h]
State after:
no goals

State before:
sz : ℕ
n' m' : FinInt sz
h_nov :
  (match next false n' + next false m' with
      | next msb r' => (next msb r', msb)).snd =
    false
h✝ : True
br : Bool
r : FinInt sz
h : next false n' + next false m' = next br r
⊢ toSint
      (match next br r with
        | next msb r' => (next msb r', msb)).fst =
    toSint (next false n') + toSint (next false m')
Tactic:
rw [h] at h_nov
State after:
sz : ℕ
n' m' : FinInt sz
h✝ : True
br : Bool
r : FinInt sz
h_nov :
  (match next br r with
      | next msb r' => (next msb r', msb)).snd =
    false
h : next false n' + next false m' = next br r
⊢ toSint
      (match next br r with
        | next msb r' => (next msb r', msb)).fst =
    toSint (next false n') + toSint (next false m')

State before:
sz : ℕ
n' m' : FinInt sz
h✝ : True
br : Bool
r : FinInt sz
h_nov :
  (match next br r with
      | next msb r' => (next msb r', msb)).snd =
    false
h : next false n' + next false m' = next br r
⊢ toSint
      (match next br r with
        | next msb r' => (next msb r', msb)).fst =
    toSint (next false n') + toSint (next false m')
Tactic:
cases br <;> simp at *
State after:
case false
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next false n' + next false m' = next false r
h_nov : True
⊢ toSint (next false r) = toSint (next false n') + toSint (next false m')

State before:
case false
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next false n' + next false m' = next false r
h_nov : True
⊢ toSint (next false r) = toSint (next false n') + toSint (next false m')
Tactic:
rw [←h]
State after:
case false
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next false n' + next false m' = next false r
h_nov : True
⊢ toSint (next false n' + next false m') = toSint (next false n') + toSint (next false m')

State before:
case false
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next false n' + next false m' = next false r
h_nov : True
⊢ toSint (next false n' + next false m') = toSint (next false n') + toSint (next false m')
Tactic:
simp [add_toSint_msb]
State after:
case false
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next false n' + next false m' = next false r
h_nov : True
⊢ (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)) =
    toSint (next false n') + toSint (next false m')

State before:
case false
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next false n' + next false m' = next false r
h_nov : True
⊢ (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)) =
    toSint (next false n') + toSint (next false m')
Tactic:
simp [h]
State after:
no goals

State before:
sz : ℕ
n' m' : FinInt sz
h_nov :
  (match next true n' + next true m' with
      | next msb r' => (next msb r', !msb)).snd =
    false
h : True
⊢ toSint
      (match next true n' + next true m' with
        | next msb r' => (next msb r', !msb)).fst =
    toSint (next true n') + toSint (next true m')
Tactic:
match h: next true n' + next true m' with
| .next br r =>
  rw [h] at h_nov
  cases br <;> simp at *
  rw [←h]; simp [add_toSint_msb]; simp [h]
State after:
no goals

State before:
sz : ℕ
n' m' : FinInt sz
h_nov :
  (match next true n' + next true m' with
      | next msb r' => (next msb r', !msb)).snd =
    false
h✝ : True
br : Bool
r : FinInt sz
h : next true n' + next true m' = next br r
⊢ toSint
      (match next br r with
        | next msb r' => (next msb r', !msb)).fst =
    toSint (next true n') + toSint (next true m')
Tactic:
rw [h] at h_nov
State after:
sz : ℕ
n' m' : FinInt sz
h✝ : True
br : Bool
r : FinInt sz
h_nov :
  (match next br r with
      | next msb r' => (next msb r', !msb)).snd =
    false
h : next true n' + next true m' = next br r
⊢ toSint
      (match next br r with
        | next msb r' => (next msb r', !msb)).fst =
    toSint (next true n') + toSint (next true m')

State before:
sz : ℕ
n' m' : FinInt sz
h✝ : True
br : Bool
r : FinInt sz
h_nov :
  (match next br r with
      | next msb r' => (next msb r', !msb)).snd =
    false
h : next true n' + next true m' = next br r
⊢ toSint
      (match next br r with
        | next msb r' => (next msb r', !msb)).fst =
    toSint (next true n') + toSint (next true m')
Tactic:
cases br <;> simp at *
State after:
case true
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next true n' + next true m' = next true r
h_nov : True
⊢ toSint (next true r) = toSint (next true n') + toSint (next true m')

State before:
case true
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next true n' + next true m' = next true r
h_nov : True
⊢ toSint (next true r) = toSint (next true n') + toSint (next true m')
Tactic:
rw [←h]
State after:
case true
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next true n' + next true m' = next true r
h_nov : True
⊢ toSint (next true n' + next true m') = toSint (next true n') + toSint (next true m')

State before:
case true
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next true n' + next true m' = next true r
h_nov : True
⊢ toSint (next true n' + next true m') = toSint (next true n') + toSint (next true m')
Tactic:
simp [add_toSint_msb]
State after:
case true
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next true n' + next true m' = next true r
h_nov : True
⊢ (match next true n' + next true m' with
    | next false a => toSint (next true n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next true m')) =
    toSint (next true n') + toSint (next true m')

State before:
case true
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next true n' + next true m' = next true r
h_nov : True
⊢ (match next true n' + next true m' with
    | next false a => toSint (next true n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next true m')) =
    toSint (next true n') + toSint (next true m')
Tactic:
simp [h]
State after:
no goals