internlm/Lean-Github huggingface dataset:
Theorem: CNF.eval_congr
Proof state before:
α : Type
f g : α → Bool
x : CNF α
w : ∀ (i : α), mem i x → f i = g i
⊢ eval f x = eval g x
Tactic:
induction x
Proof state after:
case nil
α : Type
f g : α → Bool
w : ∀ (i : α), mem i [] → f i = g i
⊢ eval f [] = eval g []

case cons
α : Type
f g : α → Bool
head✝ : Clause α
tail✝ : List (Clause α)
tail_ih✝ : (∀ (i : α), mem i tail✝ → f i = g i) → eval f tail✝ = eval g tail✝
w : ∀ (i : α), mem i (head✝ :: tail✝) → f i = g i
⊢ eval f (head✝ :: tail✝) = eval g (head✝ :: tail✝)
Theorem: CNF.eval_congr
Proof state before:
α : Type
f g : α → Bool
w : ∀ (i : α), mem i [] → f i = g i
⊢ eval f [] = eval g []
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: CNF.eval_congr
Proof state before:
α : Type
f g : α → Bool
w : ∀ (i : α), mem i [] → f i = g i
⊢ eval f [] = eval g []
Tactic:
rfl
Proof state after:
no goals
Theorem: CNF.eval_congr
Proof state before:
α : Type
f g : α → Bool
c : Clause α
x : List (Clause α)
ih : (∀ (i : α), mem i x → f i = g i) → eval f x = eval g x
w : ∀ (i : α), mem i (c :: x) → f i = g i
⊢ eval f (c :: x) = eval g (c :: x)
Tactic:
simp only [eval_succ]
Proof state after:
α : Type
f g : α → Bool
c : Clause α
x : List (Clause α)
ih : (∀ (i : α), mem i x → f i = g i) → eval f x = eval g x
w : ∀ (i : α), mem i (c :: x) → f i = g i
⊢ (Clause.eval f c && eval f x) = (Clause.eval g c && eval g x)
Theorem: CNF.eval_congr
Proof state before:
α : Type
f g : α → Bool
c : Clause α
x : List (Clause α)
ih : (∀ (i : α), mem i x → f i = g i) → eval f x = eval g x
w : ∀ (i : α), mem i (c :: x) → f i = g i
⊢ ∀ (i : α), mem i x → f i = g i
Tactic:
intro i h
Proof state after:
α : Type
f g : α → Bool
c : Clause α
x : List (Clause α)
ih : (∀ (i : α), mem i x → f i = g i) → eval f x = eval g x
w : ∀ (i : α), mem i (c :: x) → f i = g i
i : α
h : mem i x
⊢ f i = g i
Theorem: CNF.eval_congr
Proof state before:
α : Type
f g : α → Bool
c : Clause α
x : List (Clause α)
ih : (∀ (i : α), mem i x → f i = g i) → eval f x = eval g x
w : ∀ (i : α), mem i (c :: x) → f i = g i
i : α
h : mem i x
⊢ f i = g i
Tactic:
apply w
Proof state after:
case a
α : Type
f g : α → Bool
c : Clause α
x : List (Clause α)
ih : (∀ (i : α), mem i x → f i = g i) → eval f x = eval g x
w : ∀ (i : α), mem i (c :: x) → f i = g i
i : α
h : mem i x
⊢ mem i (c :: x)
Theorem: CNF.eval_congr
Proof state before:
case a
α : Type
f g : α → Bool
c : Clause α
x : List (Clause α)
ih : (∀ (i : α), mem i x → f i = g i) → eval f x = eval g x
w : ∀ (i : α), mem i (c :: x) → f i = g i
i : α
h : mem i x
⊢ mem i (c :: x)
Tactic:
simp [h]
Proof state after:
no goals
Theorem: bitvec_160
Proof state before:
⊢ ∀ (x C1 C2 : BitVec 7), x <<< C2 * C1 = x * C1 <<< C2
Tactic:
intros
Proof state after:
x✝ C1✝ C2✝ : BitVec 7
⊢ x✝ <<< C2✝ * C1✝ = x✝ * C1✝ <<< C2✝
Theorem: bitvec_160
Proof state before:
x✝ C1✝ C2✝ : BitVec 7
⊢ x✝ <<< C2✝ * C1✝ = x✝ * C1✝ <<< C2✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AddSub_1156
Proof state before:
⊢ ∀ (b : BitVec 64), b + b = b <<< 1
Tactic:
intros
Proof state after:
b✝ : BitVec 64
⊢ b✝ + b✝ = b✝ <<< 1
Theorem: bitvec_AddSub_1156
Proof state before:
b✝ : BitVec 64
⊢ b✝ + b✝ = b✝ <<< 1
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AddSub_1202
Proof state before:
⊢ ∀ (x C : BitVec 64), (x ^^^ -1) + C = C - 1 - x
Tactic:
intros
Proof state after:
x✝ C✝ : BitVec 64
⊢ (x✝ ^^^ -1) + C✝ = C✝ - 1 - x✝
Theorem: bitvec_AddSub_1202
Proof state before:
x✝ C✝ : BitVec 64
⊢ (x✝ ^^^ -1) + C✝ = C✝ - 1 - x✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: t1
Proof state before:
x y : BitVec 64
h : x = y
⊢ ~~~x &&& y = ~~~y &&& x
Tactic:
bv_decide
Proof state after:
no goals
Theorem: t2
Proof state before:
x y : BitVec 512
h : x = y
⊢ ~~~x &&& y = ~~~y &&& x
Tactic:
bv_decide
Proof state after:
no goals
Theorem: t3
Proof state before:
x y : BitVec 1024
h : x = y
⊢ ~~~x &&& y = ~~~y &&& x
Tactic:
bv_decide
Proof state after:
no goals
Theorem: t4
Proof state before:
x y : BitVec 2048
h : x = y
⊢ ~~~x &&& y = ~~~y &&& x
Tactic:
bv_decide
Proof state after:
no goals
Theorem: t5
Proof state before:
x y : BitVec 4096
h : x = y
⊢ ~~~x &&& y = ~~~y &&& x
Tactic:
bv_decide
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx1 : idx < curr
⊢ idx < newWidth
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
⊢ ∀ (idx : Nat) (hidx1 : idx < curr), (go w hw input newWidth curr hcurr s).getRef idx ⋯ = s.getRef idx hidx1
Tactic:
intro idx hidx
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
⊢ (go w hw input newWidth curr hcurr s).getRef idx ⋯ = s.getRef idx hidx
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
⊢ (go w hw input newWidth curr hcurr s).getRef idx ⋯ = s.getRef idx hidx
Tactic:
unfold go
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
⊢ (if hcurr1 : curr < newWidth then
          if hcurr2 : curr < w then
            let s := s.pushRef (input.getRef curr hcurr2);
            go w hw input newWidth (curr + 1) ⋯ s
          else
            let s := s.pushRef (input.getRef (w - 1) ⋯);
            go w hw input newWidth (curr + 1) ⋯ s
        else
          let_fun hcurr := ⋯;
          hcurr ▸ s).getRef
      idx ⋯ =
    s.getRef idx hidx
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
⊢ (if hcurr1 : curr < newWidth then
          if hcurr2 : curr < w then
            let s := s.pushRef (input.getRef curr hcurr2);
            go w hw input newWidth (curr + 1) ⋯ s
          else
            let s := s.pushRef (input.getRef (w - 1) ⋯);
            go w hw input newWidth (curr + 1) ⋯ s
        else
          let_fun hcurr := ⋯;
          hcurr ▸ s).getRef
      idx ⋯ =
    s.getRef idx hidx
