Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_addClause (LeanSAT/Encode/EncCNF.lean)

State before:
L : Type ?u.23742
ν : Type u_1
inst✝ : LitVar L ν
C : Clause (Literal ν)
s : LawfulState ν
⊢ interp (addClause C s) = fun τ =>
    interp s τ ∧ ((fun M φ => ¬M ⊨ φ) τ (Clause.toPropFun s.assumeVars) → τ ⊨ Clause.toPropFun C)
Tactic:
ext τ
State after:
case h.a
L : Type ?u.23742
ν : Type u_1
inst✝ : LitVar L ν
C : Clause (Literal ν)
s : LawfulState ν
τ : PropAssignment ν
⊢ interp (addClause C s) τ ↔
    interp s τ ∧ ((fun M φ => ¬M ⊨ φ) τ (Clause.toPropFun s.assumeVars) → τ ⊨ Clause.toPropFun C)

State before:
case h.a
L : Type ?u.23742
ν : Type u_1
inst✝ : LitVar L ν
C : Clause (Literal ν)
s : LawfulState ν
τ : PropAssignment ν
⊢ interp (addClause C s) τ ↔
    interp s τ ∧ ((fun M φ => ¬M ⊨ φ) τ (Clause.toPropFun s.assumeVars) → τ ⊨ Clause.toPropFun C)
Tactic:
simp [addClause, interp, State.addClause, imp_iff_not_or]
State after:
case h.a
L : Type ?u.23742
ν : Type u_1
inst✝ : LitVar L ν
C : Clause (Literal ν)
s : LawfulState ν
τ : PropAssignment ν
⊢ (∃ σ,
      τ = PropAssignment.map s.1.vMap σ ∧
        σ ⊨ Cnf.toPropFun s.1.cnf ∧
          (PropAssignment.map s.1.vMap σ ⊨ Clause.toPropFun s.1.assumeVars ∨
            PropAssignment.map s.1.vMap σ ⊨ Clause.toPropFun C)) ↔
    (∃ σ, τ = PropAssignment.map s.vMap σ ∧ σ ⊨ Cnf.toPropFun s.cnf) ∧
      (τ ⊨ Clause.toPropFun s.assumeVars ∨ τ ⊨ Clause.toPropFun C)

State before:
case h.a
L : Type ?u.23742
ν : Type u_1
inst✝ : LitVar L ν
C : Clause (Literal ν)
s : LawfulState ν
τ : PropAssignment ν
⊢ (∃ σ,
      τ = PropAssignment.map s.1.vMap σ ∧
        σ ⊨ Cnf.toPropFun s.1.cnf ∧
          (PropAssignment.map s.1.vMap σ ⊨ Clause.toPropFun s.1.assumeVars ∨
            PropAssignment.map s.1.vMap σ ⊨ Clause.toPropFun C)) ↔
    (∃ σ, τ = PropAssignment.map s.vMap σ ∧ σ ⊨ Cnf.toPropFun s.cnf) ∧
      (τ ⊨ Clause.toPropFun s.assumeVars ∨ τ ⊨ Clause.toPropFun C)
Tactic:
rw [← exists_and_right]
State after:
case h.a
L : Type ?u.23742
ν : Type u_1
inst✝ : LitVar L ν
C : Clause (Literal ν)
s : LawfulState ν
τ : PropAssignment ν
⊢ (∃ σ,
      τ = PropAssignment.map s.1.vMap σ ∧
        σ ⊨ Cnf.toPropFun s.1.cnf ∧
          (PropAssignment.map s.1.vMap σ ⊨ Clause.toPropFun s.1.assumeVars ∨
            PropAssignment.map s.1.vMap σ ⊨ Clause.toPropFun C)) ↔
    ∃ x,
      (τ = PropAssignment.map s.vMap x ∧ x ⊨ Cnf.toPropFun s.cnf) ∧
        (τ ⊨ Clause.toPropFun s.assumeVars ∨ τ ⊨ Clause.toPropFun C)

