internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.PPow2.two_mul_sq_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
⊢ i = j
Tactic:
by_contra ne
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.two_mul_sq_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
⊢ False
Tactic:
wlog hij : i < j
Proof state after:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚫₀] {y i j : M},
    Pow2 y → PPow2 i → PPow2 j → y < i ∧ i ≤ 2 * y ^ 2 → y < j ∧ j ≤ 2 * y ^ 2 → ¬i = j → i < j → False
hij : ¬i < j
⊢ False

M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
hij : i < j
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.two_mul_sq_uniq
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
hij : i < j
⊢ False
Tactic:
have : i^2 < (2 * y)^2 := calc
  i^2 ≤ j         := sq_le_of_lt ppi ppj hij
  _   ≤ 2 * y^2   := hj.2
  _   < (2 * y)^2 := by
    simp [sq, mul_assoc]; rw [mul_left_comm]
    exact lt_mul_of_pos_of_one_lt_left (by simpa using pos_iff_ne_zero.mp py.pos) (by simp [one_lt_two])
Proof state after:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
hij : i < j
this : i ^ 2 < (2 * y) ^ 2
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.two_mul_sq_uniq
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
hij : i < j
this : i ^ 2 < (2 * y) ^ 2
⊢ False
Tactic:
have : i < 2 * y := sq_lt_sq.mp this
Proof state after:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
hij : i < j
this✝ : i ^ 2 < (2 * y) ^ 2
this : i < 2 * y
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.two_mul_sq_uniq
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
hij : i < j
this✝ : i ^ 2 < (2 * y) ^ 2
this : i < 2 * y
⊢ False
Tactic:
have : y < y := lt_of_lt_of_le hi.1 ((ppi.pow2.le_iff_lt_two py).mpr this)
Proof state after:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
hij : i < j
this✝¹ : i ^ 2 < (2 * y) ^ 2
this✝ : i < 2 * y
this : y < y
⊢ False
Theorem: LO.FirstOrder.Arith.Model.PPow2.two_mul_sq_uniq
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
hij : i < j
this✝¹ : i ^ 2 < (2 * y) ^ 2
this✝ : i < 2 * y
this : y < y
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.two_mul_sq_uniq
Proof state before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚫₀] {y i j : M},
    Pow2 y → PPow2 i → PPow2 j → y < i ∧ i ≤ 2 * y ^ 2 → y < j ∧ j ≤ 2 * y ^ 2 → ¬i = j → i < j → False
hij : ¬i < j
⊢ False
Tactic:
exact this py ppj ppi hj hi (Ne.symm ne) (Ne.lt_of_le' ne (by simpa using hij))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.two_mul_sq_uniq
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐈𝚫₀] {y i j : M},
    Pow2 y → PPow2 i → PPow2 j → y < i ∧ i ≤ 2 * y ^ 2 → y < j ∧ j ≤ 2 * y ^ 2 → ¬i = j → i < j → False
hij : ¬i < j
⊢ j ≤ i
Tactic:
simpa using hij
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.two_mul_sq_uniq
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
hij : i < j
⊢ 2 * y ^ 2 < (2 * y) ^ 2
Tactic:
simp [sq, mul_assoc]
Proof state after:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
hij : i < j
⊢ y * y < y * (2 * y)
Theorem: LO.FirstOrder.Arith.Model.PPow2.two_mul_sq_uniq
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
hij : i < j
⊢ y * y < y * (2 * y)
Tactic:
rw [mul_left_comm]
Proof state after:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
hij : i < j
⊢ y * y < 2 * (y * y)
Theorem: LO.FirstOrder.Arith.Model.PPow2.two_mul_sq_uniq
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
hij : i < j
⊢ y * y < 2 * (y * y)
Tactic:
exact lt_mul_of_pos_of_one_lt_left (by simpa using pos_iff_ne_zero.mp py.pos) (by simp [one_lt_two])
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.two_mul_sq_uniq
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
hij : i < j
⊢ 0 < y * y
Tactic:
simpa using pos_iff_ne_zero.mp py.pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.PPow2.two_mul_sq_uniq
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y i j : M
py : Pow2 y
ppi : PPow2 i
ppj : PPow2 j
hi : y < i ∧ i ≤ 2 * y ^ 2
hj : y < j ∧ j ≤ 2 * y ^ 2
ne : ¬i = j
hij : i < j
⊢ 1 < 2
Tactic:
simp [one_lt_two]
Proof state after:
no goals
Theorem: red
Proof state before:
hA : 1 = 1
hB : 2 = 2
⊢ 2 = 2
Tactic:
sorry
Proof state after:
no goals
Theorem: redSolved
Proof state before:
hA : 1 = 1
hB : 2 = 2
⊢ 2 = 2
Tactic:
solve
Proof state after:
no goals
Theorem: test_and_then
Proof state before:
⊢ 1 = 1 ∧ 2 = 2
Tactic:
apply And.intro and_then rfl
Proof state after:
no goals
Theorem: test_custom_sorry
Proof state before:
⊢ 1 = 2
Tactic:
custom_sorry_2
Proof state after:
no goals
Theorem: test_faq_have
Proof state before:
⊢ True
Tactic:
custom_let n : Nat := 5
Proof state after:
n : Nat := 5
⊢ True
Theorem: test_faq_have
Proof state before:
n : Nat := 5
⊢ True
Tactic:
custom_have h : n = n := rfl
Proof state after:
n : Nat := 5
h : n = n
⊢ True
Theorem: test_faq_have
Proof state before:
n : Nat := 5
h : n = n
⊢ True
Tactic:
trivial
Proof state after:
no goals
Theorem: test_reverse_goals
Proof state before:
⊢ (1 = 2 ∧ 3 = 4) ∧ 5 = 6
Tactic:
constructor
Proof state after:
case left

