internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case signExtend.inr.isFalse
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
h✝ : ¬idx < originalWidth
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (originalWidth - 1) ⋯ },
      assign.toAIGAssignment⟧ =
    (eval assign inner).getLsb (originalWidth - 1)

case signExtend.inr.htarget
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ 0 < { w := originalWidth, stream := (go aig inner).1.stream }.w
Tactic:
rw [ih]
Proof state after:
case signExtend.inr.htarget
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ 0 < { w := originalWidth, stream := (go aig inner).1.stream }.w

case signExtend.inr.htarget
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ 0 < { w := originalWidth, stream := (go aig inner).1.stream }.w
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case signExtend.inr.htarget
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ 0 < { w := originalWidth, stream := (go aig inner).1.stream }.w

case signExtend.inr.htarget
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ 0 < { w := originalWidth, stream := (go aig inner).1.stream }.w
Tactic:
simp [hlt]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case extract
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
⊢ ⟦{ aig := (go aig (extract hi lo inner)).val.aig, ref := (go aig (extract hi lo inner)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (extract hi lo inner)).getLsb idx
Tactic:
simp only [go, blastExtract_eq_eval_getLsb, Bool.if_false_right, eval_extract,
  BitVec.getLsb_extract]
Proof state after:
case extract
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
⊢ (if h : lo + idx < w✝ then
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧
    else false) =
    (decide (idx ≤ hi - lo) && (eval assign inner).getLsb (lo + idx))
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case extract
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
⊢ (if h : lo + idx < w✝ then
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧
    else false) =
    (decide (idx ≤ hi - lo) && (eval assign inner).getLsb (lo + idx))
Tactic:
have : idx ≤ hi - lo := by omega
Proof state after:
case extract
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
this : idx ≤ hi - lo
⊢ (if h : lo + idx < w✝ then
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧
    else false) =
    (decide (idx ≤ hi - lo) && (eval assign inner).getLsb (lo + idx))
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case extract
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
this : idx ≤ hi - lo
⊢ (if h : lo + idx < w✝ then
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧
    else false) =
    (decide (idx ≤ hi - lo) && (eval assign inner).getLsb (lo + idx))
Tactic:
simp only [this, decide_True, Bool.true_and]
Proof state after:
case extract
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
this : idx ≤ hi - lo
⊢ (if h : lo + idx < w✝ then
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧
    else false) =
    (eval assign inner).getLsb (lo + idx)
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case extract
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
this : idx ≤ hi - lo
⊢ (if h : lo + idx < w✝ then
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧
    else false) =
    (eval assign inner).getLsb (lo + idx)
Tactic:
split
Proof state after:
case extract.isTrue
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
this : idx ≤ hi - lo
h✝ : lo + idx < w✝
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧ =
    (eval assign inner).getLsb (lo + idx)

case extract.isFalse
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
this : idx ≤ hi - lo
h✝ : ¬lo + idx < w✝
⊢ false = (eval assign inner).getLsb (lo + idx)
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case extract.isTrue
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
this : idx ≤ hi - lo
h✝ : lo + idx < w✝
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧ =
    (eval assign inner).getLsb (lo + idx)

case extract.isFalse
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
this : idx ≤ hi - lo
h✝ : ¬lo + idx < w✝
⊢ false = (eval assign inner).getLsb (lo + idx)
Tactic:
. next hsplit =>
  rw [ih]
Proof state after:
case extract.isFalse
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
this : idx ≤ hi - lo
h✝ : ¬lo + idx < w✝
⊢ false = (eval assign inner).getLsb (lo + idx)
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case extract.isFalse
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
this : idx ≤ hi - lo
h✝ : ¬lo + idx < w✝
⊢ false = (eval assign inner).getLsb (lo + idx)
Tactic:
. apply Eq.symm
  apply BitVec.getLsb_ge
  omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
⊢ idx ≤ hi - lo
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case extract.isTrue
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
this : idx ≤ hi - lo
h✝ : lo + idx < w✝
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧ =
    (eval assign inner).getLsb (lo + idx)
Tactic:
next hsplit =>
rw [ih]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
this : idx ≤ hi - lo
hsplit : lo + idx < w✝
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧ =
    (eval assign inner).getLsb (lo + idx)
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case extract.isFalse
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
this : idx ≤ hi - lo
h✝ : ¬lo + idx < w✝
⊢ false = (eval assign inner).getLsb (lo + idx)
Tactic:
apply Eq.symm
Proof state after:
case extract.isFalse.h
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
this : idx ≤ hi - lo
h✝ : ¬lo + idx < w✝
⊢ (eval assign inner).getLsb (lo + idx) = false
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case extract.isFalse.h
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
this : idx ≤ hi - lo
h✝ : ¬lo + idx < w✝
⊢ (eval assign inner).getLsb (lo + idx) = false
Tactic:
apply BitVec.getLsb_ge
Proof state after:
case extract.isFalse.h.ge
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
this : idx ≤ hi - lo
h✝ : ¬lo + idx < w✝
⊢ w✝ ≤ lo + idx
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case extract.isFalse.h.ge
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
this : idx ≤ hi - lo
h✝ : ¬lo + idx < w✝
⊢ w✝ ≤ lo + idx
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case bin
w : Nat
assign : Assignment
w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦{ aig := (go aig (lhs.bin op rhs)).val.aig, ref := (go aig (lhs.bin op rhs)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (lhs.bin op rhs)).getLsb idx
Tactic:
cases op with
| and =>
  simp only [go, RefStream.denote_zip, denote_mkAndCached, rih, eval_bin, BVBinOp.eval_and,
    BitVec.getLsb_and]
  simp only [go_val_eq_bitblast, RefStream.getRef_cast]
  rw [AIG.LawfulStreamOperator.denote_input_stream (f := bitblast)]
  rw [← go_val_eq_bitblast]
  rw [lih]
| or =>
  simp only [go, RefStream.denote_zip, denote_mkOrCached, rih, eval_bin, BVBinOp.eval_or,
    BitVec.getLsb_or]
  simp only [go_val_eq_bitblast, RefStream.getRef_cast]
  rw [AIG.LawfulStreamOperator.denote_input_stream (f := bitblast)]
  rw [← go_val_eq_bitblast]
  rw [lih]
| xor =>
  simp only [go, RefStream.denote_zip, denote_mkXorCached, rih, eval_bin, BVBinOp.eval_xor,
    BitVec.getLsb_xor]
  simp only [go_val_eq_bitblast, RefStream.getRef_cast]
  rw [AIG.LawfulStreamOperator.denote_input_stream (f := bitblast)]
  rw [← go_val_eq_bitblast]
  rw [lih]
| add =>
  simp only [go, eval_bin, BVBinOp.eval_add]
  apply blastAdd_eq_eval_getLsb
  . intros
    dsimp
    rw [go_denote_mem_prefix]
    rw [← lih (aig := aig)]
    . simp
    . assumption
    . simp [Ref.hgate]
  . intros
    rw [← rih]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case bin.and
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦{ aig := (go aig (lhs.bin BVBinOp.and rhs)).val.aig,
        ref := (go aig (lhs.bin BVBinOp.and rhs)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (lhs.bin BVBinOp.and rhs)).getLsb idx
Tactic:
simp only [go, RefStream.denote_zip, denote_mkAndCached, rih, eval_bin, BVBinOp.eval_and,
  BitVec.getLsb_and]
Proof state after:
case bin.and
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := ((go aig lhs).1.stream.cast ⋯).getRef idx hidx },
        assign.toAIGAssignment⟧ &&
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx && (eval assign rhs).getLsb idx)
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case bin.and
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := ((go aig lhs).1.stream.cast ⋯).getRef idx hidx },
        assign.toAIGAssignment⟧ &&
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx && (eval assign rhs).getLsb idx)
Tactic:
simp only [go_val_eq_bitblast, RefStream.getRef_cast]
Proof state after:
case bin.and
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (bitblast (bitblast aig lhs).aig rhs).aig, ref := ((bitblast aig lhs).stream.getRef idx hidx).cast ⋯ },
        assign.toAIGAssignment⟧ &&
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx && (eval assign rhs).getLsb idx)
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case bin.and
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (bitblast (bitblast aig lhs).aig rhs).aig, ref := ((bitblast aig lhs).stream.getRef idx hidx).cast ⋯ },
        assign.toAIGAssignment⟧ &&
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx && (eval assign rhs).getLsb idx)
Tactic:
rw [AIG.LawfulStreamOperator.denote_input_stream (f := bitblast)]
Proof state after:
case bin.and
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (bitblast aig lhs).aig, ref := (bitblast aig lhs).stream.getRef idx hidx }, assign.toAIGAssignment⟧ &&
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx && (eval assign rhs).getLsb idx)