internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.Model.PropFun.satisfies_map
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
φ : PropFun ν₁
f : ν₁ → ν₂
τ : PropAssignment ν₂
⊢ τ ⊨ map f φ ↔ PropAssignment.map f τ ⊨ φ
Tactic:
let ⟨ϕ,hϕ⟩ := φ.toTrunc.out
Proof state after:
ν₁ : Type u_1
ν₂ : Type u_2
φ : PropFun ν₁
f : ν₁ → ν₂
τ : PropAssignment ν₂
ϕ : PropForm ν₁
hϕ : ⟦ϕ⟧ = φ
⊢ τ ⊨ map f φ ↔ PropAssignment.map f τ ⊨ φ
Theorem: LeanSAT.Model.PropFun.satisfies_map
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
φ : PropFun ν₁
f : ν₁ → ν₂
τ : PropAssignment ν₂
ϕ : PropForm ν₁
hϕ : ⟦ϕ⟧ = φ
⊢ τ ⊨ map f φ ↔ PropAssignment.map f τ ⊨ φ
Tactic:
cases hϕ
Proof state after:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → ν₂
τ : PropAssignment ν₂
ϕ : PropForm ν₁
⊢ τ ⊨ map f ⟦ϕ⟧ ↔ PropAssignment.map f τ ⊨ ⟦ϕ⟧
Theorem: LeanSAT.Model.PropFun.satisfies_map
Proof state before:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → ν₂
τ : PropAssignment ν₂
ϕ : PropForm ν₁
⊢ τ ⊨ map f ⟦ϕ⟧ ↔ PropAssignment.map f τ ⊨ ⟦ϕ⟧
Tactic:
simp [map]
Proof state after:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → ν₂
τ : PropAssignment ν₂
ϕ : PropForm ν₁
⊢ τ ⊨ ⟦PropForm.map f ϕ⟧ ↔ PropAssignment.map f τ ⊨ ⟦ϕ⟧
Theorem: LeanSAT.Model.PropFun.satisfies_map
Proof state before:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → ν₂
τ : PropAssignment ν₂
ϕ : PropForm ν₁
⊢ τ ⊨ ⟦PropForm.map f ϕ⟧ ↔ PropAssignment.map f τ ⊨ ⟦ϕ⟧
Tactic:
rw [satisfies_mk, satisfies_mk]
Proof state after:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → ν₂
τ : PropAssignment ν₂
ϕ : PropForm ν₁
⊢ τ ⊨ PropForm.map f ϕ ↔ PropAssignment.map f τ ⊨ ϕ
Theorem: LeanSAT.Model.PropFun.satisfies_map
Proof state before:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → ν₂
τ : PropAssignment ν₂
ϕ : PropForm ν₁
⊢ τ ⊨ PropForm.map f ϕ ↔ PropAssignment.map f τ ⊨ ϕ
Tactic:
apply PropForm.satisfies_map
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.semVars_map
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
φ : PropFun ν₁
hf : Function.Injective f
⊢ semVars (map f φ) = Finset.map { toFun := f, inj' := hf } (semVars φ)
Tactic:
let ⟨ϕ,hϕ⟩ := φ.toTrunc.out
Proof state after:
ν₁ : Type u_1
ν₂ : Type u_2
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
φ : PropFun ν₁
hf : Function.Injective f
ϕ : PropForm ν₁
hϕ : ⟦ϕ⟧ = φ
⊢ semVars (map f φ) = Finset.map { toFun := f, inj' := hf } (semVars φ)
Theorem: LeanSAT.Model.PropFun.semVars_map
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
φ : PropFun ν₁
hf : Function.Injective f
ϕ : PropForm ν₁
hϕ : ⟦ϕ⟧ = φ
⊢ semVars (map f φ) = Finset.map { toFun := f, inj' := hf } (semVars φ)
Tactic:
cases hϕ
Proof state after:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
ϕ : PropForm ν₁
⊢ semVars (map f ⟦ϕ⟧) = Finset.map { toFun := f, inj' := hf } (semVars ⟦ϕ⟧)
Theorem: LeanSAT.Model.PropFun.semVars_map
Proof state before:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
ϕ : PropForm ν₁
⊢ semVars (map f ⟦ϕ⟧) = Finset.map { toFun := f, inj' := hf } (semVars ⟦ϕ⟧)
Tactic:
simp [map, *, PropForm.semVars_map]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.map_neg
Proof state before:
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
⊢ map f φᶜ = (map f φ)ᶜ
Tactic:
ext
Proof state after:
case a
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
τ✝ : PropAssignment ν₂
⊢ τ✝ ⊨ map f φᶜ ↔ τ✝ ⊨ (map f φ)ᶜ
Theorem: LeanSAT.Model.PropFun.map_neg
Proof state before:
case a
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
τ✝ : PropAssignment ν₂
⊢ τ✝ ⊨ map f φᶜ ↔ τ✝ ⊨ (map f φ)ᶜ
Tactic:
simp
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.map_conj
Proof state before:
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
⊢ map f (φ₁ ⊓ φ₂) = map f φ₁ ⊓ map f φ₂
Tactic:
ext
Proof state after:
case a
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
τ✝ : PropAssignment ν₂
⊢ τ✝ ⊨ map f (φ₁ ⊓ φ₂) ↔ τ✝ ⊨ map f φ₁ ⊓ map f φ₂
Theorem: LeanSAT.Model.PropFun.map_conj
Proof state before:
case a
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
τ✝ : PropAssignment ν₂
⊢ τ✝ ⊨ map f (φ₁ ⊓ φ₂) ↔ τ✝ ⊨ map f φ₁ ⊓ map f φ₂
Tactic:
simp
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.map_disj
Proof state before:
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
⊢ map f (φ₁ ⊔ φ₂) = map f φ₁ ⊔ map f φ₂
Tactic:
ext
Proof state after:
case a
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
τ✝ : PropAssignment ν₂
⊢ τ✝ ⊨ map f (φ₁ ⊔ φ₂) ↔ τ✝ ⊨ map f φ₁ ⊔ map f φ₂
Theorem: LeanSAT.Model.PropFun.map_disj
Proof state before:
case a
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
τ✝ : PropAssignment ν₂
⊢ τ✝ ⊨ map f (φ₁ ⊔ φ₂) ↔ τ✝ ⊨ map f φ₁ ⊔ map f φ₂
Tactic:
simp
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.map_impl
Proof state before:
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
⊢ map f (φ₁ ⇨ φ₂) = map f φ₁ ⇨ map f φ₂
Tactic:
ext
Proof state after:
case a
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
τ✝ : PropAssignment ν₂
⊢ τ✝ ⊨ map f (φ₁ ⇨ φ₂) ↔ τ✝ ⊨ map f φ₁ ⇨ map f φ₂
Theorem: LeanSAT.Model.PropFun.map_impl
Proof state before:
case a
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
τ✝ : PropAssignment ν₂
⊢ τ✝ ⊨ map f (φ₁ ⇨ φ₂) ↔ τ✝ ⊨ map f φ₁ ⇨ map f φ₂
Tactic:
simp
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.map_biImpl
Proof state before:
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
⊢ map f (biImpl φ₁ φ₂) = biImpl (map f φ₁) (map f φ₂)
Tactic:
ext
Proof state after:
case a
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
τ✝ : PropAssignment ν₂
⊢ τ✝ ⊨ map f (biImpl φ₁ φ₂) ↔ τ✝ ⊨ biImpl (map f φ₁) (map f φ₂)
Theorem: LeanSAT.Model.PropFun.map_biImpl
Proof state before:
case a
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
τ✝ : PropAssignment ν₂
⊢ τ✝ ⊨ map f (biImpl φ₁ φ₂) ↔ τ✝ ⊨ biImpl (map f φ₁) (map f φ₂)
Tactic:
simp
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.State.toPropFun_addClause
Proof state before:
L : Type ?u.1027
ν : Type u_1
inst✝ : LitVar L ν
C : Clause (Literal ν)
s : State ν
⊢ Cnf.toPropFun (addClause C s).cnf =
    Cnf.toPropFun s.cnf ⊓ PropFun.map s.vMap ((Clause.toPropFun s.assumeVars)ᶜ ⇨ Clause.toPropFun C)
Tactic:
simp [addClause, BooleanAlgebra.himp_eq, sup_comm]
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.LawfulState.semVars_toPropFun_cnf_lt
Proof state before:
ν : Type u_1
s : LawfulState ν
⊢ ∀ v ∈ PropFun.semVars (Cnf.toPropFun s.cnf), v < s.nextVar
Tactic:
intro v h
Proof state after:
ν : Type u_1
s : LawfulState ν
v : IVar
h : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
⊢ v < s.nextVar
Theorem: LeanSAT.Encode.EncCNF.LawfulState.semVars_toPropFun_cnf_lt
Proof state before:
ν : Type u_1
s : LawfulState ν
v : IVar
h : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
⊢ v < s.nextVar
Tactic:
replace h := Cnf.mem_semVars_toPropFun _ _ h
Proof state after:
ν : Type u_1
s : LawfulState ν
v : IVar
h : ∃ C ∈ s.cnf, v ∈ PropFun.semVars (Clause.toPropFun C)
⊢ v < s.nextVar
Theorem: LeanSAT.Encode.EncCNF.LawfulState.semVars_toPropFun_cnf_lt
Proof state before:
ν : Type u_1
s : LawfulState ν
v : IVar
h : ∃ C ∈ s.cnf, v ∈ PropFun.semVars (Clause.toPropFun C)
⊢ v < s.nextVar
Tactic:
rcases h with ⟨C,hC,h⟩
Proof state after:
case intro.intro
ν : Type u_1
s : LawfulState ν
v : IVar
C : Clause ILit
hC : C ∈ s.cnf
h : v ∈ PropFun.semVars (Clause.toPropFun C)
⊢ v < s.nextVar
Theorem: LeanSAT.Encode.EncCNF.LawfulState.semVars_toPropFun_cnf_lt
Proof state before:
case intro.intro
ν : Type u_1
s : LawfulState ν
v : IVar
C : Clause ILit
hC : C ∈ s.cnf
h : v ∈ PropFun.semVars (Clause.toPropFun C)
⊢ v < s.nextVar
Tactic:
replace h := Clause.mem_semVars_toPropFun _ _ h
Proof state after:
case intro.intro
ν : Type u_1
s : LawfulState ν
v : IVar
C : Clause ILit
hC : C ∈ s.cnf
h : ∃ l ∈ C, LitVar.toVar l = v
⊢ v < s.nextVar
Theorem: LeanSAT.Encode.EncCNF.LawfulState.semVars_toPropFun_cnf_lt
Proof state before:
case intro.intro
ν : Type u_1
s : LawfulState ν
v : IVar
C : Clause ILit
hC : C ∈ s.cnf
h : ∃ l ∈ C, LitVar.toVar l = v
⊢ v < s.nextVar
Tactic:
rcases h with ⟨l,hl,rfl⟩
Proof state after:
case intro.intro.intro.intro
ν : Type u_1
s : LawfulState ν
C : Clause ILit
hC : C ∈ s.cnf
l : ILit
hl : l ∈ C
⊢ LitVar.toVar l < s.nextVar
Theorem: LeanSAT.Encode.EncCNF.LawfulState.semVars_toPropFun_cnf_lt
Proof state before:
case intro.intro.intro.intro
ν : Type u_1
s : LawfulState ν
C : Clause ILit
hC : C ∈ s.cnf
l : ILit
hl : l ∈ C
⊢ LitVar.toVar l < s.nextVar
Tactic:
apply s.cnfVarsLt _ hC _ hl
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_new
Proof state before:
L : Type ?u.13015
ν : Type u_1
inst✝ : LitVar L ν
vars : ℕ+
f : ν ↪ IVar
h : ∀ (v : ν), f v < vars
⊢ interp (new vars f h) = fun x => True
Tactic:
ext τ
Proof state after:
case h.a
L : Type ?u.13015
ν : Type u_1
inst✝ : LitVar L ν
vars : ℕ+
f : ν ↪ IVar
h : ∀ (v : ν), f v < vars
τ : PropAssignment ν
⊢ interp (new vars f h) τ ↔ True
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_new
Proof state before:
case h.a
L : Type ?u.13015
ν : Type u_1
inst✝ : LitVar L ν
vars : ℕ+
f : ν ↪ IVar
h : ∀ (v : ν), f v < vars
τ : PropAssignment ν
⊢ interp (new vars f h) τ ↔ True
Tactic:
simp [new, State.new, interp, Cnf.toPropFun, PropAssignment.map_eq_map]
Proof state after:
case h.a
L : Type ?u.13015
ν : Type u_1
inst✝ : LitVar L ν
vars : ℕ+
f : ν ↪ IVar
h : ∀ (v : ν), f v < vars
τ : PropAssignment ν
⊢ ∃ σ, τ = PropAssignment.map (⇑f) σ
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_new
Proof state before:
case h.a
L : Type ?u.13015
ν : Type u_1
inst✝ : LitVar L ν
vars : ℕ+
f : ν ↪ IVar
h : ∀ (v : ν), f v < vars
τ : PropAssignment ν
⊢ ∃ σ, τ = PropAssignment.map (⇑f) σ
Tactic:
apply τ.exists_preimage
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_new'
Proof state before:
L : Type ?u.18246
ν : Type u_1
inst✝ : LitVar L ν
vars : ℕ
f : ν ↪ Fin vars
⊢ interp (new' vars f) = fun x => True
Tactic:
simp [new']
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_addClause
Proof 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 τ
Proof 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)
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_addClause
Proof 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]
Proof 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)
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_addClause
Proof 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]
Proof 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)
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_addClause
Proof 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
Proof 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)
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_addClause
Proof 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 σ
Proof 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)
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_addClause
Proof 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
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.State.cnf_withTemps
Proof state before:
ν : Type u_1
n : ℕ
s : State ν
⊢ (withTemps s).cnf = s.cnf
Tactic:
simp [State.withTemps]
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.LawfulState.vMap_withTemps
Proof state before:
ν : Type u_1
n : ℕ
s : LawfulState ν
⊢ (withTemps s).vMap = State.withTemps.vMap s.toState
Tactic:
simp [LawfulState.withTemps, State.withTemps]
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.LawfulState.assumeVars_withTemps
Proof state before:
ν : Type u_1
n : ℕ
s : LawfulState ν
⊢ (withTemps s).assumeVars = Clause.map (Literal (ν ⊕ Fin n)) Sum.inl s.assumeVars
Tactic:
simp [LawfulState.withTemps, State.withTemps]
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
ν : Type u_1
s : LawfulState ν
n : ℕ
⊢ interp (withTemps s) = fun τ => interp s (PropAssignment.map Sum.inl τ)
Tactic:
ext τ
Proof state after:
case h.a
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
⊢ interp (withTemps s) τ ↔ interp s (PropAssignment.map Sum.inl τ)
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.a
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
⊢ interp (withTemps s) τ ↔ interp s (PropAssignment.map Sum.inl τ)
Tactic:
simp [interp, withTemps, State.withTemps]
Proof state after:
case h.a
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
⊢ (∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf) ↔
    ∃ σ, PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ ∧ σ ⊨ Cnf.toPropFun s.cnf
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.a
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
⊢ (∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf) ↔
    ∃ σ, PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ ∧ σ ⊨ Cnf.toPropFun s.cnf
