internlm/Lean-Github huggingface dataset:
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 τ)
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 τ)
Tactic:
rcases e2 with ⟨e2,he2⟩
Proof state after:
case mk.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 : StateM (LawfulState ν) β
he2✝ : ∀ (s : LawfulState ν), s.nextVar ≤ (e2 s).2.nextVar
he2 : f a = { val := e2, property := he2✝ }
hQ :
  ∀ (s : LawfulState ν),
    (↑{ val := e2, property := he2✝ } s).2.vMap = s.vMap ∧
      (↑{ val := e2, property := he2✝ } s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑{ val := e2, property := he2✝ } s).2 τ ↔
            LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → Q τ)
⊢ (↑{ val := e2, property := he2✝ } s').2.vMap = s.vMap ∧
    (↑{ val := e2, property := he2✝ } s').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑{ val := e2, property := he2✝ } s').2 τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Theorem: LeanSAT.Encode.EncCNF.bind_encodesProp
Proof state before:
case mk.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 : StateM (LawfulState ν) β
he2✝ : ∀ (s : LawfulState ν), s.nextVar ≤ (e2 s).2.nextVar
he2 : f a = { val := e2, property := he2✝ }
hQ :
  ∀ (s : LawfulState ν),
    (↑{ val := e2, property := he2✝ } s).2.vMap = s.vMap ∧
      (↑{ val := e2, property := he2✝ } s).2.assumeVars = s.assumeVars ∧
        ∀ (τ : PropAssignment ν),
          LawfulState.interp (↑{ val := e2, property := he2✝ } s).2 τ ↔
            LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → Q τ)
