internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.Model.PropFun.equivalentOver_iff_extendsOver
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ : PropAssignment ν
⊢ (∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁) → ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Tactic:
intro ⟨σ₁, hAgree₁, hσ₁⟩
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ σ₁ : PropAssignment ν
hAgree₁ : PropAssignment.agreeOn X σ₁ τ
hσ₁ : σ₁ ⊨ φ₁
⊢ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Theorem: LeanSAT.Model.PropFun.equivalentOver_iff_extendsOver
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ σ₁ : PropAssignment ν
hAgree₁ : PropAssignment.agreeOn X σ₁ τ
hσ₁ : σ₁ ⊨ φ₁
⊢ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Tactic:
have ⟨σ₂, hAgree₂, hσ₂⟩ := h₁ σ₁ hσ₁
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ σ₁ : PropAssignment ν
hAgree₁ : PropAssignment.agreeOn X σ₁ τ
hσ₁ : σ₁ ⊨ φ₁
σ₂ : PropAssignment ν
hAgree₂ : PropAssignment.agreeOn X σ₂ σ₁
hσ₂ : σ₂ ⊨ φ₂
⊢ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Theorem: LeanSAT.Model.PropFun.equivalentOver_iff_extendsOver
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ σ₁ : PropAssignment ν
hAgree₁ : PropAssignment.agreeOn X σ₁ τ
hσ₁ : σ₁ ⊨ φ₁
σ₂ : PropAssignment ν
hAgree₂ : PropAssignment.agreeOn X σ₂ σ₁
hσ₂ : σ₂ ⊨ φ₂
⊢ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Tactic:
exact ⟨σ₂, hAgree₂.trans hAgree₁, hσ₂⟩
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.equivalentOver_iff_extendsOver
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ : PropAssignment ν
⊢ (∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂) → ∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁
Tactic:
intro ⟨σ₂, hAgree₂, hσ₂⟩
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ σ₂ : PropAssignment ν
hAgree₂ : PropAssignment.agreeOn X σ₂ τ
hσ₂ : σ₂ ⊨ φ₂
⊢ ∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁
Theorem: LeanSAT.Model.PropFun.equivalentOver_iff_extendsOver
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ σ₂ : PropAssignment ν
hAgree₂ : PropAssignment.agreeOn X σ₂ τ
hσ₂ : σ₂ ⊨ φ₂
⊢ ∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁
Tactic:
have ⟨σ₁, hAgree₁, hσ₁⟩ := h₂ σ₂ hσ₂
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ σ₂ : PropAssignment ν
hAgree₂ : PropAssignment.agreeOn X σ₂ τ
hσ₂ : σ₂ ⊨ φ₂
σ₁ : PropAssignment ν
hAgree₁ : PropAssignment.agreeOn X σ₁ σ₂
hσ₁ : σ₁ ⊨ φ₁
⊢ ∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁
Theorem: LeanSAT.Model.PropFun.equivalentOver_iff_extendsOver
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ σ₂ : PropAssignment ν
hAgree₂ : PropAssignment.agreeOn X σ₂ τ
hσ₂ : σ₂ ⊨ φ₂
σ₁ : PropAssignment ν
hAgree₁ : PropAssignment.agreeOn X σ₁ σ₂
hσ₁ : σ₁ ⊨ φ₁
⊢ ∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁
Tactic:
exact ⟨σ₁, hAgree₁.trans hAgree₂, hσ₁⟩
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.equivalentOver.subset
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X Y : Set ν
⊢ X ⊆ Y → equivalentOver Y φ₁ φ₂ → equivalentOver X φ₁ φ₂
Tactic:
intro hSub
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X Y : Set ν
hSub : X ⊆ Y
⊢ equivalentOver Y φ₁ φ₂ → equivalentOver X φ₁ φ₂
Theorem: LeanSAT.Model.PropFun.equivalentOver.subset
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X Y : Set ν
hSub : X ⊆ Y
⊢ equivalentOver Y φ₁ φ₂ → equivalentOver X φ₁ φ₂
Tactic:
suffices ∀ φ₁ φ₂ τ, equivalentOver Y φ₁ φ₂ →
    (∃ (σ₁ : PropAssignment ν), σ₁.agreeOn X τ ∧ σ₁ ⊨ φ₁) →
    ∃ (σ₂ : PropAssignment ν), σ₂.agreeOn X τ ∧ σ₂ ⊨ φ₂ from
  fun e τ => ⟨this φ₁ φ₂ τ e, this φ₂ φ₁ τ e.symm⟩
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X Y : Set ν
hSub : X ⊆ Y
⊢ ∀ (φ₁ φ₂ : PropFun ν) (τ : PropAssignment ν),
    equivalentOver Y φ₁ φ₂ →
      (∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁) → ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Theorem: LeanSAT.Model.PropFun.equivalentOver.subset
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X Y : Set ν
hSub : X ⊆ Y
⊢ ∀ (φ₁ φ₂ : PropFun ν) (τ : PropAssignment ν),
    equivalentOver Y φ₁ φ₂ →
      (∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁) → ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Tactic:
