internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_eq_eval_getLsb
Proof state before:
case isTrue.inr.isFalse.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry α w
h✝³ : curr < w
h✝² : curr < idx
h✝¹ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
h✝ : idx < distance
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx1 }, assign⟧ = false

case isTrue.inr.isFalse.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry α w
h✝³ : curr < w
h✝² : curr < idx
h✝¹ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
h✝ : ¬idx < distance
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx1 }, assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (idx - distance) ⋯ }, assign⟧
Tactic:
. omega
Proof state after:
case isTrue.inr.isFalse.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry α w
h✝³ : curr < w
h✝² : curr < idx
h✝¹ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
h✝ : ¬idx < distance
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx1 }, assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (idx - distance) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_eq_eval_getLsb
Proof state before:
case isTrue.inr.isFalse.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry α w
h✝³ : curr < w
h✝² : curr < idx
h✝¹ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
h✝ : ¬idx < distance
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx1 }, assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (idx - distance) ⋯ }, assign⟧
Tactic:
. next hidx =>
  rw [← hgo]
  rw [go_eq_eval_getLsb]
  . simp [hidx]
  . omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_eq_eval_getLsb
Proof state before:
case isTrue.inr.isFalse.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry α w
h✝³ : curr < w
h✝² : curr < idx
h✝¹ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
h✝ : idx < distance
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx1 }, assign⟧ = false
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_eq_eval_getLsb
Proof state before:
case isTrue.inr.isFalse.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry α w
h✝³ : curr < w
h✝² : curr < idx
h✝¹ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
h✝ : ¬idx < distance
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx1 }, assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (idx - distance) ⋯ }, assign⟧
Tactic:
next hidx =>
rw [← hgo]
rw [go_eq_eval_getLsb]
. simp [hidx]
. omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry α w
h✝² : curr < w
h✝¹ : curr < idx
h✝ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
hidx : ¬idx < distance
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx1 }, assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (idx - distance) ⋯ }, assign⟧
Tactic:
rw [← hgo]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry α w
h✝² : curr < w
h✝¹ : curr < idx
h✝ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
hidx : ¬idx < distance
⊢ ⟦{ aig := (go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯))).aig,
        ref :=
          (go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯))).stream.getRef idx hidx1 },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (idx - distance) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry α w
h✝² : curr < w
h✝¹ : curr < idx
h✝ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
hidx : ¬idx < distance
⊢ ⟦{ aig := (go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯))).aig,
        ref :=
          (go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯))).stream.getRef idx hidx1 },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (idx - distance) ⋯ }, assign⟧
Tactic:
rw [go_eq_eval_getLsb]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry α w
h✝² : curr < w
h✝¹ : curr < idx
h✝ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
hidx : ¬idx < distance
⊢ (if hidx : idx < distance then false else ⟦{ aig := aig, ref := input.getRef (idx - distance) ⋯ }, assign⟧) =
    ⟦{ aig := aig, ref := input.getRef (idx - distance) ⋯ }, assign⟧

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry α w
h✝² : curr < w
h✝¹ : curr < idx
h✝ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
hidx : ¬idx < distance
⊢ curr + 1 ≤ idx
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry α w
h✝² : curr < w
h✝¹ : curr < idx
h✝ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
hidx : ¬idx < distance
⊢ (if hidx : idx < distance then false else ⟦{ aig := aig, ref := input.getRef (idx - distance) ⋯ }, assign⟧) =
    ⟦{ aig := aig, ref := input.getRef (idx - distance) ⋯ }, assign⟧

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry α w
h✝² : curr < w
h✝¹ : curr < idx
h✝ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
hidx : ¬idx < distance
⊢ curr + 1 ≤ idx
Tactic:
. simp [hidx]
Proof state after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry α w
h✝² : curr < w
h✝¹ : curr < idx
h✝ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
hidx : ¬idx < distance
⊢ curr + 1 ≤ idx
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_eq_eval_getLsb
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry α w
h✝² : curr < w
h✝¹ : curr < idx
h✝ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
hidx : ¬idx < distance
⊢ curr + 1 ≤ idx
Tactic:
. omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry α w
h✝² : curr < w
h✝¹ : curr < idx
h✝ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
hidx : ¬idx < distance
⊢ (if hidx : idx < distance then false else ⟦{ aig := aig, ref := input.getRef (idx - distance) ⋯ }, assign⟧) =
    ⟦{ aig := aig, ref := input.getRef (idx - distance) ⋯ }, assign⟧
