internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ 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 < w✝),
    ⟦{ 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 < w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref :=
            { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.lhs.getRef idx hidx },
        assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx

case bin.add.hright
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ 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 < w✝),
    ⟦{ 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 < w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref :=
            { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.rhs.getRef idx hidx },
        assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
Tactic:
. intros
  dsimp
  rw [go_denote_mem_prefix]
  rw [← lih (aig := aig)]
  . simp
  . assumption
  . simp [Ref.hgate]
Proof state after:
case bin.add.hright
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ 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 < w✝),
    ⟦{ 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 < w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref :=
            { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.rhs.getRef idx hidx },
        assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case bin.add.hright
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ 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 < w✝),
    ⟦{ 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 < w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref :=
            { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.rhs.getRef idx hidx },
        assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
Tactic:
. intros
  rw [← rih]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ 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 < w✝),
    ⟦{ 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 < w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref :=
            { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.lhs.getRef idx hidx },
        assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
Tactic:
intros
Proof state after:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ 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 < w✝),
    ⟦{ 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 < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref :=
          { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.lhs.getRef idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (eval assign lhs).getLsb idx✝
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ 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 < w✝),
    ⟦{ 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 < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref :=
          { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.lhs.getRef idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (eval assign lhs).getLsb idx✝
Tactic:
dsimp
Proof state after:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ 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 < w✝),
    ⟦{ 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 < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := ((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (eval assign lhs).getLsb idx✝
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ 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 < w✝),
    ⟦{ 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 < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := ((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (eval assign lhs).getLsb idx✝
Tactic:
rw [go_denote_mem_prefix]
Proof state after:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ 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 < w✝),
    ⟦{ 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 < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (go aig lhs).1.aig,
        ref := { gate := (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate, hgate := ?bin.add.hleft.hstart } },
      assign.toAIGAssignment⟧ =
    (eval assign lhs).getLsb idx✝

case bin.add.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ 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 < w✝),
    ⟦{ 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 < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case bin.add.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ 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 < w✝),
    ⟦{ 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 < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size

case bin.add.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ 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 < w✝),
    ⟦{ 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 < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size
Tactic:
. simp [Ref.hgate]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ 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 < w✝),
    ⟦{ 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 < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (go aig lhs).1.aig,
        ref := { gate := (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate, hgate := ?bin.add.hleft.hstart } },
      assign.toAIGAssignment⟧ =
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx✝ ?bin.add.hleft.hidx },
      assign.toAIGAssignment⟧
Tactic:
simp
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case bin.add.hleft.hidx
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ 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 < w✝),
    ⟦{ 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 < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ idx✝ < w✝
Tactic:
assumption
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case bin.add.hleft.hstart
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ 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 < w✝),
    ⟦{ 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 < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ (((go aig lhs).1.stream.cast ⋯).getRef idx✝ hidx✝).gate < (go aig lhs).1.aig.decls.size
Tactic:
simp [Ref.hgate]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case bin.add.hright
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ 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 < w✝),
    ⟦{ 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 < w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref :=
            { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.rhs.getRef idx hidx },
        assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
Tactic:
intros
Proof state after:
case bin.add.hright
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ 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 < w✝),
    ⟦{ 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 < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref :=
          { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.rhs.getRef idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (eval assign rhs).getLsb idx✝
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case bin.add.hright
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ 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 < w✝),
    ⟦{ 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 < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref :=
          { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.rhs.getRef idx✝ hidx✝ },
      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 un
w : Nat
assign : Assignment
w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (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
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦{ aig := (go aig (un op expr)).val.aig, ref := (go aig (un op expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un op expr)).getLsb idx
Tactic:
cases op with
| not => simp [go, ih, hidx]
| shiftLeftConst => simp [go, ih, hidx]
| shiftRightConst =>
  simp only [go, blastShiftRight_eq_eval_getLsb, ih, dite_eq_ite, Bool.if_false_right, eval_un,
    BVUnOp.eval_shiftRightConst, BitVec.getLsb_ushiftRight, Bool.and_iff_right_iff_imp,
    decide_eq_true_eq]
  intro h
  apply BitVec.lt_of_getLsb
  assumption
| rotateLeft => simp [go, ih, hidx]
| rotateRight => simp [go, ih, hidx]
| arithShiftRightConst n =>
  rename_i w
  have : ¬(w ≤ idx) := by omega
  simp [go, ih, this, BitVec.getLsb_sshiftRight, BitVec.msb_eq_getLsb_last ]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case un.not
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (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
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦{ aig := (go aig (un BVUnOp.not expr)).val.aig, ref := (go aig (un BVUnOp.not expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un BVUnOp.not expr)).getLsb idx
Tactic:
simp [go, ih, hidx]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case un.shiftLeftConst
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (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
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
⊢ ⟦{ aig := (go aig (un (BVUnOp.shiftLeftConst n✝) expr)).val.aig,
        ref := (go aig (un (BVUnOp.shiftLeftConst n✝) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.shiftLeftConst n✝) expr)).getLsb idx
Tactic:
simp [go, ih, hidx]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case un.shiftRightConst
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (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
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
⊢ ⟦{ aig := (go aig (un (BVUnOp.shiftRightConst n✝) expr)).val.aig,
        ref := (go aig (un (BVUnOp.shiftRightConst n✝) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.shiftRightConst n✝) expr)).getLsb idx
Tactic:
simp only [go, blastShiftRight_eq_eval_getLsb, ih, dite_eq_ite, Bool.if_false_right, eval_un,
  BVUnOp.eval_shiftRightConst, BitVec.getLsb_ushiftRight, Bool.and_iff_right_iff_imp,
  decide_eq_true_eq]
Proof state after:
case un.shiftRightConst
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (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
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
⊢ (eval assign expr).getLsb (n✝ + idx) = true → n✝ + idx < w✝
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case un.shiftRightConst
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (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
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
⊢ (eval assign expr).getLsb (n✝ + idx) = true → n✝ + idx < w✝
Tactic:
intro h
Proof state after:
case un.shiftRightConst
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (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
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
h : (eval assign expr).getLsb (n✝ + idx) = true
⊢ n✝ + idx < w✝
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case un.shiftRightConst
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (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
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
h : (eval assign expr).getLsb (n✝ + idx) = true
⊢ n✝ + idx < w✝
Tactic:
apply BitVec.lt_of_getLsb
Proof state after:
case un.shiftRightConst.a
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (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
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
h : (eval assign expr).getLsb (n✝ + idx) = true
⊢ ?un.shiftRightConst.x.getLsb (n✝ + idx) = true

case un.shiftRightConst.x
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (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
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
h : (eval assign expr).getLsb (n✝ + idx) = true
⊢ BitVec w✝
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case un.shiftRightConst.a
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (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
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
h : (eval assign expr).getLsb (n✝ + idx) = true
⊢ ?un.shiftRightConst.x.getLsb (n✝ + idx) = true

case un.shiftRightConst.x
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (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
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
h : (eval assign expr).getLsb (n✝ + idx) = true
⊢ BitVec w✝
Tactic:
assumption
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case un.rotateLeft
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (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
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
⊢ ⟦{ aig := (go aig (un (BVUnOp.rotateLeft n✝) expr)).val.aig,
        ref := (go aig (un (BVUnOp.rotateLeft n✝) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.rotateLeft n✝) expr)).getLsb idx
Tactic:
simp [go, ih, hidx]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
case un.rotateRight
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (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
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
⊢ ⟦{ aig := (go aig (un (BVUnOp.rotateRight n✝) expr)).val.aig,
        ref := (go aig (un (BVUnOp.rotateRight n✝) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.rotateRight n✝) expr)).getLsb idx
Tactic:
simp [go, ih, hidx]
Proof state after:
no goals