Tactic:
split
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : curr < newWidth
⊢ (if hcurr2 : curr < w then
          let s := s.pushRef (input.getRef curr hcurr2);
          go w hw input newWidth (curr + 1) ⋯ s
        else
          let s := s.pushRef (input.getRef (w - 1) ⋯);
          go w hw input newWidth (curr + 1) ⋯ s).getRef
      idx ⋯ =
    s.getRef idx hidx

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < newWidth
⊢ (let_fun hcurr := ⋯;
        hcurr ▸ s).getRef
      idx ⋯ =
    s.getRef idx hidx
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef_aux
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : curr < newWidth
⊢ (if hcurr2 : curr < w then
          let s := s.pushRef (input.getRef curr hcurr2);
          go w hw input newWidth (curr + 1) ⋯ s
        else
          let s := s.pushRef (input.getRef (w - 1) ⋯);
          go w hw input newWidth (curr + 1) ⋯ s).getRef
      idx ⋯ =
    s.getRef idx hidx

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < newWidth
⊢ (let_fun hcurr := ⋯;
        hcurr ▸ s).getRef
      idx ⋯ =
    s.getRef idx hidx
Tactic:
. dsimp
  split
  all_goals
    rw [go_getRef_aux]
    rw [AIG.RefStream.getRef_push_ref_lt]
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < newWidth
⊢ (let_fun hcurr := ⋯;
        hcurr ▸ s).getRef
      idx ⋯ =
    s.getRef idx hidx
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef_aux
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < newWidth
⊢ (let_fun hcurr := ⋯;
        hcurr ▸ s).getRef
      idx ⋯ =
    s.getRef idx hidx
