internlm/Lean-Github huggingface dataset:
Theorem: AIG.relabel_unsat_iff
Proof state before:
case mp.h.isTrue
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h✝ : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
⊢ assign a = assign h✝.choose

case mp.h.isFalse
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h✝ : ¬∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
⊢ assign a = assign (Classical.choice ⋯)
Tactic:
. next h =>
  rcases Exists.choose_spec h with ⟨_, heq⟩
  specialize hinj _ _ (by assumption) (by assumption) heq
  simp [hinj]
Proof state after:
case mp.h.isFalse
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h✝ : ¬∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
⊢ assign a = assign (Classical.choice ⋯)
Theorem: AIG.relabel_unsat_iff
Proof state before:
case mp.h.isFalse
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h✝ : ¬∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
⊢ assign a = assign (Classical.choice ⋯)
Tactic:
. next h =>
  simp only [not_exists, not_and] at h
  specialize h a hmem
  contradiction
Proof state after:
no goals
Theorem: AIG.relabel_unsat_iff
Proof state before:
case mp.h.isTrue
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h✝ : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
⊢ assign a = assign h✝.choose
Tactic:
next h =>
rcases Exists.choose_spec h with ⟨_, heq⟩
specialize hinj _ _ (by assumption) (by assumption) heq
simp [hinj]
Proof state after:
no goals
Theorem: AIG.relabel_unsat_iff
Proof state before:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
⊢ assign a = assign h.choose
Tactic:
rcases Exists.choose_spec h with ⟨_, heq⟩
Proof state after:
case intro
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
left✝ : h.choose ∈ aig
heq : f h.choose = f a
⊢ assign a = assign h.choose
Theorem: AIG.relabel_unsat_iff
Proof state before:
case intro
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
left✝ : h.choose ∈ aig
heq : f h.choose = f a
⊢ assign a = assign h.choose
Tactic:
specialize hinj _ _ (by assumption) (by assumption) heq
Proof state after:
case intro
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
left✝ : h.choose ∈ aig
heq : f h.choose = f a
hinj : h.choose = a
⊢ assign a = assign h.choose
Theorem: AIG.relabel_unsat_iff
Proof state before:
case intro
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
left✝ : h.choose ∈ aig
heq : f h.choose = f a
hinj : h.choose = a
⊢ assign a = assign h.choose
Tactic:
simp [hinj]
Proof state after:
no goals
Theorem: AIG.relabel_unsat_iff
Proof state before:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
left✝ : h.choose ∈ aig
heq : f h.choose = f a
⊢ h.choose ∈ aig
Tactic:
assumption
Proof state after:
no goals
Theorem: AIG.relabel_unsat_iff
Proof state before:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
left✝ : h.choose ∈ aig
heq : f h.choose = f a
⊢ a ∈ aig
Tactic:
assumption
Proof state after:
no goals
Theorem: AIG.relabel_unsat_iff
Proof state before:
case mp.h.isFalse
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h✝ : ¬∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
⊢ assign a = assign (Classical.choice ⋯)
Tactic:
next h =>
simp only [not_exists, not_and] at h
specialize h a hmem
contradiction
Proof state after:
no goals
Theorem: AIG.relabel_unsat_iff
Proof state before:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ¬∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
⊢ assign a = assign (Classical.choice ⋯)
Tactic:
simp only [not_exists, not_and] at h
Proof state after:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ∀ (x : α), x ∈ aig → ¬f x = f a
⊢ assign a = assign (Classical.choice ⋯)
Theorem: AIG.relabel_unsat_iff
Proof state before:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ∀ (x : α), x ∈ aig → ¬f x = f a
⊢ assign a = assign (Classical.choice ⋯)
Tactic:
specialize h a hmem
Proof state after:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ¬f a = f a
⊢ assign a = assign (Classical.choice ⋯)
Theorem: AIG.relabel_unsat_iff
Proof state before:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ¬f a = f a
⊢ assign a = assign (Classical.choice ⋯)
Tactic:
contradiction
Proof state after:
no goals
Theorem: AIG.relabel_unsat_iff
Proof state before:
case mpr
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
⊢ aig.unsatAt idx hidx2 → (relabel f aig).unsatAt idx hidx1
Tactic:
apply unsat_relabel
Proof state after:
no goals
Theorem: AIG.Entrypoint.relabel_size_eq
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
entry : Entrypoint α
f : α → β
⊢ (relabel f entry).aig.decls.size = entry.aig.decls.size
Tactic:
simp [relabel]
Proof state after:
no goals
Theorem: AIG.Entrypoint.relabel_unsat_iff
Proof state before:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
inst✝ : Nonempty α
entry : Entrypoint α
f : α → β
hinj : ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → f x = f y → x = y
⊢ (relabel f entry).unsat ↔ entry.unsat
Tactic:
simp [relabel, unsat]
Proof state after:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
inst✝ : Nonempty α
entry : Entrypoint α
f : α → β
hinj : ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → f x = f y → x = y
⊢ (AIG.relabel f entry.aig).unsatAt entry.ref.gate ⋯ ↔ entry.aig.unsatAt entry.ref.gate ⋯
Theorem: AIG.Entrypoint.relabel_unsat_iff
Proof state before:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
inst✝ : Nonempty α
entry : Entrypoint α
f : α → β
hinj : ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → f x = f y → x = y
⊢ (AIG.relabel f entry.aig).unsatAt entry.ref.gate ⋯ ↔ entry.aig.unsatAt entry.ref.gate ⋯
Tactic:
rw [AIG.relabel_unsat_iff]
Proof state after:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
inst✝ : Nonempty α
entry : Entrypoint α
f : α → β
hinj : ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → f x = f y → x = y
⊢ ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → f x = f y → x = y
Theorem: AIG.Entrypoint.relabel_unsat_iff
Proof state before:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
inst✝ : Nonempty α
entry : Entrypoint α
f : α → β
hinj : ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → f x = f y → x = y
⊢ ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → f x = f y → x = y
Tactic:
assumption
Proof state after:
no goals
Theorem: bitvec_AddSub_1624
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_AddSub_1624
Proof state before:
A✝ B✝ : BitVec 64
⊢ (A✝ ||| B✝) - (A✝ ^^^ B✝) = A✝ &&& B✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
i : PosFin n
⊢ i.val < assignments.size
Tactic:
rw [assignments_size]
Proof state after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
i : PosFin n
⊢ i.val < n
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
i : PosFin n
⊢ i.val < n
Tactic:
exact i.2.2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
j : PosFin n
⊢ j.val < insertUnit_res.snd.fst.size
Tactic:
rw [insertUnit_preserves_size, assignments_size]
Proof state after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
j : PosFin n
⊢ j.val < n
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
j : PosFin n
⊢ j.val < n
Tactic:
exact j.2.2
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
⊢ let insertUnit_res := insertUnit (units, assignments, foundContradiction) l;
  (foundContradiction = true → ∃ i, assignments[i.val] = both) →
    insertUnit_res.snd.snd = true → ∃ j, insertUnit_res.snd.fst[j.val] = both
Tactic:
intro insertUnit_res h insertUnit_success
Proof state after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_success : insertUnit_res.snd.snd = true
⊢ ∃ j, insertUnit_res.snd.fst[j.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_success : insertUnit_res.snd.snd = true
⊢ ∃ j, insertUnit_res.snd.fst[j.val] = both
Tactic:
simp only [insertUnit_res] at *
Proof state after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_success : (insertUnit (units, assignments, foundContradiction) l).snd.snd = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Theorem: LRAT.DefaultFormula.contradiction_of_insertUnit_success
Proof state before:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_success : (insertUnit (units, assignments, foundContradiction) l).snd.snd = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
Tactic:
simp only [insertUnit, Prod.mk.eta] at insertUnit_success
Proof state after:
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_success :
  (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
        else
          (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
            foundContradiction || assignments[l.fst.val]! != unassigned)).snd.snd =
    true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both