Tactic:
constructor
Proof state after:
case h.a.mp
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
⊢ (∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf) →
    ∃ σ, PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ ∧ σ ⊨ Cnf.toPropFun s.cnf

case h.a.mpr
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
⊢ (∃ σ, PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ ∧ σ ⊨ Cnf.toPropFun s.cnf) →
    ∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.a.mp
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
⊢ (∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf) →
    ∃ σ, PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ ∧ σ ⊨ Cnf.toPropFun s.cnf
Tactic:
rintro ⟨σ,rfl,h⟩
Proof state after:
case h.a.mp.intro.intro
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h : σ ⊨ Cnf.toPropFun s.cnf
⊢ ∃ σ_1,
    PropAssignment.map Sum.inl (PropAssignment.map (State.withTemps.vMap s.toState) σ) = PropAssignment.map s.vMap σ_1 ∧
      σ_1 ⊨ Cnf.toPropFun s.cnf
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.a.mp.intro.intro
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h : σ ⊨ Cnf.toPropFun s.cnf
⊢ ∃ σ_1,
    PropAssignment.map Sum.inl (PropAssignment.map (State.withTemps.vMap s.toState) σ) = PropAssignment.map s.vMap σ_1 ∧
      σ_1 ⊨ Cnf.toPropFun s.cnf