Tactic:
. dsimp
  simp only [RefStream.getRef, Ref.mk.injEq]
  congr
  . omega
  . simp
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef_aux
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : curr < newWidth
⊢ (if hcurr2 : curr < w then
          let s := s.pushRef (input.getRef curr hcurr2);
          go w hw input newWidth (curr + 1) ⋯ s
        else
          let s := s.pushRef (input.getRef (w - 1) ⋯);
          go w hw input newWidth (curr + 1) ⋯ s).getRef
      idx ⋯ =
    s.getRef idx hidx
Tactic:
dsimp
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : curr < newWidth
⊢ (if hcurr2 : curr < w then go w hw input newWidth (curr + 1) ⋯ (s.pushRef (input.getRef curr hcurr2))
        else go w hw input newWidth (curr + 1) ⋯ (s.pushRef (input.getRef (w - 1) ⋯))).getRef
      idx ⋯ =
    s.getRef idx hidx
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef_aux
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : curr < newWidth
⊢ (if hcurr2 : curr < w then go w hw input newWidth (curr + 1) ⋯ (s.pushRef (input.getRef curr hcurr2))
        else go w hw input newWidth (curr + 1) ⋯ (s.pushRef (input.getRef (w - 1) ⋯))).getRef
      idx ⋯ =
    s.getRef idx hidx
Tactic:
split
Proof state after:
case isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝¹ : curr < newWidth
h✝ : curr < w
⊢ (go w hw input newWidth (curr + 1) ⋯ (s.pushRef (input.getRef curr h✝))).getRef idx ⋯ = s.getRef idx hidx

case isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝¹ : curr < newWidth
h✝ : ¬curr < w
⊢ (go w hw input newWidth (curr + 1) ⋯ (s.pushRef (input.getRef (w - 1) ⋯))).getRef idx ⋯ = s.getRef idx hidx
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef_aux
Proof state before:
case isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝¹ : curr < newWidth
h✝ : curr < w
⊢ (go w hw input newWidth (curr + 1) ⋯ (s.pushRef (input.getRef curr h✝))).getRef idx ⋯ = s.getRef idx hidx

case isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝¹ : curr < newWidth
h✝ : ¬curr < w
⊢ (go w hw input newWidth (curr + 1) ⋯ (s.pushRef (input.getRef (w - 1) ⋯))).getRef idx ⋯ = s.getRef idx hidx
Tactic:
all_goals
  rw [go_getRef_aux]
  rw [AIG.RefStream.getRef_push_ref_lt]
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef_aux
Proof state before:
case isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝¹ : curr < newWidth
h✝ : ¬curr < w
⊢ (go w hw input newWidth (curr + 1) ⋯ (s.pushRef (input.getRef (w - 1) ⋯))).getRef idx ⋯ = s.getRef idx hidx
Tactic:
rw [go_getRef_aux]
Proof state after:
case isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝¹ : curr < newWidth
h✝ : ¬curr < w
⊢ (s.pushRef (input.getRef (w - 1) ⋯)).getRef idx ?isTrue.isFalse.hidx1 = s.getRef idx hidx

case isTrue.isFalse.hidx1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝¹ : curr < newWidth
h✝ : ¬curr < w
⊢ idx < curr + 1
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef_aux
Proof state before:
case isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝¹ : curr < newWidth
h✝ : ¬curr < w
⊢ (s.pushRef (input.getRef (w - 1) ⋯)).getRef idx ?isTrue.isFalse.hidx1 = s.getRef idx hidx

case isTrue.isFalse.hidx1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝¹ : curr < newWidth
h✝ : ¬curr < w
⊢ idx < curr + 1
Tactic:
rw [AIG.RefStream.getRef_push_ref_lt]
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef_aux
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < newWidth
⊢ (let_fun hcurr := ⋯;
        hcurr ▸ s).getRef
      idx ⋯ =
    s.getRef idx hidx
