internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
h2 : x ∈ semVars ⟦p⟧
⊢ x ∈ semVars ⟦p⟧ ∧ v2 ∈ semVars (f x)
Tactic:
simp [h2]
Proof state after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
h2 : x ∈ semVars ⟦p⟧
⊢ v2 ∈ semVars (f x)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
h2 : x ∈ semVars ⟦p⟧
⊢ v2 ∈ semVars (f x)
Tactic:
clear h2
Proof state after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
⊢ v2 ∈ semVars (f x)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
⊢ v2 ∈ semVars (f x)
Tactic:
rw [mem_semVars]
Proof state after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)
Tactic:
simp [PropAssignment.subst] at h1
Proof state after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : ¬(τ ⊨ f x ↔ (PropAssignment.set τ v2 !τ v2) ⊨ f x)
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : ¬(τ ⊨ f x ↔ (PropAssignment.set τ v2 !τ v2) ⊨ f x)
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)
Tactic:
by_cases h : τ ⊨ f x
Proof state after:
case pos
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : ¬(τ ⊨ f x ↔ (PropAssignment.set τ v2 !τ v2) ⊨ f x)
h : τ ⊨ f x
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)

case neg
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : ¬(τ ⊨ f x ↔ (PropAssignment.set τ v2 !τ v2) ⊨ f x)
h : ¬τ ⊨ f x
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
⊢ ∀ (x : ν₁), ⟦f'' x⟧ = f x
Tactic:
simp [Quotient.choice, piSetoid, instHasEquiv, Setoid.r] at hf'
Proof state after:
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
hf' : ∀ (i : ν₁), PropForm.equivalent (Quotient.out (f i)) (f'' i)
⊢ ∀ (x : ν₁), ⟦f'' x⟧ = f x
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
hf' : ∀ (i : ν₁), PropForm.equivalent (Quotient.out (f i)) (f'' i)
⊢ ∀ (x : ν₁), ⟦f'' x⟧ = f x
Tactic:
intro x
Proof state after:
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
hf' : ∀ (i : ν₁), PropForm.equivalent (Quotient.out (f i)) (f'' i)
x : ν₁
⊢ ⟦f'' x⟧ = f x
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
hf' : ∀ (i : ν₁), PropForm.equivalent (Quotient.out (f i)) (f'' i)
x : ν₁
⊢ ⟦f'' x⟧ = f x
Tactic:
have := sound (hf' x)
Proof state after:
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
hf' : ∀ (i : ν₁), PropForm.equivalent (Quotient.out (f i)) (f'' i)
x : ν₁
this : ⟦Quotient.out (f x)⟧ = ⟦f'' x⟧
⊢ ⟦f'' x⟧ = f x
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
hf' : ∀ (i : ν₁), PropForm.equivalent (Quotient.out (f i)) (f'' i)
x : ν₁
this : ⟦Quotient.out (f x)⟧ = ⟦f'' x⟧
⊢ ⟦f'' x⟧ = f x
Tactic:
simp at this
Proof state after:
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
hf' : ∀ (i : ν₁), PropForm.equivalent (Quotient.out (f i)) (f'' i)
x : ν₁
this : f x = ⟦f'' x⟧
⊢ ⟦f'' x⟧ = f x
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
hf' : ∀ (i : ν₁), PropForm.equivalent (Quotient.out (f i)) (f'' i)
x : ν₁
this : f x = ⟦f'' x⟧
⊢ ⟦f'' x⟧ = f x
Tactic:
simp [this]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case pos
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : ¬(τ ⊨ f x ↔ (PropAssignment.set τ v2 !τ v2) ⊨ f x)
h : τ ⊨ f x
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)
Tactic:
use τ
Proof state after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : ¬(τ ⊨ f x ↔ (PropAssignment.set τ v2 !τ v2) ⊨ f x)
h : τ ⊨ f x
⊢ τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : ¬(τ ⊨ f x ↔ (PropAssignment.set τ v2 !τ v2) ⊨ f x)
h : τ ⊨ f x
⊢ τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)
Tactic:
simp [h] at h1
Proof state after:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h : τ ⊨ f x
h1 : ¬(PropAssignment.set τ v2 !τ v2) ⊨ f x
⊢ τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h : τ ⊨ f x
h1 : ¬(PropAssignment.set τ v2 !τ v2) ⊨ f x
⊢ τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)
Tactic:
simp [*]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case neg
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h1 : ¬(τ ⊨ f x ↔ (PropAssignment.set τ v2 !τ v2) ⊨ f x)
h : ¬τ ⊨ f x
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)
Tactic:
simp [h] at h1
Proof state after:
case neg
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h : ¬τ ⊨ f x
h1 : (PropAssignment.set τ v2 !τ v2) ⊨ f x
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case neg
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h : ¬τ ⊨ f x
h1 : (PropAssignment.set τ v2 !τ v2) ⊨ f x
⊢ ∃ τ, τ ⊨ f x ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) (f x)
Tactic:
refine ⟨_, h1, ?_⟩
Proof state after:
case neg
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h : ¬τ ⊨ f x
h1 : (PropAssignment.set τ v2 !τ v2) ⊨ f x
⊢ (fun M φ => ¬M ⊨ φ) (PropAssignment.set (PropAssignment.set τ v2 !τ v2) v2 !PropAssignment.set τ v2 (!τ v2) v2) (f x)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case neg
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
x : ν₁
h : ¬τ ⊨ f x
h1 : (PropAssignment.set τ v2 !τ v2) ⊨ f x
⊢ (fun M φ => ¬M ⊨ φ) (PropAssignment.set (PropAssignment.set τ v2 !τ v2) v2 !PropAssignment.set τ v2 (!τ v2) v2) (f x)
Tactic:
simp [h]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_substOne
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ ψ : PropFun ν
v : ν
τ : PropAssignment ν
⊢ τ ⊨ substOne ψ v φ ↔ PropAssignment.set τ v (decide (τ ⊨ φ)) ⊨ ψ
Tactic:
have ⟨ψ,hψ⟩ := ψ.exists_rep
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ ψ✝ : PropFun ν
v : ν
τ : PropAssignment ν
ψ : PropForm ν
hψ : ⟦ψ⟧ = ψ✝
⊢ τ ⊨ substOne ψ✝ v φ ↔ PropAssignment.set τ v (decide (τ ⊨ φ)) ⊨ ψ✝
Theorem: LeanSAT.Model.PropFun.satisfies_substOne
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ ψ✝ : PropFun ν
v : ν
τ : PropAssignment ν
ψ : PropForm ν
hψ : ⟦ψ⟧ = ψ✝
⊢ τ ⊨ substOne ψ✝ v φ ↔ PropAssignment.set τ v (decide (τ ⊨ φ)) ⊨ ψ✝
Tactic:
cases hψ
Proof state after:
case refl
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
v : ν
τ : PropAssignment ν
ψ : PropForm ν
⊢ τ ⊨ substOne ⟦ψ⟧ v φ ↔ PropAssignment.set τ v (decide (τ ⊨ φ)) ⊨ ⟦ψ⟧
Theorem: LeanSAT.Model.PropFun.satisfies_substOne
Proof state before:
case refl
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
v : ν
τ : PropAssignment ν
ψ : PropForm ν
⊢ τ ⊨ substOne ⟦ψ⟧ v φ ↔ PropAssignment.set τ v (decide (τ ⊨ φ)) ⊨ ⟦ψ⟧
Tactic:
have ⟨φ,hφ⟩ := φ.exists_rep
Proof state after:
case refl
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ : PropFun ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
hφ : ⟦φ⟧ = φ✝
⊢ τ ⊨ substOne ⟦ψ⟧ v φ✝ ↔ PropAssignment.set τ v (decide (τ ⊨ φ✝)) ⊨ ⟦ψ⟧
Theorem: LeanSAT.Model.PropFun.satisfies_substOne
Proof state before:
case refl
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ : PropFun ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
hφ : ⟦φ⟧ = φ✝
⊢ τ ⊨ substOne ⟦ψ⟧ v φ✝ ↔ PropAssignment.set τ v (decide (τ ⊨ φ✝)) ⊨ ⟦ψ⟧
Tactic:
cases hφ
Proof state after:
case refl.refl
ν : Type u_1
inst✝ : DecidableEq ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
⊢ τ ⊨ substOne ⟦ψ⟧ v ⟦φ⟧ ↔ PropAssignment.set τ v (decide (τ ⊨ ⟦φ⟧)) ⊨ ⟦ψ⟧
Theorem: LeanSAT.Model.PropFun.satisfies_substOne
Proof state before:
case refl.refl
ν : Type u_1
inst✝ : DecidableEq ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
⊢ τ ⊨ substOne ⟦ψ⟧ v ⟦φ⟧ ↔ PropAssignment.set τ v (decide (τ ⊨ ⟦φ⟧)) ⊨ ⟦ψ⟧
Tactic:
simp [substOne]
Proof state after:
case refl.refl
ν : Type u_1
inst✝ : DecidableEq ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
⊢ τ ⊨ ⟦PropForm.substOne ψ v φ⟧ ↔ PropAssignment.set τ v (decide (τ ⊨ ⟦φ⟧)) ⊨ ⟦ψ⟧
Theorem: LeanSAT.Model.PropFun.satisfies_substOne
Proof state before:
case refl.refl
ν : Type u_1
inst✝ : DecidableEq ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
⊢ τ ⊨ ⟦PropForm.substOne ψ v φ⟧ ↔ PropAssignment.set τ v (decide (τ ⊨ ⟦φ⟧)) ⊨ ⟦ψ⟧
Tactic:
rw [satisfies_mk, satisfies_mk]
Proof state after:
case refl.refl
ν : Type u_1
inst✝ : DecidableEq ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
⊢ τ ⊨ PropForm.substOne ψ v φ ↔ PropAssignment.set τ v (decide (τ ⊨ ⟦φ⟧)) ⊨ ψ
Theorem: LeanSAT.Model.PropFun.satisfies_substOne
Proof state before:
case refl.refl
ν : Type u_1
inst✝ : DecidableEq ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
⊢ τ ⊨ PropForm.substOne ψ v φ ↔ PropAssignment.set τ v (decide (τ ⊨ ⟦φ⟧)) ⊨ ψ
Tactic:
rw [PropForm.satisfies_substOne]
Proof state after:
case refl.refl
ν : Type u_1
inst✝ : DecidableEq ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
⊢ PropAssignment.set τ v (decide (τ ⊨ φ)) ⊨ ψ ↔ PropAssignment.set τ v (decide (τ ⊨ ⟦φ⟧)) ⊨ ψ
Theorem: LeanSAT.Model.PropFun.satisfies_substOne
Proof state before:
case refl.refl
ν : Type u_1
inst✝ : DecidableEq ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
⊢ PropAssignment.set τ v (decide (τ ⊨ φ)) ⊨ ψ ↔ PropAssignment.set τ v (decide (τ ⊨ ⟦φ⟧)) ⊨ ψ
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.vars_map
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → ν₂
φ φ₁ φ₂ : PropForm ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
⊢ vars (map f φ) = Finset.image f (vars φ)
Tactic:
induction φ <;> simp [*, Finset.image_union]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.satisfies_map
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ φ : PropForm ν₁
f : ν₁ → ν₂
τ : PropAssignment ν₂
⊢ τ ⊨ map f φ ↔ PropAssignment.map f τ ⊨ φ
Tactic:
induction φ <;> (simp [map, PropAssignment.map] at *) <;> (simp [*])
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.satisfies_map
Proof state before:
case biImpl
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ φ₁ φ₂ : PropForm ν₁
f : ν₁ → ν₂
τ : PropAssignment ν₂
φ₁✝ φ₂✝ : PropForm ν₁
φ₁_ih✝ : τ ⊨ map f φ₁✝ ↔ PropAssignment.map f τ ⊨ φ₁✝
φ₂_ih✝ : τ ⊨ map f φ₂✝ ↔ PropAssignment.map f τ ⊨ φ₂✝
⊢ τ ⊨ map f (biImpl φ₁✝ φ₂✝) ↔ PropAssignment.map f τ ⊨ biImpl φ₁✝ φ₂✝
Tactic:
simp [map, PropAssignment.map] at *
Proof state after:
case biImpl
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ φ₁ φ₂ : PropForm ν₁
f : ν₁ → ν₂
τ : PropAssignment ν₂
φ₁✝ φ₂✝ : PropForm ν₁
φ₁_ih✝ : τ ⊨ map f φ₁✝ ↔ τ ∘ f ⊨ φ₁✝
φ₂_ih✝ : τ ⊨ map f φ₂✝ ↔ τ ∘ f ⊨ φ₂✝
⊢ (τ ⊨ map f φ₁✝ ↔ τ ⊨ map f φ₂✝) ↔ (τ ∘ f ⊨ φ₁✝ ↔ τ ∘ f ⊨ φ₂✝)
Theorem: LeanSAT.Model.PropForm.satisfies_map
Proof state before:
case biImpl
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ φ₁ φ₂ : PropForm ν₁
f : ν₁ → ν₂
τ : PropAssignment ν₂
φ₁✝ φ₂✝ : PropForm ν₁
φ₁_ih✝ : τ ⊨ map f φ₁✝ ↔ τ ∘ f ⊨ φ₁✝
φ₂_ih✝ : τ ⊨ map f φ₂✝ ↔ τ ∘ f ⊨ φ₂✝
⊢ (τ ⊨ map f φ₁✝ ↔ τ ⊨ map f φ₂✝) ↔ (τ ∘ f ⊨ φ₁✝ ↔ τ ∘ f ⊨ φ₂✝)
Tactic:
simp [*]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
⊢ PropFun.semVars ⟦map f φ⟧ = Finset.map { toFun := f, inj' := hf } (PropFun.semVars ⟦φ⟧)
Tactic:
ext v2
Proof state after:
case a
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
⊢ v2 ∈ PropFun.semVars ⟦map f φ⟧ ↔ v2 ∈ Finset.map { toFun := f, inj' := hf } (PropFun.semVars ⟦φ⟧)
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
⊢ v2 ∈ PropFun.semVars ⟦map f φ⟧ ↔ v2 ∈ Finset.map { toFun := f, inj' := hf } (PropFun.semVars ⟦φ⟧)
Tactic:
simp
Proof state after:
case a
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
⊢ v2 ∈ PropFun.semVars ⟦map f φ⟧ ↔ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
⊢ v2 ∈ PropFun.semVars ⟦map f φ⟧ ↔ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2
Tactic:
constructor
Proof state after:
case a.mp
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
⊢ v2 ∈ PropFun.semVars ⟦map f φ⟧ → ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2

case a.mpr
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
⊢ (∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2) → v2 ∈ PropFun.semVars ⟦map f φ⟧
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a.mp
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
⊢ v2 ∈ PropFun.semVars ⟦map f φ⟧ → ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2
Tactic:
intro h
Proof state after:
case a.mp
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
h : v2 ∈ PropFun.semVars ⟦map f φ⟧
⊢ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a.mp
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
h : v2 ∈ PropFun.semVars ⟦map f φ⟧
⊢ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2
Tactic:
have isVar : v2 ∈ vars (map f φ) := semVars_subset_vars _ h
Proof state after:
case a.mp
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
h : v2 ∈ PropFun.semVars ⟦map f φ⟧
isVar : v2 ∈ vars (map f φ)
⊢ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a.mp
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
h : v2 ∈ PropFun.semVars ⟦map f φ⟧
isVar : v2 ∈ vars (map f φ)
⊢ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2
Tactic:
simp at isVar
Proof state after:
case a.mp
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
h : v2 ∈ PropFun.semVars ⟦map f φ⟧
isVar : ∃ a ∈ vars φ, f a = v2
⊢ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2
Theorem: LeanSAT.Model.PropForm.semVars_map
Proof state before:
case a.mp
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v2 : ν₂
h : v2 ∈ PropFun.semVars ⟦map f φ⟧
isVar : ∃ a ∈ vars φ, f a = v2
⊢ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = v2
Tactic:
rcases isVar with ⟨v1, _, rfl⟩
Proof state after:
case a.mp.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
⊢ ∃ a ∈ PropFun.semVars ⟦φ⟧, f a = f v1