internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.blastRotateRight.go_getRef
Proof state before:
case isTrue.inr.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
h✝¹ : curr < w
heq : curr < idx
h✝ : curr < w - distance % w
⊢ (go input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance % w + curr) ⋯))).getRef idx hidx1 =
    if hidx3 : idx < w - distance % w then input.getRef (distance % w + idx) ⋯
    else input.getRef (idx - (w - distance % w)) ⋯

case isTrue.inr.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
h✝¹ : curr < w
heq : curr < idx
h✝ : ¬curr < w - distance % w
⊢ (go input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - (w - distance % w)) ⋯))).getRef idx hidx1 =
    if hidx3 : idx < w - distance % w then input.getRef (distance % w + idx) ⋯
    else input.getRef (idx - (w - distance % w)) ⋯
Tactic:
. rw [go_getRef]
  omega
Proof state after:
case isTrue.inr.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
h✝¹ : curr < w
heq : curr < idx
h✝ : ¬curr < w - distance % w
⊢ (go input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - (w - distance % w)) ⋯))).getRef idx hidx1 =
    if hidx3 : idx < w - distance % w then input.getRef (distance % w + idx) ⋯
    else input.getRef (idx - (w - distance % w)) ⋯
Theorem: BVExpr.bitblast.blastRotateRight.go_getRef
Proof state before:
case isTrue.inr.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
h✝¹ : curr < w
heq : curr < idx
h✝ : ¬curr < w - distance % w
⊢ (go input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - (w - distance % w)) ⋯))).getRef idx hidx1 =
    if hidx3 : idx < w - distance % w then input.getRef (distance % w + idx) ⋯
    else input.getRef (idx - (w - distance % w)) ⋯
Tactic:
. rw [go_getRef]
  omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastRotateRight.go_getRef
Proof state before:
case isTrue.inr.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
h✝¹ : curr < w
heq : curr < idx
h✝ : curr < w - distance % w
⊢ (go input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance % w + curr) ⋯))).getRef idx hidx1 =
    if hidx3 : idx < w - distance % w then input.getRef (distance % w + idx) ⋯
    else input.getRef (idx - (w - distance % w)) ⋯
Tactic:
rw [go_getRef]
Proof state after:
case isTrue.inr.isTrue.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
h✝¹ : curr < w
heq : curr < idx
h✝ : curr < w - distance % w
⊢ curr + 1 ≤ idx
Theorem: BVExpr.bitblast.blastRotateRight.go_getRef
Proof state before:
case isTrue.inr.isTrue.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
h✝¹ : curr < w
heq : curr < idx
h✝ : curr < w - distance % w
⊢ curr + 1 ≤ idx
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastRotateRight.go_getRef
Proof state before:
case isTrue.inr.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
h✝¹ : curr < w
heq : curr < idx
h✝ : ¬curr < w - distance % w
⊢ (go input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - (w - distance % w)) ⋯))).getRef idx hidx1 =
    if hidx3 : idx < w - distance % w then input.getRef (distance % w + idx) ⋯
    else input.getRef (idx - (w - distance % w)) ⋯
