-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem toCNF_equisat (entry : Entrypoint Nat) : (toCNF entry).Unsat ↔ entry.Unsat

Proof state:
entry : Entrypoint Nat
⊢ CNF.Unsat
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) ↔
    entry.Unsat

Tactic:
constructor

Result:
case mp
entry : Entrypoint Nat
⊢ CNF.Unsat
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
    entry.Unsat

case mpr
entry : Entrypoint Nat
⊢ entry.Unsat →
    CNF.Unsat
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)

Proof state:
case mp.a
entry : Entrypoint Nat
h :
  CNF.Unsat
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
assign1 : Nat → Bool
⊢ (⟦assign1, { aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }⟧ &&
      toCNF.State.eval (toCNF.cnfSatAssignment entry.aig assign1)
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val) =
    false

Tactic:
specialize h (toCNF.cnfSatAssignment entry.aig assign1)

Result:
case mp.a
entry : Entrypoint Nat
assign1 : Nat → Bool
h :
  CNF.eval (toCNF.cnfSatAssignment entry.aig assign1)
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) =
    false
⊢ (⟦assign1, { aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }⟧ &&
      toCNF.State.eval (toCNF.cnfSatAssignment entry.aig assign1)
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val) =
    false

Proof state:
entry : Entrypoint Nat
a b : entry.aig.CNFVar
a✝¹ :
  CNF.Mem a
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
a✝ :
  CNF.Mem b
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
hinj : toCNF.inj a = toCNF.inj b
⊢ a = b

Tactic:
apply toCNF.inj_is_injection

Result:
case a
entry : Entrypoint Nat
a b : entry.aig.CNFVar
a✝¹ :
  CNF.Mem a
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
a✝ :
  CNF.Mem b
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
hinj : toCNF.inj a = toCNF.inj b
⊢ toCNF.inj a = toCNF.inj b

Proof state:
case mpr.a
entry : Entrypoint Nat
assign : entry.aig.CNFVar → Bool
h : ⟦toCNF.projectLeftAssign assign, { aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }⟧ = false
⊢ ⟦toCNF.projectLeftAssign assign, { aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }⟧ = false

Tactic:
assumption

Result:
no goals

Proof state:
case mpr
entry : Entrypoint Nat
⊢ entry.Unsat →
    CNF.Unsat
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)

Tactic:
intro h assign

Result:
case mpr
entry : Entrypoint Nat
h : entry.Unsat
assign : entry.aig.CNFVar → Bool
⊢ CNF.eval assign
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) =
    false

Proof state:
case mpr.a
entry : Entrypoint Nat
h : entry.Unsat
assign : entry.aig.CNFVar → Bool
⊢ ⟦toCNF.projectLeftAssign assign, { aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }⟧ = false

Tactic:
specialize h (toCNF.projectLeftAssign assign)

Result:
case mpr.a
entry : Entrypoint Nat
assign : entry.aig.CNFVar → Bool
h : ⟦toCNF.projectLeftAssign assign, { aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }⟧ = false
⊢ ⟦toCNF.projectLeftAssign assign, { aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }⟧ = false

Proof state:
case mp
entry : Entrypoint Nat
⊢ CNF.Unsat
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
    entry.Unsat

Tactic:
intro h assign1

Result:
case mp
entry : Entrypoint Nat
h :
  CNF.Unsat
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
assign1 : Nat → Bool
⊢ ⟦assign1, { aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }⟧ = false

Proof state:
case mpr
entry : Entrypoint Nat
h : entry.Unsat
assign : entry.aig.CNFVar → Bool
⊢ CNF.eval assign
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) =
    false

Tactic:
apply toCNF.denote_as_go

Result:
case mpr.a
entry : Entrypoint Nat
h : entry.Unsat
assign : entry.aig.CNFVar → Bool
⊢ ⟦toCNF.projectLeftAssign assign, { aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }⟧ = false

Proof state:
case mp.a
entry : Entrypoint Nat
assign1 : Nat → Bool
h :
  CNF.eval (toCNF.cnfSatAssignment entry.aig assign1)
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) =
    false
⊢ (⟦assign1, { aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }⟧ &&
      toCNF.State.eval (toCNF.cnfSatAssignment entry.aig assign1)
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val) =
    false

Tactic:
simpa using h

Result:
no goals

Proof state:
entry : Entrypoint Nat
⊢ (CNF.relabel toCNF.inj
        ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
          (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)).Unsat ↔
    entry.Unsat

Tactic:
rw [CNF.unsat_relabel_iff]

Result:
entry : Entrypoint Nat
⊢ CNF.Unsat
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) ↔
    entry.Unsat

entry : Entrypoint Nat
⊢ ∀ {v1 v2 : entry.aig.CNFVar},
    CNF.Mem v1
        ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
          (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
      CNF.Mem v2
          ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
            (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
        toCNF.inj v1 = toCNF.inj v2 → v1 = v2

Proof state:
entry : Entrypoint Nat
⊢ ∀ {v1 v2 : entry.aig.CNFVar},
    CNF.Mem v1
        ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
          (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
      CNF.Mem v2
          ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
            (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
        toCNF.inj v1 = toCNF.inj v2 → v1 = v2

Tactic:
intro a b _ _ hinj

Result:
entry : Entrypoint Nat
a b : entry.aig.CNFVar
a✝¹ :
  CNF.Mem a
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
a✝ :
  CNF.Mem b
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
hinj : toCNF.inj a = toCNF.inj b
⊢ a = b

Proof state:
entry : Entrypoint Nat
⊢ (toCNF entry).Unsat ↔ entry.Unsat

Tactic:
dsimp only [toCNF]

Result:
entry : Entrypoint Nat
⊢ (CNF.relabel toCNF.inj
        ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
          (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)).Unsat ↔
    entry.Unsat