internlm/Lean-Github huggingface dataset:
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
case a
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝
Tactic:
solve_by_elim
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ C✝ : Formula
a✝² : Γ✝ ⊢ A✝ || B✝
a✝¹ : insert A✝ Γ✝ ⊢ C✝
a✝ : insert B✝ Γ✝ ⊢ C✝
ih₁ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ || B✝
ih₂ : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ C✝
ih₃ : ∀ {Δ : Set Formula}, insert B✝ Γ✝ ⊆ Δ → Δ ⊢ C✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ C✝
Tactic:
apply orE <;> solve_by_elim [insert_subset_insert]
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
ih : ∀ {Δ : Set Formula}, insert (~A✝) Γ✝ ⊆ Δ → Δ ⊢ ⊥
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
apply botC
Proof state after:
case a
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
ih : ∀ {Δ : Set Formula}, insert (~A✝) Γ✝ ⊆ Δ → Δ ⊢ ⊥
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ insert (~A✝) Δ ⊢ ⊥
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
case a
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
ih : ∀ {Δ : Set Formula}, insert (~A✝) Γ✝ ⊆ Δ → Δ ⊢ ⊥
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ insert (~A✝) Δ ⊢ ⊥
Tactic:
solve_by_elim [insert_subset_insert]
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.ProvableFrom.insert
Proof state before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ Insert.insert B Γ ⊢ A
Tactic:
apply weakening h
Proof state after:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ Γ ⊆ Insert.insert B Γ
Theorem: ClassicalPropositionalLogic.ProvableFrom.insert
Proof state before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ Γ ⊆ Insert.insert B Γ
Tactic:
exact subset_insert B Γ
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.deduction_theorem
Proof state before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ insert (A ⇒ B) Γ ⊢ B
Tactic:
apply impE (ax $ mem_insert _ _)
Proof state after:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ insert (A ⇒ B) Γ ⊢ A
Theorem: ClassicalPropositionalLogic.deduction_theorem
Proof state before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ insert (A ⇒ B) Γ ⊢ A
Tactic:
exact h.insert
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.Provable.mp
Proof state before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h1 : Provable (A ⇒ B)
h2 : Γ ⊢ A
⊢ Γ ⊢ B
Tactic:
apply impE _ h2
Proof state after:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h1 : Provable (A ⇒ B)
h2 : Γ ⊢ A
⊢ Γ ⊢ A ⇒ B
Theorem: ClassicalPropositionalLogic.Provable.mp
Proof state before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h1 : Provable (A ⇒ B)
h2 : Γ ⊢ A
⊢ Γ ⊢ A ⇒ B
Tactic:
apply weakening h1
Proof state after:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h1 : Provable (A ⇒ B)
h2 : Γ ⊢ A
⊢ ∅ ⊆ Γ
Theorem: ClassicalPropositionalLogic.Provable.mp
Proof state before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h1 : Provable (A ⇒ B)
h2 : Γ ⊢ A
⊢ ∅ ⊆ Γ
Tactic:
exact empty_subset Γ
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ Γ ⊨ A
Tactic:
induction h <;> intros v hv
Proof state after:
case ax
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝

case impI
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
a_ih✝ : insert A✝ Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ ⇒ B✝)

case impE
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
a_ih✝¹ : Γ✝ ⊨ A✝ ⇒ B✝
a_ih✝ : Γ✝ ⊨ A✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝

case andI
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
a_ih✝¹ : Γ✝ ⊨ A✝
a_ih✝ : Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ && B✝)

case andE1
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝

case andE2
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝

case orI1
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
a_ih✝ : Γ✝ ⊨ A✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ || B✝)

case orI2
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
a_ih✝ : Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ || B✝)

case orE
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ C✝ : Formula
a✝² : Γ✝ ⊢ A✝ || B✝
a✝¹ : insert A✝ Γ✝ ⊢ C✝
a✝ : insert B✝ Γ✝ ⊢ C✝
a_ih✝² : Γ✝ ⊨ A✝ || B✝
a_ih✝¹ : insert A✝ Γ✝ ⊨ C✝
a_ih✝ : insert B✝ Γ✝ ⊨ C✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v C✝