Tactic:
dsimp
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < newWidth
⊢ (⋯ ▸ s).getRef idx ⋯ = s.getRef idx hidx
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef_aux
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < newWidth
⊢ (⋯ ▸ s).getRef idx ⋯ = s.getRef idx hidx
Tactic:
simp only [RefStream.getRef, Ref.mk.injEq]
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < newWidth
⊢ (⋯ ▸ s).refs[idx] = s.refs[idx]
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef_aux
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < newWidth
⊢ (⋯ ▸ s).refs[idx] = s.refs[idx]
Tactic:
congr
Proof state after:
case isFalse.e_xs.h.e_5
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < newWidth
⊢ newWidth = curr

case isFalse.e_xs.h.e_6
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < newWidth
⊢ HEq (⋯ ▸ s) s
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef_aux
Proof state before:
case isFalse.e_xs.h.e_5
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < newWidth
⊢ newWidth = curr

case isFalse.e_xs.h.e_6
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < newWidth
⊢ HEq (⋯ ▸ s) s
Tactic:
. omega
Proof state after:
case isFalse.e_xs.h.e_6
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < newWidth
⊢ HEq (⋯ ▸ s) s
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef_aux
Proof state before:
case isFalse.e_xs.h.e_6
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < newWidth
⊢ HEq (⋯ ▸ s) s
Tactic:
. simp
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef_aux
Proof state before:
case isFalse.e_xs.h.e_5
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < newWidth
⊢ newWidth = curr
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef_aux
Proof state before:
case isFalse.e_xs.h.e_6
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < newWidth
⊢ HEq (⋯ ▸ s) s
Tactic:
simp
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx1 : idx < newWidth
hidx2 : idx < w
⊢ idx < w
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx1 : idx < newWidth
hidx2 : ¬idx < w
⊢ w - 1 < w
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
⊢ ∀ (idx : Nat) (hidx1 : idx < newWidth),
    curr ≤ idx →
      (go w hw input newWidth curr hcurr s).getRef idx hidx1 =
        if hidx2 : idx < w then input.getRef idx ⋯ else input.getRef (w - 1) ⋯
Tactic:
intro idx hidx1 hcurr
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
⊢ (go w hw input newWidth curr hcurr✝ s).getRef idx hidx1 =
    if hidx2 : idx < w then input.getRef idx ⋯ else input.getRef (w - 1) ⋯
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
⊢ (go w hw input newWidth curr hcurr✝ s).getRef idx hidx1 =
    if hidx2 : idx < w then input.getRef idx ⋯ else input.getRef (w - 1) ⋯
Tactic:
unfold go
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
⊢ (if hcurr1 : curr < newWidth then
          if hcurr2 : curr < w then
            let s := s.pushRef (input.getRef curr hcurr2);
            go w hw input newWidth (curr + 1) ⋯ s
          else
            let s := s.pushRef (input.getRef (w - 1) ⋯);
            go w hw input newWidth (curr + 1) ⋯ s
        else
          let_fun hcurr := ⋯;
          hcurr ▸ s).getRef
      idx hidx1 =
    if hidx2 : idx < w then input.getRef idx ⋯ else input.getRef (w - 1) ⋯
Theorem: BVExpr.bitblast.blastSignExtend.go_getRef
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
⊢ (if hcurr1 : curr < newWidth then
          if hcurr2 : curr < w then
            let s := s.pushRef (input.getRef curr hcurr2);
            go w hw input newWidth (curr + 1) ⋯ s
          else
            let s := s.pushRef (input.getRef (w - 1) ⋯);
            go w hw input newWidth (curr + 1) ⋯ s
        else
          let_fun hcurr := ⋯;
          hcurr ▸ s).getRef
      idx hidx1 =
    if hidx2 : idx < w then input.getRef idx ⋯ else input.getRef (w - 1) ⋯
Tactic:
have : curr < newWidth := by omega
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefStream w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefStream curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
this : curr < newWidth
⊢ (if hcurr1 : curr < newWidth then
          if hcurr2 : curr < w then
            let s := s.pushRef (input.getRef curr hcurr2);
            go w hw input newWidth (curr + 1) ⋯ s
          else
            let s := s.pushRef (input.getRef (w - 1) ⋯);
            go w hw input newWidth (curr + 1) ⋯ s
        else
          let_fun hcurr := ⋯;
          hcurr ▸ s).getRef
      idx hidx1 =
    if hidx2 : idx < w then input.getRef idx ⋯ else input.getRef (w - 1) ⋯