intro φ₁ φ₂ τ e ⟨σ₁, hA, hS⟩
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X Y : Set ν
hSub : X ⊆ Y
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
e : equivalentOver Y φ₁ φ₂
σ₁ : PropAssignment ν
hA : PropAssignment.agreeOn X σ₁ τ
hS : σ₁ ⊨ φ₁
⊢ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Theorem: LeanSAT.Model.PropFun.equivalentOver.subset
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X Y : Set ν
hSub : X ⊆ Y
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
e : equivalentOver Y φ₁ φ₂
σ₁ : PropAssignment ν
hA : PropAssignment.agreeOn X σ₁ τ
hS : σ₁ ⊨ φ₁
⊢ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Tactic:
have ⟨σ₃, hA', hS'⟩ := (e σ₁).mp ⟨σ₁, σ₁.agreeOn_refl _, hS⟩
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X Y : Set ν
hSub : X ⊆ Y
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
e : equivalentOver Y φ₁ φ₂
σ₁ : PropAssignment ν
hA : PropAssignment.agreeOn X σ₁ τ
hS : σ₁ ⊨ φ₁
σ₃ : PropAssignment ν
hA' : PropAssignment.agreeOn Y σ₃ σ₁
hS' : σ₃ ⊨ φ₂
⊢ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Theorem: LeanSAT.Model.PropFun.equivalentOver.subset
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X Y : Set ν
hSub : X ⊆ Y
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
e : equivalentOver Y φ₁ φ₂
σ₁ : PropAssignment ν
hA : PropAssignment.agreeOn X σ₁ τ
hS : σ₁ ⊨ φ₁
σ₃ : PropAssignment ν
hA' : PropAssignment.agreeOn Y σ₃ σ₁
hS' : σ₃ ⊨ φ₂
⊢ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Tactic:
exact ⟨σ₃, hA'.subset hSub |>.trans hA, hS'⟩
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.equivalentOver_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X : Set ν
⊢ ↑(semVars φ₁) ⊆ X → ↑(semVars φ₂) ⊆ X → equivalentOver X φ₁ φ₂ → φ₁ = φ₂
Tactic:
suffices ∀ {φ₁ φ₂} {τ : PropAssignment ν}, φ₂.semVars ⊆ X →
    equivalentOver X φ₁ φ₂ → τ ⊨ φ₁ → τ ⊨ φ₂ by
  intro h₁ h₂ e
  ext τ
  exact ⟨this h₂ e, this h₁ e.symm⟩
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X : Set ν
⊢ ∀ {φ₁ φ₂ : PropFun ν} {τ : PropAssignment ν}, ↑(semVars φ₂) ⊆ X → equivalentOver X φ₁ φ₂ → τ ⊨ φ₁ → τ ⊨ φ₂
Theorem: LeanSAT.Model.PropFun.equivalentOver_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X : Set ν
⊢ ∀ {φ₁ φ₂ : PropFun ν} {τ : PropAssignment ν}, ↑(semVars φ₂) ⊆ X → equivalentOver X φ₁ φ₂ → τ ⊨ φ₁ → τ ⊨ φ₂
Tactic:
intro φ₁ φ₂ τ h₂ e h
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X : Set ν
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
h : τ ⊨ φ₁
⊢ τ ⊨ φ₂
Theorem: LeanSAT.Model.PropFun.equivalentOver_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X : Set ν
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
h : τ ⊨ φ₁
⊢ τ ⊨ φ₂
Tactic:
have ⟨σ₁, hA, hS⟩ := (e τ).mp ⟨τ, τ.agreeOn_refl _, h⟩
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X : Set ν
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
h : τ ⊨ φ₁
σ₁ : PropAssignment ν
hA : PropAssignment.agreeOn X σ₁ τ
hS : σ₁ ⊨ φ₂
⊢ τ ⊨ φ₂
Theorem: LeanSAT.Model.PropFun.equivalentOver_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X : Set ν
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
h : τ ⊨ φ₁
σ₁ : PropAssignment ν
hA : PropAssignment.agreeOn X σ₁ τ
hS : σ₁ ⊨ φ₂
⊢ τ ⊨ φ₂
Tactic:
have : σ₁ ⊨ φ₂ ↔ τ ⊨ φ₂ := agreeOn_semVars (hA.subset h₂)
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X : Set ν
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
h : τ ⊨ φ₁
σ₁ : PropAssignment ν
hA : PropAssignment.agreeOn X σ₁ τ
hS : σ₁ ⊨ φ₂
this : σ₁ ⊨ φ₂ ↔ τ ⊨ φ₂
⊢ τ ⊨ φ₂
Theorem: LeanSAT.Model.PropFun.equivalentOver_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X : Set ν
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
h : τ ⊨ φ₁
σ₁ : PropAssignment ν
hA : PropAssignment.agreeOn X σ₁ τ
hS : σ₁ ⊨ φ₂
this : σ₁ ⊨ φ₂ ↔ τ ⊨ φ₂
⊢ τ ⊨ φ₂
Tactic:
exact this.mp hS
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.equivalentOver_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X : Set ν
this : ∀ {φ₁ φ₂ : PropFun ν} {τ : PropAssignment ν}, ↑(semVars φ₂) ⊆ X → equivalentOver X φ₁ φ₂ → τ ⊨ φ₁ → τ ⊨ φ₂
⊢ ↑(semVars φ₁) ⊆ X → ↑(semVars φ₂) ⊆ X → equivalentOver X φ₁ φ₂ → φ₁ = φ₂
Tactic:
intro h₁ h₂ e
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X : Set ν
this : ∀ {φ₁ φ₂ : PropFun ν} {τ : PropAssignment ν}, ↑(semVars φ₂) ⊆ X → equivalentOver X φ₁ φ₂ → τ ⊨ φ₁ → τ ⊨ φ₂
h₁ : ↑(semVars φ₁) ⊆ X
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
⊢ φ₁ = φ₂
Theorem: LeanSAT.Model.PropFun.equivalentOver_semVars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X : Set ν
this : ∀ {φ₁ φ₂ : PropFun ν} {τ : PropAssignment ν}, ↑(semVars φ₂) ⊆ X → equivalentOver X φ₁ φ₂ → τ ⊨ φ₁ → τ ⊨ φ₂
h₁ : ↑(semVars φ₁) ⊆ X
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
⊢ φ₁ = φ₂
Tactic:
ext τ
Proof state after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X : Set ν
this : ∀ {φ₁ φ₂ : PropFun ν} {τ : PropAssignment ν}, ↑(semVars φ₂) ⊆ X → equivalentOver X φ₁ φ₂ → τ ⊨ φ₁ → τ ⊨ φ₂
h₁ : ↑(semVars φ₁) ⊆ X
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
τ : PropAssignment ν
⊢ τ ⊨ φ₁ ↔ τ ⊨ φ₂
Theorem: LeanSAT.Model.PropFun.equivalentOver_semVars
Proof state before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X : Set ν
this : ∀ {φ₁ φ₂ : PropFun ν} {τ : PropAssignment ν}, ↑(semVars φ₂) ⊆ X → equivalentOver X φ₁ φ₂ → τ ⊨ φ₁ → τ ⊨ φ₂
h₁ : ↑(semVars φ₁) ⊆ X
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
τ : PropAssignment ν
⊢ τ ⊨ φ₁ ↔ τ ⊨ φ₂
Tactic:
exact ⟨this h₂ e, this h₁ e.symm⟩
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.hasUniqueExtension_refl
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ : PropFun ν
⊢ hasUniqueExtension X X φ
Tactic:
simp [hasUniqueExtension]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.semVars_subset_vars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
⊢ PropFun.semVars ⟦φ⟧ ⊆ vars φ
Tactic:
simp only [PropFun.semVars, Set.Finite.toFinset_subset]
Proof state after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
⊢ LeanSAT.Model.PropFun.semVars' ⟦φ⟧ ⊆ ↑(vars φ)
Theorem: LeanSAT.Model.PropForm.semVars_subset_vars
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
⊢ LeanSAT.Model.PropFun.semVars' ⟦φ⟧ ⊆ ↑(vars φ)
Tactic:
exact PropFun.semVars'_subset_vars φ
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_exists
Proof state before:
ν' : Type u_2
inst✝ : Fintype ν'
ν : Type u_1
φ : PropFun ν
f : PropAssignment ν → PropAssignment ν'
τ : PropAssignment ν'
⊢ τ ⊨ existsAssn f φ ↔ ∃ σ, σ ⊨ φ ∧ τ = f σ
Tactic:
simp [existsAssn]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_existsInv
Proof state before:
ν' : Type u_2
inst✝ : Fintype ν'
ν : Type u_1
f : ν' → ν
φ : PropFun ν
τ : PropAssignment ν'
⊢ τ ⊨ existsInv f φ ↔ ∃ σ, σ ⊨ φ ∧ τ = PropAssignment.map f σ
Tactic:
simp [existsInv]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.existsInv_existsInv
Proof state before:
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
⊢ existsInv f (existsInv g φ) = existsInv (g ∘ f) φ
Tactic:
ext τ
Proof state after:
case a
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
τ : PropAssignment ν''
⊢ τ ⊨ existsInv f (existsInv g φ) ↔ τ ⊨ existsInv (g ∘ f) φ
Theorem: LeanSAT.Model.PropFun.existsInv_existsInv
Proof state before:
case a
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
τ : PropAssignment ν''
⊢ τ ⊨ existsInv f (existsInv g φ) ↔ τ ⊨ existsInv (g ∘ f) φ
Tactic:
simp
Proof state after:
case a
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
τ : PropAssignment ν''
⊢ (∃ σ, (∃ σ_1, σ_1 ⊨ φ ∧ σ = PropAssignment.map g σ_1) ∧ τ = PropAssignment.map f σ) ↔
    ∃ σ, σ ⊨ φ ∧ τ = PropAssignment.map (g ∘ f) σ
