internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.Model.PropForm.vars_substOne
Proof state before:
case biImpl.inl
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ₁ φ₂ : PropForm ν
ih₁ : vars (substOne φ₁ v✝ ψ) ⊆ vars φ₁ \ {v✝} ∪ vars ψ
ih₂ : vars (substOne φ₂ v✝ ψ) ⊆ vars φ₂ \ {v✝} ∪ vars ψ
v : ν
h✝ : v ∈ vars (subst φ₁ fun v' => if v' = v✝ then ψ else var v')
this : v ∈ vars φ₁ \ {v✝} ∪ vars ψ
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ
Tactic:
simp at this
Proof state after:
case biImpl.inl
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ₁ φ₂ : PropForm ν
ih₁ : vars (substOne φ₁ v✝ ψ) ⊆ vars φ₁ \ {v✝} ∪ vars ψ
ih₂ : vars (substOne φ₂ v✝ ψ) ⊆ vars φ₂ \ {v✝} ∪ vars ψ
v : ν
h✝ : v ∈ vars (subst φ₁ fun v' => if v' = v✝ then ψ else var v')
this : v ∈ vars φ₁ ∧ ¬v = v✝ ∨ v ∈ vars ψ
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ
Theorem: LeanSAT.Model.PropForm.vars_substOne
Proof state before:
case biImpl.inl
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ₁ φ₂ : PropForm ν
ih₁ : vars (substOne φ₁ v✝ ψ) ⊆ vars φ₁ \ {v✝} ∪ vars ψ
ih₂ : vars (substOne φ₂ v✝ ψ) ⊆ vars φ₂ \ {v✝} ∪ vars ψ
v : ν
h✝ : v ∈ vars (subst φ₁ fun v' => if v' = v✝ then ψ else var v')
this : v ∈ vars φ₁ ∧ ¬v = v✝ ∨ v ∈ vars ψ
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ
Tactic:
rcases this with ⟨a,b⟩|c <;> simp [*]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.vars_substOne
Proof state before:
case biImpl.inr
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ₁ φ₂ : PropForm ν
ih₁ : vars (substOne φ₁ v✝ ψ) ⊆ vars φ₁ \ {v✝} ∪ vars ψ
ih₂ : vars (substOne φ₂ v✝ ψ) ⊆ vars φ₂ \ {v✝} ∪ vars ψ
v : ν
h✝ : v ∈ vars (subst φ₂ fun v' => if v' = v✝ then ψ else var v')
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ
Tactic:
have := ih₂ ‹_›
Proof state after:
case biImpl.inr
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ₁ φ₂ : PropForm ν
ih₁ : vars (substOne φ₁ v✝ ψ) ⊆ vars φ₁ \ {v✝} ∪ vars ψ
ih₂ : vars (substOne φ₂ v✝ ψ) ⊆ vars φ₂ \ {v✝} ∪ vars ψ
v : ν
h✝ : v ∈ vars (subst φ₂ fun v' => if v' = v✝ then ψ else var v')
this : v ∈ vars φ₂ \ {v✝} ∪ vars ψ
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ
Theorem: LeanSAT.Model.PropForm.vars_substOne
Proof state before:
case biImpl.inr
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ₁ φ₂ : PropForm ν
ih₁ : vars (substOne φ₁ v✝ ψ) ⊆ vars φ₁ \ {v✝} ∪ vars ψ
ih₂ : vars (substOne φ₂ v✝ ψ) ⊆ vars φ₂ \ {v✝} ∪ vars ψ
v : ν
h✝ : v ∈ vars (subst φ₂ fun v' => if v' = v✝ then ψ else var v')
this : v ∈ vars φ₂ \ {v✝} ∪ vars ψ
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ
Tactic:
simp at this
Proof state after:
case biImpl.inr
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ₁ φ₂ : PropForm ν
ih₁ : vars (substOne φ₁ v✝ ψ) ⊆ vars φ₁ \ {v✝} ∪ vars ψ
ih₂ : vars (substOne φ₂ v✝ ψ) ⊆ vars φ₂ \ {v✝} ∪ vars ψ
v : ν
h✝ : v ∈ vars (subst φ₂ fun v' => if v' = v✝ then ψ else var v')
this : v ∈ vars φ₂ ∧ ¬v = v✝ ∨ v ∈ vars ψ
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ
Theorem: LeanSAT.Model.PropForm.vars_substOne
Proof state before:
case biImpl.inr
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ₁ φ₂ : PropForm ν
ih₁ : vars (substOne φ₁ v✝ ψ) ⊆ vars φ₁ \ {v✝} ∪ vars ψ
ih₂ : vars (substOne φ₂ v✝ ψ) ⊆ vars φ₂ \ {v✝} ∪ vars ψ
v : ν
h✝ : v ∈ vars (subst φ₂ fun v' => if v' = v✝ then ψ else var v')
this : v ∈ vars φ₂ ∧ ¬v = v✝ ∨ v ∈ vars ψ
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ
Tactic:
rcases this with ⟨a,b⟩|c <;> simp [*]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.substL_disj
Proof state before:
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
⊢ substL (φ₁ ⊔ φ₂) f = substL φ₁ f ⊔ substL φ₂ f
Tactic:
have ⟨φ₁, hφ₁⟩ := φ₁.exists_rep
Proof state after:
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₁✝ φ₂ : PropFun ν₁
v : ν₁
φ₁ : PropForm ν₁
hφ₁ : ⟦φ₁⟧ = φ₁✝
⊢ substL (φ₁✝ ⊔ φ₂) f = substL φ₁✝ f ⊔ substL φ₂ f
Theorem: LeanSAT.Model.PropFun.substL_disj
Proof state before:
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₁✝ φ₂ : PropFun ν₁
v : ν₁
φ₁ : PropForm ν₁
hφ₁ : ⟦φ₁⟧ = φ₁✝
⊢ substL (φ₁✝ ⊔ φ₂) f = substL φ₁✝ f ⊔ substL φ₂ f
Tactic:
cases hφ₁
Proof state after:
case refl
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₂ : PropFun ν₁
v : ν₁
φ₁ : PropForm ν₁
⊢ substL (⟦φ₁⟧ ⊔ φ₂) f = substL ⟦φ₁⟧ f ⊔ substL φ₂ f
Theorem: LeanSAT.Model.PropFun.substL_disj
Proof state before:
case refl
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₂ : PropFun ν₁
v : ν₁
φ₁ : PropForm ν₁
⊢ substL (⟦φ₁⟧ ⊔ φ₂) f = substL ⟦φ₁⟧ f ⊔ substL φ₂ f
Tactic:
have ⟨φ₂, hφ₂⟩ := φ₂.exists_rep
Proof state after:
case refl
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₂✝ : PropFun ν₁
v : ν₁
φ₁ φ₂ : PropForm ν₁
hφ₂ : ⟦φ₂⟧ = φ₂✝
⊢ substL (⟦φ₁⟧ ⊔ φ₂✝) f = substL ⟦φ₁⟧ f ⊔ substL φ₂✝ f
Theorem: LeanSAT.Model.PropFun.substL_disj
Proof state before:
case refl
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₂✝ : PropFun ν₁
v : ν₁
φ₁ φ₂ : PropForm ν₁
hφ₂ : ⟦φ₂⟧ = φ₂✝
⊢ substL (⟦φ₁⟧ ⊔ φ₂✝) f = substL ⟦φ₁⟧ f ⊔ substL φ₂✝ f
Tactic:
cases hφ₂
Proof state after:
case refl.refl
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
v : ν₁
φ₁ φ₂ : PropForm ν₁
⊢ substL (⟦φ₁⟧ ⊔ ⟦φ₂⟧) f = substL ⟦φ₁⟧ f ⊔ substL ⟦φ₂⟧ f
Theorem: LeanSAT.Model.PropFun.substL_disj
Proof state before:
case refl.refl
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
v : ν₁
φ₁ φ₂ : PropForm ν₁
⊢ substL (⟦φ₁⟧ ⊔ ⟦φ₂⟧) f = substL ⟦φ₁⟧ f ⊔ substL ⟦φ₂⟧ f
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.substL_conj
Proof state before:
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
⊢ substL (φ₁ ⊓ φ₂) f = substL φ₁ f ⊓ substL φ₂ f
Tactic:
have ⟨φ₁, hφ₁⟩ := φ₁.exists_rep
Proof state after:
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₁✝ φ₂ : PropFun ν₁
v : ν₁
φ₁ : PropForm ν₁
hφ₁ : ⟦φ₁⟧ = φ₁✝
⊢ substL (φ₁✝ ⊓ φ₂) f = substL φ₁✝ f ⊓ substL φ₂ f
Theorem: LeanSAT.Model.PropFun.substL_conj
Proof state before:
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₁✝ φ₂ : PropFun ν₁
v : ν₁
φ₁ : PropForm ν₁
hφ₁ : ⟦φ₁⟧ = φ₁✝
⊢ substL (φ₁✝ ⊓ φ₂) f = substL φ₁✝ f ⊓ substL φ₂ f
Tactic:
cases hφ₁
Proof state after:
case refl
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₂ : PropFun ν₁
v : ν₁
φ₁ : PropForm ν₁
⊢ substL (⟦φ₁⟧ ⊓ φ₂) f = substL ⟦φ₁⟧ f ⊓ substL φ₂ f
Theorem: LeanSAT.Model.PropFun.substL_conj
Proof state before:
case refl
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₂ : PropFun ν₁
v : ν₁
φ₁ : PropForm ν₁
⊢ substL (⟦φ₁⟧ ⊓ φ₂) f = substL ⟦φ₁⟧ f ⊓ substL φ₂ f
Tactic:
have ⟨φ₂, hφ₂⟩ := φ₂.exists_rep
Proof state after:
case refl
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₂✝ : PropFun ν₁
v : ν₁
φ₁ φ₂ : PropForm ν₁
hφ₂ : ⟦φ₂⟧ = φ₂✝
⊢ substL (⟦φ₁⟧ ⊓ φ₂✝) f = substL ⟦φ₁⟧ f ⊓ substL φ₂✝ f
Theorem: LeanSAT.Model.PropFun.substL_conj
Proof state before:
case refl
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
φ₂✝ : PropFun ν₁
v : ν₁
φ₁ φ₂ : PropForm ν₁
hφ₂ : ⟦φ₂⟧ = φ₂✝
⊢ substL (⟦φ₁⟧ ⊓ φ₂✝) f = substL ⟦φ₁⟧ f ⊓ substL φ₂✝ f
Tactic:
cases hφ₂
Proof state after:
case refl.refl
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
v : ν₁
φ₁ φ₂ : PropForm ν₁
⊢ substL (⟦φ₁⟧ ⊓ ⟦φ₂⟧) f = substL ⟦φ₁⟧ f ⊓ substL ⟦φ₂⟧ f
Theorem: LeanSAT.Model.PropFun.substL_conj
Proof state before:
case refl.refl
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → PropForm ν₂
v : ν₁
φ₁ φ₂ : PropForm ν₁
⊢ substL (⟦φ₁⟧ ⊓ ⟦φ₂⟧) f = substL ⟦φ₁⟧ f ⊓ substL ⟦φ₂⟧ f
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.substL_neg
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
φ : PropFun ν₁
⊢ substL (neg φ) f = neg (substL φ f)
Tactic:
have ⟨φ, hφ⟩ := φ.exists_rep
Proof state after:
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
φ✝ : PropFun ν₁
φ : PropForm ν₁
hφ : ⟦φ⟧ = φ✝
⊢ substL (neg φ✝) f = neg (substL φ✝ f)
Theorem: LeanSAT.Model.PropFun.substL_neg
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
φ✝ : PropFun ν₁
φ : PropForm ν₁
hφ : ⟦φ⟧ = φ✝
⊢ substL (neg φ✝) f = neg (substL φ✝ f)
Tactic:
cases hφ
Proof state after:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
φ : PropForm ν₁
⊢ substL (neg ⟦φ⟧) f = neg (substL ⟦φ⟧ f)
Theorem: LeanSAT.Model.PropFun.substL_neg
Proof state before:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
φ : PropForm ν₁
⊢ substL (neg ⟦φ⟧) f = neg (substL ⟦φ⟧ f)
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_substL
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
⊢ τ ⊨ substL φ f ↔ PropAssignment.subst (fun x => ⟦f x⟧) τ ⊨ φ
Tactic:
have ⟨φ, hφ⟩ := φ.exists_rep
Proof state after:
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
φ✝ : PropFun ν₁
f : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
φ : PropForm ν₁
hφ : ⟦φ⟧ = φ✝
⊢ τ ⊨ substL φ✝ f ↔ PropAssignment.subst (fun x => ⟦f x⟧) τ ⊨ φ✝
Theorem: LeanSAT.Model.PropFun.satisfies_substL
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
φ✝ : PropFun ν₁
f : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
φ : PropForm ν₁
hφ : ⟦φ⟧ = φ✝
⊢ τ ⊨ substL φ✝ f ↔ PropAssignment.subst (fun x => ⟦f x⟧) τ ⊨ φ✝
Tactic:
cases hφ
Proof state after:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
f : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
φ : PropForm ν₁
⊢ τ ⊨ substL ⟦φ⟧ f ↔ PropAssignment.subst (fun x => ⟦f x⟧) τ ⊨ ⟦φ⟧
Theorem: LeanSAT.Model.PropFun.satisfies_substL
Proof state before:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
f : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
φ : PropForm ν₁
⊢ τ ⊨ substL ⟦φ⟧ f ↔ PropAssignment.subst (fun x => ⟦f x⟧) τ ⊨ ⟦φ⟧
Tactic:
simp [substL]
Proof state after:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
f : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
φ : PropForm ν₁
⊢ τ ⊨ ⟦PropForm.subst φ f⟧ ↔ PropAssignment.subst (fun x => ⟦f x⟧) τ ⊨ ⟦φ⟧
Theorem: LeanSAT.Model.PropFun.satisfies_substL
Proof state before:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
f : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
φ : PropForm ν₁
⊢ τ ⊨ ⟦PropForm.subst φ f⟧ ↔ PropAssignment.subst (fun x => ⟦f x⟧) τ ⊨ ⟦φ⟧
Tactic:
rw [satisfies_mk, satisfies_mk, PropForm.satisfies_subst]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_subst
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
⊢ τ ⊨ subst φ f ↔ PropAssignment.subst f τ ⊨ φ
Tactic:
unfold subst
Proof state after:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
⊢ τ ⊨
      Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod φ (Quotient.choice f)) ↔
    PropAssignment.subst f τ ⊨ φ
Theorem: LeanSAT.Model.PropFun.satisfies_subst
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
⊢ τ ⊨
      Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod φ (Quotient.choice f)) ↔
    PropAssignment.subst f τ ⊨ φ
Tactic:
generalize hq : φ.prod (Quotient.choice f) = q
Proof state after:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
q : Quotient (Setoid.prod (setoid ν₁) inferInstance)
hq : Quotient.prod φ (Quotient.choice f) = q
⊢ τ ⊨
      Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ q ↔
    PropAssignment.subst f τ ⊨ φ
Theorem: LeanSAT.Model.PropFun.satisfies_subst
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
q : Quotient (Setoid.prod (setoid ν₁) inferInstance)
hq : Quotient.prod φ (Quotient.choice f) = q
⊢ τ ⊨
      Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ q ↔
    PropAssignment.subst f τ ⊨ φ
Tactic:
rcases q.exists_rep with ⟨⟨p, f'⟩, rfl⟩
Proof state after:
case intro.mk
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.prod φ (Quotient.choice f) = ⟦(p, f')⟧
⊢ τ ⊨
      Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ ⟦(p, f')⟧ ↔
    PropAssignment.subst f τ ⊨ φ
Theorem: LeanSAT.Model.PropFun.satisfies_subst
Proof state before:
case intro.mk
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.prod φ (Quotient.choice f) = ⟦(p, f')⟧
⊢ τ ⊨
      Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ ⟦(p, f')⟧ ↔
    PropAssignment.subst f τ ⊨ φ
Tactic:
simp [Quotient.lift_mk (s := .prod _ _)]
Proof state after:
case intro.mk
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.prod φ (Quotient.choice f) = ⟦(p, f')⟧
⊢ τ ⊨ ⟦PropForm.subst p f'⟧ ↔ PropAssignment.subst f τ ⊨ φ
Theorem: LeanSAT.Model.PropFun.satisfies_subst
Proof state before:
case intro.mk
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.prod φ (Quotient.choice f) = ⟦(p, f')⟧
⊢ τ ⊨ ⟦PropForm.subst p f'⟧ ↔ PropAssignment.subst f τ ⊨ φ
Tactic:
rw [satisfies_mk, PropForm.satisfies_subst, ← satisfies_mk]
Proof state after:
case intro.mk
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.prod φ (Quotient.choice f) = ⟦(p, f')⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ ⊨ ⟦p⟧ ↔ PropAssignment.subst f τ ⊨ φ
Theorem: LeanSAT.Model.PropFun.satisfies_subst
Proof state before:
case intro.mk
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.prod φ (Quotient.choice f) = ⟦(p, f')⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ ⊨ ⟦p⟧ ↔ PropAssignment.subst f τ ⊨ φ
Tactic:
rw [Quotient.prod_eq_mk] at hq
Proof state after:
case intro.mk
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : φ = ⟦p⟧ ∧ Quotient.choice f = ⟦f'⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ ⊨ ⟦p⟧ ↔ PropAssignment.subst f τ ⊨ φ
Theorem: LeanSAT.Model.PropFun.satisfies_subst
Proof state before:
case intro.mk
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : φ = ⟦p⟧ ∧ Quotient.choice f = ⟦f'⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ ⊨ ⟦p⟧ ↔ PropAssignment.subst f τ ⊨ φ
Tactic:
rcases hq with ⟨rfl,hq⟩
Proof state after:
case intro.mk.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ ⊨ ⟦p⟧ ↔ PropAssignment.subst f τ ⊨ ⟦p⟧
Theorem: LeanSAT.Model.PropFun.satisfies_subst
Proof state before:
case intro.mk.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ ⊨ ⟦p⟧ ↔ PropAssignment.subst f τ ⊨ ⟦p⟧
Tactic:
apply iff_of_eq
Proof state after:
case intro.mk.intro.a
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ ⊨ ⟦p⟧ = PropAssignment.subst f τ ⊨ ⟦p⟧
Theorem: LeanSAT.Model.PropFun.satisfies_subst
Proof state before:
case intro.mk.intro.a
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ ⊨ ⟦p⟧ = PropAssignment.subst f τ ⊨ ⟦p⟧
Tactic:
congr
Proof state after:
case intro.mk.intro.a.e_a
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ = PropAssignment.subst f τ
Theorem: LeanSAT.Model.PropFun.satisfies_subst
Proof state before:
case intro.mk.intro.a.e_a
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ = PropAssignment.subst f τ
Tactic:
apply congrFun
Proof state after:
case intro.mk.intro.a.e_a.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ (PropAssignment.subst fun x => ⟦f' x⟧) = fun {τ} => PropAssignment.subst f τ
Theorem: LeanSAT.Model.PropFun.satisfies_subst
Proof state before:
case intro.mk.intro.a.e_a.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ (PropAssignment.subst fun x => ⟦f' x⟧) = fun {τ} => PropAssignment.subst f τ
Tactic:
apply congrArg
Proof state after:
case intro.mk.intro.a.e_a.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ (fun x => ⟦f' x⟧) = f
Theorem: LeanSAT.Model.PropFun.satisfies_subst
Proof state before:
case intro.mk.intro.a.e_a.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ (fun x => ⟦f' x⟧) = f
Tactic:
funext x
Proof state after:
case intro.mk.intro.a.e_a.h.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
x : ν₁
⊢ ⟦f' x⟧ = f x
Theorem: LeanSAT.Model.PropFun.satisfies_subst
Proof state before:
case intro.mk.intro.a.e_a.h.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
x : ν₁
⊢ ⟦f' x⟧ = f x
Tactic:
simp [Quotient.choice] at hq
Proof state after:
case intro.mk.intro.a.e_a.h.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
x : ν₁
hq : (fun i => Quotient.out (f i)) ≈ f'
⊢ ⟦f' x⟧ = f x
Theorem: LeanSAT.Model.PropFun.satisfies_subst
Proof state before:
case intro.mk.intro.a.e_a.h.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
x : ν₁
hq : (fun i => Quotient.out (f i)) ≈ f'
⊢ ⟦f' x⟧ = f x
Tactic:
have := Quotient.sound (hq x)
Proof state after:
case intro.mk.intro.a.e_a.h.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
x : ν₁
hq : (fun i => Quotient.out (f i)) ≈ f'
this : ⟦(fun i => Quotient.out (f i)) x⟧ = ⟦f' x⟧
⊢ ⟦f' x⟧ = f x
Theorem: LeanSAT.Model.PropFun.satisfies_subst
Proof state before:
case intro.mk.intro.a.e_a.h.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
x : ν₁
hq : (fun i => Quotient.out (f i)) ≈ f'
this : ⟦(fun i => Quotient.out (f i)) x⟧ = ⟦f' x⟧
⊢ ⟦f' x⟧ = f x
Tactic:
simp at this
Proof state after:
case intro.mk.intro.a.e_a.h.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
x : ν₁
hq : (fun i => Quotient.out (f i)) ≈ f'
this : f x = ⟦f' x⟧
⊢ ⟦f' x⟧ = f x
Theorem: LeanSAT.Model.PropFun.satisfies_subst
Proof state before:
case intro.mk.intro.a.e_a.h.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
x : ν₁
hq : (fun i => Quotient.out (f i)) ≈ f'
this : f x = ⟦f' x⟧
⊢ ⟦f' x⟧ = f x
Tactic:
exact this.symm
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.subst_distrib
Proof state before:
ν₁ : Type u_2
ν₂ : Type u_1
φ φ₁ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
⊢ subst ⟦PropForm.var v⟧ f = f v
Tactic:
ext
Proof state after:
case a
ν₁ : Type u_2
ν₂ : Type u_1
φ φ₁ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
τ✝ : PropAssignment ν₂
⊢ τ✝ ⊨ subst ⟦PropForm.var v⟧ f ↔ τ✝ ⊨ f v
Theorem: LeanSAT.Model.PropFun.subst_distrib
Proof state before:
case a
ν₁ : Type u_2
ν₂ : Type u_1
φ φ₁ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
τ✝ : PropAssignment ν₂
⊢ τ✝ ⊨ subst ⟦PropForm.var v⟧ f ↔ τ✝ ⊨ f v
Tactic:
simp [PropAssignment.subst]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.subst_disj
Proof state before:
ν₁ : Type u_2
ν₂ : Type u_1
φ φ₁ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
⊢ subst (φ₁ ⊔ φ₂) f = subst φ₁ f ⊔ subst φ₂ f
Tactic:
have ⟨φ₁, hφ₁⟩ := φ₁.exists_rep
Proof state after:
ν₁ : Type u_2
ν₂ : Type u_1
φ φ₁✝ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
φ₁ : PropForm ν₁
hφ₁ : ⟦φ₁⟧ = φ₁✝
⊢ subst (φ₁✝ ⊔ φ₂) f = subst φ₁✝ f ⊔ subst φ₂ f
Theorem: LeanSAT.Model.PropFun.subst_disj
Proof state before:
ν₁ : Type u_2
ν₂ : Type u_1
φ φ₁✝ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
φ₁ : PropForm ν₁
hφ₁ : ⟦φ₁⟧ = φ₁✝
⊢ subst (φ₁✝ ⊔ φ₂) f = subst φ₁✝ f ⊔ subst φ₂ f
Tactic:
cases hφ₁
Proof state after:
case refl
ν₁ : Type u_2
ν₂ : Type u_1
φ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
φ₁ : PropForm ν₁
⊢ subst (⟦φ₁⟧ ⊔ φ₂) f = subst ⟦φ₁⟧ f ⊔ subst φ₂ f