internlm/Lean-Github huggingface dataset:
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:
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:
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:
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:
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:
apply orI1
Proof state after:
case a
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✝
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✝ : Γ✝ ⊢ A✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ 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✝ : Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝
Tactic:
apply orI2
Proof state after:
case a
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 : Γ✝ ⊆ Δ
⊢ Δ ⊢ 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✝ : Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝
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✝ 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: 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:
apply botE
Proof state after:
case a
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 : Γ✝ ⊆ Δ
⊢ Δ ⊢ bot
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✝ : Γ✝ ⊢ bot
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ bot
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ bot
Tactic:
solve_by_elim [insert_subset_insert]
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.ProvableFrom.insert
Proof state before:
H : Type ?u.104134
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ Insert.insert B Γ ⊢ A
Tactic:
apply weakening h
Proof state after:
H : Type ?u.104134
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ Γ ⊆ Insert.insert B Γ
Theorem: IntuitionisticPropositionalLogic.ProvableFrom.insert
Proof state before:
H : Type ?u.104134
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ Γ ⊆ Insert.insert B Γ
Tactic:
exact subset_insert B Γ
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.deduction_theorem
Proof state before:
H : Type ?u.104205
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ insert (A ⇒ B) Γ ⊢ B
Tactic:
apply impE (ax $ mem_insert _ _)
Proof state after:
H : Type ?u.104205
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ insert (A ⇒ B) Γ ⊢ A
Theorem: IntuitionisticPropositionalLogic.deduction_theorem
Proof state before:
H : Type ?u.104205
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ insert (A ⇒ B) Γ ⊢ A
Tactic:
exact h.insert
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.Provable.mp
Proof state before:
H : Type ?u.104299
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h1 : Provable (A ⇒ B)
h2 : Γ ⊢ A
⊢ Γ ⊢ B
Tactic:
apply impE _ h2
Proof state after:
H : Type ?u.104299
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h1 : Provable (A ⇒ B)
h2 : Γ ⊢ A
⊢ Γ ⊢ A ⇒ B
Theorem: IntuitionisticPropositionalLogic.Provable.mp
Proof state before:
H : Type ?u.104299
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h1 : Provable (A ⇒ B)
h2 : Γ ⊢ A
⊢ Γ ⊢ A ⇒ B
Tactic:
apply weakening h1
Proof state after:
H : Type ?u.104299
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h1 : Provable (A ⇒ B)
h2 : Γ ⊢ A
⊢ ∅ ⊆ Γ
Theorem: IntuitionisticPropositionalLogic.Provable.mp
Proof state before:
H : Type ?u.104299
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h1 : Provable (A ⇒ B)
h2 : Γ ⊢ A
⊢ ∅ ⊆ Γ
Tactic:
exact empty_subset Γ
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H : Type ?u.104354
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ Γ ⊨ A
Tactic:
induction h <;> intros H hH v c hv
Proof state after:
case ax
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝

case impI
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
a_ih✝ : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ ⇒ B✝)

case impE
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
a_ih✝¹ : Γ✝ ⊨ A✝ ⇒ B✝
a_ih✝ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v B✝

case andI
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
a_ih✝¹ : Γ✝ ⊨ A✝
a_ih✝ : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ && B✝)

case andE1
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : Γ✝ ⊨ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝

case andE2
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : Γ✝ ⊨ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v B✝

case orI1
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
a_ih✝ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ || B✝)

case orI2
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
a_ih✝ : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ || B✝)

case orE
H✝ : Type ?u.104354
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✝² : Γ✝ ⊨ A✝ || B✝
a_ih✝¹ : insert A✝ Γ✝ ⊨ C✝
a_ih✝ : insert B✝ Γ✝ ⊨ C✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v C✝