Theorem: LeanSAT.Model.PropFun.existsInv_existsInv
Proof state before:
case a
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
τ : PropAssignment ν''
⊢ (∃ σ, (∃ σ_1, σ_1 ⊨ φ ∧ σ = PropAssignment.map g σ_1) ∧ τ = PropAssignment.map f σ) ↔
    ∃ σ, σ ⊨ φ ∧ τ = PropAssignment.map (g ∘ f) σ
Tactic:
constructor
Proof state after:
case a.mp
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
τ : PropAssignment ν''
⊢ (∃ σ, (∃ σ_1, σ_1 ⊨ φ ∧ σ = PropAssignment.map g σ_1) ∧ τ = PropAssignment.map f σ) →
    ∃ σ, σ ⊨ φ ∧ τ = PropAssignment.map (g ∘ f) σ

case a.mpr
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
τ : PropAssignment ν''
⊢ (∃ σ, σ ⊨ φ ∧ τ = PropAssignment.map (g ∘ f) σ) →
    ∃ σ, (∃ σ_1, σ_1 ⊨ φ ∧ σ = PropAssignment.map g σ_1) ∧ τ = PropAssignment.map f σ
Theorem: LeanSAT.Model.PropFun.existsInv_existsInv
Proof state before:
case a.mp
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
τ : PropAssignment ν''
⊢ (∃ σ, (∃ σ_1, σ_1 ⊨ φ ∧ σ = PropAssignment.map g σ_1) ∧ τ = PropAssignment.map f σ) →
    ∃ σ, σ ⊨ φ ∧ τ = PropAssignment.map (g ∘ f) σ
