-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem carry_succ_one (i : Nat) (x : BitVec w) (h : 0 < w) :
    carry (i+1) x (1#w) false = decide (∀ j ≤ i, x.getLsbD j = true)

Proof state:
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = false
⊢ (false && decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)) = decide (∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true)

Tactic:
have : ∃ j ≤ i + 1, x.getLsbD j = false :=
  ⟨i+1, by omega, hx⟩

Result:
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = false
this : ∃ j, j ≤ i + 1 ∧ x.getLsbD j = false
⊢ (false && decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)) = decide (∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true)

Proof state:
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
this : (∀ (j : Nat), j ≤ i → x.getLsbD j = true) ↔ ∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true
⊢ (true && decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)) = decide (∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true)

Tactic:
simpa

Result:
no goals

Proof state:
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = false
this : ∃ j, j ≤ i + 1 ∧ x.getLsbD j = false
⊢ (false && decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)) = decide (∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true)

Tactic:
simpa

Result:
no goals

Proof state:
case succ
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
⊢ (x.getLsbD (i + 1)).atLeastTwo ((1#w).getLsbD (i + 1)) (decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)) =
    decide (∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true)

Tactic:
simp only [getLsbD_one, add_one_ne_zero, decide_false, Bool.and_false, atLeastTwo_false_mid]

Result:
case succ
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
⊢ (x.getLsbD (i + 1) && decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)) =
    decide (∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true)

Proof state:
case mp
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
⊢ (∀ (j : Nat), j ≤ i → x.getLsbD j = true) → ∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true

Tactic:
intro h j hj

Result:
case mp
w : Nat
x : BitVec w
h✝ : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
h : ∀ (j : Nat), j ≤ i → x.getLsbD j = true
j : Nat
hj : j ≤ i + 1
⊢ x.getLsbD j = true

Proof state:
case mp.inr
w : Nat
x : BitVec w
h✝ : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
h : ∀ (j : Nat), j ≤ i → x.getLsbD j = true
hj : i.succ ≤ i + 1
⊢ x.getLsbD i.succ = true

Tactic:
exact hx

Result:
no goals

Proof state:
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
⊢ (∀ (j : Nat), j ≤ i → x.getLsbD j = true) ↔ ∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true

Tactic:
constructor

Result:
case mp
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
⊢ (∀ (j : Nat), j ≤ i → x.getLsbD j = true) → ∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true

case mpr
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
⊢ (∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true) → ∀ (j : Nat), j ≤ i → x.getLsbD j = true

Proof state:
case mpr
w : Nat
x : BitVec w
h✝ : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
h : ∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true
j : Nat
hj : j ≤ i
⊢ x.getLsbD j = true

Tactic:
apply h

Result:
case mpr.a
w : Nat
x : BitVec w
h✝ : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
h : ∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true
j : Nat
hj : j ≤ i
⊢ j ≤ i + 1

Proof state:
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
⊢ (true && decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)) = decide (∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true)

Tactic:
suffices
    (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
    ↔ (∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true) by
  simpa

Result:
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
⊢ (∀ (j : Nat), j ≤ i → x.getLsbD j = true) ↔ ∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true

Proof state:
case mp.inl
w : Nat
x : BitVec w
h✝ : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
h : ∀ (j : Nat), j ≤ i → x.getLsbD j = true
j : Nat
hj : j ≤ i + 1
hj' : j ≤ i
⊢ x.getLsbD j = true

Tactic:
apply h

Result:
case mp.inl.a
w : Nat
x : BitVec w
h✝ : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
h : ∀ (j : Nat), j ≤ i → x.getLsbD j = true
j : Nat
hj : j ≤ i + 1
hj' : j ≤ i
⊢ j ≤ i

Proof state:
case succ
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
⊢ carry (i + 1 + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true)

Tactic:
rw [carry_succ, ih]

Result:
case succ
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
⊢ (x.getLsbD (i + 1)).atLeastTwo ((1#w).getLsbD (i + 1)) (decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)) =
    decide (∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true)

Proof state:
case succ
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
⊢ (x.getLsbD (i + 1) && decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)) =
    decide (∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true)

Tactic:
cases hx : x.getLsbD (i+1)

Result:
case succ.false
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = false
⊢ (false && decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)) = decide (∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true)

case succ.true
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = true
⊢ (true && decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)) = decide (∀ (j : Nat), j ≤ i + 1 → x.getLsbD j = true)

Proof state:
w : Nat
x : BitVec w
h : 0 < w
i : Nat
ih : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)
hx : x.getLsbD (i + 1) = false
⊢ i + 1 ≤ i + 1

Tactic:
omega

Result:
no goals