internlm/Lean-Github huggingface dataset:
Theorem: AIG.denote_relabel
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
lhs rhs : Nat
linv rinv : Bool
heq1 : (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ start < (relabel f aig).decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.unsat_relabel
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
aig : AIG α
f : α → β
hidx : idx < aig.decls.size
⊢ idx < (relabel f aig).decls.size
Tactic:
simp[hidx]
Proof state after:
no goals
Theorem: AIG.unsat_relabel
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
aig : AIG α
f : α → β
hidx : idx < aig.decls.size
⊢ aig.unsatAt idx hidx → (relabel f aig).unsatAt idx ⋯
Tactic:
intro h assign
Proof state after:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
aig : AIG α
f : α → β
hidx : idx < aig.decls.size
h : aig.unsatAt idx hidx
assign : β → Bool
⊢ ⟦{ aig := relabel f aig, ref := { gate := idx, hgate := ⋯ } }, assign⟧ = false
Theorem: AIG.unsat_relabel
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
aig : AIG α
f : α → β
hidx : idx < aig.decls.size
h : aig.unsatAt idx hidx
assign : β → Bool
⊢ ⟦{ aig := relabel f aig, ref := { gate := idx, hgate := ⋯ } }, assign⟧ = false
Tactic:
specialize h (assign ∘ f)
Proof state after:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
aig : AIG α
f : α → β
hidx : idx < aig.decls.size
assign : β → Bool
h : ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign ∘ f⟧ = false
⊢ ⟦{ aig := relabel f aig, ref := { gate := idx, hgate := ⋯ } }, assign⟧ = false
Theorem: AIG.unsat_relabel
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
aig : AIG α
f : α → β
hidx : idx < aig.decls.size
assign : β → Bool
h : ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign ∘ f⟧ = false
⊢ ⟦{ aig := relabel f aig, ref := { gate := idx, hgate := ⋯ } }, assign⟧ = false
Tactic:
simp [h]
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
⊢ (relabel f aig).unsatAt idx hidx1 ↔ aig.unsatAt idx hidx2
Tactic:
constructor
Proof state after:
case mp
α : 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
⊢ (relabel f aig).unsatAt idx hidx1 → aig.unsatAt idx hidx2

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
Theorem: AIG.relabel_unsat_iff
Proof state before:
case mp
α : 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
⊢ (relabel f aig).unsatAt idx hidx1 → aig.unsatAt idx hidx2

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:
. intro h assign
  have em := Classical.propDecidable
  let g : β → α := fun b =>
    if h:∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice inferInstance
  have h' := unsat_relabel g h
  specialize h' assign
  simp only [denote_relabel] at h'
  rw [← h']
  apply denote_congr
  . intro a hmem
    simp [g]
    split
    . next h =>
      rcases Exists.choose_spec h with ⟨_, heq⟩
      specialize hinj _ _ (by assumption) (by assumption) heq
      simp [hinj]
    . next h =>
      simp only [not_exists, not_and] at h
      specialize h a hmem
      contradiction
Proof state after:
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
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.relabel_unsat_iff
Proof state before:
case mp
α : 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
⊢ (relabel f aig).unsatAt idx hidx1 → aig.unsatAt idx hidx2
Tactic:
intro h assign
Proof state after:
case mp
α : 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
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false
Theorem: AIG.relabel_unsat_iff
Proof state before:
case mp
α : 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
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false
Tactic:
have em := Classical.propDecidable
Proof state after:
case mp
α : 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
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false
Theorem: AIG.relabel_unsat_iff
Proof state before:
case mp
α : 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
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false
Tactic:
let g : β → α := fun b =>
  if h:∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice inferInstance
Proof state after:
case mp
α : 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 ⋯
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false
Theorem: AIG.relabel_unsat_iff
Proof state before:
case mp
α : 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 ⋯
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false
Tactic:
have h' := unsat_relabel g h
Proof state after:
case mp
α : 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' : (relabel g (relabel f aig)).unsatAt idx ⋯
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false
Theorem: AIG.relabel_unsat_iff
Proof state before:
case mp
α : 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' : (relabel g (relabel f aig)).unsatAt idx ⋯
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false
Tactic:
specialize h' assign
Proof state after:
case mp
α : 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 := relabel g (relabel f aig), ref := { gate := idx, hgate := ⋯ } }, assign⟧ = false
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false
Theorem: AIG.relabel_unsat_iff
Proof state before:
case mp
α : 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 := relabel g (relabel f aig), ref := { gate := idx, hgate := ⋯ } }, assign⟧ = false
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false
Tactic:
simp only [denote_relabel] at h'
Proof state after:
case mp
α : 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
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false
Theorem: AIG.relabel_unsat_iff
Proof state before:
case mp
α : 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
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false
Tactic:
rw [← h']
Proof state after:
case mp
α : 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
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧
Theorem: AIG.relabel_unsat_iff
Proof state before:
case mp
α : 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
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧
Tactic:
apply denote_congr
Proof state after:
case mp.h
α : 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 : α), a ∈ aig → assign a = ((assign ∘ g) ∘ f) a
Theorem: AIG.relabel_unsat_iff
Proof state before:
case mp.h
α : 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 : α), a ∈ aig → assign a = ((assign ∘ g) ∘ f) a
Tactic:
. intro a hmem
  simp [g]
  split
  . next h =>
    rcases Exists.choose_spec h with ⟨_, heq⟩
    specialize hinj _ _ (by assumption) (by assumption) heq
    simp [hinj]
  . 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
α : 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 : α), a ∈ aig → assign a = ((assign ∘ g) ∘ f) a
Tactic:
intro a hmem
Proof state after:
case mp.h
α : 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
⊢ assign a = ((assign ∘ g) ∘ f) a
Theorem: AIG.relabel_unsat_iff
Proof state before:
case mp.h
α : 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
⊢ assign a = ((assign ∘ g) ∘ f) a
Tactic:
simp [g]
Proof state after:
case mp.h
α : 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
⊢ assign a = assign (if h : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a then h.choose else Classical.choice ⋯)
Theorem: AIG.relabel_unsat_iff
Proof state before:
case mp.h
α : 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
⊢ assign a = assign (if h : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a then h.choose else Classical.choice ⋯)
Tactic:
split
Proof state after:
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 ⋯)