⊢ 1 = 2 ∧ 3 = 4

case right

⊢ 5 = 6
Theorem: test_reverse_goals
Proof state before:
case left

⊢ 1 = 2 ∧ 3 = 4

case right

⊢ 5 = 6
Tactic:
constructor
Proof state after:
case left.left

⊢ 1 = 2

case left.right

⊢ 3 = 4

case right

⊢ 5 = 6
Theorem: test_reverse_goals
Proof state before:
case left.left

⊢ 1 = 2

case left.right

⊢ 3 = 4

case right

⊢ 5 = 6
Tactic:
reverse_goals
Proof state after:
case right

⊢ 5 = 6

case left.right

⊢ 3 = 4

case left.left

⊢ 1 = 2
Theorem: test_reverse_goals
Proof state before:
case right

⊢ 5 = 6

case left.right

⊢ 3 = 4

case left.left

⊢ 1 = 2
Tactic:
all_goals sorry
Proof state after:
no goals
Theorem: test_reverse_goals
Proof state before:
case left.left

⊢ 1 = 2
Tactic:
sorry
Proof state after:
no goals
Theorem: gradual
Proof state before:
p q : Prop
⊢ p ∧ q ↔ q ∧ p
Tactic:
step_1
Proof state after:
case red
p q : Prop
⊢ p ∧ q → q ∧ p

case blue
p q : Prop
⊢ q ∧ p → p ∧ q
Theorem: gradual
Proof state before:
case red
p q : Prop
⊢ p ∧ q → q ∧ p

case blue
p q : Prop
⊢ q ∧ p → p ∧ q
Tactic:
step_2
Proof state after:
case red
p q : Prop
hA : p ∧ q
⊢ q ∧ p
Theorem: gradual
Proof state before:
case red
p q : Prop
hA : p ∧ q
⊢ q ∧ p
Tactic:
step_3
Proof state after:
case red1
p q : Prop
hA : p ∧ q
⊢ q

case red2
p q : Prop
hA : p ∧ q
⊢ p
Theorem: gradual
Proof state before:
case red1
p q : Prop
hA : p ∧ q
⊢ q

case red2
p q : Prop
hA : p ∧ q
⊢ p
Tactic:
step_4
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2647
Proof state before:
⊢ ∀ (a b : BitVec 64), a &&& b ^^^ (a ^^^ b) = a ||| b
Tactic:
intros
Proof state after:
a✝ b✝ : BitVec 64
⊢ a✝ &&& b✝ ^^^ (a✝ ^^^ b✝) = a✝ ||| b✝
Theorem: bitvec_AndOrXor_2647
Proof state before:
a✝ b✝ : BitVec 64
⊢ a✝ &&& b✝ ^^^ (a✝ ^^^ b✝) = a✝ ||| b✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: BVLogicalExpr.bitblast.go_eval_eq_eval
Proof state before:
expr : BVLogicalExpr
aig : AIG BVBit
assign : BVExpr.Assignment
⊢ ⟦(ofBoolExprCached.go expr aig BVPred.bitblast).val, assign.toAIGAssignment⟧ = eval assign expr
Tactic:
induction expr generalizing aig with
| const => simp [ofBoolExprCached.go]
| literal => simp [ofBoolExprCached.go]
| not expr ih => simp [ofBoolExprCached.go, ih]
| gate g lhs rhs lih rih => cases g <;> simp [ofBoolExprCached.go, Gate.eval, lih, rih]
Proof state after:
no goals
Theorem: BVLogicalExpr.bitblast.go_eval_eq_eval
Proof state before:
case const
assign : BVExpr.Assignment
a✝ : Bool
aig : AIG BVBit
⊢ ⟦(ofBoolExprCached.go (BoolExpr.const a✝) aig BVPred.bitblast).val, assign.toAIGAssignment⟧ =
    eval assign (BoolExpr.const a✝)
