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

State before:
sz : ℕ
⊢ -1 = minusOne
Tactic:
match H: sz with
| 0 => decide
| sz'+1 =>
    have h: sz' + 1 > 0 := by sorry_arith
    apply eq_of_toUint_cong2
    simp [toUint_minusOne]
    simp [neg_toUint]
    apply cong2_mod2_left
    simp [ofInt_1, toUint_one h]
    sorry_arith
State after:
no goals

State before:
sz : ℕ
H : sz = 0
⊢ -1 = minusOne
Tactic:
decide
State after:
no goals

State before:
sz sz' : ℕ
H : sz = Nat.succ sz'
⊢ -1 = minusOne
Tactic:
have h: sz' + 1 > 0 := by sorry_arith
State after:
sz sz' : ℕ
H : sz = Nat.succ sz'
h : sz' + 1 > 0
⊢ -1 = minusOne

State before:
sz sz' : ℕ
H : sz = Nat.succ sz'
h : sz' + 1 > 0
⊢ -1 = minusOne
Tactic:
apply eq_of_toUint_cong2
State after:
case a
sz sz' : ℕ
H : sz = Nat.succ sz'
h : sz' + 1 > 0
⊢ toUint (-1) ≡ toUint minusOne [2^sz' + 1]

State before:
case a
sz sz' : ℕ
H : sz = Nat.succ sz'
h : sz' + 1 > 0
⊢ toUint (-1) ≡ toUint minusOne [2^sz' + 1]
Tactic:
simp [toUint_minusOne]
State after:
case a
sz sz' : ℕ
H : sz = Nat.succ sz'
h : sz' + 1 > 0
⊢ toUint (-1) ≡ 2 ^ sz' + (2 ^ sz' - 1) [2^sz' + 1]

State before:
case a
sz sz' : ℕ
H : sz = Nat.succ sz'
h : sz' + 1 > 0
⊢ toUint (-1) ≡ 2 ^ sz' + (2 ^ sz' - 1) [2^sz' + 1]
Tactic:
simp [neg_toUint]
State after:
case a
sz sz' : ℕ
H : sz = Nat.succ sz'
h : sz' + 1 > 0
⊢ mod2 (-toUint 1) (sz' + 1) ≡ 2 ^ sz' + (2 ^ sz' - 1) [2^sz' + 1]

State before:
case a
sz sz' : ℕ
H : sz = Nat.succ sz'
h : sz' + 1 > 0
⊢ mod2 (-toUint 1) (sz' + 1) ≡ 2 ^ sz' + (2 ^ sz' - 1) [2^sz' + 1]
Tactic:
apply cong2_mod2_left
State after:
case a.a
sz sz' : ℕ
H : sz = Nat.succ sz'
h : sz' + 1 > 0
⊢ (-toUint 1) ≡ 2 ^ sz' + (2 ^ sz' - 1) [2^sz' + 1]

State before:
case a.a
sz sz' : ℕ
H : sz = Nat.succ sz'
h : sz' + 1 > 0
⊢ (-toUint 1) ≡ 2 ^ sz' + (2 ^ sz' - 1) [2^sz' + 1]
Tactic:
sorry_arith
State after:
no goals

State before:
sz sz' : ℕ
H : sz = Nat.succ sz'
⊢ sz' + 1 > 0
Tactic:
sorry_arith
State after:
no goals