Tactic:
rintro ⟨_, ⟨σ,h,rfl⟩, rfl⟩
Proof state after:
case a.mp.intro.intro.intro.intro
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ ∃ σ_1, σ_1 ⊨ φ ∧ PropAssignment.map f (PropAssignment.map g σ) = PropAssignment.map (g ∘ f) σ_1
Theorem: LeanSAT.Model.PropFun.existsInv_existsInv
Proof state before:
case a.mp.intro.intro.intro.intro
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ ∃ σ_1, σ_1 ⊨ φ ∧ PropAssignment.map f (PropAssignment.map g σ) = PropAssignment.map (g ∘ f) σ_1
Tactic:
use σ
Proof state after:
case h
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ σ ⊨ φ ∧ PropAssignment.map f (PropAssignment.map g σ) = PropAssignment.map (g ∘ f) σ
Theorem: LeanSAT.Model.PropFun.existsInv_existsInv
Proof state before:
case h
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ σ ⊨ φ ∧ PropAssignment.map f (PropAssignment.map g σ) = PropAssignment.map (g ∘ f) σ
Tactic:
simp [*, PropAssignment.map]
Proof state after:
case h
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ (σ ∘ g) ∘ f = σ ∘ g ∘ f
Theorem: LeanSAT.Model.PropFun.existsInv_existsInv
Proof state before:
case h
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ (σ ∘ g) ∘ f = σ ∘ g ∘ f
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.existsInv_existsInv
Proof state before:
case a.mpr
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
τ : PropAssignment ν''
⊢ (∃ σ, σ ⊨ φ ∧ τ = PropAssignment.map (g ∘ f) σ) →
    ∃ σ, (∃ σ_1, σ_1 ⊨ φ ∧ σ = PropAssignment.map g σ_1) ∧ τ = PropAssignment.map f σ
