Theorem: AIG.toCNF_equisat (LeanSAT/AIG/CNF.lean)

State before:
entry : Entrypoint Nat
⊢ (toCNF entry).unsat ↔ entry.unsat
Tactic:
dsimp [toCNF]
State after:
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

State before:
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]
State after:
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
⊢ ∀ {a b : entry.aig.CNFVar},
    CNF.mem a
        ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
          (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
      CNF.mem b
          ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
            (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
        toCNF.inj a = toCNF.inj b → a = b

State before:
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
⊢ ∀ {a b : entry.aig.CNFVar},
    CNF.mem a
        ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
          (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
      CNF.mem b
          ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
            (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
        toCNF.inj a = toCNF.inj b → a = b
Tactic:
. constructor
  . intro h assign1
    apply toCNF.go_as_denote
    specialize h (toCNF.cnfSatAssignment entry.aig assign1)
    simpa using h
  . intro h assign
    apply toCNF.denote_as_go
    specialize h (toCNF.projectLeftAssign assign)
    assumption
State after:
entry : Entrypoint Nat
⊢ ∀ {a b : entry.aig.CNFVar},
    CNF.mem a
        ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
          (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
      CNF.mem b
          ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
            (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
        toCNF.inj a = toCNF.inj b → a = b

State before:
entry : Entrypoint Nat
⊢ ∀ {a b : entry.aig.CNFVar},
    CNF.mem a
        ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
          (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
      CNF.mem b
          ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
            (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
        toCNF.inj a = toCNF.inj b → a = b
Tactic:
. intro a b _ _ hinj
  apply toCNF.inj_is_injection
  assumption
State after:
no goals

State before:
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
State after:
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)

State before:
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)
Tactic:
. intro h assign1
  apply toCNF.go_as_denote
  specialize h (toCNF.cnfSatAssignment entry.aig assign1)
  simpa using h
State after:
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)

State before:
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
  apply toCNF.denote_as_go
  specialize h (toCNF.projectLeftAssign assign)
  assumption
State after:
no goals

State before:
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
State after:
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
⊢ ⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, assign1⟧ = false

State before:
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
⊢ ⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, assign1⟧ = false
Tactic:
apply toCNF.go_as_denote
State after:
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
⊢ (⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, assign1⟧ &&
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.eval
        (toCNF.cnfSatAssignment entry.aig assign1)) =
    false

State before:
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
⊢ (⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, assign1⟧ &&
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.eval
        (toCNF.cnfSatAssignment entry.aig assign1)) =
    false
Tactic:
specialize h (toCNF.cnfSatAssignment entry.aig assign1)
State after:
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
⊢ (⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, assign1⟧ &&
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.eval
        (toCNF.cnfSatAssignment entry.aig assign1)) =
    false

State before:
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
⊢ (⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, assign1⟧ &&
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.eval
        (toCNF.cnfSatAssignment entry.aig assign1)) =
    false
Tactic:
simpa using h
State after:
no goals

State before:
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
State after:
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

State before:
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
State after:
case mpr.a
entry : Entrypoint Nat
h : entry.unsat
assign : entry.aig.CNFVar → Bool
⊢ ⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, toCNF.projectLeftAssign assign⟧ = false

State before:
case mpr.a
entry : Entrypoint Nat
h : entry.unsat
assign : entry.aig.CNFVar → Bool
⊢ ⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, toCNF.projectLeftAssign assign⟧ = false
Tactic:
specialize h (toCNF.projectLeftAssign assign)
State after:
case mpr.a
entry : Entrypoint Nat
assign : entry.aig.CNFVar → Bool
h : ⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, toCNF.projectLeftAssign assign⟧ = false
⊢ ⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, toCNF.projectLeftAssign assign⟧ = false

State before:
case mpr.a
entry : Entrypoint Nat
assign : entry.aig.CNFVar → Bool
h : ⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, toCNF.projectLeftAssign assign⟧ = false
⊢ ⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, toCNF.projectLeftAssign assign⟧ = false
Tactic:
assumption
State after:
no goals

State before:
entry : Entrypoint Nat
⊢ ∀ {a b : entry.aig.CNFVar},
    CNF.mem a
        ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
          (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
      CNF.mem b
          ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
            (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
        toCNF.inj a = toCNF.inj b → a = b
Tactic:
intro a b _ _ hinj
State after:
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

State before:
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
State after:
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

State before:
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
Tactic:
assumption
State after:
no goals