-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Carry.lean
theorem mkOverflowBit_eq_carry (aig : AIG α) (input : OverflowInput aig) (lhs rhs : BitVec input.w)
    (assign : α → Bool)
    (hleft : ∀ (idx : Nat) (hidx : idx < input.w), ⟦aig, input.vec.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < input.w), ⟦aig, input.vec.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
    ⟦mkOverflowBit aig input, assign⟧
      =
    BitVec.carry input.w lhs rhs ⟦aig, input.cin, assign⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ ⟦assign, mkOverflowBit.go aig input.2.lhs input.2.rhs 0 input.cin⟧ =
    BitVec.carry input.w lhs rhs ⟦assign, { aig := aig, ref := input.cin }⟧

Tactic:
apply mkOverflowBit.go_eq_carry

Result:
case hcurr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ 0 ≤ input.w

case hleft
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.2.lhs.get idx hidx }⟧ = lhs.getLsbD idx

case hright
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.2.rhs.get idx hidx }⟧ = rhs.getLsbD idx

case hcin
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ ⟦assign, { aig := aig, ref := input.cin }⟧ = BitVec.carry 0 lhs rhs ⟦assign, { aig := aig, ref := input.cin }⟧

Proof state:
case hcurr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ 0 ≤ input.w

Tactic:
omega

Result:
no goals

Proof state:
case hright
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.2.rhs.get idx hidx }⟧ = rhs.getLsbD idx

Tactic:
assumption

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ ⟦assign,
      match input with
      | { w := w, vec := { lhs := lhs, rhs := rhs }, cin := cin } => mkOverflowBit.go aig lhs rhs 0 cin⟧ =
    BitVec.carry input.w lhs rhs ⟦assign, { aig := aig, ref := input.cin }⟧

Tactic:
dsimp only

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ ⟦assign, mkOverflowBit.go aig input.2.lhs input.2.rhs 0 input.cin⟧ =
    BitVec.carry input.w lhs rhs ⟦assign, { aig := aig, ref := input.cin }⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ ⟦assign, mkOverflowBit aig input⟧ = BitVec.carry input.w lhs rhs ⟦assign, { aig := aig, ref := input.cin }⟧

Tactic:
unfold mkOverflowBit

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ ⟦assign,
      match input with
      | { w := w, vec := { lhs := lhs, rhs := rhs }, cin := cin } => mkOverflowBit.go aig lhs rhs 0 cin⟧ =
    BitVec.carry input.w lhs rhs ⟦assign, { aig := aig, ref := input.cin }⟧

Proof state:
case hleft
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.2.lhs.get idx hidx }⟧ = lhs.getLsbD idx

Tactic:
assumption

Result:
no goals

Proof state:
case hcin
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w), ⟦assign, { aig := aig, ref := input.vec.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ ⟦assign, { aig := aig, ref := input.cin }⟧ = BitVec.carry 0 lhs rhs ⟦assign, { aig := aig, ref := input.cin }⟧

Tactic:
simp [BitVec.carry_zero]

Result:
no goals