-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem getLsbD_neg {i : Nat} {x : BitVec w} :
    getLsbD (-x) i =
      (getLsbD x i ^^ decide (i < w) && decide (∃ j < i, getLsbD x j = true))

Proof state:
w : Nat
x : BitVec w
this hi : 0 < w
⊢ (2 ^ w - 1 - x.toNat) % 1 = 0

Tactic:
omega

Result:
no goals

Proof state:
case pos.succ.mpr
w : Nat
x : BitVec w
this : 0 < w
n✝ : Nat
hi : n✝ + 1 < w
⊢ (∀ (x_1 : Nat), x_1 < n✝ + 1 → x.getLsbD x_1 = false) → ∀ (j : Nat), j ≤ n✝ → j < w ∧ x.getLsbD j = false

Tactic:
rintro h j hj

Result:
case pos.succ.mpr
w : Nat
x : BitVec w
this : 0 < w
n✝ : Nat
hi : n✝ + 1 < w
h : ∀ (x_1 : Nat), x_1 < n✝ + 1 → x.getLsbD x_1 = false
j : Nat
hj : j ≤ n✝
⊢ j < w ∧ x.getLsbD j = false

Proof state:
case pos
w i : Nat
x : BitVec w
hi : i < w
⊢ (~~~x + 1#w).getLsbD i = (x.getLsbD i ^^ decide (i < w) && decide (∃ j, j < i ∧ x.getLsbD j = true))

Tactic:
rw [getLsbD_add hi]

Result:
case pos
w i : Nat
x : BitVec w
hi : i < w
⊢ ((~~~x).getLsbD i ^^ ((1#w).getLsbD i ^^ carry i (~~~x) (1#w) false)) =
    (x.getLsbD i ^^ decide (i < w) && decide (∃ j, j < i ∧ x.getLsbD j = true))

Proof state:
case pos.succ
w : Nat
x : BitVec w
this : 0 < w
n✝ : Nat
hi : n✝ + 1 < w
⊢ (x.getLsbD (n✝ + 1) != (decide (n✝ + 1 = 0) ^^ carry (n✝ + 1) (~~~x) (1#w) false)) =
    !(x.getLsbD (n✝ + 1) ^^ decide (∃ j, j < n✝ + 1 ∧ x.getLsbD j = true))

Tactic:
rw [carry_succ_one _ _ (by omega), ← Bool.xor_not, ← decide_not]

Result:
case pos.succ
w : Nat
x : BitVec w
this : 0 < w
n✝ : Nat
hi : n✝ + 1 < w
⊢ (x.getLsbD (n✝ + 1) != (decide (n✝ + 1 = 0) ^^ decide (∀ (j : Nat), j ≤ n✝ → (~~~x).getLsbD j = true))) =
    (x.getLsbD (n✝ + 1) ^^ decide ¬∃ j, j < n✝ + 1 ∧ x.getLsbD j = true)

Proof state:
case pos.succ.mp
w : Nat
x : BitVec w
this : 0 < w
n✝ : Nat
hi : n✝ + 1 < w
h : ∀ (j : Nat), j ≤ n✝ → j < w ∧ x.getLsbD j = false
j : Nat
hj : j < n✝ + 1
⊢ x.getLsbD j = false

Tactic:
exact And.right <| h j (by omega)

Result:
no goals

Proof state:
case pos.succ
w : Nat
x : BitVec w
this : 0 < w
n✝ : Nat
hi : n✝ + 1 < w
⊢ (∀ (j : Nat), j ≤ n✝ → j < w ∧ x.getLsbD j = false) ↔ ∀ (x_1 : Nat), x_1 < n✝ + 1 → x.getLsbD x_1 = false

Tactic:
constructor

Result:
case pos.succ.mp
w : Nat
x : BitVec w
this : 0 < w
n✝ : Nat
hi : n✝ + 1 < w
⊢ (∀ (j : Nat), j ≤ n✝ → j < w ∧ x.getLsbD j = false) → ∀ (x_1 : Nat), x_1 < n✝ + 1 → x.getLsbD x_1 = false

case pos.succ.mpr
w : Nat
x : BitVec w
this : 0 < w
n✝ : Nat
hi : n✝ + 1 < w
⊢ (∀ (x_1 : Nat), x_1 < n✝ + 1 → x.getLsbD x_1 = false) → ∀ (j : Nat), j ≤ n✝ → j < w ∧ x.getLsbD j = false

Proof state:
case pos.succ.mp
w : Nat
x : BitVec w
this : 0 < w
n✝ : Nat
hi : n✝ + 1 < w
⊢ (∀ (j : Nat), j ≤ n✝ → j < w ∧ x.getLsbD j = false) → ∀ (x_1 : Nat), x_1 < n✝ + 1 → x.getLsbD x_1 = false

Tactic:
rintro h j hj

Result:
case pos.succ.mp
w : Nat
x : BitVec w
this : 0 < w
n✝ : Nat
hi : n✝ + 1 < w
h : ∀ (j : Nat), j ≤ n✝ → j < w ∧ x.getLsbD j = false
j : Nat
hj : j < n✝ + 1
⊢ x.getLsbD j = false

Proof state:
case pos
w i : Nat
x : BitVec w
hi : i < w
this : 0 < w
⊢ ((~~~x).getLsbD i ^^ ((1#w).getLsbD i ^^ carry i (~~~x) (1#w) false)) =
    (x.getLsbD i ^^ decide (i < w) && decide (∃ j, j < i ∧ x.getLsbD j = true))

Tactic:
simp only [getLsbD_not, hi, decide_true, Bool.true_and, getLsbD_one, this, not_bne,
  _root_.true_and, not_eq_eq_eq_not]

Result:
case pos
w i : Nat
x : BitVec w
hi : i < w
this : 0 < w
⊢ (x.getLsbD i != (decide (i = 0) ^^ carry i (~~~x) (1#w) false)) =
    !(x.getLsbD i ^^ decide (∃ j, j < i ∧ x.getLsbD j = true))

Proof state:
w : Nat
x : BitVec w
this : 0 < w
n✝ : Nat
hi : n✝ + 1 < w
h : ∀ (x_1 : Nat), x_1 < n✝ + 1 → x.getLsbD x_1 = false
j : Nat
hj : j ≤ n✝
⊢ j < w

Tactic:
omega

Result:
no goals

Proof state:
w i : Nat
x : BitVec w
hi : i < w
⊢ 0 < w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
this hi : 0 < w
⊢ carry 0 (~~~x) (1#w) false = false

Tactic:
simp [carry]

Result:
w : Nat
x : BitVec w
this hi : 0 < w
⊢ (2 ^ w - 1 - x.toNat) % 1 = 0

Proof state:
case neg
w i : Nat
x : BitVec w
hi : ¬i < w
⊢ (~~~x + 1#w).getLsbD i = (x.getLsbD i ^^ decide (i < w) && decide (∃ j, j < i ∧ x.getLsbD j = true))

Tactic:
have h_ge : w ≤ i := by omega

Result:
case neg
w i : Nat
x : BitVec w
hi : ¬i < w
h_ge : w ≤ i
⊢ (~~~x + 1#w).getLsbD i = (x.getLsbD i ^^ decide (i < w) && decide (∃ j, j < i ∧ x.getLsbD j = true))

Proof state:
w i : Nat
x : BitVec w
hi : ¬i < w
⊢ w ≤ i

Tactic:
omega

Result:
no goals

Proof state:
case pos.succ
w : Nat
x : BitVec w
this : 0 < w
n✝ : Nat
hi : n✝ + 1 < w
⊢ (x.getLsbD (n✝ + 1) != (decide (n✝ + 1 = 0) ^^ decide (∀ (j : Nat), j ≤ n✝ → (~~~x).getLsbD j = true))) =
    (x.getLsbD (n✝ + 1) ^^ decide ¬∃ j, j < n✝ + 1 ∧ x.getLsbD j = true)

Tactic:
simp only [add_one_ne_zero, decide_false, getLsbD_not, and_eq_true, decide_eq_true_eq,
  not_eq_eq_eq_not, Bool.not_true, false_bne, not_exists, _root_.not_and, not_eq_true,
  bne_right_inj, decide_eq_decide]

Result:
case pos.succ
w : Nat
x : BitVec w
this : 0 < w
n✝ : Nat
hi : n✝ + 1 < w
⊢ (∀ (j : Nat), j ≤ n✝ → j < w ∧ x.getLsbD j = false) ↔ ∀ (x_1 : Nat), x_1 < n✝ + 1 → x.getLsbD x_1 = false

Proof state:
case pos.succ.mpr
w : Nat
x : BitVec w
this : 0 < w
n✝ : Nat
hi : n✝ + 1 < w
h : ∀ (x_1 : Nat), x_1 < n✝ + 1 → x.getLsbD x_1 = false
j : Nat
hj : j ≤ n✝
⊢ j < w ∧ x.getLsbD j = false

Tactic:
exact ⟨by omega, h j (by omega)⟩

Result:
no goals

Proof state:
case pos.zero
w : Nat
x : BitVec w
this hi : 0 < w
carry_zero : carry 0 (~~~x) (1#w) false = false
⊢ (x.getLsbD 0 != (decide (0 = 0) ^^ carry 0 (~~~x) (1#w) false)) =
    !(x.getLsbD 0 ^^ decide (∃ j, j < 0 ∧ x.getLsbD j = true))

Tactic:
simp [hi, carry_zero]

Result:
no goals

Proof state:
case pos.zero
w : Nat
x : BitVec w
this hi : 0 < w
⊢ (x.getLsbD 0 != (decide (0 = 0) ^^ carry 0 (~~~x) (1#w) false)) =
    !(x.getLsbD 0 ^^ decide (∃ j, j < 0 ∧ x.getLsbD j = true))

Tactic:
have carry_zero : carry 0 ?x ?y false = false := by
  simp [carry]; omega

Result:
case pos.zero
w : Nat
x : BitVec w
this hi : 0 < w
carry_zero : carry 0 (~~~x) (1#w) false = false
⊢ (x.getLsbD 0 != (decide (0 = 0) ^^ carry 0 (~~~x) (1#w) false)) =
    !(x.getLsbD 0 ^^ decide (∃ j, j < 0 ∧ x.getLsbD j = true))

Proof state:
w i : Nat
x : BitVec w
⊢ (-x).getLsbD i = (x.getLsbD i ^^ decide (i < w) && decide (∃ j, j < i ∧ x.getLsbD j = true))

Tactic:
rw [neg_eq_not_add]

Result:
w i : Nat
x : BitVec w
⊢ (~~~x + 1#w).getLsbD i = (x.getLsbD i ^^ decide (i < w) && decide (∃ j, j < i ∧ x.getLsbD j = true))

Proof state:
case neg
w i : Nat
x : BitVec w
hi : ¬i < w
h_ge : w ≤ i
⊢ (~~~x + 1#w).getLsbD i = (x.getLsbD i ^^ decide (i < w) && decide (∃ j, j < i ∧ x.getLsbD j = true))

Tactic:
simp [getLsbD_ge _ _ h_ge, h_ge, hi]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
this : 0 < w
n✝ : Nat
hi : n✝ + 1 < w
⊢ 0 < w

Tactic:
omega

Result:
no goals

Proof state:
w i : Nat
x : BitVec w
⊢ (~~~x + 1#w).getLsbD i = (x.getLsbD i ^^ decide (i < w) && decide (∃ j, j < i ∧ x.getLsbD j = true))

Tactic:
by_cases hi : i < w

Result:
case pos
w i : Nat
x : BitVec w
hi : i < w
⊢ (~~~x + 1#w).getLsbD i = (x.getLsbD i ^^ decide (i < w) && decide (∃ j, j < i ∧ x.getLsbD j = true))

case neg
w i : Nat
x : BitVec w
hi : ¬i < w
⊢ (~~~x + 1#w).getLsbD i = (x.getLsbD i ^^ decide (i < w) && decide (∃ j, j < i ∧ x.getLsbD j = true))

Proof state:
w : Nat
x : BitVec w
this : 0 < w
n✝ : Nat
hi : n✝ + 1 < w
h : ∀ (x_1 : Nat), x_1 < n✝ + 1 → x.getLsbD x_1 = false
j : Nat
hj : j ≤ n✝
⊢ j < n✝ + 1

Tactic:
omega

Result:
no goals

Proof state:
case pos
w i : Nat
x : BitVec w
hi : i < w
⊢ ((~~~x).getLsbD i ^^ ((1#w).getLsbD i ^^ carry i (~~~x) (1#w) false)) =
    (x.getLsbD i ^^ decide (i < w) && decide (∃ j, j < i ∧ x.getLsbD j = true))

Tactic:
have : 0 < w := by omega

Result:
case pos
w i : Nat
x : BitVec w
hi : i < w
this : 0 < w
⊢ ((~~~x).getLsbD i ^^ ((1#w).getLsbD i ^^ carry i (~~~x) (1#w) false)) =
    (x.getLsbD i ^^ decide (i < w) && decide (∃ j, j < i ∧ x.getLsbD j = true))