-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean
theorem bitblast.go_eval_eq_eval (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExpr.Assignment) :
    ⟦ofBoolExprCached.go aig expr BVPred.bitblast, assign.toAIGAssignment⟧ = expr.eval assign

Proof state:
case literal
assign : BVExpr.Assignment
a✝ : BVPred
aig : AIG BVBit
⊢ ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig (BoolExpr.literal a✝) BVPred.bitblast).val⟧ =
    eval assign (BoolExpr.literal a✝)

Tactic:
simp [ofBoolExprCached.go]

Result:
no goals

Proof state:
case ite
assign : BVExpr.Assignment
discr lhs rhs : BoolExpr BVPred
dih :
  ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig discr BVPred.bitblast).val⟧ = eval assign discr
lih : ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig lhs BVPred.bitblast).val⟧ = eval assign lhs
rih : ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig rhs BVPred.bitblast).val⟧ = eval assign rhs
aig : AIG BVBit
⊢ (if
        ⟦assign.toAIGAssignment,
            {
              aig :=
                (ofBoolExprCached.go
                      (ofBoolExprCached.go (ofBoolExprCached.go aig discr BVPred.bitblast).1.aig lhs
                            BVPred.bitblast).1.aig
                      rhs BVPred.bitblast).1.aig,
              ref := { gate := (ofBoolExprCached.go aig discr BVPred.bitblast).1.ref.gate, hgate := ⋯ } }⟧ =
          true then
      ⟦assign.toAIGAssignment,
        (ofBoolExprCached.go (ofBoolExprCached.go aig discr BVPred.bitblast).1.aig lhs BVPred.bitblast).1⟧
    else
      ⟦assign.toAIGAssignment,
        {
          aig :=
            (ofBoolExprCached.go
                  (ofBoolExprCached.go (ofBoolExprCached.go aig discr BVPred.bitblast).1.aig lhs BVPred.bitblast).1.aig
                  rhs BVPred.bitblast).1.aig,
          ref :=
            (ofBoolExprCached.go
                  (ofBoolExprCached.go (ofBoolExprCached.go aig discr BVPred.bitblast).1.aig lhs BVPred.bitblast).1.aig
                  rhs BVPred.bitblast).1.ref }⟧) =
    bif eval assign discr then eval assign lhs else eval assign rhs

Tactic:
rw [ofBoolExprCached.go_denote_mem_prefix, ofBoolExprCached.go_denote_mem_prefix]

Result:
case ite
assign : BVExpr.Assignment
discr lhs rhs : BoolExpr BVPred
dih :
  ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig discr BVPred.bitblast).val⟧ = eval assign discr
lih : ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig lhs BVPred.bitblast).val⟧ = eval assign lhs
rih : ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig rhs BVPred.bitblast).val⟧ = eval assign rhs
aig : AIG BVBit
⊢ (if
        ⟦assign.toAIGAssignment,
            { aig := (ofBoolExprCached.go aig discr BVPred.bitblast).1.aig,
              ref := { gate := (ofBoolExprCached.go aig discr BVPred.bitblast).1.ref.gate, hgate := ?ite.hstart } }⟧ =
          true then
      ⟦assign.toAIGAssignment,
        (ofBoolExprCached.go (ofBoolExprCached.go aig discr BVPred.bitblast).1.aig lhs BVPred.bitblast).1⟧
    else
      ⟦assign.toAIGAssignment,
        {
          aig :=
            (ofBoolExprCached.go
                  (ofBoolExprCached.go (ofBoolExprCached.go aig discr BVPred.bitblast).1.aig lhs BVPred.bitblast).1.aig
                  rhs BVPred.bitblast).1.aig,
          ref :=
            (ofBoolExprCached.go
                  (ofBoolExprCached.go (ofBoolExprCached.go aig discr BVPred.bitblast).1.aig lhs BVPred.bitblast).1.aig
                  rhs BVPred.bitblast).1.ref }⟧) =
    bif eval assign discr then eval assign lhs else eval assign rhs