Tactic:
rintro ⟨σ,h,rfl⟩
Proof state after:
case a.mpr.intro.intro
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ ∃ σ_1, (∃ σ, σ ⊨ φ ∧ σ_1 = PropAssignment.map g σ) ∧ PropAssignment.map (g ∘ f) σ = PropAssignment.map f σ_1
Theorem: LeanSAT.Model.PropFun.existsInv_existsInv
Proof state before:
case a.mpr.intro.intro
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ ∃ σ_1, (∃ σ, σ ⊨ φ ∧ σ_1 = PropAssignment.map g σ) ∧ PropAssignment.map (g ∘ f) σ = PropAssignment.map f σ_1
Tactic:
use σ.map g
Proof state after:
case h
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ (∃ σ_1, σ_1 ⊨ φ ∧ PropAssignment.map g σ = PropAssignment.map g σ_1) ∧
    PropAssignment.map (g ∘ f) σ = PropAssignment.map f (PropAssignment.map g σ)
Theorem: LeanSAT.Model.PropFun.existsInv_existsInv
Proof state before:
case h
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ (∃ σ_1, σ_1 ⊨ φ ∧ PropAssignment.map g σ = PropAssignment.map g σ_1) ∧
    PropAssignment.map (g ∘ f) σ = PropAssignment.map f (PropAssignment.map g σ)