State before:
case h.a
L : Type ?u.23742
ν : Type u_1
inst✝ : LitVar L ν
C : Clause (Literal ν)
s : LawfulState ν
τ : PropAssignment ν
⊢ (∃ σ,
      τ = PropAssignment.map s.1.vMap σ ∧
        σ ⊨ Cnf.toPropFun s.1.cnf ∧
          (PropAssignment.map s.1.vMap σ ⊨ Clause.toPropFun s.1.assumeVars ∨
            PropAssignment.map s.1.vMap σ ⊨ Clause.toPropFun C)) ↔
    ∃ x,
      (τ = PropAssignment.map s.vMap x ∧ x ⊨ Cnf.toPropFun s.cnf) ∧
        (τ ⊨ Clause.toPropFun s.assumeVars ∨ τ ⊨ Clause.toPropFun C)
Tactic:
apply exists_congr
State after:
case h.a.h
L : Type ?u.23742
ν : Type u_1
inst✝ : LitVar L ν
C : Clause (Literal ν)
s : LawfulState ν
τ : PropAssignment ν
⊢ ∀ (a : PropAssignment IVar),
    τ = PropAssignment.map s.1.vMap a ∧
        a ⊨ Cnf.toPropFun s.1.cnf ∧
          (PropAssignment.map s.1.vMap a ⊨ Clause.toPropFun s.1.assumeVars ∨
            PropAssignment.map s.1.vMap a ⊨ Clause.toPropFun C) ↔
      (τ = PropAssignment.map s.vMap a ∧ a ⊨ Cnf.toPropFun s.cnf) ∧
        (τ ⊨ Clause.toPropFun s.assumeVars ∨ τ ⊨ Clause.toPropFun C)

State before:
case h.a.h
L : Type ?u.23742
ν : Type u_1
inst✝ : LitVar L ν
C : Clause (Literal ν)
s : LawfulState ν
τ : PropAssignment ν
⊢ ∀ (a : PropAssignment IVar),
    τ = PropAssignment.map s.1.vMap a ∧
        a ⊨ Cnf.toPropFun s.1.cnf ∧
          (PropAssignment.map s.1.vMap a ⊨ Clause.toPropFun s.1.assumeVars ∨
            PropAssignment.map s.1.vMap a ⊨ Clause.toPropFun C) ↔
      (τ = PropAssignment.map s.vMap a ∧ a ⊨ Cnf.toPropFun s.cnf) ∧
        (τ ⊨ Clause.toPropFun s.assumeVars ∨ τ ⊨ Clause.toPropFun C)
Tactic:
intro σ
State after:
case h.a.h
L : Type ?u.23742
ν : Type u_1
inst✝ : LitVar L ν
C : Clause (Literal ν)
s : LawfulState ν
τ : PropAssignment ν
σ : PropAssignment IVar
⊢ τ = PropAssignment.map s.1.vMap σ ∧
      σ ⊨ Cnf.toPropFun s.1.cnf ∧
        (PropAssignment.map s.1.vMap σ ⊨ Clause.toPropFun s.1.assumeVars ∨
          PropAssignment.map s.1.vMap σ ⊨ Clause.toPropFun C) ↔
    (τ = PropAssignment.map s.vMap σ ∧ σ ⊨ Cnf.toPropFun s.cnf) ∧
      (τ ⊨ Clause.toPropFun s.assumeVars ∨ τ ⊨ Clause.toPropFun C)

State before:
case h.a.h
L : Type ?u.23742
ν : Type u_1
inst✝ : LitVar L ν
C : Clause (Literal ν)
s : LawfulState ν
τ : PropAssignment ν
σ : PropAssignment IVar
⊢ τ = PropAssignment.map s.1.vMap σ ∧
      σ ⊨ Cnf.toPropFun s.1.cnf ∧
        (PropAssignment.map s.1.vMap σ ⊨ Clause.toPropFun s.1.assumeVars ∨
          PropAssignment.map s.1.vMap σ ⊨ Clause.toPropFun C) ↔
    (τ = PropAssignment.map s.vMap σ ∧ σ ⊨ Cnf.toPropFun s.cnf) ∧
      (τ ⊨ Clause.toPropFun s.assumeVars ∨ τ ⊨ Clause.toPropFun C)
Tactic:
aesop
State after:
no goals