case ite.hstart
assign : BVExpr.Assignment
discr lhs rhs : BoolExpr BVPred
dih :
  ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig discr BVPred.bitblast).val⟧ = eval assign discr
lih : ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig lhs BVPred.bitblast).val⟧ = eval assign lhs
rih : ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig rhs BVPred.bitblast).val⟧ = eval assign rhs
aig : AIG BVBit
⊢ (ofBoolExprCached.go aig discr BVPred.bitblast).1.ref.gate <
    (ofBoolExprCached.go aig discr BVPred.bitblast).1.aig.decls.size

Proof state:
case const
assign : BVExpr.Assignment
a✝ : Bool
aig : AIG BVBit
⊢ ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig (BoolExpr.const a✝) BVPred.bitblast).val⟧ =
    eval assign (BoolExpr.const a✝)

Tactic:
simp [ofBoolExprCached.go]

Result:
no goals

Proof state:
case ite
assign : BVExpr.Assignment
discr lhs rhs : BoolExpr BVPred
dih :
  ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig discr BVPred.bitblast).val⟧ = eval assign discr
lih : ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig lhs BVPred.bitblast).val⟧ = eval assign lhs
rih : ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig rhs BVPred.bitblast).val⟧ = eval assign rhs
aig : AIG BVBit
⊢ ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig (discr.ite lhs rhs) BVPred.bitblast).val⟧ =
    eval assign (discr.ite lhs rhs)

Tactic:
simp only [ofBoolExprCached.go, Ref.cast_eq, denote_mkIfCached,
  ofBoolExprCached.go_denote_entry, eval_ite]

Result:
case ite
assign : BVExpr.Assignment
discr lhs rhs : BoolExpr BVPred
dih :
  ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig discr BVPred.bitblast).val⟧ = eval assign discr
lih : ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig lhs BVPred.bitblast).val⟧ = eval assign lhs
rih : ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig rhs BVPred.bitblast).val⟧ = eval assign rhs
aig : AIG BVBit
⊢ (if
        ⟦assign.toAIGAssignment,
            {
              aig :=
                (ofBoolExprCached.go
                      (ofBoolExprCached.go (ofBoolExprCached.go aig discr BVPred.bitblast).1.aig lhs
                            BVPred.bitblast).1.aig
                      rhs BVPred.bitblast).1.aig,
              ref := { gate := (ofBoolExprCached.go aig discr BVPred.bitblast).1.ref.gate, hgate := ⋯ } }⟧ =
          true then
      ⟦assign.toAIGAssignment,
        (ofBoolExprCached.go (ofBoolExprCached.go aig discr BVPred.bitblast).1.aig lhs BVPred.bitblast).1⟧
    else
      ⟦assign.toAIGAssignment,
        {
          aig :=
            (ofBoolExprCached.go
                  (ofBoolExprCached.go (ofBoolExprCached.go aig discr BVPred.bitblast).1.aig lhs BVPred.bitblast).1.aig
                  rhs BVPred.bitblast).1.aig,
          ref :=
            (ofBoolExprCached.go
                  (ofBoolExprCached.go (ofBoolExprCached.go aig discr BVPred.bitblast).1.aig lhs BVPred.bitblast).1.aig
                  rhs BVPred.bitblast).1.ref }⟧) =
    bif eval assign discr then eval assign lhs else eval assign rhs

Proof state:
case ite.hstart
assign : BVExpr.Assignment
discr lhs rhs : BoolExpr BVPred
dih :
  ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig discr BVPred.bitblast).val⟧ = eval assign discr
lih : ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig lhs BVPred.bitblast).val⟧ = eval assign lhs
rih : ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig rhs BVPred.bitblast).val⟧ = eval assign rhs
aig : AIG BVBit
⊢ (ofBoolExprCached.go aig discr BVPred.bitblast).1.ref.gate <
    (ofBoolExprCached.go aig discr BVPred.bitblast).1.aig.decls.size

Tactic:
simp [Ref.hgate]

Result:
no goals