Tactic:
simp [ofBoolExprCached.go]
Proof state after:
no goals
Theorem: BVLogicalExpr.bitblast.go_eval_eq_eval
Proof state before:
case literal
assign : BVExpr.Assignment
a✝ : BVPred
aig : AIG BVBit
⊢ ⟦(ofBoolExprCached.go (BoolExpr.literal a✝) aig BVPred.bitblast).val, assign.toAIGAssignment⟧ =
    eval assign (BoolExpr.literal a✝)
Tactic:
simp [ofBoolExprCached.go]
Proof state after:
no goals
Theorem: BVLogicalExpr.bitblast.go_eval_eq_eval
Proof state before:
case not
assign : BVExpr.Assignment
expr : BoolExpr BVPred
ih :
  ∀ (aig : AIG BVBit), ⟦(ofBoolExprCached.go expr aig BVPred.bitblast).val, assign.toAIGAssignment⟧ = eval assign expr
aig : AIG BVBit
⊢ ⟦(ofBoolExprCached.go expr.not aig BVPred.bitblast).val, assign.toAIGAssignment⟧ = eval assign expr.not
Tactic:
simp [ofBoolExprCached.go, ih]
Proof state after:
no goals
Theorem: BVLogicalExpr.bitblast.go_eval_eq_eval
Proof state before:
case gate
assign : BVExpr.Assignment
g : Gate
lhs rhs : BoolExpr BVPred
lih : ∀ (aig : AIG BVBit), ⟦(ofBoolExprCached.go lhs aig BVPred.bitblast).val, assign.toAIGAssignment⟧ = eval assign lhs
rih : ∀ (aig : AIG BVBit), ⟦(ofBoolExprCached.go rhs aig BVPred.bitblast).val, assign.toAIGAssignment⟧ = eval assign rhs
aig : AIG BVBit
⊢ ⟦(ofBoolExprCached.go (BoolExpr.gate g lhs rhs) aig BVPred.bitblast).val, assign.toAIGAssignment⟧ =
    eval assign (BoolExpr.gate g lhs rhs)