Tactic:
use σ
Proof state after:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h : σ ⊨ Cnf.toPropFun s.cnf
⊢ PropAssignment.map Sum.inl (PropAssignment.map (State.withTemps.vMap s.toState) σ) = PropAssignment.map s.vMap σ ∧
    σ ⊨ Cnf.toPropFun s.cnf
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h : σ ⊨ Cnf.toPropFun s.cnf
⊢ PropAssignment.map Sum.inl (PropAssignment.map (State.withTemps.vMap s.toState) σ) = PropAssignment.map s.vMap σ ∧
    σ ⊨ Cnf.toPropFun s.cnf
Tactic:
simp [h]
Proof state after:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h : σ ⊨ Cnf.toPropFun s.cnf
⊢ PropAssignment.map Sum.inl (PropAssignment.map (State.withTemps.vMap s.toState) σ) = PropAssignment.map s.vMap σ
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h : σ ⊨ Cnf.toPropFun s.cnf
⊢ PropAssignment.map Sum.inl (PropAssignment.map (State.withTemps.vMap s.toState) σ) = PropAssignment.map s.vMap σ
Tactic:
ext v
Proof state after:
case h.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h : σ ⊨ Cnf.toPropFun s.cnf
v : ν
⊢ PropAssignment.map Sum.inl (PropAssignment.map (State.withTemps.vMap s.toState) σ) v = PropAssignment.map s.vMap σ v
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h : σ ⊨ Cnf.toPropFun s.cnf
v : ν
⊢ PropAssignment.map Sum.inl (PropAssignment.map (State.withTemps.vMap s.toState) σ) v = PropAssignment.map s.vMap σ v
Tactic:
simp [State.withTemps.vMap]
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.a.mpr
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
⊢ (∃ σ, PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ ∧ σ ⊨ Cnf.toPropFun s.cnf) →
    ∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf
Tactic:
rintro ⟨σ,h1,h2⟩
Proof state after:
case h.a.mpr.intro.intro
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
σ : PropAssignment IVar
h1 : PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ
h2 : σ ⊨ Cnf.toPropFun s.cnf
⊢ ∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.a.mpr.intro.intro
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
σ : PropAssignment IVar
h1 : PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ
h2 : σ ⊨ Cnf.toPropFun s.cnf
⊢ ∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf
Tactic:
have ⟨σ',hσ'⟩ := τ.exists_preimage ⟨State.withTemps.vMap s.toState, (LawfulState.withTemps s).vMapInj⟩
Proof state after:
case h.a.mpr.intro.intro
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
σ : PropAssignment IVar
h1 : PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
hσ' : τ = PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ'
⊢ ∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.a.mpr.intro.intro
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
σ : PropAssignment IVar
h1 : PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
hσ' : τ = PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ'
⊢ ∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf
Tactic:
cases hσ'
Proof state after:
case h.a.mpr.intro.intro.refl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ ∃ σ,
    PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ' =
        PropAssignment.map (State.withTemps.vMap s.toState) σ ∧
      σ ⊨ Cnf.toPropFun s.cnf