case botC
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
a_ih✝ : insert (~A✝) Γ✝ ⊨ ⊥
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ ⇒ B✝)
Tactic:
case impI ih => intro hA; apply ih; simp [*]
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₁ : Γ✝ ⊨ A✝ ⇒ B✝
ih₂ : Γ✝ ⊨ A✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝
Tactic:
case impE ih₁ ih₂ => exact ih₁ hv (ih₂ hv)
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
ih : insert (~A✝) Γ✝ ⊨ ⊥
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝
Tactic:
case botC ih => by_contra hA; apply ih (satisfies_insert_iff.mpr ⟨by exact hA, hv⟩)
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
ih₁ : Γ✝ ⊨ A✝
ih₂ : Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ && B✝)
Tactic:
case andI ih₁ ih₂ => exact ⟨ih₁ hv, ih₂ hv⟩
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝
Tactic:
case andE1 ih => exact (ih hv).1
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝
Tactic:
case andE2 ih => exact (ih hv).2
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : Γ✝ ⊨ A✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ || B✝)
Tactic:
case orI1 ih => exact .inl (ih hv)
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ || B✝)
Tactic:
case orI2 ih => exact .inr (ih hv)
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ C✝ : Formula
a✝² : Γ✝ ⊢ A✝ || B✝
a✝¹ : insert A✝ Γ✝ ⊢ C✝
a✝ : insert B✝ Γ✝ ⊢ C✝
ih₁ : Γ✝ ⊨ A✝ || B✝
ih₂ : insert A✝ Γ✝ ⊨ C✝
ih₃ : insert B✝ Γ✝ ⊨ C✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v C✝
Tactic:
case orE ih₁ ih₂ ih₃ => refine (ih₁ hv).elim (fun hA => ih₂ ?_) (fun hB => ih₃ ?_) <;> simp [*]
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ ⇒ B✝)
Tactic:
intro hA
Proof state after:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
hA : IsTrue v A✝
⊢ IsTrue v B✝
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
hA : IsTrue v A✝
⊢ IsTrue v B✝
Tactic:
apply ih
Proof state after:
case a
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
hA : IsTrue v A✝
⊢ Satisfies v (insert A✝ Γ✝)
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
case a
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
hA : IsTrue v A✝
⊢ Satisfies v (insert A✝ Γ✝)
Tactic:
simp [*]
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₁ : Γ✝ ⊨ A✝ ⇒ B✝
ih₂ : Γ✝ ⊨ A✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝
Tactic:
exact ih₁ hv (ih₂ hv)
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
ih : insert (~A✝) Γ✝ ⊨ ⊥
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝
Tactic:
by_contra hA
Proof state after:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
ih : insert (~A✝) Γ✝ ⊨ ⊥
v : Variable → Prop
hv : Satisfies v Γ✝
hA : ¬IsTrue v A✝
⊢ False
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
ih : insert (~A✝) Γ✝ ⊨ ⊥
v : Variable → Prop
hv : Satisfies v Γ✝
hA : ¬IsTrue v A✝
⊢ False
Tactic:
apply ih (satisfies_insert_iff.mpr ⟨by exact hA, hv⟩)
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝¹ : Formula
a✝ : insert (~A✝¹) Γ✝ ⊢ ⊥
ih : insert (~A✝¹) Γ✝ ⊨ ⊥
v : Variable → Prop
hv : Satisfies v Γ✝
hA : ¬IsTrue v A✝¹
A✝ : Formula
⊢ IsTrue v ~A✝¹
Tactic:
exact hA
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
ih₁ : Γ✝ ⊨ A✝
ih₂ : Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ && B✝)
Tactic:
exact ⟨ih₁ hv, ih₂ hv⟩
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v A✝
Tactic:
exact (ih hv).1
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : Γ✝ ⊨ A✝ && B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v B✝
Tactic:
exact (ih hv).2
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : Γ✝ ⊨ A✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ || B✝)
Tactic:
exact .inl (ih hv)
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : Γ✝ ⊨ B✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v (A✝ || B✝)
Tactic:
exact .inr (ih hv)
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v✝ : Variable → Prop
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ C✝ : Formula
a✝² : Γ✝ ⊢ A✝ || B✝
a✝¹ : insert A✝ Γ✝ ⊢ C✝
a✝ : insert B✝ Γ✝ ⊢ C✝
ih₁ : Γ✝ ⊨ A✝ || B✝
ih₂ : insert A✝ Γ✝ ⊨ C✝
ih₃ : insert B✝ Γ✝ ⊨ C✝
v : Variable → Prop
hv : Satisfies v Γ✝
⊢ IsTrue v C✝
Tactic:
refine (ih₁ hv).elim (fun hA => ih₂ ?_) (fun hB => ih₃ ?_) <;> simp [*]
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.valid_of_provable
Proof state before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Provable A
⊢ Valid A
Tactic:
exact soundness_theorem h
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.isTrue_top
Proof state before:
v : Variable → Prop
A B : Formula
⊢ IsTrue v ⊤
Tactic:
sorry
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.isTrue_equiv
Proof state before:
v : Variable → Prop
A B : Formula
⊢ IsTrue v (A ⇔ B) ↔ (IsTrue v A ↔ IsTrue v B)
Tactic:
sorry
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
h2 : Γ ⊆ Δ
⊢ Δ ⊢ A
Tactic:
sorry
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.ProvableFrom.insert
Proof state before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ Insert.insert B Γ ⊢ A
Tactic:
sorry
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.deduction_theorem
Proof state before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ insert (A ⇒ B) Γ ⊢ B
Tactic:
sorry
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.Provable.mp
Proof state before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h1 : Provable (A ⇒ B)
h2 : Γ ⊢ A
⊢ Γ ⊢ B
Tactic:
sorry
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.soundness_theorem
Proof state before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ Γ ⊨ A
Tactic:
sorry
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.valid_of_provable
Proof state before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Provable A
⊢ Valid A
Tactic:
sorry
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.eval_neg
Proof state before:
H : Type u_1
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
⊢ eval v ~A = (eval v A)ᶜ
Tactic:
simp
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.eval_top
Proof state before:
H : Type u_1
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
⊢ eval v top = ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.isTrue_equiv
Proof state before:
H : Type u_1
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
⊢ eval v (A ⇔ B) = (eval v A ⇨ eval v B) ⊓ (eval v B ⇨ eval v A)
Tactic:
simp
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.weakening
Proof state before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
h2 : Γ ⊆ Δ
⊢ Δ ⊢ A
Tactic:
induction h generalizing Δ
Proof state after:
case ax
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝

case impI
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
a_ih✝ : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ ⇒ B✝

case impE
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
a_ih✝¹ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ ⇒ B✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝

case andI
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
a_ih✝¹ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ && B✝

case andE1
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ && B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝

case andE2
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ && B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝

case orI1
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝

case orI2
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝

case orE
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ C✝ : Formula
a✝² : Γ✝ ⊢ A✝ || B✝
a✝¹ : insert A✝ Γ✝ ⊢ C✝
a✝ : insert B✝ Γ✝ ⊢ C✝
a_ih✝² : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ || B✝
a_ih✝¹ : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ C✝
a_ih✝ : ∀ {Δ : Set Formula}, insert B✝ Γ✝ ⊆ Δ → Δ ⊢ C✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ C✝

case botE
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ bot
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Theorem: IntuitionisticPropositionalLogic.weakening
Proof state before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
case ax => apply ax; solve_by_elim
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.weakening
Proof state before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ ⇒ B✝
Tactic:
case impI ih => apply impI; solve_by_elim [insert_subset_insert]
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.weakening
Proof state before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₁ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ ⇒ B✝
ih₂ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝
Tactic:
case impE ih₁ ih₂ => apply impE <;> solve_by_elim
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.weakening
Proof state before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
ih₁ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
ih₂ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ && B✝
Tactic:
case andI ih₁ ih₂ => apply andI <;> solve_by_elim
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.weakening
Proof state before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ && B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
case andE1 ih => apply andE1 <;> solve_by_elim
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.weakening
Proof state before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ && B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝
Tactic:
case andE2 ih => apply andE2 <;> solve_by_elim
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.weakening
Proof state before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝
Tactic:
case orI1 ih => apply orI1; solve_by_elim
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.weakening
Proof state before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝
Tactic:
case orI2 ih => apply orI2; solve_by_elim
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.weakening
Proof state before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ C✝ : Formula
a✝² : Γ✝ ⊢ A✝ || B✝
a✝¹ : insert A✝ Γ✝ ⊢ C✝
a✝ : insert B✝ Γ✝ ⊢ C✝
ih₁ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ || B✝
ih₂ : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ C✝
ih₃ : ∀ {Δ : Set Formula}, insert B✝ Γ✝ ⊆ Δ → Δ ⊢ C✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ C✝
Tactic:
case orE ih₁ ih₂ ih₃ => apply orE <;> solve_by_elim [insert_subset_insert]
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.weakening
Proof state before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ bot
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
case botE ih => apply botE; solve_by_elim [insert_subset_insert]
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.weakening
Proof state before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
apply ax
Proof state after:
case a
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ A✝ ∈ Δ
Theorem: IntuitionisticPropositionalLogic.weakening
Proof state before:
case a
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ A✝ ∈ Δ
Tactic:
solve_by_elim
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.weakening
Proof state before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ ⇒ B✝
Tactic:
apply impI
Proof state after:
case a
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ insert A✝ Δ ⊢ B✝
Theorem: IntuitionisticPropositionalLogic.weakening
Proof state before:
case a
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ insert A✝ Δ ⊢ B✝
Tactic:
solve_by_elim [insert_subset_insert]
Proof state after:
no goals