Tactic:
cases g <;> simp [ofBoolExprCached.go, Gate.eval, lih, rih]
Proof state after:
no goals
Theorem: BVLogicalExpr.eval_eq_bitblast_denote
Proof state before:
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ eval assign expr = ⟦expr.bitblast, assign.toAIGAssignment⟧
Tactic:
unfold bitblast
Proof state after:
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ eval assign expr = ⟦ofBoolExprCached expr BVPred.bitblast, assign.toAIGAssignment⟧
Theorem: BVLogicalExpr.eval_eq_bitblast_denote
Proof state before:
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ eval assign expr = ⟦ofBoolExprCached expr BVPred.bitblast, assign.toAIGAssignment⟧
Tactic:
unfold ofBoolExprCached
Proof state after:
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ eval assign expr = ⟦(ofBoolExprCached.go expr empty BVPred.bitblast).val, assign.toAIGAssignment⟧
Theorem: BVLogicalExpr.eval_eq_bitblast_denote
Proof state before:
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ eval assign expr = ⟦(ofBoolExprCached.go expr empty BVPred.bitblast).val, assign.toAIGAssignment⟧
Tactic:
rw [bitblast.go_eval_eq_eval]
Proof state after:
no goals
Theorem: BVLogicalExpr.bitblast_denote_eq_eval
Proof state before:
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ ⟦expr.bitblast, assign.toAIGAssignment⟧ = eval assign expr
Tactic:
unfold bitblast
Proof state after:
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ ⟦ofBoolExprCached expr BVPred.bitblast, assign.toAIGAssignment⟧ = eval assign expr
Theorem: BVLogicalExpr.bitblast_denote_eq_eval
Proof state before:
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ ⟦ofBoolExprCached expr BVPred.bitblast, assign.toAIGAssignment⟧ = eval assign expr
Tactic:
unfold ofBoolExprCached
Proof state after:
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ ⟦(ofBoolExprCached.go expr empty BVPred.bitblast).val, assign.toAIGAssignment⟧ = eval assign expr
Theorem: BVLogicalExpr.bitblast_denote_eq_eval
Proof state before:
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ ⟦(ofBoolExprCached.go expr empty BVPred.bitblast).val, assign.toAIGAssignment⟧ = eval assign expr
Tactic:
rw [bitblast.go_eval_eq_eval]
Proof state after:
no goals
Theorem: BVLogicalExpr.unsat_of_bitblast
Proof state before:
expr : BVLogicalExpr
⊢ expr.bitblast.unsat → expr.unsat
Tactic:
intro h assign
Proof state after:
expr : BVLogicalExpr
h : expr.bitblast.unsat
assign : BVExpr.Assignment
⊢ eval assign expr = false
Theorem: BVLogicalExpr.unsat_of_bitblast
Proof state before:
expr : BVLogicalExpr
h : expr.bitblast.unsat
assign : BVExpr.Assignment
⊢ eval assign expr = false
Tactic:
rw [← bitblast_denote_eq_eval]
Proof state after:
expr : BVLogicalExpr
h : expr.bitblast.unsat
assign : BVExpr.Assignment
⊢ ⟦expr.bitblast, assign.toAIGAssignment⟧ = false
Theorem: BVLogicalExpr.unsat_of_bitblast
Proof state before:
expr : BVLogicalExpr
h : expr.bitblast.unsat
assign : BVExpr.Assignment
⊢ ⟦expr.bitblast, assign.toAIGAssignment⟧ = false
Tactic:
apply h
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2443
Proof state before:
⊢ ∀ (y x : BitVec 64), (x ^^^ -1).sshiftRight y.toNat ^^^ -1 = x.sshiftRight y.toNat
Tactic:
intros
Proof state after:
y✝ x✝ : BitVec 64
⊢ (x✝ ^^^ -1).sshiftRight y✝.toNat ^^^ -1 = x✝.sshiftRight y✝.toNat
Theorem: bitvec_AndOrXor_2443
Proof state before:
y✝ x✝ : BitVec 64
⊢ (x✝ ^^^ -1).sshiftRight y✝.toNat ^^^ -1 = x✝.sshiftRight y✝.toNat
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_716
Proof state before:
⊢ ∀ (a b d : BitVec 64), (a &&& b == a && a &&& d == a) = (a &&& (b &&& d) == a)
Tactic:
intros
Proof state after:
a✝ b✝ d✝ : BitVec 64
⊢ (a✝ &&& b✝ == a✝ && a✝ &&& d✝ == a✝) = (a✝ &&& (b✝ &&& d✝) == a✝)
Theorem: bitvec_AndOrXor_716
Proof state before:
a✝ b✝ d✝ : BitVec 64
⊢ (a✝ &&& b✝ == a✝ && a✝ &&& d✝ == a✝) = (a✝ &&& (b✝ &&& d✝) == a✝)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: BVPred.mkEq_denote_eq_eval_beq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦mkEq aig pair, assign⟧ = (lhs == rhs)
Tactic:
unfold mkEq
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦let res := RefStream.zip aig (RefStream.ZipTarget.mk pair mkBEqCached);
      let aig := res.aig;
      let bits := res.stream;
      RefStream.fold aig (RefStream.FoldTarget.mkAnd bits),
      assign⟧ =
    (lhs == rhs)
Theorem: BVPred.mkEq_denote_eq_eval_beq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦let res := RefStream.zip aig (RefStream.ZipTarget.mk pair mkBEqCached);
      let aig := res.aig;
      let bits := res.stream;
      RefStream.fold aig (RefStream.FoldTarget.mkAnd bits),
      assign⟧ =
    (lhs == rhs)
Tactic:
rw [Bool.eq_iff_iff]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦let res := RefStream.zip aig (RefStream.ZipTarget.mk pair mkBEqCached);
        let aig := res.aig;
        let bits := res.stream;
        RefStream.fold aig (RefStream.FoldTarget.mkAnd bits),
        assign⟧ =
      true ↔
    (lhs == rhs) = true
Theorem: BVPred.mkEq_denote_eq_eval_beq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦let res := RefStream.zip aig (RefStream.ZipTarget.mk pair mkBEqCached);
        let aig := res.aig;
        let bits := res.stream;
        RefStream.fold aig (RefStream.FoldTarget.mkAnd bits),
        assign⟧ =
      true ↔
    (lhs == rhs) = true
Tactic:
simp
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ (∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧) ↔
    lhs = rhs
Theorem: BVPred.mkEq_denote_eq_eval_beq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ (∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧) ↔
    lhs = rhs
Tactic:
constructor
Proof state after:
case mp
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ (∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧) →
    lhs = rhs

case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ lhs = rhs →
    ∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