internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.Encode.EncCNF.encodesProp_equisatisfiable
Proof 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]
Proof 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
Theorem: LeanSAT.Encode.EncCNF.encodesProp_equisatisfiable
Proof 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]
Proof 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
Theorem: LeanSAT.Encode.EncCNF.encodesProp_equisatisfiable
Proof 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
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.bind_encodesProp
Proof state before:
ν α β : Type u_1
P Q : PropPred ν
e1 : EncCNF ν α
f : α → EncCNF ν β
⊢ encodesProp e1 P → (∀ (s : LawfulState ν), encodesProp (f (↑e1 s).1) Q) → encodesProp (e1 >>= f) (P ⊓ Q)
Tactic:
intro hP hQ s
Proof state after:
ν α β : Type u_1
P Q : PropPred ν
e1 : EncCNF ν α
f : α → EncCNF ν β
hP : encodesProp e1 P
hQ : ∀ (s : LawfulState ν), encodesProp (f (↑e1 s).1) Q
s : LawfulState ν
⊢ let s' := (↑(e1 >>= f) s).2;
  s'.vMap = s.vMap ∧
    s'.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp s τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun s.assumeVars)ᶜ ⇨ P ⊓ Q
Theorem: LeanSAT.Encode.EncCNF.bind_encodesProp
Proof state before:
ν α β : Type u_1
P Q : PropPred ν
e1 : EncCNF ν α
f : α → EncCNF ν β
hP : encodesProp e1 P
hQ : ∀ (s : LawfulState ν), encodesProp (f (↑e1 s).1) Q
s : LawfulState ν
⊢ let s' := (↑(e1 >>= f) s).2;
  s'.vMap = s.vMap ∧
    s'.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp s τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun s.assumeVars)ᶜ ⇨ P ⊓ Q
Tactic:
simp [encodesProp, encodesProp.aux] at hP hQ
Proof state after:
ν α β : Type u_1
P Q : PropPred ν
e1 : EncCNF ν α
f : α → EncCNF ν β
s : LawfulState ν
hP :
  ∀ (s : LawfulState ν),
    (↑e1 s).2.vMap = s.vMap ∧
      (↑e1 s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑e1 s).2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s s_1 : LawfulState ν),
    (↑(f (↑e1 s).1) s_1).2.vMap = s_1.vMap ∧
      (↑(f (↑e1 s).1) s_1).2.assumeVars = s_1.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f (↑e1 s).1) s_1).2 τ ↔
            LawfulState.interp s_1 τ ∧ (¬τ ⊨ Clause.toPropFun s_1.assumeVars → Q τ)
⊢ let s' := (↑(e1 >>= f) s).2;
  s'.vMap = s.vMap ∧
    s'.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp s τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun s.assumeVars)ᶜ ⇨ P ⊓ Q
Theorem: LeanSAT.Encode.EncCNF.bind_encodesProp
Proof state before:
ν α β : Type u_1
P Q : PropPred ν
e1 : EncCNF ν α
f : α → EncCNF ν β
s : LawfulState ν
hP :
  ∀ (s : LawfulState ν),
    (↑e1 s).2.vMap = s.vMap ∧
      (↑e1 s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑e1 s).2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s s_1 : LawfulState ν),
    (↑(f (↑e1 s).1) s_1).2.vMap = s_1.vMap ∧
      (↑(f (↑e1 s).1) s_1).2.assumeVars = s_1.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f (↑e1 s).1) s_1).2 τ ↔
            LawfulState.interp s_1 τ ∧ (¬τ ⊨ Clause.toPropFun s_1.assumeVars → Q τ)
⊢ let s' := (↑(e1 >>= f) s).2;
  s'.vMap = s.vMap ∧
    s'.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp s τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun s.assumeVars)ᶜ ⇨ P ⊓ Q
