Theorem: AIG.toCNF.go_as_denote (LeanSAT/AIG/CNF.lean)

State before:
sat? : Bool
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
⊢ (⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ &&
        (go aig start h1 (State.empty aig)).val.eval (cnfSatAssignment aig assign1)) =
      sat? →
    ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ = sat?
Tactic:
intro h
State after:
sat? : Bool
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
h :
  (⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ &&
      (go aig start h1 (State.empty aig)).val.eval (cnfSatAssignment aig assign1)) =
    sat?
⊢ ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ = sat?

State before:
sat? : Bool
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
h :
  (⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ &&
      (go aig start h1 (State.empty aig)).val.eval (cnfSatAssignment aig assign1)) =
    sat?
⊢ ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ = sat?
Tactic:
have := go_sat aig start h1 assign1 (.empty aig)
State after:
sat? : Bool
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
h :
  (⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ &&
      (go aig start h1 (State.empty aig)).val.eval (cnfSatAssignment aig assign1)) =
    sat?
this : (go aig start h1 (State.empty aig)).val.sat (cnfSatAssignment aig assign1)
⊢ ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ = sat?

State before:
sat? : Bool
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
h :
  (⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ &&
      (go aig start h1 (State.empty aig)).val.eval (cnfSatAssignment aig assign1)) =
    sat?
this : (go aig start h1 (State.empty aig)).val.sat (cnfSatAssignment aig assign1)
⊢ ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ = sat?
Tactic:
simp [CNF.sat] at this
State after:
sat? : Bool
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
h :
  (⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ &&
      (go aig start h1 (State.empty aig)).val.eval (cnfSatAssignment aig assign1)) =
    sat?
this : CNF.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val.cnf = true
⊢ ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ = sat?

State before:
sat? : Bool
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
h :
  (⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ &&
      (go aig start h1 (State.empty aig)).val.eval (cnfSatAssignment aig assign1)) =
    sat?
this : CNF.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val.cnf = true
⊢ ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, assign1⟧ = sat?
Tactic:
simpa [this] using h
State after:
no goals