⊢ (↑{ val := e2, property := he2✝ } s').2.vMap = s.vMap ∧
    (↑{ val := e2, property := he2✝ } s').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑{ val := e2, property := he2✝ } s').2 τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Tactic:
replace hQ := hQ s'
Proof state after:
case mk.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 : StateM (LawfulState ν) β
he2✝ : ∀ (s : LawfulState ν), s.nextVar ≤ (e2 s).2.nextVar
he2 : f a = { val := e2, property := he2✝ }
hQ :
  (↑{ val := e2, property := he2✝ } s').2.vMap = s'.vMap ∧
    (↑{ val := e2, property := he2✝ } s').2.assumeVars = s'.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑{ val := e2, property := he2✝ } s').2 τ ↔
          LawfulState.interp s' τ ∧ (¬τ ⊨ Clause.toPropFun s'.assumeVars → Q τ)
⊢ (↑{ val := e2, property := he2✝ } s').2.vMap = s.vMap ∧
    (↑{ val := e2, property := he2✝ } s').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑{ val := e2, property := he2✝ } s').2 τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Theorem: LeanSAT.Encode.EncCNF.bind_encodesProp
Proof state before:
case mk.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 : StateM (LawfulState ν) β
he2✝ : ∀ (s : LawfulState ν), s.nextVar ≤ (e2 s).2.nextVar
he2 : f a = { val := e2, property := he2✝ }
hQ :
  (↑{ val := e2, property := he2✝ } s').2.vMap = s'.vMap ∧
    (↑{ val := e2, property := he2✝ } s').2.assumeVars = s'.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑{ val := e2, property := he2✝ } s').2 τ ↔
          LawfulState.interp s' τ ∧ (¬τ ⊨ Clause.toPropFun s'.assumeVars → Q τ)
⊢ (↑{ val := e2, property := he2✝ } s').2.vMap = s.vMap ∧
    (↑{ val := e2, property := he2✝ } s').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (↑{ val := e2, property := he2✝ } s').2 τ ↔
          LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Tactic:
simp at *
Proof state after:
case mk.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 : StateM (LawfulState ν) β
he2✝ : ∀ (s : LawfulState ν), s.nextVar ≤ (e2 s).2.nextVar
he2 : f a = { val := e2, property := he2✝ }
hQ :
  (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 τ)
Theorem: LeanSAT.Encode.EncCNF.bind_encodesProp
Proof state before:
case mk.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 : StateM (LawfulState ν) β
he2✝ : ∀ (s : LawfulState ν), s.nextVar ≤ (e2 s).2.nextVar
he2 : f a = { val := e2, property := he2✝ }
hQ :
  (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 τ)
Tactic:
generalize hs'' : e2 s' = s'' at *
Proof state after:
case mk.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 : StateM (LawfulState ν) β
he2✝ : ∀ (s : LawfulState ν), s.nextVar ≤ (e2 s).2.nextVar
he2 : f a = { val := e2, property := he2✝ }
s'' : Id (β × LawfulState ν)
hs'' : e2 s' = s''
hQ :
  s''.2.vMap = s'.vMap ∧
    s''.2.assumeVars = s'.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s''.2 τ ↔ LawfulState.interp s' τ ∧ (¬τ ⊨ Clause.toPropFun s'.assumeVars → Q τ)
⊢ s''.2.vMap = s.vMap ∧
    s''.2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s''.2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Theorem: LeanSAT.Encode.EncCNF.bind_encodesProp
Proof state before:
case mk.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 : StateM (LawfulState ν) β
he2✝ : ∀ (s : LawfulState ν), s.nextVar ≤ (e2 s).2.nextVar
he2 : f a = { val := e2, property := he2✝ }
s'' : Id (β × LawfulState ν)
hs'' : e2 s' = s''
hQ :
  s''.2.vMap = s'.vMap ∧
    s''.2.assumeVars = s'.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s''.2 τ ↔ LawfulState.interp s' τ ∧ (¬τ ⊨ Clause.toPropFun s'.assumeVars → Q τ)
⊢ s''.2.vMap = s.vMap ∧
    s''.2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s''.2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Tactic:
rcases s'' with ⟨b,s''⟩
Proof state after:
case mk.mk.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 : StateM (LawfulState ν) β
he2✝ : ∀ (s : LawfulState ν), s.nextVar ≤ (e2 s).2.nextVar
he2 : f a = { val := e2, property := he2✝ }
b : β
s'' : LawfulState ν
hs'' : e2 s' = (b, s'')
hQ :
  (b, s'').2.vMap = s'.vMap ∧
    (b, s'').2.assumeVars = s'.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (b, s'').2 τ ↔ LawfulState.interp s' τ ∧ (¬τ ⊨ Clause.toPropFun s'.assumeVars → Q τ)
⊢ (b, s'').2.vMap = s.vMap ∧
    (b, s'').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (b, s'').2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Theorem: LeanSAT.Encode.EncCNF.bind_encodesProp
Proof state before:
case mk.mk.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 : StateM (LawfulState ν) β
he2✝ : ∀ (s : LawfulState ν), s.nextVar ≤ (e2 s).2.nextVar
he2 : f a = { val := e2, property := he2✝ }
b : β
s'' : LawfulState ν
hs'' : e2 s' = (b, s'')
hQ :
  (b, s'').2.vMap = s'.vMap ∧
    (b, s'').2.assumeVars = s'.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (b, s'').2 τ ↔ LawfulState.interp s' τ ∧ (¬τ ⊨ Clause.toPropFun s'.assumeVars → Q τ)
⊢ (b, s'').2.vMap = s.vMap ∧
    (b, s'').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (b, s'').2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Tactic:
open PropPred in simp at hP hQ ⊢
aesop
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.bind_encodesProp
Proof state before:
case mk.mk.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 : StateM (LawfulState ν) β
he2✝ : ∀ (s : LawfulState ν), s.nextVar ≤ (e2 s).2.nextVar
he2 : f a = { val := e2, property := he2✝ }
b : β
s'' : LawfulState ν
hs'' : e2 s' = (b, s'')
hQ :
  (b, s'').2.vMap = s'.vMap ∧
    (b, s'').2.assumeVars = s'.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (b, s'').2 τ ↔ LawfulState.interp s' τ ∧ (¬τ ⊨ Clause.toPropFun s'.assumeVars → Q τ)
⊢ (b, s'').2.vMap = s.vMap ∧
    (b, s'').2.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp (b, s'').2 τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Tactic:
simp at hP hQ ⊢
Proof state after:
case mk.mk.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 : StateM (LawfulState ν) β
he2✝ : ∀ (s : LawfulState ν), s.nextVar ≤ (e2 s).2.nextVar
he2 : f a = { val := e2, property := he2✝ }
b : β
s'' : LawfulState ν
hs'' : e2 s' = (b, s'')
hQ :
  s''.vMap = s'.vMap ∧
    s''.assumeVars = s'.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s'' τ ↔ LawfulState.interp s' τ ∧ (¬τ ⊨ Clause.toPropFun s'.assumeVars → Q τ)
⊢ s''.vMap = s.vMap ∧
    s''.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s'' τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Theorem: LeanSAT.Encode.EncCNF.bind_encodesProp
Proof state before:
case mk.mk.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 : StateM (LawfulState ν) β
he2✝ : ∀ (s : LawfulState ν), s.nextVar ≤ (e2 s).2.nextVar
he2 : f a = { val := e2, property := he2✝ }
b : β
s'' : LawfulState ν
hs'' : e2 s' = (b, s'')
hQ :
  s''.vMap = s'.vMap ∧
    s''.assumeVars = s'.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s'' τ ↔ LawfulState.interp s' τ ∧ (¬τ ⊨ Clause.toPropFun s'.assumeVars → Q τ)
⊢ s''.vMap = s.vMap ∧
    s''.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s'' τ ↔ LawfulState.interp s τ ∧ (¬τ ⊨ Clause.toPropFun s.assumeVars → P τ ∧ Q τ)
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.encodesProp_pure
Proof state before:
α ν : Type u_1
a : α
⊢ encodesProp (pure a) ⊤
Tactic:
intro s
Proof state after:
α ν : Type u_1
a : α
s : LawfulState ν
⊢ let s' := (↑(pure a) s).2;
  s'.vMap = s.vMap ∧
    s'.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp s τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun s.assumeVars)ᶜ ⇨ ⊤
Theorem: LeanSAT.Encode.EncCNF.encodesProp_pure
Proof state before:
α ν : Type u_1
a : α
s : LawfulState ν
⊢ let s' := (↑(pure a) s).2;
  s'.vMap = s.vMap ∧
    s'.assumeVars = s.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp s τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun s.assumeVars)ᶜ ⇨ ⊤
Tactic:
simp [Pure.pure, StateT.pure]
Proof state after:
no goals
Theorem: LeanSAT.Encode.VEncCNF.toICnf_equisatisfiable
Proof state before:
ν α : Type u_1
P : PropPred ν
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
v : VEncCNF ν α P
⊢ (∃ τ, τ ⊨ Cnf.toPropFun (toICnf ↑v)) ↔ ∃ τ, τ ⊨ P
Tactic:
rw [v.val.encodesProp_equisatisfiable _ v.property]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.satisfies_var
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ τ ⊨ var x ↔ τ x = true
Tactic:
simp [sEntails, satisfies]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.satisfies_tr
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ τ ⊨ tr
Tactic:
simp [sEntails, satisfies]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.satisfies_neg
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ τ ⊨ neg φ ↔ (fun M φ => ¬M ⊨ φ) τ φ
Tactic:
simp [sEntails, satisfies]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.satisfies_conj
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ τ ⊨ conj φ₁ φ₂ ↔ τ ⊨ φ₁ ∧ τ ⊨ φ₂
Tactic:
simp [sEntails, satisfies]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.satisfies_disj
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ τ ⊨ disj φ₁ φ₂ ↔ τ ⊨ φ₁ ∨ τ ⊨ φ₂
Tactic:
simp [sEntails, satisfies]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.satisfies_impl
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ τ ⊨ impl φ₁ φ₂ ↔ τ ⊨ φ₁ → τ ⊨ φ₂
Tactic:
simp only [sEntails, satisfies, eval]
Proof state after:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ eval τ φ₁ ⇨ eval τ φ₂ = true ↔ eval τ φ₁ = true → eval τ φ₂ = true
Theorem: LeanSAT.Model.PropForm.satisfies_impl
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ eval τ φ₁ ⇨ eval τ φ₂ = true ↔ eval τ φ₁ = true → eval τ φ₂ = true
Tactic:
cases (eval τ φ₁) <;> simp [himp_eq]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.satisfies_impl'
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ τ ⊨ impl φ₁ φ₂ ↔ (fun M φ => ¬M ⊨ φ) τ φ₁ ∨ τ ⊨ φ₂
Tactic:
simp only [sEntails, satisfies, eval]
Proof state after:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ eval τ φ₁ ⇨ eval τ φ₂ = true ↔ ¬eval τ φ₁ = true ∨ eval τ φ₂ = true
Theorem: LeanSAT.Model.PropForm.satisfies_impl'
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ eval τ φ₁ ⇨ eval τ φ₂ = true ↔ ¬eval τ φ₁ = true ∨ eval τ φ₂ = true
Tactic:
cases (eval τ φ₁) <;> simp [himp_eq]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.satisfies_biImpl
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ τ ⊨ biImpl φ₁ φ₂ ↔ (τ ⊨ φ₁ ↔ τ ⊨ φ₂)
Tactic:
simp [sEntails, satisfies]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.satisfies_biImpl'
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ τ ⊨ biImpl φ₁ φ₂ ↔ τ ⊨ φ₁ ∧ τ ⊨ φ₂ ∨ (fun M φ => ¬M ⊨ φ) τ φ₁ ∧ (fun M φ => ¬M ⊨ φ) τ φ₂
Tactic:
simp only [sEntails, satisfies, eval]
Proof state after:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ decide (eval τ φ₁ = eval τ φ₂) = true ↔ eval τ φ₁ = true ∧ eval τ φ₂ = true ∨ ¬eval τ φ₁ = true ∧ ¬eval τ φ₂ = true
Theorem: LeanSAT.Model.PropForm.satisfies_biImpl'
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ decide (eval τ φ₁ = eval τ φ₂) = true ↔ eval τ φ₁ = true ∧ eval τ φ₂ = true ∨ ¬eval τ φ₁ = true ∧ ¬eval τ φ₂ = true
Tactic:
cases (eval τ φ₁) <;> aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.entails_ext
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ entails φ₁ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁ → τ ⊨ φ₂
Tactic:
have : ∀ τ, (φ₁.eval τ → φ₂.eval τ) ↔ φ₁.eval τ ≤ φ₂.eval τ := by
  intro τ
  cases (eval τ φ₁)
  . simp
  . simp only [true_implies]
    exact ⟨fun h => h ▸ le_rfl, top_unique⟩
Proof state after:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
this : ∀ (τ : PropAssignment ν), eval τ φ₁ = true → eval τ φ₂ = true ↔ eval τ φ₁ ≤ eval τ φ₂
⊢ entails φ₁ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁ → τ ⊨ φ₂
Theorem: LeanSAT.Model.PropForm.entails_ext
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
this : ∀ (τ : PropAssignment ν), eval τ φ₁ = true → eval τ φ₂ = true ↔ eval τ φ₁ ≤ eval τ φ₂
⊢ entails φ₁ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁ → τ ⊨ φ₂
Tactic:
simp [sEntails, entails, satisfies, this]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.entails_ext
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ ∀ (τ : PropAssignment ν), eval τ φ₁ = true → eval τ φ₂ = true ↔ eval τ φ₁ ≤ eval τ φ₂
Tactic:
intro τ
Proof state after:
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ eval τ φ₁ = true → eval τ φ₂ = true ↔ eval τ φ₁ ≤ eval τ φ₂
Theorem: LeanSAT.Model.PropForm.entails_ext
Proof state before:
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ eval τ φ₁ = true → eval τ φ₂ = true ↔ eval τ φ₁ ≤ eval τ φ₂
Tactic:
cases (eval τ φ₁)
Proof state after:
case false
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ false = true → eval τ φ₂ = true ↔ false ≤ eval τ φ₂

case true
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ true = true → eval τ φ₂ = true ↔ true ≤ eval τ φ₂
Theorem: LeanSAT.Model.PropForm.entails_ext
Proof state before:
case false
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ false = true → eval τ φ₂ = true ↔ false ≤ eval τ φ₂

case true
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ true = true → eval τ φ₂ = true ↔ true ≤ eval τ φ₂
Tactic:
. simp
Proof state after:
case true
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ true = true → eval τ φ₂ = true ↔ true ≤ eval τ φ₂
Theorem: LeanSAT.Model.PropForm.entails_ext
Proof state before:
case true
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ true = true → eval τ φ₂ = true ↔ true ≤ eval τ φ₂
Tactic:
. simp only [true_implies]
  exact ⟨fun h => h ▸ le_rfl, top_unique⟩
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.entails_ext
Proof state before:
case false
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ false = true → eval τ φ₂ = true ↔ false ≤ eval τ φ₂
Tactic:
simp
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.entails_ext
Proof state before:
case true
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ true = true → eval τ φ₂ = true ↔ true ≤ eval τ φ₂
Tactic:
simp only [true_implies]
Proof state after:
case true
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ eval τ φ₂ = true ↔ true ≤ eval τ φ₂
Theorem: LeanSAT.Model.PropForm.entails_ext
Proof state before:
case true
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ eval τ φ₂ = true ↔ true ≤ eval τ φ₂
Tactic:
exact ⟨fun h => h ▸ le_rfl, top_unique⟩
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.equivalent_iff_entails
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ equivalent φ₁ φ₂ ↔ entails φ₁ φ₂ ∧ entails φ₂ φ₁
Tactic:
simp only [equivalent, entails]
Proof state after:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ (∀ (τ : PropAssignment ν), eval τ φ₁ = eval τ φ₂) ↔
    (∀ (τ : PropAssignment ν), eval τ φ₁ ≤ eval τ φ₂) ∧ ∀ (τ : PropAssignment ν), eval τ φ₂ ≤ eval τ φ₁
Theorem: LeanSAT.Model.PropForm.equivalent_iff_entails
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ (∀ (τ : PropAssignment ν), eval τ φ₁ = eval τ φ₂) ↔
    (∀ (τ : PropAssignment ν), eval τ φ₁ ≤ eval τ φ₂) ∧ ∀ (τ : PropAssignment ν), eval τ φ₂ ≤ eval τ φ₁
Tactic:
aesop (add safe le_antisymm)
Proof state after:
no goals