internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.blastAdd_eq_eval_getLsb
Proof state before:
case i_lt
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ idx < w
Tactic:
. assumption
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (blastAdd aig input).aig, ref := (blastAdd aig input).stream.getRef idx hidx }, assign⟧ =
    (lhs.getLsb idx).xor ((rhs.getLsb idx).xor (BitVec.carry idx lhs rhs false))
Tactic:
rw [← hleft idx hidx]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (blastAdd aig input).aig, ref := (blastAdd aig input).stream.getRef idx hidx }, assign⟧ =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      ((rhs.getLsb idx).xor (BitVec.carry idx lhs rhs false))
Theorem: BVExpr.bitblast.blastAdd_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (blastAdd aig input).aig, ref := (blastAdd aig input).stream.getRef idx hidx }, assign⟧ =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      ((rhs.getLsb idx).xor (BitVec.carry idx lhs rhs false))
Tactic:
rw [← hright idx hidx]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (blastAdd aig input).aig, ref := (blastAdd aig input).stream.getRef idx hidx }, assign⟧ =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))
Theorem: BVExpr.bitblast.blastAdd_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (blastAdd aig input).aig, ref := (blastAdd aig input).stream.getRef idx hidx }, assign⟧ =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))
Tactic:
unfold blastAdd
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{
        aig :=
          (let res := aig.mkConstCached false;
            let aig_1 := res.aig;
            let cin := res.ref;
            let input := input.cast ⋯;
            match input with
            | { lhs := lhs, rhs := rhs } => blastAdd.go aig_1 0 ⋯ cin RefStream.empty lhs rhs).aig,
        ref :=
          (let res := aig.mkConstCached false;
                let aig_1 := res.aig;
                let cin := res.ref;
                let input := input.cast ⋯;
                match input with
                | { lhs := lhs, rhs := rhs } => blastAdd.go aig_1 0 ⋯ cin RefStream.empty lhs rhs).stream.getRef
            idx hidx },
      assign⟧ =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))
Theorem: BVExpr.bitblast.blastAdd_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{
        aig :=
          (let res := aig.mkConstCached false;
            let aig_1 := res.aig;
            let cin := res.ref;
            let input := input.cast ⋯;
            match input with
            | { lhs := lhs, rhs := rhs } => blastAdd.go aig_1 0 ⋯ cin RefStream.empty lhs rhs).aig,
        ref :=
          (let res := aig.mkConstCached false;
                let aig_1 := res.aig;
                let cin := res.ref;
                let input := input.cast ⋯;
                match input with
                | { lhs := lhs, rhs := rhs } => blastAdd.go aig_1 0 ⋯ cin RefStream.empty lhs rhs).stream.getRef
            idx hidx },
      assign⟧ =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))
Tactic:
dsimp
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{
        aig :=
          (blastAdd.go (aig.mkConstCached false).aig 0 ⋯ (aig.mkConstCached false).ref RefStream.empty
              (input.cast ⋯).lhs (input.cast ⋯).rhs).aig,
        ref :=
          (blastAdd.go (aig.mkConstCached false).aig 0 ⋯ (aig.mkConstCached false).ref RefStream.empty
                  (input.cast ⋯).lhs (input.cast ⋯).rhs).stream.getRef
            idx hidx },
      assign⟧ =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))
Theorem: BVExpr.bitblast.blastAdd_eq_eval_getLsb
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ 0 ≤ idx

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

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
Tactic:
. omega
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
Theorem: BVExpr.bitblast.blastAdd_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
Tactic:
. intros
  simp only [BinaryRefStream.lhs_getRef_cast, Ref_cast']
  rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
  rw [hleft]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
Theorem: BVExpr.bitblast.blastAdd_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
Tactic:
. intros
  simp only [BinaryRefStream.rhs_getRef_cast, Ref_cast']
  rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
  rw [hright]
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ 0 ≤ w
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).rhs.getRef idx hidx }, assign⟧.xor
        (BitVec.carry idx lhs rhs false)) =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))
Tactic:
simp only [BinaryRefStream.lhs_getRef_cast, Ref_cast', BinaryRefStream.rhs_getRef_cast]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := { gate := (input.lhs.getRef idx hidx).gate, hgate := ⋯ } },
          assign⟧.xor
      (⟦{ aig := (aig.mkConstCached false).aig, ref := { gate := (input.rhs.getRef idx hidx).gate, hgate := ⋯ } },
            assign⟧.xor
        (BitVec.carry idx lhs rhs false)) =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))
Theorem: BVExpr.bitblast.blastAdd_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := { gate := (input.lhs.getRef idx hidx).gate, hgate := ⋯ } },
          assign⟧.xor
      (⟦{ aig := (aig.mkConstCached false).aig, ref := { gate := (input.rhs.getRef idx hidx).gate, hgate := ⋯ } },
            assign⟧.xor
        (BitVec.carry idx lhs rhs false)) =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))
Tactic:
rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := aig, ref := { gate := (input.lhs.getRef idx hidx).gate, hgate := ?m.39871 } }, assign⟧.xor
      (⟦{ aig := (aig.mkConstCached false).aig, ref := { gate := (input.rhs.getRef idx hidx).gate, hgate := ⋯ } },
            assign⟧.xor
        (BitVec.carry idx lhs rhs false)) =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ (input.lhs.getRef idx hidx).gate < aig.decls.size
Theorem: BVExpr.bitblast.blastAdd_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := aig, ref := { gate := (input.lhs.getRef idx hidx).gate, hgate := ?m.39871 } }, assign⟧.xor
      (⟦{ aig := (aig.mkConstCached false).aig, ref := { gate := (input.rhs.getRef idx hidx).gate, hgate := ⋯ } },
            assign⟧.xor
        (BitVec.carry idx lhs rhs false)) =
    ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧.xor
      (⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧.xor (BitVec.carry idx lhs rhs false))

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ (input.lhs.getRef idx hidx).gate < aig.decls.size
Tactic:
rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd_eq_eval_getLsb
Proof state before:
case hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (aig.mkConstCached false).ref }, assign⟧ =
    BitVec.carry 0 lhs rhs false
Tactic:
simp
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd_eq_eval_getLsb
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ 0 ≤ idx
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastAdd_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
Tactic:
intros
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.getRef idx✝ hidx✝ }, assign⟧ = lhs.getLsb idx✝
Theorem: BVExpr.bitblast.blastAdd_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).lhs.getRef idx✝ hidx✝ }, assign⟧ = lhs.getLsb idx✝
Tactic:
simp only [BinaryRefStream.lhs_getRef_cast, Ref_cast']
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := { gate := (input.lhs.getRef idx✝ hidx✝).gate, hgate := ⋯ } },
      assign⟧ =
    lhs.getLsb idx✝