Tactic:
rcases e1 with ⟨e1,he1⟩
Proof state after:
case mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
he1 : ∀ (s : LawfulState ν), s.nextVar ≤ (e1 s).2.nextVar
hP :
  ∀ (s : LawfulState ν),
    (↑{ val := e1, property := he1 } s).2.vMap = s.vMap ∧
      (↑{ val := e1, property := he1 } s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑{ val := e1, property := he1 } s).2 τ ↔
            LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s s_1 : LawfulState ν),
    (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2.vMap = s_1.vMap ∧
      (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2.assumeVars = s_1.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2 τ ↔
            LawfulState.interp s_1 τ ∧ (¬τ ⊨ Clause.toPropFun s_1.assumeVars → Q τ)
⊢ let s' := (↑({ val := e1, property := he1 } >>= f) s).2;
  s'.vMap = s.vMap ∧
    s'.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp s τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun s.assumeVars)ᶜ ⇨ P ⊓ Q
Theorem: LeanSAT.Encode.EncCNF.bind_encodesProp
Proof state before:
case mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
he1 : ∀ (s : LawfulState ν), s.nextVar ≤ (e1 s).2.nextVar
hP :
  ∀ (s : LawfulState ν),
    (↑{ val := e1, property := he1 } s).2.vMap = s.vMap ∧
      (↑{ val := e1, property := he1 } s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑{ val := e1, property := he1 } s).2 τ ↔
            LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s s_1 : LawfulState ν),
    (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2.vMap = s_1.vMap ∧
      (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2.assumeVars = s_1.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2 τ ↔
            LawfulState.interp s_1 τ ∧ (¬τ ⊨ Clause.toPropFun s_1.assumeVars → Q τ)
⊢ let s' := (↑({ val := e1, property := he1 } >>= f) s).2;
  s'.vMap = s.vMap ∧
    s'.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp s τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun s.assumeVars)ᶜ ⇨ P ⊓ Q
Tactic:
replace hP := hP s
Proof state after:
case mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
he1 : ∀ (s : LawfulState ν), s.nextVar ≤ (e1 s).2.nextVar
hQ :
  ∀ (s s_1 : LawfulState ν),
    (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2.vMap = s_1.vMap ∧
      (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2.assumeVars = s_1.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2 τ ↔
            LawfulState.interp s_1 τ ∧ (¬τ ⊨ Clause.toPropFun s_1.assumeVars → Q τ)
hP :
  (↑{ val := e1, property := he1 } s).2.vMap = s.vMap ∧
    (↑{ val := e1, property := he1 } s).2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑{ val := e1, property := he1 } s).2 τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
⊢ let s' := (↑({ val := e1, property := he1 } >>= f) s).2;
  s'.vMap = s.vMap ∧
    s'.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp s τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun s.assumeVars)ᶜ ⇨ P ⊓ Q
Theorem: LeanSAT.Encode.EncCNF.bind_encodesProp
Proof state before:
case mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
he1 : ∀ (s : LawfulState ν), s.nextVar ≤ (e1 s).2.nextVar
hQ :
  ∀ (s s_1 : LawfulState ν),
    (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2.vMap = s_1.vMap ∧
      (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2.assumeVars = s_1.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2 τ ↔
            LawfulState.interp s_1 τ ∧ (¬τ ⊨ Clause.toPropFun s_1.assumeVars → Q τ)
hP :
  (↑{ val := e1, property := he1 } s).2.vMap = s.vMap ∧
    (↑{ val := e1, property := he1 } s).2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑{ val := e1, property := he1 } s).2 τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
⊢ let s' := (↑({ val := e1, property := he1 } >>= f) s).2;
  s'.vMap = s.vMap ∧
    s'.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp s τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun s.assumeVars)ᶜ ⇨ P ⊓ Q
Tactic:
replace hQ := hQ s
Proof state after:
case mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
he1 : ∀ (s : LawfulState ν), s.nextVar ≤ (e1 s).2.nextVar
hP :
  (↑{ val := e1, property := he1 } s).2.vMap = s.vMap ∧
    (↑{ val := e1, property := he1 } s).2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑{ val := e1, property := he1 } s).2 τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s_1 : LawfulState ν),
    (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2.vMap = s_1.vMap ∧
      (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2.assumeVars = s_1.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2 τ ↔
            LawfulState.interp s_1 τ ∧ (¬τ ⊨ Clause.toPropFun s_1.assumeVars → Q τ)
⊢ let s' := (↑({ val := e1, property := he1 } >>= f) s).2;
  s'.vMap = s.vMap ∧
    s'.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp s τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun s.assumeVars)ᶜ ⇨ P ⊓ Q
Theorem: LeanSAT.Encode.EncCNF.bind_encodesProp
Proof state before:
case mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
he1 : ∀ (s : LawfulState ν), s.nextVar ≤ (e1 s).2.nextVar
hP :
  (↑{ val := e1, property := he1 } s).2.vMap = s.vMap ∧
    (↑{ val := e1, property := he1 } s).2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑{ val := e1, property := he1 } s).2 τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s_1 : LawfulState ν),
    (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2.vMap = s_1.vMap ∧
      (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2.assumeVars = s_1.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f (↑{ val := e1, property := he1 } s).1) s_1).2 τ ↔
            LawfulState.interp s_1 τ ∧ (¬τ ⊨ Clause.toPropFun s_1.assumeVars → Q τ)
⊢ let s' := (↑({ val := e1, property := he1 } >>= f) s).2;
  s'.vMap = s.vMap ∧
    s'.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp s τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun s.assumeVars)ᶜ ⇨ P ⊓ Q
Tactic:
simp [Bind.bind, StateT.bind] at hP hQ ⊢
Proof state after:
case mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
he1 : ∀ (s : LawfulState ν), s.nextVar ≤ (e1 s).2.nextVar
hP :
  (e1 s).2.vMap = s.vMap ∧
    (e1 s).2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (e1 s).2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s_1 : LawfulState ν),
    (↑(f (e1 s).1) s_1).2.vMap = s_1.vMap ∧
      (↑(f (e1 s).1) s_1).2.assumeVars = s_1.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f (e1 s).1) s_1).2 τ ↔
            LawfulState.interp s_1 τ ∧ (¬τ ⊨ Clause.toPropFun s_1.assumeVars → Q τ)
