internlm/Lean-Github huggingface dataset:
Theorem: LRAT.Clause.entails_of_entails_delete
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
h : ∃ a, (a, false) ∈ toList (delete c l) ∧ p a = false ∨ (a, true) ∈ toList (delete c l) ∧ p a = true
⊢ ∃ a, (a, false) ∈ toList c ∧ p a = false ∨ (a, true) ∈ toList c ∧ p a = true
Tactic:
rcases h with ⟨v, ⟨h1, h2⟩ | ⟨h1, h2⟩⟩
Proof state after:
case intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
v : α
h1 : (v, false) ∈ toList (delete c l)
h2 : p v = false
⊢ ∃ a, (a, false) ∈ toList c ∧ p a = false ∨ (a, true) ∈ toList c ∧ p a = true

case intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
v : α
h1 : (v, true) ∈ toList (delete c l)
h2 : p v = true
⊢ ∃ a, (a, false) ∈ toList c ∧ p a = false ∨ (a, true) ∈ toList c ∧ p a = true
Theorem: LRAT.Clause.entails_of_entails_delete
Proof state before:
case intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
v : α
h1 : (v, false) ∈ toList (delete c l)
h2 : p v = false
⊢ ∃ a, (a, false) ∈ toList c ∧ p a = false ∨ (a, true) ∈ toList c ∧ p a = true

case intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
v : α
h1 : (v, true) ∈ toList (delete c l)
h2 : p v = true
⊢ ∃ a, (a, false) ∈ toList c ∧ p a = false ∨ (a, true) ∈ toList c ∧ p a = true
Tactic:
. simp only [delete_iff, ne_eq] at h1
  exact Exists.intro v $ Or.inl ⟨h1.2, h2⟩
Proof state after:
case intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
v : α
h1 : (v, true) ∈ toList (delete c l)
h2 : p v = true
⊢ ∃ a, (a, false) ∈ toList c ∧ p a = false ∨ (a, true) ∈ toList c ∧ p a = true
Theorem: LRAT.Clause.entails_of_entails_delete
Proof state before:
case intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
v : α
h1 : (v, true) ∈ toList (delete c l)
h2 : p v = true
⊢ ∃ a, (a, false) ∈ toList c ∧ p a = false ∨ (a, true) ∈ toList c ∧ p a = true
Tactic:
. simp only [delete_iff, ne_eq] at h1
  exact Exists.intro v $ Or.inr ⟨h1.2, h2⟩
Proof state after:
no goals
Theorem: LRAT.Clause.entails_of_entails_delete
Proof state before:
case intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
v : α
h1 : (v, false) ∈ toList (delete c l)
h2 : p v = false
⊢ ∃ a, (a, false) ∈ toList c ∧ p a = false ∨ (a, true) ∈ toList c ∧ p a = true
Tactic:
simp only [delete_iff, ne_eq] at h1
Proof state after:
case intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
v : α
h2 : p v = false
h1 : ¬(v, false) = l ∧ (v, false) ∈ toList c
⊢ ∃ a, (a, false) ∈ toList c ∧ p a = false ∨ (a, true) ∈ toList c ∧ p a = true
Theorem: LRAT.Clause.entails_of_entails_delete
Proof state before:
case intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
v : α
h2 : p v = false
h1 : ¬(v, false) = l ∧ (v, false) ∈ toList c
⊢ ∃ a, (a, false) ∈ toList c ∧ p a = false ∨ (a, true) ∈ toList c ∧ p a = true
Tactic:
exact Exists.intro v $ Or.inl ⟨h1.2, h2⟩
Proof state after:
no goals
Theorem: LRAT.Clause.entails_of_entails_delete
Proof state before:
case intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
v : α
h1 : (v, true) ∈ toList (delete c l)
h2 : p v = true
⊢ ∃ a, (a, false) ∈ toList c ∧ p a = false ∨ (a, true) ∈ toList c ∧ p a = true
Tactic:
simp only [delete_iff, ne_eq] at h1
Proof state after:
case intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
v : α
h2 : p v = true
h1 : ¬(v, true) = l ∧ (v, true) ∈ toList c
⊢ ∃ a, (a, false) ∈ toList c ∧ p a = false ∨ (a, true) ∈ toList c ∧ p a = true
Theorem: LRAT.Clause.entails_of_entails_delete
Proof state before:
case intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
v : α
h2 : p v = true
h1 : ¬(v, true) = l ∧ (v, true) ∈ toList c
⊢ ∃ a, (a, false) ∈ toList c ∧ p a = false ∨ (a, true) ∈ toList c ∧ p a = true
Tactic:
exact Exists.intro v $ Or.inr ⟨h1.2, h2⟩
Proof state after:
no goals
Theorem: LRAT.Formula.sat_iff_forall
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
p : α → Bool
f : σ
⊢ ((toList f).all fun c => decide (((Clause.toList c).any fun l => decide (p l.fst = l.snd)) = true)) = true ↔
    ∀ (c : β), c ∈ toList f → ((Clause.toList c).any fun l => decide (p l.fst = l.snd)) = true
