-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
    ∀ (idx : Nat) (hidx : idx < w),
        ⟦(go aig expr).val.aig, (go aig expr).val.vec.get idx hidx, assign.toAIGAssignment⟧
          =
        (expr.eval assign).getLsbD idx

Proof state:
case signExtend.inr
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦assign.toAIGAssignment, { aig := (go aig inner).val.aig, ref := (go aig inner).val.vec.get idx hidx }⟧ =
      (eval assign inner).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefVecEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, vec := (go aig inner).1.vec } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ (if h : idx < originalWidth then
      ⟦assign.toAIGAssignment, { aig := (go aig inner).1.aig, ref := (go aig inner).1.vec.get idx ⋯ }⟧
    else
      ⟦assign.toAIGAssignment,
        { aig := (go aig inner).1.aig, ref := (go aig inner).1.vec.get (originalWidth - 1) ⋯ }⟧) =
    (BitVec.signExtend v (eval assign inner)).getLsbD idx

case signExtend.inr.htarget
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦assign.toAIGAssignment, { aig := (go aig inner).val.aig, ref := (go aig inner).val.vec.get idx hidx }⟧ =
      (eval assign inner).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefVecEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, vec := (go aig inner).1.vec } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ 0 < { w := originalWidth, vec := (go aig inner).1.vec }.w

Tactic:
rw [BitVec.getLsbD_signExtend]

Result:
case signExtend.inr
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦assign.toAIGAssignment, { aig := (go aig inner).val.aig, ref := (go aig inner).val.vec.get idx hidx }⟧ =
      (eval assign inner).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefVecEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, vec := (go aig inner).1.vec } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ (if h : idx < originalWidth then
      ⟦assign.toAIGAssignment, { aig := (go aig inner).1.aig, ref := (go aig inner).1.vec.get idx ⋯ }⟧
    else
      ⟦assign.toAIGAssignment,
        { aig := (go aig inner).1.aig, ref := (go aig inner).1.vec.get (originalWidth - 1) ⋯ }⟧) =
    (decide (idx < v) && if idx < originalWidth then (eval assign inner).getLsbD idx else (eval assign inner).msb)

case signExtend.inr.htarget
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦assign.toAIGAssignment, { aig := (go aig inner).val.aig, ref := (go aig inner).val.vec.get idx hidx }⟧ =
      (eval assign inner).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefVecEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, vec := (go aig inner).1.vec } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ 0 < { w := originalWidth, vec := (go aig inner).1.vec }.w

Proof state:
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦assign.toAIGAssignment, { aig := (go aig inner).val.aig, ref := (go aig inner).val.vec.get idx hidx }⟧ =
      (eval assign inner).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefVecEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, vec := (go aig inner).1.vec } = res
⊢ 0 ≤ originalWidth

Tactic:
omega

Result:
no goals

Proof state:
case bin.xor
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig rhs).val.aig, ref := (go aig rhs).val.vec.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦assign.toAIGAssignment, { aig := (bitblast aig lhs).aig, ref := (bitblast aig lhs).vec.get idx hidx }⟧ ^^
      (eval assign rhs).getLsbD idx) =
    ((eval assign lhs).getLsbD idx ^^ (eval assign rhs).getLsbD idx)

Tactic:
rw [← go_val_eq_bitblast]

Result:
case bin.xor
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig rhs).val.aig, ref := (go aig rhs).val.vec.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ ^^
      (eval assign rhs).getLsbD idx) =
    ((eval assign lhs).getLsbD idx ^^ (eval assign rhs).getLsbD idx)

Proof state:
case signExtend.inr.isFalse
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦assign.toAIGAssignment, { aig := (go aig inner).val.aig, ref := (go aig inner).val.vec.get idx hidx }⟧ =
      (eval assign inner).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefVecEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, vec := (go aig inner).1.vec } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
h✝ : ¬idx < originalWidth
⊢ ⟦assign.toAIGAssignment, { aig := (go aig inner).1.aig, ref := (go aig inner).1.vec.get (originalWidth - 1) ⋯ }⟧ =
    (eval assign inner).msb

Tactic:
rw [BitVec.msb_eq_getLsbD_last]

Result:
case signExtend.inr.isFalse
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦assign.toAIGAssignment, { aig := (go aig inner).val.aig, ref := (go aig inner).val.vec.get idx hidx }⟧ =
      (eval assign inner).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
res : RefVecEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, vec := (go aig inner).1.vec } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
h✝ : ¬idx < originalWidth
⊢ ⟦assign.toAIGAssignment, { aig := (go aig inner).1.aig, ref := (go aig inner).1.vec.get (originalWidth - 1) ⋯ }⟧ =
    (eval assign inner).getLsbD (originalWidth - 1)