internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h
ν : 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 σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : v < s.nextVar
⊢ v ∉ Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ
Tactic:
simp [State.withTemps.vMap]
Proof state after:
case h
ν : 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 σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : v < s.nextVar
⊢ ∀ (x : Fin n), ¬{ val := ↑s.nextVar + ↑x, property := ⋯ } = v
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h
ν : 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 σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : v < s.nextVar
⊢ ∀ (x : Fin n), ¬{ val := ↑s.nextVar + ↑x, property := ⋯ } = v
Tactic:
intro v'
Proof state after:
case h
ν : 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 σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : v < s.nextVar
v' : Fin n
⊢ ¬{ val := ↑s.nextVar + ↑v', property := ⋯ } = v
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h
ν : 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 σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : v < s.nextVar
v' : Fin n
⊢ ¬{ val := ↑s.nextVar + ↑v', property := ⋯ } = v
Tactic:
rw [←Subtype.val_inj]
Proof state after:
case h
ν : 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 σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : v < s.nextVar
v' : Fin n
⊢ ¬↑{ val := ↑s.nextVar + ↑v', property := ⋯ } = ↑v
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h
ν : 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 σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : v < s.nextVar
v' : Fin n
⊢ ¬↑{ val := ↑s.nextVar + ↑v', property := ⋯ } = ↑v
Tactic:
rw [← PNat.coe_lt_coe] at this
Proof state after:
case h
ν : 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 σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : ↑v < ↑s.nextVar
v' : Fin n
⊢ ¬↑{ val := ↑s.nextVar + ↑v', property := ⋯ } = ↑v
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h
ν : 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 σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : ↑v < ↑s.nextVar
v' : Fin n
⊢ ¬↑{ val := ↑s.nextVar + ↑v', property := ⋯ } = ↑v
Tactic:
simp
Proof state after:
case h
ν : 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 σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : ↑v < ↑s.nextVar
v' : Fin n
⊢ ¬↑s.nextVar + ↑v' = ↑v
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h
ν : 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 σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : ↑v < ↑s.nextVar
v' : Fin n
⊢ ¬↑s.nextVar + ↑v' = ↑v
Tactic:
apply Nat.ne_of_gt
Proof state after:
case h.h
ν : 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 σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : ↑v < ↑s.nextVar
v' : Fin n
⊢ ↑v < ↑s.nextVar + ↑v'
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withTemps
Proof state before:
case h.h
ν : 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 σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : ↑v < ↑s.nextVar
v' : Fin n
⊢ ↑v < ↑s.nextVar + ↑v'
Tactic:
exact Nat.lt_add_right _ this
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.State.vMap_withoutTemps
Proof state before:
ν : Type u_1
n : ℕ
vm : ν → IVar
av : Array (Literal ν)
s : State (ν ⊕ Fin n)
⊢ (withoutTemps vm av s).vMap = vm
Tactic:
simp [State.withoutTemps]
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.State.assumeVars_withoutTemps
Proof state before:
ν : Type u_1
n : ℕ
vm : ν → IVar
av : Array (Literal ν)
s : State (ν ⊕ Fin n)
⊢ (withoutTemps vm av s).assumeVars = av
Tactic:
simp [State.withoutTemps]
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.LawfulState.vMap_withoutTemps
Proof state before:
ν : Type u_1
n : ℕ
av : Array (Literal ν)
s : LawfulState (ν ⊕ Fin n)
vMap : ν → IVar
vMapLt : ∀ (v : ν), vMap v < s.nextVar
vMapInj : Function.Injective vMap
⊢ (withoutTemps s vMap vMapLt vMapInj av).vMap = vMap
Tactic:
simp [LawfulState.withoutTemps]
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.LawfulState.assumeVars_withoutTemps
Proof state before:
ν : Type u_1
n : ℕ
av : Array (Literal ν)
s : LawfulState (ν ⊕ Fin n)
vMap : ν → IVar
vMapLt : ∀ (v : ν), vMap v < s.nextVar
vMapInj : Function.Injective vMap
⊢ (withoutTemps s vMap vMapLt vMapInj av).assumeVars = av
Tactic:
simp [LawfulState.withoutTemps]
Proof state after:
no goals
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withoutTemps
Proof state before:
ν : Type u_1
n : ℕ
av : Array (Literal ν)
s : LawfulState (ν ⊕ Fin n)
vMap : ν → IVar
vMapLt : ∀ (v : ν), vMap v < s.nextVar
vMapInj : Function.Injective vMap
h : vMap = s.vMap ∘ Sum.inl
⊢ interp (withoutTemps s vMap vMapLt vMapInj av) = fun τ => ∃ σ, τ = PropAssignment.map Sum.inl σ ∧ interp s σ
Tactic:
ext τ
Proof state after:
case h.a
ν : Type u_1
n : ℕ
av : Array (Literal ν)
s : LawfulState (ν ⊕ Fin n)
vMap : ν → IVar
vMapLt : ∀ (v : ν), vMap v < s.nextVar
vMapInj : Function.Injective vMap
h : vMap = s.vMap ∘ Sum.inl
τ : PropAssignment ν
⊢ interp (withoutTemps s vMap vMapLt vMapInj av) τ ↔ ∃ σ, τ = PropAssignment.map Sum.inl σ ∧ interp s σ
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withoutTemps
Proof state before:
case h.a
ν : Type u_1
n : ℕ
av : Array (Literal ν)
s : LawfulState (ν ⊕ Fin n)
vMap : ν → IVar
vMapLt : ∀ (v : ν), vMap v < s.nextVar
vMapInj : Function.Injective vMap
h : vMap = s.vMap ∘ Sum.inl
τ : PropAssignment ν
⊢ interp (withoutTemps s vMap vMapLt vMapInj av) τ ↔ ∃ σ, τ = PropAssignment.map Sum.inl σ ∧ interp s σ
Tactic:
cases h
Proof state after:
case h.a.refl
ν : Type u_1
n : ℕ
av : Array (Literal ν)
s : LawfulState (ν ⊕ Fin n)
τ : PropAssignment ν
vMapLt : ∀ (v : ν), (s.vMap ∘ Sum.inl) v < s.nextVar
vMapInj : Function.Injective (s.vMap ∘ Sum.inl)
⊢ interp (withoutTemps s (s.vMap ∘ Sum.inl) vMapLt vMapInj av) τ ↔ ∃ σ, τ = PropAssignment.map Sum.inl σ ∧ interp s σ
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withoutTemps
Proof state before:
case h.a.refl
ν : Type u_1
n : ℕ
av : Array (Literal ν)
s : LawfulState (ν ⊕ Fin n)
τ : PropAssignment ν
vMapLt : ∀ (v : ν), (s.vMap ∘ Sum.inl) v < s.nextVar
vMapInj : Function.Injective (s.vMap ∘ Sum.inl)
⊢ interp (withoutTemps s (s.vMap ∘ Sum.inl) vMapLt vMapInj av) τ ↔ ∃ σ, τ = PropAssignment.map Sum.inl σ ∧ interp s σ
Tactic:
simp [LawfulState.withoutTemps, State.withoutTemps, interp]
Proof state after:
case h.a.refl
ν : Type u_1
n : ℕ
av : Array (Literal ν)
s : LawfulState (ν ⊕ Fin n)
τ : PropAssignment ν
vMapLt : ∀ (v : ν), (s.vMap ∘ Sum.inl) v < s.nextVar
vMapInj : Function.Injective (s.vMap ∘ Sum.inl)
⊢ (∃ σ, τ = PropAssignment.map (s.vMap ∘ Sum.inl) σ ∧ σ ⊨ Cnf.toPropFun s.cnf) ↔
    ∃ σ, τ = PropAssignment.map Sum.inl σ ∧ ∃ σ_1, σ = PropAssignment.map s.vMap σ_1 ∧ σ_1 ⊨ Cnf.toPropFun s.cnf
Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_withoutTemps
Proof state before:
case h.a.refl
ν : Type u_1
n : ℕ
av : Array (Literal ν)
s : LawfulState (ν ⊕ Fin n)
τ : PropAssignment ν
vMapLt : ∀ (v : ν), (s.vMap ∘ Sum.inl) v < s.nextVar
vMapInj : Function.Injective (s.vMap ∘ Sum.inl)
⊢ (∃ σ, τ = PropAssignment.map (s.vMap ∘ Sum.inl) σ ∧ σ ⊨ Cnf.toPropFun s.cnf) ↔
    ∃ σ, τ = PropAssignment.map Sum.inl σ ∧ ∃ σ_1, σ = PropAssignment.map s.vMap σ_1 ∧ σ_1 ⊨ Cnf.toPropFun s.cnf
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropPred.satisfies_def
Proof state before:
ν : Type u_1
τ : PropAssignment ν
f : PropPred ν
⊢ τ ⊨ f ↔ f τ
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanSAT.Model.PropAssignment.set_get
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x : ν
v : Bool
⊢ set τ x v x = v
Tactic:
simp [set]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropAssignment.set_get_of_ne
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
x y : ν
τ : PropAssignment ν
v : Bool
⊢ x ≠ y → set τ x v y = τ y
Tactic:
intro h
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
x y : ν
τ : PropAssignment ν
v : Bool
h : x ≠ y
⊢ set τ x v y = τ y
Theorem: LeanSAT.Model.PropAssignment.set_get_of_ne
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
x y : ν
τ : PropAssignment ν
v : Bool
h : x ≠ y
⊢ set τ x v y = τ y
Tactic:
simp [set, h.symm]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropAssignment.set_set
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x : ν
v v' : Bool
⊢ set (set τ x v) x v' = set τ x v'
Tactic:
ext x'
Proof state after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x : ν
v v' : Bool
x' : ν
⊢ set (set τ x v) x v' x' = set τ x v' x'
Theorem: LeanSAT.Model.PropAssignment.set_set
Proof state before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x : ν
v v' : Bool
x' : ν
⊢ set (set τ x v) x v' x' = set τ x v' x'
Tactic:
dsimp [set]
Proof state after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x : ν
v v' : Bool
x' : ν
⊢ (if x' = x then v' else if x' = x then v else τ x') = if x' = x then v' else τ x'
Theorem: LeanSAT.Model.PropAssignment.set_set
Proof state before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x : ν
v v' : Bool
x' : ν
⊢ (if x' = x then v' else if x' = x then v else τ x') = if x' = x then v' else τ x'
Tactic:
split <;> simp_all
Proof state after:
no goals
Theorem: LeanSAT.Model.PropAssignment.set_same
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x : ν
⊢ set τ x (τ x) = τ
Tactic:
ext x'
Proof state after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x x' : ν
⊢ set τ x (τ x) x' = τ x'
Theorem: LeanSAT.Model.PropAssignment.set_same
Proof state before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x x' : ν
⊢ set τ x (τ x) x' = τ x'
Tactic:
dsimp [set]
Proof state after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x x' : ν
⊢ (if x' = x then τ x else τ x') = τ x'
Theorem: LeanSAT.Model.PropAssignment.set_same
Proof state before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x x' : ν
⊢ (if x' = x then τ x else τ x') = τ x'
Tactic:
split <;> simp_all
Proof state after:
no goals
Theorem: LeanSAT.Model.PropAssignment.set_comm
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x₁ : ν
b₁ : Bool
x₂ : ν
b₂ : Bool
h : x₁ ≠ x₂
⊢ set (set τ x₂ b₂) x₁ b₁ = set (set τ x₁ b₁) x₂ b₂
Tactic:
ext v
Proof state after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x₁ : ν
b₁ : Bool
x₂ : ν
b₂ : Bool
h : x₁ ≠ x₂
v : ν
⊢ set (set τ x₂ b₂) x₁ b₁ v = set (set τ x₁ b₁) x₂ b₂ v
Theorem: LeanSAT.Model.PropAssignment.set_comm
Proof state before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x₁ : ν
b₁ : Bool
x₂ : ν
b₂ : Bool
h : x₁ ≠ x₂
v : ν
⊢ set (set τ x₂ b₂) x₁ b₁ v = set (set τ x₁ b₁) x₂ b₂ v
Tactic:
simp [set]
Proof state after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x₁ : ν
b₁ : Bool
x₂ : ν
b₂ : Bool
h : x₁ ≠ x₂
v : ν
⊢ (if v = x₁ then b₁ else if v = x₂ then b₂ else τ v) = if v = x₂ then b₂ else if v = x₁ then b₁ else τ v
Theorem: LeanSAT.Model.PropAssignment.set_comm
Proof state before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x₁ : ν
b₁ : Bool
x₂ : ν
b₂ : Bool
h : x₁ ≠ x₂
v : ν
⊢ (if v = x₁ then b₁ else if v = x₂ then b₂ else τ v) = if v = x₂ then b₂ else if v = x₁ then b₁ else τ v
Tactic:
split <;> split <;> (subst_vars; simp at *)
Proof state after:
no goals
Theorem: LeanSAT.Model.PropAssignment.set_comm
Proof state before:
case h.inr.inl
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x₁ : ν
b₁ : Bool
x₂ : ν
b₂ : Bool
h : x₁ ≠ x₂
v : ν
h✝¹ : ¬v = x₁
h✝ : v = x₂
⊢ b₂ = b₂
Tactic:
subst_vars
Proof state after:
case h.inr.inl
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x₁ : ν
b₁ b₂ : Bool
v : ν
h✝ : ¬v = x₁
h : x₁ ≠ v
⊢ b₂ = b₂
Theorem: LeanSAT.Model.PropAssignment.set_comm
Proof state before:
case h.inr.inr
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x₁ : ν
b₁ : Bool
x₂ : ν
b₂ : Bool
h : x₁ ≠ x₂
v : ν
h✝¹ : ¬v = x₁
h✝ : ¬v = x₂
⊢ τ v = τ v
Tactic:
simp at *
Proof state after:
no goals
Theorem: LeanSAT.Model.PropAssignment.setMany_mem
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
v : ν
xs : Finset ν
τ' : PropAssignment ν
h : v ∈ xs
⊢ setMany τ xs τ' v = τ' v
Tactic:
simp [setMany, h]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropAssignment.setMany_not_mem
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
v : ν
xs : Finset ν
τ' : PropAssignment ν
h : v ∉ xs
⊢ setMany τ xs τ' v = τ v
Tactic:
simp [setMany, h]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropAssignment.setMany_same
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
⊢ setMany τ xs τ = τ
Tactic:
ext v
Proof state after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
v : ν
⊢ setMany τ xs τ v = τ v
Theorem: LeanSAT.Model.PropAssignment.setMany_same
Proof state before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
v : ν
⊢ setMany τ xs τ v = τ v
Tactic:
simp [setMany]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropAssignment.setMany_setMany
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs₁ : Finset ν
τ₁ : PropAssignment ν
xs₂ : Finset ν
τ₂ : PropAssignment ν
⊢ setMany (setMany τ xs₁ τ₁) xs₂ τ₂ = setMany τ (xs₁ ∪ xs₂) (setMany τ₁ xs₂ τ₂)
Tactic:
ext v
Proof state after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs₁ : Finset ν
τ₁ : PropAssignment ν
xs₂ : Finset ν
τ₂ : PropAssignment ν
v : ν
⊢ setMany (setMany τ xs₁ τ₁) xs₂ τ₂ v = setMany τ (xs₁ ∪ xs₂) (setMany τ₁ xs₂ τ₂) v
Theorem: LeanSAT.Model.PropAssignment.setMany_setMany
Proof state before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs₁ : Finset ν
τ₁ : PropAssignment ν
xs₂ : Finset ν
τ₂ : PropAssignment ν
v : ν
⊢ setMany (setMany τ xs₁ τ₁) xs₂ τ₂ v = setMany τ (xs₁ ∪ xs₂) (setMany τ₁ xs₂ τ₂) v
Tactic:
simp [setMany]
Proof state after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs₁ : Finset ν
τ₁ : PropAssignment ν
xs₂ : Finset ν
τ₂ : PropAssignment ν
v : ν
⊢ (if v ∈ xs₂ then τ₂ v else if v ∈ xs₁ then τ₁ v else τ v) =
    if v ∈ xs₁ ∨ v ∈ xs₂ then if v ∈ xs₂ then τ₂ v else τ₁ v else τ v
Theorem: LeanSAT.Model.PropAssignment.setMany_setMany
Proof state before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs₁ : Finset ν
τ₁ : PropAssignment ν
xs₂ : Finset ν
τ₂ : PropAssignment ν
v : ν
⊢ (if v ∈ xs₂ then τ₂ v else if v ∈ xs₁ then τ₁ v else τ v) =
    if v ∈ xs₁ ∨ v ∈ xs₂ then if v ∈ xs₂ then τ₂ v else τ₁ v else τ v
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropAssignment.setMany_union
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs₁ xs₂ : Finset ν
τ' : PropAssignment ν
⊢ setMany τ (xs₁ ∪ xs₂) τ' = setMany (setMany τ xs₁ τ') xs₂ τ'
Tactic:
ext v
Proof state after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs₁ xs₂ : Finset ν
τ' : PropAssignment ν
v : ν
⊢ setMany τ (xs₁ ∪ xs₂) τ' v = setMany (setMany τ xs₁ τ') xs₂ τ' v
Theorem: LeanSAT.Model.PropAssignment.setMany_union
Proof state before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs₁ xs₂ : Finset ν
τ' : PropAssignment ν
v : ν
⊢ setMany τ (xs₁ ∪ xs₂) τ' v = setMany (setMany τ xs₁ τ') xs₂ τ' v
Tactic:
simp [setMany]
Proof state after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs₁ xs₂ : Finset ν
τ' : PropAssignment ν
v : ν
⊢ (if v ∈ xs₁ ∨ v ∈ xs₂ then τ' v else τ v) = if v ∈ xs₂ then τ' v else if v ∈ xs₁ then τ' v else τ v
Theorem: LeanSAT.Model.PropAssignment.setMany_union
Proof state before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs₁ xs₂ : Finset ν
τ' : PropAssignment ν
v : ν
⊢ (if v ∈ xs₁ ∨ v ∈ xs₂ then τ' v else τ v) = if v ∈ xs₂ then τ' v else if v ∈ xs₁ then τ' v else τ v
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropAssignment.setMany_singleton
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
v : ν
τ' : PropAssignment ν
⊢ setMany τ {v} τ' = set τ v (τ' v)
Tactic:
ext v
Proof state after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
v✝ : ν
τ' : PropAssignment ν
v : ν
⊢ setMany τ {v✝} τ' v = set τ v✝ (τ' v✝) v
Theorem: LeanSAT.Model.PropAssignment.setMany_singleton
Proof state before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
v✝ : ν
τ' : PropAssignment ν
v : ν
⊢ setMany τ {v✝} τ' v = set τ v✝ (τ' v✝) v
Tactic:
simp [setMany, set]
Proof state after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
v✝ : ν
τ' : PropAssignment ν
v : ν
⊢ (if v = v✝ then τ' v else τ v) = if v = v✝ then τ' v✝ else τ v
Theorem: LeanSAT.Model.PropAssignment.setMany_singleton
Proof state before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
v✝ : ν
τ' : PropAssignment ν
v : ν
⊢ (if v = v✝ then τ' v else τ v) = if v = v✝ then τ' v✝ else τ v
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropAssignment.set_setMany_comm
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
v : ν
b : Bool
h : v ∉ xs
⊢ set (setMany τ xs τ') v b = setMany (set τ v b) xs τ'
Tactic:
ext v
Proof state after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
v✝ : ν
b : Bool
h : v✝ ∉ xs
v : ν
⊢ set (setMany τ xs τ') v✝ b v = setMany (set τ v✝ b) xs τ' v
Theorem: LeanSAT.Model.PropAssignment.set_setMany_comm
Proof state before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
v✝ : ν
b : Bool
h : v✝ ∉ xs
v : ν
⊢ set (setMany τ xs τ') v✝ b v = setMany (set τ v✝ b) xs τ' v
Tactic:
simp [setMany, set]
Proof state after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
v✝ : ν
b : Bool
h : v✝ ∉ xs
v : ν
⊢ (if v = v✝ then b else if v ∈ xs then τ' v else τ v) = if v ∈ xs then τ' v else if v = v✝ then b else τ v
Theorem: LeanSAT.Model.PropAssignment.set_setMany_comm
Proof state before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
v✝ : ν
b : Bool
h : v✝ ∉ xs
v : ν
⊢ (if v = v✝ then b else if v ∈ xs then τ' v else τ v) = if v ∈ xs then τ' v else if v = v✝ then b else τ v
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropAssignment.agreeOn_set_of_not_mem
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x : ν
X : Set ν
σ : PropAssignment ν
v : Bool
⊢ x ∉ X → agreeOn X (set σ x v) σ
Tactic:
aesop (add norm unfold agreeOn, norm unfold set)
Proof state after:
no goals
Theorem: LeanSAT.Model.PropAssignment.agreeOn_setMany
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
⊢ agreeOn (↑xs) (setMany τ xs τ') τ'
Tactic:
intro v hv
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
v : ν
hv : v ∈ ↑xs
⊢ setMany τ xs τ' v = τ' v
Theorem: LeanSAT.Model.PropAssignment.agreeOn_setMany
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
v : ν
hv : v ∈ ↑xs
⊢ setMany τ xs τ' v = τ' v
Tactic:
simp at hv
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
v : ν
hv : v ∈ xs
⊢ setMany τ xs τ' v = τ' v
Theorem: LeanSAT.Model.PropAssignment.agreeOn_setMany
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
τ' : PropAssignment ν
v : ν
hv : v ∈ xs
⊢ setMany τ xs τ' v = τ' v
Tactic:
simp [setMany, hv]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropAssignment.agreeOn_setMany_of_disjoint
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Set ν
xs' : Finset ν
τ' : PropAssignment ν
h : Disjoint xs ↑xs'
⊢ agreeOn xs (setMany τ xs' τ') τ
Tactic:
intro v hv
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Set ν
xs' : Finset ν
τ' : PropAssignment ν
h : Disjoint xs ↑xs'
v : ν
hv : v ∈ xs
⊢ setMany τ xs' τ' v = τ v
Theorem: LeanSAT.Model.PropAssignment.agreeOn_setMany_of_disjoint
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Set ν
xs' : Finset ν
τ' : PropAssignment ν
h : Disjoint xs ↑xs'
v : ν
hv : v ∈ xs
⊢ setMany τ xs' τ' v = τ v
Tactic:
simp [setMany]
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Set ν
xs' : Finset ν
τ' : PropAssignment ν
h : Disjoint xs ↑xs'
v : ν
hv : v ∈ xs
⊢ v ∈ xs' → τ' v = τ v
Theorem: LeanSAT.Model.PropAssignment.agreeOn_setMany_of_disjoint
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Set ν
xs' : Finset ν
τ' : PropAssignment ν
h : Disjoint xs ↑xs'
v : ν
hv : v ∈ xs
⊢ v ∈ xs' → τ' v = τ v
Tactic:
intro hv'
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Set ν
xs' : Finset ν
τ' : PropAssignment ν
h : Disjoint xs ↑xs'
v : ν
hv : v ∈ xs
hv' : v ∈ xs'
⊢ τ' v = τ v