internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.go_denote_mem_prefix
Proof state before:
case hprefix
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ IsPrefix { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls (go aig expr).val.aig.decls
Tactic:
apply IsPrefix.of
Proof state after:
case hprefix.idx_eq
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ ∀ (idx : Nat) (h : idx < { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls[idx]

case hprefix.size_le
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size ≤ (go aig expr).val.aig.decls.size
Theorem: BVExpr.bitblast.go_denote_mem_prefix
Proof state before:
case hprefix.idx_eq
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ ∀ (idx : Nat) (h : idx < { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls[idx]

case hprefix.size_le
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size ≤ (go aig expr).val.aig.decls.size
Tactic:
. intros
  apply go_decl_eq
Proof state after:
case hprefix.size_le
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size ≤ (go aig expr).val.aig.decls.size
Theorem: BVExpr.bitblast.go_denote_mem_prefix
Proof state before:
case hprefix.size_le
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size ≤ (go aig expr).val.aig.decls.size
Tactic:
. intros
  apply (go aig expr).property
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_mem_prefix
Proof state before:
case hprefix.idx_eq
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ ∀ (idx : Nat) (h : idx < { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls[idx]
Tactic:
intros
Proof state after:
case hprefix.idx_eq
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
idx✝ : Nat
h✝ : idx✝ < { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size
⊢ (go aig expr).val.aig.decls[idx✝] = { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls[idx✝]
Theorem: BVExpr.bitblast.go_denote_mem_prefix
Proof state before:
case hprefix.idx_eq
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
idx✝ : Nat
h✝ : idx✝ < { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size
⊢ (go aig expr).val.aig.decls[idx✝] = { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls[idx✝]
Tactic:
apply go_decl_eq
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_mem_prefix
Proof state before:
case hprefix.size_le
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size ≤ (go aig expr).val.aig.decls.size
Tactic:
apply (go aig expr).property
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
Tactic:
intro idx hidx
Proof state after:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
    (eval assign expr).getLsb idx
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case const
w : Nat
assign : Assignment
w✝ : Nat
val✝ : BitVec w✝
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦{ aig := (go aig (const val✝)).val.aig, ref := (go aig (const val✝)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (const val✝)).getLsb idx
Tactic:
simp [go, blastConst_eq_eval_getLsb]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case var
w : Nat
assign : Assignment
w✝ idx✝ : Nat
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦{ aig := (go aig (var idx✝)).val.aig, ref := (go aig (var idx✝)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (var idx✝)).getLsb idx
Tactic:
simp [go, hidx, blastVar_eq_eval_getLsb]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case zeroExtend
w : Nat
assign : Assignment
w✝ v : 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 < v
⊢ ⟦{ aig := (go aig (zeroExtend v inner)).val.aig, ref := (go aig (zeroExtend v inner)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (zeroExtend v inner)).getLsb idx
Tactic:
simp only [go, blastZeroExtend_eq_eval_getLsb, ih, dite_eq_ite, Bool.if_false_right,
  eval_zeroExtend, BitVec.getLsb_zeroExtend, hidx, decide_True, Bool.true_and,
  Bool.and_iff_right_iff_imp, decide_eq_true_eq]
Proof state after:
case zeroExtend
w : Nat
assign : Assignment
w✝ v : 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 < v
⊢ (eval assign inner).getLsb idx = true → idx < w✝
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case zeroExtend
w : Nat
assign : Assignment
w✝ v : 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 < v
⊢ (eval assign inner).getLsb idx = true → idx < w✝
Tactic:
apply BitVec.lt_of_getLsb
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case append
w : Nat
assign : Assignment
l✝ r✝ : Nat
lhs : BVExpr l✝
rhs : BVExpr r✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < l✝),
    ⟦{ 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 < r✝),
    ⟦{ 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 < l✝ + r✝
⊢ ⟦{ aig := (go aig (lhs.append rhs)).val.aig, ref := (go aig (lhs.append rhs)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (lhs.append rhs)).getLsb idx
Tactic:
rename_i lw rw
Proof state after:
case append
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ 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 < rw),
    ⟦{ 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 < lw + rw
⊢ ⟦{ aig := (go aig (lhs.append rhs)).val.aig, ref := (go aig (lhs.append rhs)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (lhs.append rhs)).getLsb idx
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case append
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ 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 < rw),
    ⟦{ 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 < lw + rw
⊢ ⟦{ aig := (go aig (lhs.append rhs)).val.aig, ref := (go aig (lhs.append rhs)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (lhs.append rhs)).getLsb idx
Tactic:
simp only [go, blastAppend_eq_eval_getLsb, RefStream.getRef_cast, Ref_cast', eval_append,
  BitVec.getLsb_append]
Proof state after:
case append
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ 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 < rw),
    ⟦{ 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 < lw + rw
⊢ (if h : idx < rw then
      ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := (go (go aig lhs).1.aig rhs).1.stream.getRef idx ⋯ },
        assign.toAIGAssignment⟧
    else
      ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
        assign.toAIGAssignment⟧) =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case append
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ 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 < rw),
    ⟦{ 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 < lw + rw
⊢ (if h : idx < rw then
      ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := (go (go aig lhs).1.aig rhs).1.stream.getRef idx ⋯ },
        assign.toAIGAssignment⟧
    else
      ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
        assign.toAIGAssignment⟧) =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)
Tactic:
split
Proof state after:
case append.isTrue
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ 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 < rw),
    ⟦{ 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 < lw + rw
h✝ : idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := (go (go aig lhs).1.aig rhs).1.stream.getRef idx ⋯ },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)

case append.isFalse
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ 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 < rw),
    ⟦{ 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 < lw + rw
h✝ : ¬idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case append.isTrue
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ 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 < rw),
    ⟦{ 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 < lw + rw
h✝ : idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := (go (go aig lhs).1.aig rhs).1.stream.getRef idx ⋯ },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)

case append.isFalse
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ 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 < rw),
    ⟦{ 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 < lw + rw
h✝ : ¬idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)
Tactic:
. next hsplit =>
  simp only [hsplit, decide_True, cond_true]
  rw [rih]
Proof state after:
case append.isFalse
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ 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 < rw),
    ⟦{ 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 < lw + rw
h✝ : ¬idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case append.isFalse
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ 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 < rw),
    ⟦{ 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 < lw + rw
h✝ : ¬idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)
Tactic:
. next hsplit =>
  simp only [hsplit, decide_False, cond_false]
  rw [go_denote_mem_prefix, lih]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case append.isTrue
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ 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 < rw),
    ⟦{ 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 < lw + rw
h✝ : idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := (go (go aig lhs).1.aig rhs).1.stream.getRef idx ⋯ },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)
Tactic:
next hsplit =>
simp only [hsplit, decide_True, cond_true]
rw [rih]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ 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 < rw),
    ⟦{ 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 < lw + rw
hsplit : idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := (go (go aig lhs).1.aig rhs).1.stream.getRef idx ⋯ },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)
Tactic:
simp only [hsplit, decide_True, cond_true]
Proof state after:
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ 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 < rw),
    ⟦{ 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 < lw + rw
hsplit : idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := (go (go aig lhs).1.aig rhs).1.stream.getRef idx ⋯ },
      assign.toAIGAssignment⟧ =
    (eval assign rhs).getLsb idx
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ 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 < rw),
    ⟦{ 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 < lw + rw
hsplit : idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := (go (go aig lhs).1.aig rhs).1.stream.getRef idx ⋯ },
      assign.toAIGAssignment⟧ =
    (eval assign rhs).getLsb idx
Tactic:
rw [rih]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case append.isFalse
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ 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 < rw),
    ⟦{ 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 < lw + rw
h✝ : ¬idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)
Tactic:
next hsplit =>
simp only [hsplit, decide_False, cond_false]
rw [go_denote_mem_prefix, lih]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ 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 < rw),
    ⟦{ 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 < lw + rw
hsplit : ¬idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)
Tactic:
simp only [hsplit, decide_False, cond_false]
Proof state after:
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ 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 < rw),
    ⟦{ 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 < lw + rw
hsplit : ¬idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    (eval assign lhs).getLsb (idx - rw)
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ 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 < rw),
    ⟦{ 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 < lw + rw
hsplit : ¬idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    (eval assign lhs).getLsb (idx - rw)
Tactic:
rw [go_denote_mem_prefix, lih]
Proof state after:
no goals