Theorem: LeanSAT.Encode.EncCNF.encodesProp_equisatisfiable (LeanSAT/Encode/VEncCNF.lean)

State before:
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
⊢ (∃ τ, τ ⊨ P) ↔ ∃ τ, τ ⊨ Cnf.toPropFun (toICnf e)
Tactic:
simp [toICnf, run, StateT.run]
State after:
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
⊢ (∃ τ, P τ) ↔
    ∃ τ, τ ⊨ Cnf.toPropFun (↑e (LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv))).2.cnf

State before:
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
⊢ (∃ τ, P τ) ↔
    ∃ τ, τ ⊨ Cnf.toPropFun (↑e (LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv))).2.cnf
Tactic:
generalize hls : LawfulState.new' _ _ = ls
State after:
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun (↑e ls).2.cnf

State before:
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun (↑e ls).2.cnf
Tactic:
have := h ls
State after:
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
this :
  let s' := (↑e ls).2;
  s'.vMap = ls.vMap ∧
    s'.assumeVars = ls.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun (↑e ls).2.cnf

State before:
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
this :
  let s' := (↑e ls).2;
  s'.vMap = ls.vMap ∧
    s'.assumeVars = ls.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun (↑e ls).2.cnf
Tactic:
generalize hls' : e.1 ls = ls' at this
State after:
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
ls' : Id (α × LawfulState ν)
hls' : ↑e ls = ls'
this :
  let s' := ls'.2;
  s'.vMap = ls.vMap ∧
    s'.assumeVars = ls.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.2.cnf

State before:
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
ls' : Id (α × LawfulState ν)
hls' : ↑e ls = ls'
this :
  let s' := ls'.2;
  s'.vMap = ls.vMap ∧
    s'.assumeVars = ls.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.2.cnf
Tactic:
rcases ls' with ⟨a,ls'⟩
State after:
case mk
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
this :
  let s' := (a, ls').2;
  s'.vMap = ls.vMap ∧
    s'.assumeVars = ls.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun (a, ls').2.cnf

State before:
case mk
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
this :
  let s' := (a, ls').2;
  s'.vMap = ls.vMap ∧
    s'.assumeVars = ls.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun (a, ls').2.cnf
Tactic:
simp only at this ⊢
State after:
case mk
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
this :
  ls'.vMap = ls.vMap ∧
    ls'.assumeVars = ls.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp ls' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf

State before:
case mk
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
this :
  ls'.vMap = ls.vMap ∧
    ls'.assumeVars = ls.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp ls' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf
Tactic:
rcases this with ⟨-,-,h3⟩
State after:
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
h3 :
  ∀ (τ : PropAssignment ν),
    LawfulState.interp ls' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf

State before:
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
h3 :
  ∀ (τ : PropAssignment ν),
    LawfulState.interp ls' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf
Tactic:
rw [←hls] at h3
State after:
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
h3 :
  ∀ (τ : PropAssignment ν),
    LawfulState.interp ls' τ ↔
      LawfulState.interp (LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv)) τ ∧
        τ ⊨
          (fun τ =>
                τ ⊨
                  Clause.toPropFun
                    (LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv)).assumeVars)ᶜ ⇨
            P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf

State before:
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
h3 :
  ∀ (τ : PropAssignment ν),
    LawfulState.interp ls' τ ↔
      LawfulState.interp (LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv)) τ ∧
        τ ⊨
          (fun τ =>
                τ ⊨
                  Clause.toPropFun
                    (LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv)).assumeVars)ᶜ ⇨
            P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf
Tactic:
simp [LawfulState.new', State.new, Clause.toPropFun] at h3
State after:
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
h3 : ∀ (τ : PropAssignment ν), LawfulState.interp ls' τ ↔ P τ
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf

State before:
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
h3 : ∀ (τ : PropAssignment ν), LawfulState.interp ls' τ ↔ P τ
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf
Tactic:
clear hls' hls
State after:
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
a : α
ls' : LawfulState ν
h3 : ∀ (τ : PropAssignment ν), LawfulState.interp ls' τ ↔ P τ
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf

State before:
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
a : α
ls' : LawfulState ν
h3 : ∀ (τ : PropAssignment ν), LawfulState.interp ls' τ ↔ P τ
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf
Tactic:
simp_rw [← h3]
State after:
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
a : α
ls' : LawfulState ν
h3 : ∀ (τ : PropAssignment ν), LawfulState.interp ls' τ ↔ P τ
⊢ (∃ τ, LawfulState.interp ls' τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf

State before:
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
a : α
ls' : LawfulState ν
h3 : ∀ (τ : PropAssignment ν), LawfulState.interp ls' τ ↔ P τ
⊢ (∃ τ, LawfulState.interp ls' τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf
Tactic:
simp [LawfulState.interp]
State after:
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
a : α
ls' : LawfulState ν
h3 : ∀ (τ : PropAssignment ν), LawfulState.interp ls' τ ↔ P τ
⊢ (∃ τ σ, τ = PropAssignment.map ls'.vMap σ ∧ σ ⊨ Cnf.toPropFun ls'.cnf) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf

State before:
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
a : α
ls' : LawfulState ν
h3 : ∀ (τ : PropAssignment ν), LawfulState.interp ls' τ ↔ P τ
⊢ (∃ τ σ, τ = PropAssignment.map ls'.vMap σ ∧ σ ⊨ Cnf.toPropFun ls'.cnf) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf
Tactic:
aesop
State after:
no goals