Tactic:
rw [go_getRef]
Proof state after:
case isTrue.inr.isFalse.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
h✝¹ : curr < w
heq : curr < idx
h✝ : ¬curr < w - distance % w
⊢ curr + 1 ≤ idx
Theorem: BVExpr.bitblast.blastRotateRight.go_getRef
Proof state before:
case isTrue.inr.isFalse.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
h✝¹ : curr < w
heq : curr < idx
h✝ : ¬curr < w - distance % w
⊢ curr + 1 ≤ idx
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastRotateRight.go_getRef
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
h✝ : ¬curr < w
⊢ (let_fun hcurr := ⋯;
        hcurr ▸ s).getRef
      idx hidx1 =
    if hidx3 : idx < w - distance % w then input.getRef (distance % w + idx) ⋯
    else input.getRef (idx - (w - distance % w)) ⋯
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastRotateRight_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
hidx2 : idx < w - target.distance % w
⊢ target.distance % w + idx < w
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastRotateRight_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
hidx2 : ¬idx < w - target.distance % w
⊢ idx - (w - target.distance % w) < w
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastRotateRight_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 := (blastRotateRight aig target).aig, ref := (blastRotateRight aig target).stream.getRef idx hidx },
        assign⟧ =
      if hidx2 : idx < w - target.distance % w then
        ⟦{ aig := aig, ref := target.stream.getRef (target.distance % w + idx) ⋯ }, assign⟧
      else ⟦{ aig := aig, ref := target.stream.getRef (idx - (w - target.distance % w)) ⋯ }, 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 := (blastRotateRight aig target).aig, ref := (blastRotateRight aig target).stream.getRef idx✝ hidx✝ },
      assign⟧ =
    if hidx2 : idx✝ < w - target.distance % w then
      ⟦{ aig := aig, ref := target.stream.getRef (target.distance % w + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastRotateRight_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 := (blastRotateRight aig target).aig, ref := (blastRotateRight aig target).stream.getRef idx✝ hidx✝ },
      assign⟧ =
    if hidx2 : idx✝ < w - target.distance % w then
      ⟦{ aig := aig, ref := target.stream.getRef (target.distance % w + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ }, assign⟧
Tactic:
unfold blastRotateRight
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 } =>
              { aig := aig, stream := blastRotateRight.go input distance 0 ⋯ RefStream.empty }).aig,
        ref :=
          (match target with
                | { stream := input, distance := distance } =>
                  { aig := aig, stream := blastRotateRight.go input distance 0 ⋯ RefStream.empty }).stream.getRef
            idx✝ hidx✝ },
      assign⟧ =
    if hidx2 : idx✝ < w - target.distance % w then
      ⟦{ aig := aig, ref := target.stream.getRef (target.distance % w + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastRotateRight_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 } =>
              { aig := aig, stream := blastRotateRight.go input distance 0 ⋯ RefStream.empty }).aig,
        ref :=
          (match target with
                | { stream := input, distance := distance } =>
                  { aig := aig, stream := blastRotateRight.go input distance 0 ⋯ RefStream.empty }).stream.getRef
            idx✝ hidx✝ },
      assign⟧ =
    if hidx2 : idx✝ < w - target.distance % w then
      ⟦{ aig := aig, ref := target.stream.getRef (target.distance % w + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ }, assign⟧
Tactic:
dsimp
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 := aig, ref := (blastRotateRight.go target.stream target.distance 0 ⋯ RefStream.empty).getRef idx✝ hidx✝ },
      assign⟧ =
    if hidx2 : idx✝ < w - target.distance % w then
      ⟦{ aig := aig, ref := target.stream.getRef (target.distance % w + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastRotateRight_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 := aig, ref := (blastRotateRight.go target.stream target.distance 0 ⋯ RefStream.empty).getRef idx✝ hidx✝ },
      assign⟧ =
    if hidx2 : idx✝ < w - target.distance % w then
      ⟦{ aig := aig, ref := target.stream.getRef (target.distance % w + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ }, assign⟧
Tactic:
rw [blastRotateRight.go_getRef]
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 := aig,
        ref :=
          if hidx3 : idx✝ < w - target.distance % w then target.stream.getRef (target.distance % w + idx✝) ⋯
          else target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ },
      assign⟧ =
    if hidx2 : idx✝ < w - target.distance % w then
      ⟦{ aig := aig, ref := target.stream.getRef (target.distance % w + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ }, assign⟧

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.blastRotateRight_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 := aig,
        ref :=
          if hidx3 : idx✝ < w - target.distance % w then target.stream.getRef (target.distance % w + idx✝) ⋯
          else target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ },
      assign⟧ =
    if hidx2 : idx✝ < w - target.distance % w then
      ⟦{ aig := aig, ref := target.stream.getRef (target.distance % w + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ }, assign⟧

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:
. split
  . rfl
  . rfl
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.blastRotateRight_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: BVExpr.bitblast.blastRotateRight_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 := aig,
        ref :=
          if hidx3 : idx✝ < w - target.distance % w then target.stream.getRef (target.distance % w + idx✝) ⋯
          else target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ },
      assign⟧ =
    if hidx2 : idx✝ < w - target.distance % w then
      ⟦{ aig := aig, ref := target.stream.getRef (target.distance % w + idx✝) ⋯ }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ }, assign⟧