⊢ (match e1 s with
          | (a, s) => ↑(f a) s).2.vMap =
      s.vMap ∧
    (match e1 s with
            | (a, s) => ↑(f a) s).2.assumeVars =
        s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp
            (match e1 s with
              | (a, s) => ↑(f a) s).2
            τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Theorem: LeanSAT.Encode.EncCNF.bind_encodesProp
Proof state before:
case mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
he1 : ∀ (s : LawfulState ν), s.nextVar ≤ (e1 s).2.nextVar
hP :
  (e1 s).2.vMap = s.vMap ∧
    (e1 s).2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (e1 s).2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s_1 : LawfulState ν),
    (↑(f (e1 s).1) s_1).2.vMap = s_1.vMap ∧
      (↑(f (e1 s).1) s_1).2.assumeVars = s_1.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f (e1 s).1) s_1).2 τ ↔
            LawfulState.interp s_1 τ ∧ (¬τ ⊨ Clause.toPropFun s_1.assumeVars → Q τ)
⊢ (match e1 s with
          | (a, s) => ↑(f a) s).2.vMap =
      s.vMap ∧
    (match e1 s with
            | (a, s) => ↑(f a) s).2.assumeVars =
        s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp
            (match e1 s with
              | (a, s) => ↑(f a) s).2
            τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Tactic:
replace he1 := he1 s
Proof state after:
case mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
hP :
  (e1 s).2.vMap = s.vMap ∧
    (e1 s).2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (e1 s).2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s_1 : LawfulState ν),
    (↑(f (e1 s).1) s_1).2.vMap = s_1.vMap ∧
      (↑(f (e1 s).1) s_1).2.assumeVars = s_1.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f (e1 s).1) s_1).2 τ ↔
            LawfulState.interp s_1 τ ∧ (¬τ ⊨ Clause.toPropFun s_1.assumeVars → Q τ)
he1 : s.nextVar ≤ (e1 s).2.nextVar
⊢ (match e1 s with
          | (a, s) => ↑(f a) s).2.vMap =
      s.vMap ∧
    (match e1 s with
            | (a, s) => ↑(f a) s).2.assumeVars =
        s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp
            (match e1 s with
              | (a, s) => ↑(f a) s).2
            τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Theorem: LeanSAT.Encode.EncCNF.bind_encodesProp
Proof state before:
case mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
hP :
  (e1 s).2.vMap = s.vMap ∧
    (e1 s).2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (e1 s).2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s_1 : LawfulState ν),
    (↑(f (e1 s).1) s_1).2.vMap = s_1.vMap ∧
      (↑(f (e1 s).1) s_1).2.assumeVars = s_1.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f (e1 s).1) s_1).2 τ ↔
            LawfulState.interp s_1 τ ∧ (¬τ ⊨ Clause.toPropFun s_1.assumeVars → Q τ)
he1 : s.nextVar ≤ (e1 s).2.nextVar
⊢ (match e1 s with
          | (a, s) => ↑(f a) s).2.vMap =
      s.vMap ∧
    (match e1 s with
            | (a, s) => ↑(f a) s).2.assumeVars =
        s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp
            (match e1 s with
              | (a, s) => ↑(f a) s).2
            τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Tactic:
