Theorem: BVExpr.bitblast.mkOverflowBit_eq_carry (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/Carry.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦mkOverflowBit aig input, assign⟧ = BitVec.carry input.w lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧
Tactic:
unfold mkOverflowBit
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦match input with
      | { w := w, stream := { lhs := lhs, rhs := rhs }, cin := cin } => mkOverflowBit.go aig 0 ⋯ cin lhs rhs,
      assign⟧ =
    BitVec.carry input.w lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦match input with
      | { w := w, stream := { lhs := lhs, rhs := rhs }, cin := cin } => mkOverflowBit.go aig 0 ⋯ cin lhs rhs,
      assign⟧ =
    BitVec.carry input.w lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧
Tactic:
dsimp
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦mkOverflowBit.go aig 0 ⋯ input.cin input.2.lhs input.2.rhs, assign⟧ =
    BitVec.carry input.w lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦mkOverflowBit.go aig 0 ⋯ input.cin input.2.lhs input.2.rhs, assign⟧ =
    BitVec.carry input.w lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧
Tactic:
apply mkOverflowBit.go_eq_carry
State after:
case hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat) (hidx : idx < input.w), ⟦{ aig := aig, ref := input.2.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx

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

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

State before:
case hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat) (hidx : idx < input.w), ⟦{ aig := aig, ref := input.2.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx

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

case hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦{ aig := aig, ref := input.cin }, assign⟧ = BitVec.carry 0 lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧
Tactic:
. assumption
State after:
case hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat) (hidx : idx < input.w), ⟦{ aig := aig, ref := input.2.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx

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

State before:
case hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat) (hidx : idx < input.w), ⟦{ aig := aig, ref := input.2.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx

case hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦{ aig := aig, ref := input.cin }, assign⟧ = BitVec.carry 0 lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧
Tactic:
. assumption
State after:
case hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦{ aig := aig, ref := input.cin }, assign⟧ = BitVec.carry 0 lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧

State before:
case hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦{ aig := aig, ref := input.cin }, assign⟧ = BitVec.carry 0 lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧
Tactic:
. simp [BitVec.carry_zero]
State after:
no goals

State before:
case hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat) (hidx : idx < input.w), ⟦{ aig := aig, ref := input.2.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
Tactic:
assumption
State after:
no goals

State before:
case hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat) (hidx : idx < input.w), ⟦{ aig := aig, ref := input.2.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
Tactic:
assumption
State after:
no goals

State before:
case hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦{ aig := aig, ref := input.cin }, assign⟧ = BitVec.carry 0 lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧
Tactic:
simp [BitVec.carry_zero]
State after:
no goals