Tactic:
simp only [List.all_eq_true, decide_eq_true_eq]
Proof state after:
no goals
Theorem: LRAT.Formula.limplies_of_insert
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
c : β
f : σ
⊢ limplies α (insert f c) f
Tactic:
intro p
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
⊢ p ⊨ insert f c → p ⊨ f
Theorem: LRAT.Formula.limplies_of_insert
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
⊢ p ⊨ insert f c → p ⊨ f
Tactic:
simp only [formulaHSat_def, List.all_eq_true, decide_eq_true_eq]
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
⊢ (∀ (x : β), x ∈ toList (insert f c) → p ⊨ x) → ∀ (x : β), x ∈ toList f → p ⊨ x
Theorem: LRAT.Formula.limplies_of_insert
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
⊢ (∀ (x : β), x ∈ toList (insert f c) → p ⊨ x) → ∀ (x : β), x ∈ toList f → p ⊨ x
Tactic:
intro h c' c'_in_f
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
h : ∀ (x : β), x ∈ toList (insert f c) → p ⊨ x
c' : β
c'_in_f : c' ∈ toList f
⊢ p ⊨ c'
Theorem: LRAT.Formula.limplies_of_insert
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
h : ∀ (x : β), x ∈ toList (insert f c) → p ⊨ x
c' : β
c'_in_f : c' ∈ toList f
⊢ p ⊨ c'
Tactic:
have c'_in_fc : c' ∈ toList (insert f c) := by
  simp only [insert_iff, Array.toList_eq, Array.data_toArray, List.mem_singleton]
  exact Or.inr c'_in_f
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
h : ∀ (x : β), x ∈ toList (insert f c) → p ⊨ x
c' : β
c'_in_f : c' ∈ toList f
c'_in_fc : c' ∈ toList (insert f c)
⊢ p ⊨ c'
Theorem: LRAT.Formula.limplies_of_insert
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
h : ∀ (x : β), x ∈ toList (insert f c) → p ⊨ x
c' : β
c'_in_f : c' ∈ toList f
c'_in_fc : c' ∈ toList (insert f c)
⊢ p ⊨ c'
Tactic:
exact h c' c'_in_fc
Proof state after:
no goals
Theorem: LRAT.Formula.limplies_of_insert
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
h : ∀ (x : β), x ∈ toList (insert f c) → p ⊨ x
c' : β
c'_in_f : c' ∈ toList f
⊢ c' ∈ toList (insert f c)
Tactic:
simp only [insert_iff, Array.toList_eq, Array.data_toArray, List.mem_singleton]
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
h : ∀ (x : β), x ∈ toList (insert f c) → p ⊨ x
c' : β
c'_in_f : c' ∈ toList f
⊢ c' = c ∨ c' ∈ toList f
Theorem: LRAT.Formula.limplies_of_insert
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
h : ∀ (x : β), x ∈ toList (insert f c) → p ⊨ x
c' : β
c'_in_f : c' ∈ toList f
⊢ c' = c ∨ c' ∈ toList f
Tactic:
exact Or.inr c'_in_f
Proof state after:
no goals
Theorem: LRAT.Formula.limplies_delete
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
⊢ limplies α f (delete f arr)
Tactic:
intro p
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
⊢ p ⊨ f → p ⊨ delete f arr
Theorem: LRAT.Formula.limplies_delete
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
⊢ p ⊨ f → p ⊨ delete f arr
Tactic:
simp only [formulaHSat_def, List.all_eq_true, decide_eq_true_eq]
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
⊢ (∀ (x : β), x ∈ toList f → p ⊨ x) → ∀ (x : β), x ∈ toList (delete f arr) → p ⊨ x
Theorem: LRAT.Formula.limplies_delete
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
⊢ (∀ (x : β), x ∈ toList f → p ⊨ x) → ∀ (x : β), x ∈ toList (delete f arr) → p ⊨ x
Tactic:
intro h c c_in_f_del
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
h : ∀ (x : β), x ∈ toList f → p ⊨ x
c : β
c_in_f_del : c ∈ toList (delete f arr)
⊢ p ⊨ c
Theorem: LRAT.Formula.limplies_delete
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
h : ∀ (x : β), x ∈ toList f → p ⊨ x
c : β
c_in_f_del : c ∈ toList (delete f arr)
⊢ p ⊨ c
Tactic:
have del_f_subset := delete_subset f arr
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
h : ∀ (x : β), x ∈ toList f → p ⊨ x
c : β
c_in_f_del : c ∈ toList (delete f arr)
del_f_subset : ∀ (c : β), c ∈ toList (delete f arr) → c ∈ toList f
⊢ p ⊨ c
Theorem: LRAT.Formula.limplies_delete
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
h : ∀ (x : β), x ∈ toList f → p ⊨ x
c : β
c_in_f_del : c ∈ toList (delete f arr)
del_f_subset : ∀ (c : β), c ∈ toList (delete f arr) → c ∈ toList f
⊢ p ⊨ c
Tactic:
specialize del_f_subset c c_in_f_del
Proof state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
h : ∀ (x : β), x ∈ toList f → p ⊨ x
c : β
c_in_f_del : c ∈ toList (delete f arr)
del_f_subset : c ∈ toList f
⊢ p ⊨ c
Theorem: LRAT.Formula.limplies_delete
Proof state before:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
h : ∀ (x : β), x ∈ toList f → p ⊨ x
c : β
c_in_f_del : c ∈ toList (delete f arr)
del_f_subset : c ∈ toList f
⊢ p ⊨ c
Tactic:
exact h c del_f_subset
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2297
Proof state before:
⊢ ∀ (A B : BitVec 64), A &&& B ||| A ^^^ -1 ^^^ B = A ^^^ -1 ^^^ B
Tactic:
intros
Proof state after:
A✝ B✝ : BitVec 64
⊢ A✝ &&& B✝ ||| A✝ ^^^ -1 ^^^ B✝ = A✝ ^^^ -1 ^^^ B✝
Theorem: bitvec_AndOrXor_2297
Proof state before:
A✝ B✝ : BitVec 64
⊢ A✝ &&& B✝ ||| A✝ ^^^ -1 ^^^ B✝ = A✝ ^^^ -1 ^^^ B✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: timeout
Proof state before:
x y : BitVec 2048
⊢ x + y = y + x
Tactic:
bv_decide
Proof state after:
no goals
Theorem: no_hyps
Proof state before:
x y : Nat
⊢ x * y = y * x
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AddSub_1556
Proof state before:
⊢ ∀ (y x : BitVec 1), x - y = x ^^^ y
Tactic:
intros
Proof state after:
y✝ x✝ : BitVec 1
⊢ x✝ - y✝ = x✝ ^^^ y✝
Theorem: bitvec_AddSub_1556
Proof state before:
y✝ x✝ : BitVec 1
⊢ x✝ - y✝ = x✝ ^^^ y✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2416
Proof state before:
⊢ ∀ (nx y : BitVec 64), (nx ^^^ -1) &&& y ^^^ -1 = nx ||| y ^^^ -1
Tactic:
intros
Proof state after:
nx✝ y✝ : BitVec 64
⊢ (nx✝ ^^^ -1) &&& y✝ ^^^ -1 = nx✝ ||| y✝ ^^^ -1
Theorem: bitvec_AndOrXor_2416
Proof state before:
nx✝ y✝ : BitVec 64
⊢ (nx✝ ^^^ -1) &&& y✝ ^^^ -1 = nx✝ ||| y✝ ^^^ -1
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2663
Proof state before:
⊢ ∀ (a b : BitVec 64), (xor (decide (a ≤ b)) (a != b) = true) = (b ≤ a)
Tactic:
intros
Proof state after:
a✝ b✝ : BitVec 64
⊢ (xor (decide (a✝ ≤ b✝)) (a✝ != b✝) = true) = (b✝ ≤ a✝)
Theorem: bitvec_AndOrXor_2663
Proof state before:
a✝ b✝ : BitVec 64
⊢ (xor (decide (a✝ ≤ b✝)) (a✝ != b✝) = true) = (b✝ ≤ a✝)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_InstCombineShift__724
Proof state before:
⊢ ∀ (A C2 C1 : BitVec 31), C1 <<< A <<< C2 = C1 <<< C2 <<< A
Tactic:
intros
Proof state after:
A✝ C2✝ C1✝ : BitVec 31
⊢ C1✝ <<< A✝ <<< C2✝ = C1✝ <<< C2✝ <<< A✝
Theorem: bitvec_InstCombineShift__724
Proof state before:
A✝ C2✝ C1✝ : BitVec 31
⊢ C1✝ <<< A✝ <<< C2✝ = C1✝ <<< C2✝ <<< A✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_decls_size_le
Proof state before:
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
Tactic:
exact (ofBoolExprCached.go expr aig atomHandler).property
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
idx : Nat
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr aig atomHandler).val.aig.decls.size
⊢ (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
induction expr generalizing aig with
| const =>
  simp only [go]
  rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]
