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

Proof state:
case bin.ult
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ⟦assign.toAIGAssignment, bitblast aig (bin lhs BVBinPred.ult rhs)⟧ = eval assign (bin lhs BVBinPred.ult rhs)

Tactic:
simp only [bitblast, eval_bin, BVBinPred.eval_ult]

Result:
case bin.ult
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ⟦assign.toAIGAssignment,
      mkUlt (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig
        { lhs := (BVExpr.bitblast aig lhs).vec.cast ⋯,
          rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).vec }⟧ =
    (BVExpr.eval assign lhs).ult (BVExpr.eval assign rhs)

Proof state:
case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment,
        { aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
          ref :=
            { lhs := (BVExpr.bitblast aig lhs).vec.cast ⋯,
                    rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).vec }.lhs.get
              idx hidx }⟧ =
      (BVExpr.eval assign lhs).getLsbD idx

Tactic:
intros

Result:
case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦assign.toAIGAssignment,
      { aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
        ref :=
          { lhs := (BVExpr.bitblast aig lhs).vec.cast ⋯,
                  rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).vec }.lhs.get
            idx✝ hidx✝ }⟧ =
    (BVExpr.eval assign lhs).getLsbD idx✝

Proof state:
case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦assign.toAIGAssignment,
      { aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
        ref :=
          { lhs := (BVExpr.bitblast aig lhs).vec.cast ⋯,
                  rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).vec }.lhs.get
            idx✝ hidx✝ }⟧ =
    (BVExpr.eval assign lhs).getLsbD idx✝

Tactic:
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := BVExpr.bitblast)]

Result:
case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦assign.toAIGAssignment,
      { aig := (BVExpr.bitblast aig lhs).aig,
        ref :=
          {
            gate :=
              ({ lhs := (BVExpr.bitblast aig lhs).vec.cast ⋯,
                        rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).vec }.lhs.get
                  idx✝ hidx✝).gate,
            hgate := ?bin.ult.hleft } }⟧ =
    (BVExpr.eval assign lhs).getLsbD idx✝

case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ({ lhs := (BVExpr.bitblast aig lhs).vec.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).vec }.lhs.get
        idx✝ hidx✝).gate <
    (BVExpr.bitblast aig lhs).aig.decls.size

Proof state:
case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦assign.toAIGAssignment,
      { aig := (BVExpr.bitblast aig lhs).aig,
        ref := { gate := ((BVExpr.bitblast aig lhs).vec.get idx✝ hidx✝).gate, hgate := ⋯ } }⟧ =
    (BVExpr.eval assign lhs).getLsbD idx✝

Tactic:
rw [BVExpr.denote_bitblast]

Result:
no goals

Proof state:
case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦assign.toAIGAssignment,
      { aig := (BVExpr.bitblast aig lhs).aig,
        ref := { gate := ((BVExpr.bitblast aig lhs).vec.get idx✝ hidx✝).gate, hgate := ⋯ } }⟧ =
    (BVExpr.eval assign lhs).getLsbD idx✝

Tactic:
rw [BVExpr.denote_bitblast]

Result:
no goals

Proof state:
case bin.ult.hright
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment,
        { aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
          ref :=
            { lhs := (BVExpr.bitblast aig lhs).vec.cast ⋯,
                    rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).vec }.rhs.get
              idx hidx }⟧ =
      (BVExpr.eval assign rhs).getLsbD idx

Tactic:
intros

Result:
case bin.ult.hright
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦assign.toAIGAssignment,
      { aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
        ref :=
          { lhs := (BVExpr.bitblast aig lhs).vec.cast ⋯,
                  rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).vec }.rhs.get
            idx✝ hidx✝ }⟧ =
    (BVExpr.eval assign rhs).getLsbD idx✝

Proof state:
case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦assign.toAIGAssignment,
      { aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
        ref :=
          { lhs := (BVExpr.bitblast aig lhs).vec.cast ⋯,
                  rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).vec }.lhs.get
            idx✝ hidx✝ }⟧ =
    (BVExpr.eval assign lhs).getLsbD idx✝

Tactic:
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := BVExpr.bitblast)]

Result:
case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦assign.toAIGAssignment,
      { aig := (BVExpr.bitblast aig lhs).aig,
        ref :=
          {
            gate :=
              ({ lhs := (BVExpr.bitblast aig lhs).vec.cast ⋯,
                        rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).vec }.lhs.get
                  idx✝ hidx✝).gate,
            hgate := ?bin.eq.hleft } }⟧ =
    (BVExpr.eval assign lhs).getLsbD idx✝

case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ({ lhs := (BVExpr.bitblast aig lhs).vec.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).vec }.lhs.get
        idx✝ hidx✝).gate <
    (BVExpr.bitblast aig lhs).aig.decls.size

Proof state:
case getLsbD
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ ⟦assign.toAIGAssignment, bitblast aig (getLsbD expr idx)⟧ = eval assign (getLsbD expr idx)

Tactic:
simp only [bitblast, denote_blastGetLsbD, BVExpr.denote_bitblast, dite_eq_ite,
  Bool.if_false_right, eval_getLsbD, Bool.and_iff_right_iff_imp, decide_eq_true_eq]

Result:
case getLsbD
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ (BVExpr.eval assign expr).getLsbD idx = true → idx < w✝