Tactic:
simp [*, PropAssignment.map, Function.comp]
Proof state after:
case h
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ ∃ σ_1, σ_1 ⊨ φ ∧ (fun x => σ (g x)) = fun x => σ_1 (g x)
Theorem: LeanSAT.Model.PropFun.existsInv_existsInv
Proof state before:
case h
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ ∃ σ_1, σ_1 ⊨ φ ∧ (fun x => σ (g x)) = fun x => σ_1 (g x)
Tactic:
use σ
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_forallAssn
Proof state before:
ν' : Type u_2
inst✝ : Fintype ν'
ν : Type u_1
φ : PropFun ν
f : PropAssignment ν → PropAssignment ν'
τ : PropAssignment ν'
⊢ τ ⊨ forallAssn f φ ↔ ∀ (σ : PropAssignment ν), σ ⊨ φ → τ = f σ
Tactic:
simp [forallAssn]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_forallInv
Proof state before:
ν' : Type u_2
inst✝ : Fintype ν'
ν : Type u_1
f : ν' → ν
φ : PropFun ν
τ : PropAssignment ν'
⊢ τ ⊨ forallInv f φ ↔ ∀ (σ : PropAssignment ν), σ ⊨ φ → τ = PropAssignment.map f σ
Tactic:
simp [forallInv]
Proof state after:
no goals
Theorem: LeanSAT.LitVar.satisfies_iff
Proof state before:
L : Type u
ν : Type v
inst✝ : LitVar L ν
τ : PropAssignment ν
l : L
⊢ τ ⊨ toPropFun l ↔ τ (toVar l) = polarity l
Tactic:
dsimp [toPropFun, polarity]
Proof state after:
L : Type u
ν : Type v
inst✝ : LitVar L ν
τ : PropAssignment ν
l : L
⊢ (τ ⊨ if polarity l = true then var (toVar l) else (var (toVar l))ᶜ) ↔ τ (toVar l) = polarity l
Theorem: LeanSAT.LitVar.satisfies_iff
Proof state before:
L : Type u
ν : Type v
inst✝ : LitVar L ν
τ : PropAssignment ν
l : L
⊢ (τ ⊨ if polarity l = true then var (toVar l) else (var (toVar l))ᶜ) ↔ τ (toVar l) = polarity l
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.LitVar.var_mkLit
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
x : ν
p : Bool
⊢ toVar (mkLit L x p) = x
Tactic:
dsimp [mkLit]
Proof state after:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
x : ν
p : Bool
⊢ toVar (if p = true then mkPos x else mkNeg x) = x
Theorem: LeanSAT.LitVar.var_mkLit
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
x : ν
p : Bool
⊢ toVar (if p = true then mkPos x else mkNeg x) = x
Tactic:
split <;> simp
Proof state after:
no goals
Theorem: LeanSAT.LitVar.polarity_mkLit
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
x : ν
p : Bool
⊢ polarity (mkLit L x p) = p
Tactic:
dsimp [mkLit]
Proof state after:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
x : ν
p : Bool
⊢ polarity (if p = true then mkPos x else mkNeg x) = p
Theorem: LeanSAT.LitVar.polarity_mkLit
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
x : ν
p : Bool
⊢ polarity (if p = true then mkPos x else mkNeg x) = p
Tactic:
split <;> simp_all
Proof state after:
no goals
Theorem: LeanSAT.LitVar.eta
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) (polarity l) = l
Tactic:
ext <;> simp
Proof state after:
no goals
Theorem: LeanSAT.LitVar.eta_neg
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ (mkLit L (toVar l) !polarity l) = -l
Tactic:
ext <;> simp
Proof state after:
no goals
Theorem: LeanSAT.LitVar.mkPos_or_mkNeg
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ l = mkPos (toVar l) ∨ l = mkNeg (toVar l)
Tactic:
rw [← eta l]
Proof state after:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) (polarity l) = mkPos (toVar (mkLit L (toVar l) (polarity l))) ∨
    mkLit L (toVar l) (polarity l) = mkNeg (toVar (mkLit L (toVar l) (polarity l)))
Theorem: LeanSAT.LitVar.mkPos_or_mkNeg
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) (polarity l) = mkPos (toVar (mkLit L (toVar l) (polarity l))) ∨
    mkLit L (toVar l) (polarity l) = mkNeg (toVar (mkLit L (toVar l) (polarity l)))
Tactic:
cases polarity l
Proof state after:
case false
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) false = mkPos (toVar (mkLit L (toVar l) false)) ∨
    mkLit L (toVar l) false = mkNeg (toVar (mkLit L (toVar l) false))

case true
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) true = mkPos (toVar (mkLit L (toVar l) true)) ∨
    mkLit L (toVar l) true = mkNeg (toVar (mkLit L (toVar l) true))
Theorem: LeanSAT.LitVar.mkPos_or_mkNeg
Proof state before:
case false
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) false = mkPos (toVar (mkLit L (toVar l) false)) ∨
    mkLit L (toVar l) false = mkNeg (toVar (mkLit L (toVar l) false))

case true
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) true = mkPos (toVar (mkLit L (toVar l) true)) ∨
    mkLit L (toVar l) true = mkNeg (toVar (mkLit L (toVar l) true))
Tactic:
. apply Or.inr
  simp [mkLit]
Proof state after:
case true
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) true = mkPos (toVar (mkLit L (toVar l) true)) ∨
    mkLit L (toVar l) true = mkNeg (toVar (mkLit L (toVar l) true))
Theorem: LeanSAT.LitVar.mkPos_or_mkNeg
Proof state before:
case true
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ mkLit L (toVar l) true = mkPos (toVar (mkLit L (toVar l) true)) ∨
    mkLit L (toVar l) true = mkNeg (toVar (mkLit L (toVar l) true))
Tactic:
. apply Or.inl
  simp [mkLit]
Proof state after:
no goals