| literal =>
  simp only [go]
  rw [AIG.LawfulOperator.decl_eq (f := atomHandler)]
| not expr ih =>
  simp only [go]
  have := go_decls_size_le atomHandler expr aig
  specialize ih aig (by omega) (by omega)
  rw [AIG.LawfulOperator.decl_eq (f := mkNotCached)]
  assumption
| gate g lhs rhs lih rih =>
  have := go_decls_size_le atomHandler lhs aig
  have := go_decls_size_le atomHandler rhs (go lhs aig atomHandler).val.aig
  specialize lih aig (by omega) (by omega)
  specialize rih (go lhs aig atomHandler).val.aig (by omega) (by omega)
  cases g with
  | and =>
    simp only [go]
    rw [AIG.LawfulOperator.decl_eq (f := mkAndCached)]
    rw [rih, lih]
  | or =>
    simp only [go]
    rw [AIG.LawfulOperator.decl_eq (f := mkOrCached)]
    rw [rih, lih]
  | xor =>
    simp only [go]
    rw [AIG.LawfulOperator.decl_eq (f := mkXorCached)]
    rw [rih, lih]
  | beq =>
    simp only [go]
    rw [AIG.LawfulOperator.decl_eq (f := mkBEqCached)]
    rw [rih, lih]
  | imp =>
    simp only [go]
    rw [AIG.LawfulOperator.decl_eq (f := mkImpCached)]
    rw [rih, lih]
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
case const
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
a✝ : Bool
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.const a✝) aig atomHandler).val.aig.decls.size
⊢ (go (BoolExpr.const a✝) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [go]
Proof state after:
case const
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
a✝ : Bool
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.const a✝) aig atomHandler).val.aig.decls.size
⊢ (aig.mkConstCached a✝).aig.decls[idx] = aig.decls[idx]
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
case const
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
a✝ : Bool
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.const a✝) aig atomHandler).val.aig.decls.size
⊢ (aig.mkConstCached a✝).aig.decls[idx] = aig.decls[idx]
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
case literal
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
a✝ : α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.literal a✝) aig atomHandler).val.aig.decls.size
⊢ (go (BoolExpr.literal a✝) aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [go]
Proof state after:
case literal
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
a✝ : α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.literal a✝) aig atomHandler).val.aig.decls.size
⊢ (atomHandler aig a✝).aig.decls[idx] = aig.decls[idx]
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
case literal
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
a✝ : α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go (BoolExpr.literal a✝) aig atomHandler).val.aig.decls.size
⊢ (atomHandler aig a✝).aig.decls[idx] = aig.decls[idx]
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := atomHandler)]
Proof state after:
no goals
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
case not
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
ih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go expr aig atomHandler).val.aig.decls.size),
    (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
⊢ (go expr.not aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [go]
Proof state after:
case not
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
ih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go expr aig atomHandler).val.aig.decls.size),
    (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
⊢ ((go expr aig atomHandler).1.aig.mkNotCached (go expr aig atomHandler).1.ref).aig.decls[idx] = aig.decls[idx]
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
case not
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
ih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go expr aig atomHandler).val.aig.decls.size),
    (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
⊢ ((go expr aig atomHandler).1.aig.mkNotCached (go expr aig atomHandler).1.ref).aig.decls[idx] = aig.decls[idx]
Tactic:
have := go_decls_size_le atomHandler expr aig
Proof state after:
case not
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
ih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go expr aig atomHandler).val.aig.decls.size),
    (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
⊢ ((go expr aig atomHandler).1.aig.mkNotCached (go expr aig atomHandler).1.ref).aig.decls[idx] = aig.decls[idx]
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
case not
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
ih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go expr aig atomHandler).val.aig.decls.size),
    (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
⊢ ((go expr aig atomHandler).1.aig.mkNotCached (go expr aig atomHandler).1.ref).aig.decls[idx] = aig.decls[idx]
Tactic:
specialize ih aig (by omega) (by omega)
Proof state after:
case not
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
ih : (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ ((go expr aig atomHandler).1.aig.mkNotCached (go expr aig atomHandler).1.ref).aig.decls[idx] = aig.decls[idx]
Theorem: AIG.ofBoolExprCached.go_decl_eq
Proof state before:
case not
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
ih : (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ ((go expr aig atomHandler).1.aig.mkNotCached (go expr aig atomHandler).1.ref).aig.decls[idx] = aig.decls[idx]
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkNotCached)]
Proof state after:
case not
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
ih : (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ (go expr aig atomHandler).1.aig.decls[idx] = aig.decls[idx]

case not.h1
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
expr : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go expr.not aig atomHandler).val.aig.decls.size
this : aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
ih : (go expr aig atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ idx < (go expr aig atomHandler).1.aig.decls.size