Tactic:
split
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
h✝ : idx✝ < w - target.distance % w
⊢ ⟦{ aig := aig, ref := target.stream.getRef (target.distance % w + idx✝) ⋯ }, assign⟧ =
    ⟦{ aig := aig, ref := target.stream.getRef (target.distance % w + idx✝) ⋯ }, assign⟧

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
h✝ : ¬idx✝ < w - target.distance % w
⊢ ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ }, assign⟧ =
    ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastRotateRight_eq_eval_getLsb
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
h✝ : idx✝ < w - target.distance % w
⊢ ⟦{ aig := aig, ref := target.stream.getRef (target.distance % w + idx✝) ⋯ }, assign⟧ =
    ⟦{ aig := aig, ref := target.stream.getRef (target.distance % w + idx✝) ⋯ }, assign⟧

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
h✝ : ¬idx✝ < w - target.distance % w
⊢ ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ }, assign⟧ =
    ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ }, assign⟧
Tactic:
. rfl
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
h✝ : ¬idx✝ < w - target.distance % w
⊢ ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ }, assign⟧ =
    ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ }, assign⟧
Theorem: BVExpr.bitblast.blastRotateRight_eq_eval_getLsb
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
h✝ : ¬idx✝ < w - target.distance % w
⊢ ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ }, assign⟧ =
    ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ }, assign⟧
Tactic:
. rfl
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastRotateRight_eq_eval_getLsb
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
h✝ : idx✝ < w - target.distance % w
⊢ ⟦{ aig := aig, ref := target.stream.getRef (target.distance % w + idx✝) ⋯ }, assign⟧ =
    ⟦{ aig := aig, ref := target.stream.getRef (target.distance % w + idx✝) ⋯ }, assign⟧
Tactic:
rfl
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastRotateRight_eq_eval_getLsb
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
h✝ : ¬idx✝ < w - target.distance % w
⊢ ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ }, assign⟧ =
    ⟦{ aig := aig, ref := target.stream.getRef (idx✝ - (w - target.distance % w)) ⋯ }, assign⟧
Tactic:
rfl
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastRotateRight_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: BoolExpr.eval_map
Proof state before:
α β : Type
x : BoolExpr α
f : α → β
g : β → Bool
⊢ eval g (map f x) = eval (g ∘ f) x
Tactic:
cases x <;> simp_all [map, eval, eval_map]
Proof state after:
no goals
Theorem: BoolExpr.eval_congr
Proof state before:
x : BoolExpr Nat
f g : Nat → Bool
w : ∀ (i : Nat), i < x.vars → f i = g i
⊢ eval f x = eval g x
Tactic:
match x with
| .literal i => dsimp [eval]; apply w; simp
| .const b => rfl
| .not x =>
  dsimp [eval]
  rw [eval_congr f g]
  exact w
| .gate h x y =>
  dsimp [eval]
  rw [eval_congr f g, eval_congr f g]
  exact fun i h => w i (Nat.lt_of_lt_of_le h (Nat.le_max_right _ _))
  exact fun i h => w i (Nat.lt_of_lt_of_le h (Nat.le_max_left _ _))
