internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.Model.PropFun.subst_disj
Proof state before:
case refl
ν₁ : Type u_2
ν₂ : Type u_1
φ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
φ₁ : PropForm ν₁
⊢ subst (⟦φ₁⟧ ⊔ φ₂) f = subst ⟦φ₁⟧ f ⊔ subst φ₂ f
Tactic:
have ⟨φ₂, hφ₂⟩ := φ₂.exists_rep
Proof state after:
case refl
ν₁ : 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:
case refl
ν₁ : 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.refl
ν₁ : Type u_2
ν₂ : Type u_1
φ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
φ₁ φ₂ : PropForm ν₁
⊢ subst (⟦φ₁⟧ ⊔ ⟦φ₂⟧) f = subst ⟦φ₁⟧ f ⊔ subst ⟦φ₂⟧ f
Theorem: LeanSAT.Model.PropFun.subst_disj
Proof state before:
case refl.refl
ν₁ : Type u_2
ν₂ : Type u_1
φ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
φ₁ φ₂ : PropForm ν₁
⊢ subst (⟦φ₁⟧ ⊔ ⟦φ₂⟧) f = subst ⟦φ₁⟧ f ⊔ subst ⟦φ₂⟧ f
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.subst_conj
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_conj
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
Theorem: LeanSAT.Model.PropFun.subst_conj
Proof state before:
case refl
ν₁ : Type u_2
ν₂ : Type u_1
φ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
φ₁ : PropForm ν₁
⊢ subst (⟦φ₁⟧ ⊓ φ₂) f = subst ⟦φ₁⟧ f ⊓ subst φ₂ f
Tactic:
have ⟨φ₂, hφ₂⟩ := φ₂.exists_rep
Proof state after:
case refl
ν₁ : 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_conj
Proof state before:
case refl
ν₁ : 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.refl
ν₁ : Type u_2
ν₂ : Type u_1
φ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
φ₁ φ₂ : PropForm ν₁
⊢ subst (⟦φ₁⟧ ⊓ ⟦φ₂⟧) f = subst ⟦φ₁⟧ f ⊓ subst ⟦φ₂⟧ f
Theorem: LeanSAT.Model.PropFun.subst_conj
Proof state before:
case refl.refl
ν₁ : Type u_2
ν₂ : Type u_1
φ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
φ₁ φ₂ : PropForm ν₁
⊢ subst (⟦φ₁⟧ ⊓ ⟦φ₂⟧) f = subst ⟦φ₁⟧ f ⊓ subst ⟦φ₂⟧ f
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.subst_neg
Proof state before:
ν₁ : Type u_2
ν₂ : Type u_1
φ φ₁ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
⊢ subst (neg φ) f = neg (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 (neg φ✝) f = neg (subst φ✝ f)
Theorem: LeanSAT.Model.PropFun.subst_neg
Proof state before:
ν₁ : Type u_2
ν₂ : Type u_1
φ✝ φ₁ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
φ : PropForm ν₁
hφ : ⟦φ⟧ = φ✝
⊢ subst (neg φ✝) f = neg (subst φ✝ f)
Tactic:
cases hφ
Proof state after:
case refl
ν₁ : Type u_2
ν₂ : Type u_1
φ₁ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
φ : PropForm ν₁
⊢ subst (neg ⟦φ⟧) f = neg (subst ⟦φ⟧ f)
Theorem: LeanSAT.Model.PropFun.subst_neg
Proof state before:
case refl
ν₁ : Type u_2
ν₂ : Type u_1
φ₁ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
φ : PropForm ν₁
⊢ subst (neg ⟦φ⟧) f = neg (subst ⟦φ⟧ f)
Tactic:
rfl
Proof state after:
no goals
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 ν₂
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
⊢ semVars (subst φ f) ⊆ Finset.biUnion (semVars φ) fun v1 => semVars (f v1)
Tactic:
intro v2 hv2
Proof state after:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
v2 : ν₂
hv2 : v2 ∈ semVars (subst φ f)
⊢ v2 ∈ Finset.biUnion (semVars φ) fun v1 => semVars (f v1)
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 ν₂
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
v2 : ν₂
hv2 : v2 ∈ semVars (subst φ f)
⊢ v2 ∈ Finset.biUnion (semVars φ) fun v1 => semVars (f v1)
Tactic:
unfold subst at hv2
Proof state after:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
v2 : ν₂
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod φ (Quotient.choice f)))
⊢ v2 ∈ Finset.biUnion (semVars φ) fun v1 => semVars (f v1)
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 ν₂
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
v2 : ν₂
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod φ (Quotient.choice f)))
⊢ v2 ∈ Finset.biUnion (semVars φ) fun v1 => semVars (f v1)
Tactic:
rw [Finset.mem_biUnion]
Proof state after:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
v2 : ν₂
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod φ (Quotient.choice f)))
⊢ ∃ a ∈ semVars φ, v2 ∈ semVars (f a)
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 ν₂
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
v2 : ν₂
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod φ (Quotient.choice f)))
⊢ ∃ a ∈ semVars φ, v2 ∈ semVars (f a)
Tactic:
have ⟨p,hp⟩ := φ.exists_rep
Proof state after:
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
v2 : ν₂
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod φ (Quotient.choice f)))
p : PropForm ν₁
hp : ⟦p⟧ = φ
⊢ ∃ a ∈ semVars φ, v2 ∈ semVars (f a)
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 ν₂
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
v2 : ν₂
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod φ (Quotient.choice f)))
p : PropForm ν₁
hp : ⟦p⟧ = φ
⊢ ∃ a ∈ semVars φ, v2 ∈ semVars (f a)
Tactic:
cases hp
Proof state after:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod ⟦p⟧ (Quotient.choice f)))
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod ⟦p⟧ (Quotient.choice f)))
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
generalize hf' : Quotient.choice f = f' at hv2
Proof state after:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f' : Quotient inferInstance
hf' : Quotient.choice f = f'
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod ⟦p⟧ f'))
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f' : Quotient inferInstance
hf' : Quotient.choice f = f'
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod ⟦p⟧ f'))
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
have ⟨f'', hf''⟩ := f'.exists_rep
Proof state after:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f' : Quotient inferInstance
hf' : Quotient.choice f = f'
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod ⟦p⟧ f'))
f'' : ν₁ → PropForm ν₂
hf'' : ⟦f''⟧ = f'
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f' : Quotient inferInstance
hf' : Quotient.choice f = f'
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod ⟦p⟧ f'))
f'' : ν₁ → PropForm ν₂
hf'' : ⟦f''⟧ = f'
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
cases hf''
Proof state after:
case refl.refl
ν₁ : 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''⟧
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod ⟦p⟧ ⟦f''⟧))
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case refl.refl
ν₁ : 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''⟧
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod ⟦p⟧ ⟦f''⟧))
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
simp [Quotient.lift_mk (s := .prod _ _)] at hv2
Proof state after:
case refl.refl
ν₁ : 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''⟧
hv2 : v2 ∈ semVars ⟦PropForm.subst p f''⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case refl.refl
ν₁ : 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''⟧
hv2 : v2 ∈ semVars ⟦PropForm.subst p f''⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
rw [mem_semVars] at hv2
Proof state after:
case refl.refl
ν₁ : 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''⟧
hv2 : ∃ τ, τ ⊨ ⟦PropForm.subst p f''⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) ⟦PropForm.subst p f''⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case refl.refl
ν₁ : 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''⟧
hv2 : ∃ τ, τ ⊨ ⟦PropForm.subst p f''⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ v2 !τ v2) ⟦PropForm.subst p f''⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
rcases hv2 with ⟨τ,hsat,hunsat⟩
Proof state after:
case refl.refl.intro.intro
ν₁ : 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 : τ ⊨ ⟦PropForm.subst p f''⟧
hunsat : ¬(PropAssignment.set τ v2 !τ v2) ⊨ ⟦PropForm.subst p f''⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case refl.refl.intro.intro
ν₁ : 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 : τ ⊨ ⟦PropForm.subst p f''⟧
hunsat : ¬(PropAssignment.set τ v2 !τ v2) ⊨ ⟦PropForm.subst p f''⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
rw [satisfies_mk] at hsat hunsat
Proof state after:
case refl.refl.intro.intro
ν₁ : 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 : τ ⊨ PropForm.subst p f''
hunsat : ¬(PropAssignment.set τ v2 !τ v2) ⊨ PropForm.subst p f''
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case refl.refl.intro.intro
ν₁ : 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 : τ ⊨ PropForm.subst p f''
hunsat : ¬(PropAssignment.set τ v2 !τ v2) ⊨ PropForm.subst p f''
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
simp at hsat hunsat
Proof state after:
case refl.refl.intro.intro
ν₁ : 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
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case refl.refl.intro.intro
ν₁ : 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
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
have : ∀ x, ⟦f'' x⟧ = f x := by
  simp [Quotient.choice, piSetoid, instHasEquiv, Setoid.r] at hf'
  intro x; have := sound (hf' x); simp at this; simp [this]
Proof state after:
case refl.refl.intro.intro
ν₁ : 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
this : ∀ (x : ν₁), ⟦f'' x⟧ = f x
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case refl.refl.intro.intro
ν₁ : 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
this : ∀ (x : ν₁), ⟦f'' x⟧ = f x
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
simp [this] at hsat hunsat
Proof state after:
case refl.refl.intro.intro
ν₁ : 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 ν₂
this : ∀ (x : ν₁), ⟦f'' x⟧ = f x
hsat : PropAssignment.subst (fun x => f x) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) ⊨ p
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case refl.refl.intro.intro
ν₁ : 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 ν₂
this : ∀ (x : ν₁), ⟦f'' x⟧ = f x
hsat : PropAssignment.subst (fun x => f x) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) ⊨ p
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
clear this hf' f''
Proof state after:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => f x) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) ⊨ p
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => f x) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) ⊨ p
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
rw [← satisfies_mk] at hsat hunsat
Proof state after:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => f x) τ ⊨ ⟦p⟧
hunsat : ¬PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) ⊨ ⟦p⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => f x) τ ⊨ ⟦p⟧
hunsat : ¬PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) ⊨ ⟦p⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
have ⟨x,h1,h2⟩ := exists_semVar hsat hunsat
Proof state after:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => f x) τ ⊨ ⟦p⟧
hunsat : ¬PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) ⊨ ⟦p⟧
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
h2 : x ∈ semVars ⟦p⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case refl.refl.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => f x) τ ⊨ ⟦p⟧
hunsat : ¬PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) ⊨ ⟦p⟧
x : ν₁
h1 : PropAssignment.subst (fun x => f x) τ x ≠ PropAssignment.subst (fun x => f x) (PropAssignment.set τ v2 !τ v2) x
h2 : x ∈ semVars ⟦p⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
clear hsat hunsat
Proof state after:
case refl.refl.intro.intro
ν₁ : 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⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Theorem: LeanSAT.Model.PropFun.semVars_subst
Proof state before:
case refl.refl.intro.intro
ν₁ : 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⟧
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
Tactic:
use x
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⟧
⊢ x ∈ semVars ⟦p⟧ ∧ v2 ∈ semVars (f x)