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

State before:
sz : ℕ
n : FinInt sz
⊢ toUint (comp n) = 2 ^ sz - 1 - toUint n
Tactic:
induction sz
State after:
case zero
n : FinInt Nat.zero
⊢ toUint (comp n) = 2 ^ Nat.zero - 1 - toUint n

case succ
n✝ : ℕ
n_ih✝ : ∀ (n : FinInt n✝), toUint (comp n) = 2 ^ n✝ - 1 - toUint n
n : FinInt (Nat.succ n✝)
⊢ toUint (comp n) = 2 ^ Nat.succ n✝ - 1 - toUint n

State before:
n : FinInt Nat.zero
⊢ toUint (comp n) = 2 ^ Nat.zero - 1 - toUint n
Tactic:
case zero =>
  cases n; simp
State after:
no goals

State before:
sz : ℕ
ih : ∀ (n : FinInt sz), toUint (comp n) = 2 ^ sz - 1 - toUint n
n : FinInt (Nat.succ sz)
⊢ toUint (comp n) = 2 ^ Nat.succ sz - 1 - toUint n
Tactic:
case succ sz ih =>
  simp [comp] at ih
  cases n; case next sz bn n' =>
  cases bn <;> simp [ih]
  . sorry_arith
  . sorry_arith
State after:
no goals

State before:
n : FinInt Nat.zero
⊢ toUint (comp n) = 2 ^ Nat.zero - 1 - toUint n
Tactic:
cases n
State after:
case nil

⊢ toUint (comp nil) = 2 ^ Nat.zero - 1 - toUint nil

State before:
case nil

⊢ toUint (comp nil) = 2 ^ Nat.zero - 1 - toUint nil
Tactic:
simp
State after:
no goals

State before:
sz : ℕ
ih : ∀ (n : FinInt sz), toUint (comp n) = 2 ^ sz - 1 - toUint n
n : FinInt (Nat.succ sz)
⊢ toUint (comp n) = 2 ^ Nat.succ sz - 1 - toUint n
Tactic:
simp [comp] at ih
State after:
sz : ℕ
ih : ∀ (n : FinInt sz), toUint (logic1 (fun x => !x) n) = 2 ^ sz - 1 - toUint n
n : FinInt (Nat.succ sz)
⊢ toUint (comp n) = 2 ^ Nat.succ sz - 1 - toUint n

State before:
sz : ℕ
ih : ∀ (n : FinInt sz), toUint (logic1 (fun x => !x) n) = 2 ^ sz - 1 - toUint n
n : FinInt (Nat.succ sz)
⊢ toUint (comp n) = 2 ^ Nat.succ sz - 1 - toUint n
Tactic:
cases n
State after:
case next
n✝ : ℕ
a✝¹ : Bool
a✝ : FinInt n✝
ih : ∀ (n : FinInt (Nat.add n✝ 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add n✝ 0 - 1 - toUint n
⊢ toUint (comp (next a✝¹ a✝)) = 2 ^ Nat.succ (Nat.add n✝ 0) - 1 - toUint (next a✝¹ a✝)

State before:
sz : ℕ
bn : Bool
n' : FinInt sz
ih : ∀ (n : FinInt (Nat.add sz 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add sz 0 - 1 - toUint n
⊢ toUint (comp (next bn n')) = 2 ^ Nat.succ (Nat.add sz 0) - 1 - toUint (next bn n')
Tactic:
case next sz bn n' =>
cases bn <;> simp [ih]
. sorry_arith
. sorry_arith
State after:
no goals

State before:
sz : ℕ
bn : Bool
n' : FinInt sz
ih : ∀ (n : FinInt (Nat.add sz 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add sz 0 - 1 - toUint n
⊢ toUint (comp (next bn n')) = 2 ^ Nat.succ (Nat.add sz 0) - 1 - toUint (next bn n')
Tactic:
cases bn <;> simp [ih]
State after:
case false
sz : ℕ
n' : FinInt sz
ih : ∀ (n : FinInt (Nat.add sz 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add sz 0 - 1 - toUint n
⊢ 2 ^ sz + (2 ^ sz - 1 - toUint n') = 2 ^ Nat.succ sz - 1 - toUint n'

case true
sz : ℕ
n' : FinInt sz
ih : ∀ (n : FinInt (Nat.add sz 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add sz 0 - 1 - toUint n
⊢ 2 ^ sz - 1 - toUint n' = 2 ^ Nat.succ sz - 1 - (2 ^ sz + toUint n')

State before:
case false
sz : ℕ
n' : FinInt sz
ih : ∀ (n : FinInt (Nat.add sz 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add sz 0 - 1 - toUint n
⊢ 2 ^ sz + (2 ^ sz - 1 - toUint n') = 2 ^ Nat.succ sz - 1 - toUint n'

case true
sz : ℕ
n' : FinInt sz
ih : ∀ (n : FinInt (Nat.add sz 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add sz 0 - 1 - toUint n
⊢ 2 ^ sz - 1 - toUint n' = 2 ^ Nat.succ sz - 1 - (2 ^ sz + toUint n')
Tactic:
. sorry_arith
State after:
case true
sz : ℕ
n' : FinInt sz
ih : ∀ (n : FinInt (Nat.add sz 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add sz 0 - 1 - toUint n
⊢ 2 ^ sz - 1 - toUint n' = 2 ^ Nat.succ sz - 1 - (2 ^ sz + toUint n')

State before:
case true
sz : ℕ
n' : FinInt sz
ih : ∀ (n : FinInt (Nat.add sz 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add sz 0 - 1 - toUint n
⊢ 2 ^ sz - 1 - toUint n' = 2 ^ Nat.succ sz - 1 - (2 ^ sz + toUint n')
Tactic:
. sorry_arith
State after:
no goals