Proof state after:
no goals
Theorem: BoolExpr.eval_congr
Proof state before:
x : BoolExpr Nat
f g : Nat → Bool
i : Nat
w : ∀ (i_1 : Nat), i_1 < (literal i).vars → f i_1 = g i_1
⊢ eval f (literal i) = eval g (literal i)
Tactic:
dsimp [eval]
Proof state after:
x : BoolExpr Nat
f g : Nat → Bool
i : Nat
w : ∀ (i_1 : Nat), i_1 < (literal i).vars → f i_1 = g i_1
⊢ f i = g i
Theorem: BoolExpr.eval_congr
Proof state before:
x : BoolExpr Nat
f g : Nat → Bool
i : Nat
w : ∀ (i_1 : Nat), i_1 < (literal i).vars → f i_1 = g i_1
⊢ f i = g i
Tactic:
apply w
Proof state after:
case a
x : BoolExpr Nat
f g : Nat → Bool
i : Nat
w : ∀ (i_1 : Nat), i_1 < (literal i).vars → f i_1 = g i_1
⊢ i < (literal i).vars
Theorem: BoolExpr.eval_congr
Proof state before:
case a
x : BoolExpr Nat
f g : Nat → Bool
i : Nat
w : ∀ (i_1 : Nat), i_1 < (literal i).vars → f i_1 = g i_1
⊢ i < (literal i).vars
Tactic:
simp
Proof state after:
no goals
Theorem: BoolExpr.eval_congr
Proof state before:
x : BoolExpr Nat
f g : Nat → Bool
b : Bool
w : ∀ (i : Nat), i < (const b).vars → f i = g i
⊢ eval f (const b) = eval g (const b)
Tactic:
rfl
Proof state after:
no goals
Theorem: BoolExpr.eval_congr
Proof state before:
x✝ : BoolExpr Nat
f g : Nat → Bool
x : BoolExpr Nat
w : ∀ (i : Nat), i < x.not.vars → f i = g i
⊢ eval f x.not = eval g x.not
Tactic:
dsimp [eval]
Proof state after:
x✝ : BoolExpr Nat
f g : Nat → Bool
x : BoolExpr Nat
w : ∀ (i : Nat), i < x.not.vars → f i = g i
⊢ (!eval f x) = !eval g x
Theorem: BoolExpr.eval_congr
Proof state before:
x✝ : BoolExpr Nat
f g : Nat → Bool
x : BoolExpr Nat
w : ∀ (i : Nat), i < x.not.vars → f i = g i
⊢ (!eval f x) = !eval g x
Tactic:
rw [eval_congr f g]
Proof state after:
x✝ : BoolExpr Nat
f g : Nat → Bool
x : BoolExpr Nat
w : ∀ (i : Nat), i < x.not.vars → f i = g i
⊢ ∀ (i : Nat), i < x.vars → f i = g i
Theorem: BoolExpr.eval_congr
Proof state before:
x✝ : BoolExpr Nat
f g : Nat → Bool
x : BoolExpr Nat
w : ∀ (i : Nat), i < x.not.vars → f i = g i
⊢ ∀ (i : Nat), i < x.vars → f i = g i
Tactic:
exact w
Proof state after:
no goals
Theorem: BoolExpr.eval_congr
Proof state before:
x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ eval f (gate h x y) = eval g (gate h x y)
Tactic:
dsimp [eval]
Proof state after:
x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ h.eval (eval f x) (eval f y) = h.eval (eval g x) (eval g y)
Theorem: BoolExpr.eval_congr
Proof state before:
x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ h.eval (eval f x) (eval f y) = h.eval (eval g x) (eval g y)
Tactic:
rw [eval_congr f g, eval_congr f g]
Proof state after:
x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ ∀ (i : Nat), i < y.vars → f i = g i

x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ ∀ (i : Nat), i < x.vars → f i = g i
Theorem: BoolExpr.eval_congr
Proof state before:
x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ ∀ (i : Nat), i < y.vars → f i = g i

x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ ∀ (i : Nat), i < x.vars → f i = g i
Tactic:
exact fun i h => w i (Nat.lt_of_lt_of_le h (Nat.le_max_right _ _))
Proof state after:
x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ ∀ (i : Nat), i < x.vars → f i = g i
Theorem: BoolExpr.eval_congr
Proof state before:
x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ ∀ (i : Nat), i < x.vars → f i = g i
Tactic:
exact fun i h => w i (Nat.lt_of_lt_of_le h (Nat.le_max_left _ _))
Proof state after:
no goals
Theorem: BoolExpr.map_fin_val_attach_go
Proof state before:
x : BoolExpr Nat
k : Nat
h : x.vars ≤ k
⊢ map Fin.val (attach.go x k h) = x
Tactic:
cases x <;> simp [attach.go, map, map_fin_val_attach_go]
Proof state after:
no goals
Theorem: BoolExpr.eval_attach
Proof state before:
x : BoolExpr Nat
f : Fin x.vars → Bool
⊢ eval f x.attach = eval (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) x
Tactic:
generalize h : (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) = f'
Proof state after:
x : BoolExpr Nat
f : Fin x.vars → Bool
f' : Nat → Bool
h : (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) = f'
⊢ eval f x.attach = eval f' x
Theorem: BoolExpr.eval_attach
Proof state before:
x : BoolExpr Nat
f : Fin x.vars → Bool
f' : Nat → Bool
h : (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) = f'
⊢ eval f x.attach = eval f' x
Tactic:
obtain rfl := show f = fun i : Fin _ => f' i by subst h; simp
Proof state after:
x : BoolExpr Nat
f' : Nat → Bool
h : (fun i => if h : i < x.vars then (fun i => f' ↑i) ⟨i, h⟩ else false) = f'
⊢ eval (fun i => f' ↑i) x.attach = eval f' x
Theorem: BoolExpr.eval_attach
Proof state before:
x : BoolExpr Nat
f' : Nat → Bool
h : (fun i => if h : i < x.vars then (fun i => f' ↑i) ⟨i, h⟩ else false) = f'
⊢ eval (fun i => f' ↑i) x.attach = eval f' x
Tactic:
rw [← eval_forget, forget_attach]
Proof state after:
no goals