Tactic:
simp [hidx]
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_eq_eval_getLsb
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry α w
h✝² : curr < w
h✝¹ : curr < idx
h✝ : ¬curr < distance
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - distance) ⋯)) = res
hidx : ¬idx < distance
⊢ curr + 1 ≤ idx
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastShiftLeftConst.go_eq_eval_getLsb
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
assign : α → Bool
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry α w
h✝ : ¬curr < w
hgo :
  (let_fun hcurr := ⋯;
    { aig := aig, stream := hcurr ▸ s }) =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx1 }, assign⟧ =
    if hidx : idx < distance then false else ⟦{ aig := aig, ref := input.getRef (idx - distance) ⋯ }, assign⟧
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastShiftLeft_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx : Nat
hidx✝ : idx < w
hidx : ¬idx < target.distance
⊢ idx - target.distance < w
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastShiftLeft_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (blastShiftLeftConst aig target).aig, ref := (blastShiftLeftConst aig target).stream.getRef idx hidx },
        assign⟧ =
      if hidx : idx < target.distance then false
      else ⟦{ aig := aig, ref := target.stream.getRef (idx - target.distance) ⋯ }, assign⟧
Tactic:
intros
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (blastShiftLeftConst aig target).aig, ref := (blastShiftLeftConst aig target).stream.getRef idx✝ hidx✝ },
      assign⟧ =
    if hidx : idx✝ < target.distance then false
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastShiftLeft_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (blastShiftLeftConst aig target).aig, ref := (blastShiftLeftConst aig target).stream.getRef idx✝ hidx✝ },
      assign⟧ =
    if hidx : idx✝ < target.distance then false
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance) ⋯ }, assign⟧
Tactic:
unfold blastShiftLeftConst
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{
        aig :=
          (match target with
            | { stream := input, distance := distance } =>
              blastShiftLeftConst.go aig input distance 0 ⋯ RefStream.empty).aig,
        ref :=
          (match target with
                | { stream := input, distance := distance } =>
                  blastShiftLeftConst.go aig input distance 0 ⋯ RefStream.empty).stream.getRef
            idx✝ hidx✝ },
      assign⟧ =
    if hidx : idx✝ < target.distance then false
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastShiftLeft_eq_eval_getLsb
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{
        aig :=
          (match target with
            | { stream := input, distance := distance } =>
              blastShiftLeftConst.go aig input distance 0 ⋯ RefStream.empty).aig,
        ref :=
          (match target with
                | { stream := input, distance := distance } =>
                  blastShiftLeftConst.go aig input distance 0 ⋯ RefStream.empty).stream.getRef
            idx✝ hidx✝ },
      assign⟧ =
    if hidx : idx✝ < target.distance then false
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - target.distance) ⋯ }, assign⟧
Tactic:
apply blastShiftLeftConst.go_eq_eval_getLsb
Proof state after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ 0 ≤ idx✝
Theorem: BVExpr.bitblast.blastShiftLeft_eq_eval_getLsb
Proof state before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ 0 ≤ idx✝
Tactic:
omega
Proof state after:
no goals
Theorem: bitvec_AndOrXor_144
Proof state before:
⊢ ∀ (X C1 C2 : BitVec 64), (X ||| C1) &&& C2 = (X ||| C1 &&& C2) &&& C2
Tactic:
intros
Proof state after:
X✝ C1✝ C2✝ : BitVec 64
⊢ (X✝ ||| C1✝) &&& C2✝ = (X✝ ||| C1✝ &&& C2✝) &&& C2✝
Theorem: bitvec_AndOrXor_144
Proof state before:
X✝ C1✝ C2✝ : BitVec 64
⊢ (X✝ ||| C1✝) &&& C2✝ = (X✝ ||| C1✝ &&& C2✝) &&& C2✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2247__A__B__A__B
Proof state before:
⊢ ∀ (A B : BitVec 64), A ^^^ -1 ||| B ^^^ -1 = A &&& B ^^^ -1
Tactic:
intros
Proof state after:
A✝ B✝ : BitVec 64
⊢ A✝ ^^^ -1 ||| B✝ ^^^ -1 = A✝ &&& B✝ ^^^ -1
Theorem: bitvec_AndOrXor_2247__A__B__A__B
Proof state before:
A✝ B✝ : BitVec 64
⊢ A✝ ^^^ -1 ||| B✝ ^^^ -1 = A✝ &&& B✝ ^^^ -1
Tactic:
bv_decide
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVExpr.and_congr
Proof state before:
w : Nat
lhs rhs lhs' rhs' : BitVec w
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ lhs' &&& rhs' = lhs &&& rhs
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVExpr.or_congr
Proof state before:
w : Nat
lhs rhs lhs' rhs' : BitVec w
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ lhs' ||| rhs' = lhs ||| rhs
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVExpr.xor_congr
Proof state before:
w : Nat
lhs rhs lhs' rhs' : BitVec w
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ lhs' ^^^ rhs' = lhs ^^^ rhs
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVExpr.not_congr
Proof state before:
w : Nat
x x' : BitVec w
h : x = x'
⊢ ~~~x' = ~~~x
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVExpr.shiftLeft_congr
Proof state before:
n w : Nat
x x' : BitVec w
h : x = x'
⊢ x' <<< n = x <<< n
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVExpr.shiftRight_congr
Proof state before:
n w : Nat
x x' : BitVec w
h : x = x'
⊢ x' >>> n = x >>> n
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVExpr.arithShiftRight_congr
Proof state before:
n w : Nat
x x' : BitVec w
h : x = x'
⊢ x'.sshiftRight n = x.sshiftRight n
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVExpr.add_congr
Proof state before:
w : Nat
lhs rhs lhs' rhs' : BitVec w
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ lhs' + rhs' = lhs + rhs
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVExpr.zeroExtend_congr
Proof state before:
n w : Nat
x x' : BitVec w
h1 : x = x'
⊢ BitVec.zeroExtend n x' = BitVec.zeroExtend n x
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVExpr.signExtend_congr
Proof state before:
n w : Nat
x x' : BitVec w
h1 : x = x'
⊢ BitVec.signExtend n x' = BitVec.signExtend n x
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVExpr.append_congr
Proof state before:
lw rw : Nat
lhs lhs' : BitVec lw
rhs rhs' : BitVec rw
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ lhs' ++ rhs' = lhs ++ rhs
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVExpr.extract_congr
Proof state before:
hi lo w : Nat
x x' : BitVec w
h1 : x = x'
⊢ BitVec.extractLsb hi lo x' = BitVec.extractLsb hi lo x
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVExpr.rotateLeft_congr
Proof state before:
n w : Nat
x x' : BitVec w
h : x = x'
⊢ x'.rotateLeft n = x.rotateLeft n
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVExpr.rotateRight_congr
Proof state before:
n w : Nat
x x' : BitVec w
h : x = x'
⊢ x'.rotateRight n = x.rotateRight n
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVPred.beq_congr
Proof state before:
w : Nat
lhs rhs lhs' rhs' : BitVec w
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ (lhs' == rhs') = (lhs == rhs)
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVPred.ult_congr
Proof state before:
w : Nat
lhs rhs lhs' rhs' : BitVec w
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ lhs'.ult rhs' = lhs.ult rhs
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVPred.getLsb_congr
Proof state before:
i w : Nat
e e' : BitVec w
h : e' = e
⊢ e'.getLsb i = e.getLsb i
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVPred.ofBool_congr
Proof state before:
b : Bool
e' : BitVec 1
h : e' = BitVec.ofBool b
⊢ e'.getLsb 0 = b
Tactic:
cases b <;> simp [h]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVLogical.not_congr
Proof state before:
x x' : Bool
h : x' = x
⊢ (!x') = !x
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVLogical.and_congr
Proof state before:
lhs rhs lhs' rhs' : Bool
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ (lhs' && rhs') = (lhs && rhs)
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVLogical.or_congr
Proof state before:
lhs rhs lhs' rhs' : Bool
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ (lhs' || rhs') = (lhs || rhs)
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVLogical.xor_congr
Proof state before:
lhs rhs lhs' rhs' : Bool
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ xor lhs' rhs' = xor lhs rhs
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.ReifiedBVLogical.beq_congr
Proof state before:
lhs rhs lhs' rhs' : Bool
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ (lhs' == rhs') = (lhs == rhs)
Tactic:
simp[*]
Proof state after:
no goals
Theorem: BVDecide.SatAtBVLogical.false_of_eq_true_of_eq_false
Proof state before:
x : Bool
h₁ : x = true
h₂ : x = false
⊢ False
Tactic:
cases h₁
Proof state after:
case refl
h₂ : true = false
⊢ False
Theorem: BVDecide.SatAtBVLogical.false_of_eq_true_of_eq_false
Proof state before:
case refl
h₂ : true = false
⊢ False
Tactic:
cases h₂
Proof state after:
no goals
Theorem: BVDecide.unsat_of_verifyBVExpr_eq_true
Proof state before:
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ bv.unsat
Tactic:
apply BVLogicalExpr.unsat_of_bitblast
Proof state after:
case a
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ bv.bitblast.unsat
Theorem: BVDecide.unsat_of_verifyBVExpr_eq_true
Proof state before:
case a
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ bv.bitblast.unsat
Tactic:
rw [← AIG.Entrypoint.relabelNat_unsat_iff]
Proof state after:
case a
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ bv.bitblast.relabelNat.unsat
Theorem: BVDecide.unsat_of_verifyBVExpr_eq_true
Proof state before:
case a
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ bv.bitblast.relabelNat.unsat
Tactic:
rw [← AIG.toCNF_equisat]
Proof state after:
case a
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ (AIG.toCNF bv.bitblast.relabelNat).unsat
Theorem: BVDecide.unsat_of_verifyBVExpr_eq_true
Proof state before:
case a
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ (AIG.toCNF bv.bitblast.relabelNat).unsat
Tactic:
apply verifyCert_correct
Proof state after:
case a.a
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ verifyCert (LratFormula.ofCnf (AIG.toCNF bv.bitblast.relabelNat)) ?a.cert✝ = true

case a.cert
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ LratCert
Theorem: BVDecide.unsat_of_verifyBVExpr_eq_true
Proof state before:
case a.a
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ verifyCert (LratFormula.ofCnf (AIG.toCNF bv.bitblast.relabelNat)) ?a.cert✝ = true

case a.cert
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ LratCert
Tactic:
rw [verifyBVExpr] at h
Proof state after:
case a.a
bv : BVLogicalExpr
c : LratCert
h✝ : verifyBVExpr bv c = true
h : verifyCert (LratFormula.ofCnf (AIG.toCNF bv.bitblast.relabelNat)) c = true
⊢ verifyCert (LratFormula.ofCnf (AIG.toCNF bv.bitblast.relabelNat)) ?a.cert✝ = true

case a.cert
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ LratCert
Theorem: BVDecide.unsat_of_verifyBVExpr_eq_true
Proof state before:
case a.a
bv : BVLogicalExpr
c : LratCert
h✝ : verifyBVExpr bv c = true
h : verifyCert (LratFormula.ofCnf (AIG.toCNF bv.bitblast.relabelNat)) c = true
⊢ verifyCert (LratFormula.ofCnf (AIG.toCNF bv.bitblast.relabelNat)) ?a.cert✝ = true

case a.cert
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ LratCert
Tactic:
assumption
Proof state after:
no goals
Theorem: LRAT.DefaultClause.not_tautology
Proof state before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ ¬l ∈ c.toList ∨ ¬l.negateLiteral ∈ c.toList
Tactic:
simp only [toList, negateLiteral]
Proof state after:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause