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

State before:
sz : ℕ
n : ℤ
⊢ toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
Tactic:
induction sz
State after:
case zero
n : ℤ
⊢ toUint (FinInt.ofIntAux Nat.zero n).fst = mod2 n Nat.zero ∧ (FinInt.ofIntAux Nat.zero n).snd = n / 2 ^ Nat.zero

case succ
n : ℤ
n✝ : ℕ
n_ih✝ : toUint (FinInt.ofIntAux n✝ n).fst = mod2 n n✝ ∧ (FinInt.ofIntAux n✝ n).snd = n / 2 ^ n✝
⊢ toUint (FinInt.ofIntAux (Nat.succ n✝) n).fst = mod2 n (Nat.succ n✝) ∧
    (FinInt.ofIntAux (Nat.succ n✝) n).snd = n / 2 ^ Nat.succ n✝

State before:
n : ℤ
⊢ toUint (FinInt.ofIntAux Nat.zero n).fst = mod2 n Nat.zero ∧ (FinInt.ofIntAux Nat.zero n).snd = n / 2 ^ Nat.zero
Tactic:
case zero =>
  simp [FinInt.ofIntAux]; sorry_arith
State after:
no goals

State before:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ toUint (FinInt.ofIntAux (Nat.succ sz) n).fst = mod2 n (Nat.succ sz) ∧
    (FinInt.ofIntAux (Nat.succ sz) n).snd = n / 2 ^ Nat.succ sz
Tactic:
case succ sz ih =>
  simp [FinInt.ofIntAux, ih]; constructor
  . have h: (n / 2^sz % 2 = 0) ∨ (n / 2^sz %2 = 1) := by sorry
    match h with
    | .inl h => simp [h, ih]; sorry_arith
    | .inr h => simp [h, ih]; sorry_arith
  . sorry_arith
State after:
no goals

State before:
n : ℤ
⊢ toUint (FinInt.ofIntAux Nat.zero n).fst = mod2 n Nat.zero ∧ (FinInt.ofIntAux Nat.zero n).snd = n / 2 ^ Nat.zero
Tactic:
simp [FinInt.ofIntAux]
State after:
n : ℤ
⊢ 0 = mod2 n 0

State before:
n : ℤ
⊢ 0 = mod2 n 0
Tactic:
sorry_arith
State after:
no goals

State before:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ toUint (FinInt.ofIntAux (Nat.succ sz) n).fst = mod2 n (Nat.succ sz) ∧
    (FinInt.ofIntAux (Nat.succ sz) n).snd = n / 2 ^ Nat.succ sz
Tactic:
simp [FinInt.ofIntAux, ih]
State after:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ toUint (next (n / 2 ^ sz % 2 == 1) (FinInt.ofIntAux sz n).fst) = mod2 n (Nat.succ sz) ∧
    n / 2 ^ sz / 2 = n / 2 ^ Nat.succ sz

State before:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ toUint (next (n / 2 ^ sz % 2 == 1) (FinInt.ofIntAux sz n).fst) = mod2 n (Nat.succ sz) ∧
    n / 2 ^ sz / 2 = n / 2 ^ Nat.succ sz
Tactic:
constructor
State after:
case left
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ toUint (next (n / 2 ^ sz % 2 == 1) (FinInt.ofIntAux sz n).fst) = mod2 n (Nat.succ sz)

case right
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ n / 2 ^ sz / 2 = n / 2 ^ Nat.succ sz

State before:
case left
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ toUint (next (n / 2 ^ sz % 2 == 1) (FinInt.ofIntAux sz n).fst) = mod2 n (Nat.succ sz)

case right
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ n / 2 ^ sz / 2 = n / 2 ^ Nat.succ sz
Tactic:
. have h: (n / 2^sz % 2 = 0) ∨ (n / 2^sz %2 = 1) := by sorry
  match h with
  | .inl h => simp [h, ih]; sorry_arith
  | .inr h => simp [h, ih]; sorry_arith
State after:
case right
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ n / 2 ^ sz / 2 = n / 2 ^ Nat.succ sz

State before:
case right
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ n / 2 ^ sz / 2 = n / 2 ^ Nat.succ sz
Tactic:
. sorry_arith
State after:
no goals

State before:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ n / 2 ^ sz % 2 = 0 ∨ n / 2 ^ sz % 2 = 1
Tactic:
sorry
State after:
no goals

State before:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
h✝ : n / 2 ^ sz % 2 = 0 ∨ n / 2 ^ sz % 2 = 1
h : n / 2 ^ sz % 2 = 0
⊢ toUint (next (n / 2 ^ sz % 2 == 1) (FinInt.ofIntAux sz n).fst) = mod2 n (Nat.succ sz)
Tactic:
simp [h, ih]
State after:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
h✝ : n / 2 ^ sz % 2 = 0 ∨ n / 2 ^ sz % 2 = 1
h : n / 2 ^ sz % 2 = 0
⊢ mod2 n sz = mod2 n (Nat.succ sz)

State before:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
h✝ : n / 2 ^ sz % 2 = 0 ∨ n / 2 ^ sz % 2 = 1
h : n / 2 ^ sz % 2 = 0
⊢ mod2 n sz = mod2 n (Nat.succ sz)
Tactic:
sorry_arith
State after:
no goals

State before:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
h✝ : n / 2 ^ sz % 2 = 0 ∨ n / 2 ^ sz % 2 = 1
h : n / 2 ^ sz % 2 = 1
⊢ toUint (next (n / 2 ^ sz % 2 == 1) (FinInt.ofIntAux sz n).fst) = mod2 n (Nat.succ sz)
Tactic:
simp [h, ih]
State after:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
h✝ : n / 2 ^ sz % 2 = 0 ∨ n / 2 ^ sz % 2 = 1
h : n / 2 ^ sz % 2 = 1
⊢ 2 ^ sz + mod2 n sz = mod2 n (Nat.succ sz)

State before:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
h✝ : n / 2 ^ sz % 2 = 0 ∨ n / 2 ^ sz % 2 = 1
h : n / 2 ^ sz % 2 = 1
⊢ 2 ^ sz + mod2 n sz = mod2 n (Nat.succ sz)
Tactic:
sorry_arith
State after:
no goals