generalize hs' : e1 s = s' at *
Proof state after:
case mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
s' : Id (α × LawfulState ν)
hs' : e1 s = s'
hP :
  s'.2.vMap = s.vMap ∧
    s'.2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s'.2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s : LawfulState ν),
    (↑(f s'.1) s).2.vMap = s.vMap ∧
      (↑(f s'.1) s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f s'.1) s).2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → Q τ)
he1 : s.nextVar ≤ s'.2.nextVar
⊢ (match s' with
          | (a, s) => ↑(f a) s).2.vMap =
      s.vMap ∧
    (match s' with
            | (a, s) => ↑(f a) s).2.assumeVars =
        s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp
            (match s' with
              | (a, s) => ↑(f a) s).2
            τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Theorem: LeanSAT.Encode.EncCNF.bind_encodesProp
Proof state before:
case mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
s' : Id (α × LawfulState ν)
hs' : e1 s = s'
hP :
  s'.2.vMap = s.vMap ∧
    s'.2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s'.2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s : LawfulState ν),
    (↑(f s'.1) s).2.vMap = s.vMap ∧
      (↑(f s'.1) s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f s'.1) s).2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → Q τ)
he1 : s.nextVar ≤ s'.2.nextVar
⊢ (match s' with
          | (a, s) => ↑(f a) s).2.vMap =
      s.vMap ∧
    (match s' with
            | (a, s) => ↑(f a) s).2.assumeVars =
        s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp
            (match s' with
              | (a, s) => ↑(f a) s).2
            τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Tactic:
rcases s' with ⟨a,s'⟩
Proof state after:
case mk.mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
a : α
s' : LawfulState ν
hs' : e1 s = (a, s')
hP :
  (a, s').2.vMap = s.vMap ∧
    (a, s').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (a, s').2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s : LawfulState ν),
    (↑(f (a, s').1) s).2.vMap = s.vMap ∧
      (↑(f (a, s').1) s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f (a, s').1) s).2 τ ↔
            LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → Q τ)
he1 : s.nextVar ≤ (a, s').2.nextVar
⊢ (match (a, s') with
          | (a, s) => ↑(f a) s).2.vMap =
      s.vMap ∧
    (match (a, s') with
            | (a, s) => ↑(f a) s).2.assumeVars =
        s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp
            (match (a, s') with
              | (a, s) => ↑(f a) s).2
            τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Theorem: LeanSAT.Encode.EncCNF.bind_encodesProp
Proof state before:
case mk.mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
a : α
s' : LawfulState ν
hs' : e1 s = (a, s')
hP :
  (a, s').2.vMap = s.vMap ∧
    (a, s').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (a, s').2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s : LawfulState ν),
    (↑(f (a, s').1) s).2.vMap = s.vMap ∧
      (↑(f (a, s').1) s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f (a, s').1) s).2 τ ↔
            LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → Q τ)
he1 : s.nextVar ≤ (a, s').2.nextVar
⊢ (match (a, s') with
          | (a, s) => ↑(f a) s).2.vMap =
      s.vMap ∧
    (match (a, s') with
            | (a, s) => ↑(f a) s).2.assumeVars =
        s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp
            (match (a, s') with
              | (a, s) => ↑(f a) s).2
            τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Tactic:
simp at *
Proof state after:
case mk.mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
a : α
s' : LawfulState ν
hs' : e1 s = (a, s')
hP :
  s'.vMap = s.vMap ∧
    s'.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s : LawfulState ν),
    (↑(f a) s).2.vMap = s.vMap ∧
      (↑(f a) s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f a) s).2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → Q τ)
he1 : s.nextVar ≤ s'.nextVar
⊢ (↑(f a) s').2.vMap = s.vMap ∧
    (↑(f a) s').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑(f a) s').2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Theorem: LeanSAT.Encode.EncCNF.bind_encodesProp
Proof state before:
case mk.mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
a : α
s' : LawfulState ν
hs' : e1 s = (a, s')
hP :
  s'.vMap = s.vMap ∧
    s'.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
hQ :
  ∀ (s : LawfulState ν),
    (↑(f a) s).2.vMap = s.vMap ∧
      (↑(f a) s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑(f a) s).2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → Q τ)
he1 : s.nextVar ≤ s'.nextVar
⊢ (↑(f a) s').2.vMap = s.vMap ∧
    (↑(f a) s').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑(f a) s').2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Tactic:
generalize he2 : (f a) = e2 at *
Proof state after:
case mk.mk
ν α β : Type u_1
P Q : PropPred ν
f : α → EncCNF ν β
s : LawfulState ν
e1 : StateM (LawfulState ν) α
a : α
s' : LawfulState ν
hs' : e1 s = (a, s')
hP :
  s'.vMap = s.vMap ∧
    s'.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ)
he1 : s.nextVar ≤ s'.nextVar
e2 : EncCNF ν β
he2 : f a = e2
hQ :
  ∀ (s : LawfulState ν),
    (↑e2 s).2.vMap = s.vMap ∧
      (↑e2 s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑e2 s).2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → Q τ)
⊢ (↑e2 s').2.vMap = s.vMap ∧
    (↑e2 s').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑e2 s').2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)