Theorem: BVLogicalExpr.bitblast.go_eval_eq_eval (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas.lean)

State before:
expr : BVLogicalExpr
aig : AIG BVBit
assign : BVExpr.Assignment
⊢ ⟦(ofBoolExprCached.go expr aig BVPred.bitblast).val, assign.toAIGAssignment⟧ = eval assign expr
Tactic:
induction expr generalizing aig with
| const => simp [ofBoolExprCached.go]
| literal => simp [ofBoolExprCached.go]
| not expr ih => simp [ofBoolExprCached.go, ih]
| gate g lhs rhs lih rih => cases g <;> simp [ofBoolExprCached.go, Gate.eval, lih, rih]
State after:
no goals

State before:
case const
assign : BVExpr.Assignment
a✝ : Bool
aig : AIG BVBit
⊢ ⟦(ofBoolExprCached.go (BoolExpr.const a✝) aig BVPred.bitblast).val, assign.toAIGAssignment⟧ =
    eval assign (BoolExpr.const a✝)
Tactic:
simp [ofBoolExprCached.go]
State after:
no goals

State before:
case literal
assign : BVExpr.Assignment
a✝ : BVPred
aig : AIG BVBit
⊢ ⟦(ofBoolExprCached.go (BoolExpr.literal a✝) aig BVPred.bitblast).val, assign.toAIGAssignment⟧ =
    eval assign (BoolExpr.literal a✝)
Tactic:
simp [ofBoolExprCached.go]
State after:
no goals

State before:
case not
assign : BVExpr.Assignment
expr : BoolExpr BVPred
ih :
  ∀ (aig : AIG BVBit), ⟦(ofBoolExprCached.go expr aig BVPred.bitblast).val, assign.toAIGAssignment⟧ = eval assign expr
aig : AIG BVBit
⊢ ⟦(ofBoolExprCached.go expr.not aig BVPred.bitblast).val, assign.toAIGAssignment⟧ = eval assign expr.not
Tactic:
simp [ofBoolExprCached.go, ih]
State after:
no goals

State before:
case gate
assign : BVExpr.Assignment
g : Gate
lhs rhs : BoolExpr BVPred
lih : ∀ (aig : AIG BVBit), ⟦(ofBoolExprCached.go lhs aig BVPred.bitblast).val, assign.toAIGAssignment⟧ = eval assign lhs
rih : ∀ (aig : AIG BVBit), ⟦(ofBoolExprCached.go rhs aig BVPred.bitblast).val, assign.toAIGAssignment⟧ = eval assign rhs
aig : AIG BVBit
⊢ ⟦(ofBoolExprCached.go (BoolExpr.gate g lhs rhs) aig BVPred.bitblast).val, assign.toAIGAssignment⟧ =
    eval assign (BoolExpr.gate g lhs rhs)
Tactic:
cases g <;> simp [ofBoolExprCached.go, Gate.eval, lih, rih]
State after:
no goals