case botE
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
a_ih✝ : Γ✝ ⊨ bot
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ ⇒ B✝)
Tactic:
case impI ih =>
  simp
  apply ih
  simp
  intros B hB
  exact inf_le_of_left_le (hv B hB)
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₁ : Γ✝ ⊨ A✝ ⇒ B✝
ih₂ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v B✝
Tactic:
case impE ih₁ ih₂ =>
  specialize ih₁ hv
  simp at ih₁
  rwa [inf_eq_left.mpr (ih₂ hv)] at ih₁
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
ih₁ : Γ✝ ⊨ A✝
ih₂ : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ && B✝)
Tactic:
case andI ih₁ ih₂ => simp [ih₁ hv, ih₂ hv]
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : Γ✝ ⊨ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝
Tactic:
case andE1 ih =>
  specialize ih hv
  simp at ih
  exact ih.1
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : Γ✝ ⊨ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v B✝
Tactic:
case andE2 ih =>
  specialize ih hv
  simp at ih
  exact ih.2
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ || B✝)
Tactic:
case orI1 ih =>
  simp
  exact le_trans (ih hv) le_sup_left
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ || B✝)
Tactic:
case orI2 ih =>
  simp
  exact le_trans (ih hv) le_sup_right
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
ih : Γ✝ ⊨ bot
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝
Tactic:
case botE ih =>
  specialize ih hv
  simp at ih
  simp [ih]
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ ⇒ B✝)
Tactic:
simp
Proof state after:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ⊓ eval v A✝ ≤ eval v B✝
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ⊓ eval v A✝ ≤ eval v B✝
Tactic:
apply ih
Proof state after:
case a
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ ∀ B ∈ insert A✝ Γ✝, c ⊓ eval v A✝ ≤ eval v B
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
case a
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ ∀ B ∈ insert A✝ Γ✝, c ⊓ eval v A✝ ≤ eval v B
Tactic:
simp
Proof state after:
case a
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ ∀ a ∈ Γ✝, c ⊓ eval v A✝ ≤ eval v a
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
case a
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ ∀ a ∈ Γ✝, c ⊓ eval v A✝ ≤ eval v a
Tactic:
intros B hB
Proof state after:
case a
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B✝¹ : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
B : Formula
hB : B ∈ Γ✝
⊢ c ⊓ eval v A✝ ≤ eval v B
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
case a
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B✝¹ : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
B : Formula
hB : B ∈ Γ✝
⊢ c ⊓ eval v A✝ ≤ eval v B
Tactic:
exact inf_le_of_left_le (hv B hB)
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₁ : Γ✝ ⊨ A✝ ⇒ B✝
ih₂ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v B✝
Tactic:
specialize ih₁ hv
Proof state after:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₂ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih₁ : c ≤ eval v (A✝ ⇒ B✝)
⊢ c ≤ eval v B✝
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₂ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih₁ : c ≤ eval v (A✝ ⇒ B✝)
⊢ c ≤ eval v B✝
Tactic:
simp at ih₁
Proof state after:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₂ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih₁ : c ⊓ eval v A✝ ≤ eval v B✝
⊢ c ≤ eval v B✝
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₂ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih₁ : c ⊓ eval v A✝ ≤ eval v B✝
⊢ c ≤ eval v B✝
Tactic:
rwa [inf_eq_left.mpr (ih₂ hv)] at ih₁
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
ih₁ : Γ✝ ⊨ A✝
ih₂ : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ && B✝)
Tactic:
simp [ih₁ hv, ih₂ hv]
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : Γ✝ ⊨ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝
Tactic:
specialize ih hv
Proof state after:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v (A✝ && B✝)
⊢ c ≤ eval v A✝
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v (A✝ && B✝)
⊢ c ≤ eval v A✝
Tactic:
simp at ih
Proof state after:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v A✝ ∧ c ≤ eval v B✝
⊢ c ≤ eval v A✝
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v A✝ ∧ c ≤ eval v B✝
⊢ c ≤ eval v A✝
Tactic:
exact ih.1
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : Γ✝ ⊨ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v B✝
Tactic:
specialize ih hv
Proof state after:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v (A✝ && B✝)
⊢ c ≤ eval v B✝
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v (A✝ && B✝)
⊢ c ≤ eval v B✝
Tactic:
simp at ih
Proof state after:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v A✝ ∧ c ≤ eval v B✝
⊢ c ≤ eval v B✝
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v A✝ ∧ c ≤ eval v B✝
⊢ c ≤ eval v B✝
Tactic:
exact ih.2
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ || B✝)
Tactic:
simp
Proof state after:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝ ⊔ eval v B✝
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝ ⊔ eval v B✝
Tactic:
exact le_trans (ih hv) le_sup_left
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ || B✝)
Tactic:
simp
Proof state after:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝ ⊔ eval v B✝
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝ ⊔ eval v B✝
Tactic:
exact le_trans (ih hv) le_sup_right
Proof state after:
no goals