internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.trivTranslated_of_K4
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐊𝟒 ⊢! p → 𝐂𝐥 ⊢! (pᵀᴾ) ⋯
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐊𝟒 ⊢! p
⊢ 𝐂𝐥 ⊢! (pᵀᴾ) ⋯
Theorem: LO.Modal.Standard.trivTranslated_of_K4
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐊𝟒 ⊢! p
⊢ 𝐂𝐥 ⊢! (pᵀᴾ) ⋯
Tactic:
apply iff_Triv_classical.mp
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐊𝟒 ⊢! p
⊢ 𝐓𝐫𝐢𝐯 ⊢! p
Theorem: LO.Modal.Standard.trivTranslated_of_K4
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐊𝟒 ⊢! p
⊢ 𝐓𝐫𝐢𝐯 ⊢! p
Tactic:
exact System.reducible_iff.mp reducible_K4_Triv h
Proof state after:
no goals
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐆𝐋 ⊢! p → 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐆𝐋 ⊢! p
⊢ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐆𝐋 ⊢! p
⊢ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
Tactic:
induction h.some using Deduction.inducition_with_nec with
  | hMaxm a =>
    rcases a with (hK | hVer)
    . obtain ⟨_, _, e⟩ := hK; subst_vars; dsimp only [Axioms.K, VerTranslation, toPropFormula]; apply imply₁!;
    . obtain ⟨_, e⟩ := hVer; subst_vars; dsimp [Axioms.Ver, VerTranslation, toPropFormula]; apply imp_id!;
  | hMdp h₁ h₂ ih₁ ih₂ =>
    dsimp [VerTranslation, toPropFormula] at ih₁ ih₂;
    exact (ih₁ ⟨h₁⟩) ⨀ (ih₂ ⟨h₂⟩);
  | hNec => dsimp [toPropFormula]; exact verum!;
  | _ =>
    dsimp [VerTranslation, toPropFormula];
    try first
    | apply verum!;
    | apply imply₁!;
    | apply imply₂!;
    | apply conj₁!;
    | apply conj₂!;
    | apply conj₃!;
    | apply disj₁!;
    | apply disj₂!;
    | apply disj₃!;
    | apply dne!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a : p✝ ∈ Ax(𝐆𝐋)
h : 𝐆𝐋 ⊢! p✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Tactic:
rcases a with (hK | hVer)
Proof state after:
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
hK : p✝ ∈ 𝗞
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
hVer : p✝ ∈ 𝗟
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
hK : p✝ ∈ 𝗞
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
hVer : p✝ ∈ 𝗟
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Tactic:
. obtain ⟨_, _, e⟩ := hK; subst_vars; dsimp only [Axioms.K, VerTranslation, toPropFormula]; apply imply₁!;
Proof state after:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
hVer : p✝ ∈ 𝗟
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
hVer : p✝ ∈ 𝗟
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Tactic:
. obtain ⟨_, e⟩ := hVer; subst_vars; dsimp [Axioms.Ver, VerTranslation, toPropFormula]; apply imp_id!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hMaxm.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
hK : p✝ ∈ 𝗞
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Tactic:
obtain ⟨_, _, e⟩ := hK
Proof state after:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Tactic:
subst_vars
Proof state after:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐆𝐋 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐂𝐥 ⊢! (Axioms.K w✝¹ w✝ⱽᴾ) ⋯
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐆𝐋 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐂𝐥 ⊢! (Axioms.K w✝¹ w✝ⱽᴾ) ⋯
Tactic:
dsimp only [Axioms.K, VerTranslation, toPropFormula]
Proof state after:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐆𝐋 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐂𝐥 ⊢! ⊤ ⟶ ⊤ ⟶ ⊤
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hMaxm.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐆𝐋 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐂𝐥 ⊢! ⊤ ⟶ ⊤ ⟶ ⊤
Tactic:
apply imply₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
hVer : p✝ ∈ 𝗟
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Tactic:
obtain ⟨_, e⟩ := hVer
Proof state after:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
w✝ : Formula α
e : Axioms.L w✝ = p✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! p✝
w✝ : Formula α
e : Axioms.L w✝ = p✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
Tactic:
subst_vars
Proof state after:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐆𝐋 ⊢! Axioms.L w✝
⊢ 𝐂𝐥 ⊢! (Axioms.L w✝ⱽᴾ) ⋯
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐆𝐋 ⊢! Axioms.L w✝
⊢ 𝐂𝐥 ⊢! (Axioms.L w✝ⱽᴾ) ⋯
Tactic:
dsimp [Axioms.Ver, VerTranslation, toPropFormula]
Proof state after:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐆𝐋 ⊢! Axioms.L w✝
⊢ 𝐂𝐥 ⊢! ⊤ ⟶ ⊤
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐆𝐋 ⊢! Axioms.L w✝
⊢ 𝐂𝐥 ⊢! ⊤ ⟶ ⊤
Tactic:
apply imp_id!
Proof state after:
no goals
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hMdp
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h₁ : 𝐆𝐋 ⊢ p✝ ⟶ q✝
h₂ : 𝐆𝐋 ⊢ p✝
ih₁ : 𝐆𝐋 ⊢! p✝ ⟶ q✝ → 𝐂𝐥 ⊢! ((p✝ ⟶ q✝)ⱽᴾ) ⋯
ih₂ : 𝐆𝐋 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐆𝐋 ⊢! q✝
⊢ 𝐂𝐥 ⊢! (q✝ⱽᴾ) ⋯
Tactic:
dsimp [VerTranslation, toPropFormula] at ih₁ ih₂
Proof state after:
case hMdp
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h₁ : 𝐆𝐋 ⊢ p✝ ⟶ q✝
h₂ : 𝐆𝐋 ⊢ p✝
ih₁ : 𝐆𝐋 ⊢! p✝ ⟶ q✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯ ⟶ (q✝ⱽᴾ) ⋯
ih₂ : 𝐆𝐋 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐆𝐋 ⊢! q✝
⊢ 𝐂𝐥 ⊢! (q✝ⱽᴾ) ⋯
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hMdp
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h₁ : 𝐆𝐋 ⊢ p✝ ⟶ q✝
h₂ : 𝐆𝐋 ⊢ p✝
ih₁ : 𝐆𝐋 ⊢! p✝ ⟶ q✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯ ⟶ (q✝ⱽᴾ) ⋯
ih₂ : 𝐆𝐋 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐆𝐋 ⊢! q✝
⊢ 𝐂𝐥 ⊢! (q✝ⱽᴾ) ⋯
Tactic:
exact (ih₁ ⟨h₁⟩) ⨀ (ih₂ ⟨h₂⟩)
Proof state after:
no goals
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp✝ : 𝐆𝐋 ⊢ p✝
a✝ : 𝐆𝐋 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐆𝐋 ⊢! □p✝
⊢ 𝐂𝐥 ⊢! ((□p✝)ⱽᴾ) ⋯
Tactic:
dsimp [toPropFormula]
Proof state after:
case hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp✝ : 𝐆𝐋 ⊢ p✝
a✝ : 𝐆𝐋 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐆𝐋 ⊢! □p✝
⊢ 𝐂𝐥 ⊢! ⊤
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp✝ : 𝐆𝐋 ⊢ p✝
a✝ : 𝐆𝐋 ⊢! p✝ → 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯
h : 𝐆𝐋 ⊢! □p✝
⊢ 𝐂𝐥 ⊢! ⊤
Tactic:
exact verum!
Proof state after:
no goals
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! ((~~p✝ ⟶ p✝)ⱽᴾ) ⋯
Tactic:
dsimp [VerTranslation, toPropFormula]
Proof state after:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (((p✝ⱽᴾ) ⋯ ⟶ ⊥) ⟶ ⊥) ⟶ (p✝ⱽᴾ) ⋯
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (((p✝ⱽᴾ) ⋯ ⟶ ⊥) ⟶ ⊥) ⟶ (p✝ⱽᴾ) ⋯
Tactic:
try first
| apply verum!;
| apply imply₁!;
| apply imply₂!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
| apply dne!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (((p✝ⱽᴾ) ⋯ ⟶ ⊥) ⟶ ⊥) ⟶ (p✝ⱽᴾ) ⋯
Tactic:
first
| apply verum!;
| apply imply₁!;
| apply imply₂!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
| apply dne!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hVerum
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐆𝐋 ⊢! ⊤
⊢ 𝐂𝐥 ⊢! ⊤
Tactic:
apply verum!
Proof state after:
no goals
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hImply₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐆𝐋 ⊢! p✝ ⟶ q✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯ ⟶ (q✝ⱽᴾ) ⋯ ⟶ (p✝ⱽᴾ) ⋯
Tactic:
apply imply₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hImply₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ r✝ : Formula α
h : 𝐆𝐋 ⊢! (p✝ ⟶ q✝ ⟶ r✝) ⟶ (p✝ ⟶ q✝) ⟶ p✝ ⟶ r✝
⊢ 𝐂𝐥 ⊢! ((p✝ⱽᴾ) ⋯ ⟶ (q✝ⱽᴾ) ⋯ ⟶ (r✝ⱽᴾ) ⋯) ⟶ ((p✝ⱽᴾ) ⋯ ⟶ (q✝ⱽᴾ) ⋯) ⟶ (p✝ⱽᴾ) ⋯ ⟶ (r✝ⱽᴾ) ⋯
Tactic:
apply imply₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hConj₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐆𝐋 ⊢! p✝ ⋏ q✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯ ⋏ (q✝ⱽᴾ) ⋯ ⟶ (p✝ⱽᴾ) ⋯
Tactic:
apply conj₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hConj₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐆𝐋 ⊢! p✝ ⋏ q✝ ⟶ q✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯ ⋏ (q✝ⱽᴾ) ⋯ ⟶ (q✝ⱽᴾ) ⋯
Tactic:
apply conj₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hConj₃
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐆𝐋 ⊢! p✝ ⟶ q✝ ⟶ p✝ ⋏ q✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯ ⟶ (q✝ⱽᴾ) ⋯ ⟶ (p✝ⱽᴾ) ⋯ ⋏ (q✝ⱽᴾ) ⋯
Tactic:
apply conj₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hDisj₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐆𝐋 ⊢! p✝ ⟶ p✝ ⋎ q✝
⊢ 𝐂𝐥 ⊢! (p✝ⱽᴾ) ⋯ ⟶ (p✝ⱽᴾ) ⋯ ⋎ (q✝ⱽᴾ) ⋯
Tactic:
apply disj₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hDisj₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐆𝐋 ⊢! q✝ ⟶ p✝ ⋎ q✝
⊢ 𝐂𝐥 ⊢! (q✝ⱽᴾ) ⋯ ⟶ (p✝ⱽᴾ) ⋯ ⋎ (q✝ⱽᴾ) ⋯
Tactic:
apply disj₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hDisj₃
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ r✝ : Formula α
h : 𝐆𝐋 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
⊢ 𝐂𝐥 ⊢! ((p✝ⱽᴾ) ⋯ ⟶ (r✝ⱽᴾ) ⋯) ⟶ ((q✝ⱽᴾ) ⋯ ⟶ (r✝ⱽᴾ) ⋯) ⟶ (p✝ⱽᴾ) ⋯ ⋎ (q✝ⱽᴾ) ⋯ ⟶ (r✝ⱽᴾ) ⋯
Tactic:
apply disj₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.verTranslated_of_GL
Proof state before:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐆𝐋 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐂𝐥 ⊢! (((p✝ⱽᴾ) ⋯ ⟶ ⊥) ⟶ ⊥) ⟶ (p✝ⱽᴾ) ⋯
Tactic:
apply dne!
Proof state after:
no goals
Theorem: LO.Modal.Standard.unprovable_AxiomL_K4
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ⊬! Axioms.L (atom default)
Tactic:
apply not_imp_not.mpr trivTranslated_of_K4
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐂𝐥 ⊢! (Axioms.L (atom default)ᵀᴾ) ⋯
Theorem: LO.Modal.Standard.unprovable_AxiomL_K4
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐂𝐥 ⊢! (Axioms.L (atom default)ᵀᴾ) ⋯
Tactic:
apply unprovable_classical_of_exists_ClassicalValuation
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ V, ¬V ⊧ (Axioms.L (atom default)ᵀᴾ) ⋯
Theorem: LO.Modal.Standard.unprovable_AxiomL_K4
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ V, ¬V ⊧ (Axioms.L (atom default)ᵀᴾ) ⋯
Tactic:
simp [Axioms.L, TrivTranslation, toPropFormula]
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ V, ¬V default
Theorem: LO.Modal.Standard.unprovable_AxiomL_K4
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ V, ¬V default
Tactic:
use (λ _ => False)
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬False
Theorem: LO.Modal.Standard.unprovable_AxiomL_K4
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬False
Tactic:
trivial
Proof state after:
no goals
Theorem: LO.Modal.Standard.strictReducible_K4_GL
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 <ₛ 𝐆𝐋
Tactic:
dsimp [StrictReducible]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ≤ₛ 𝐆𝐋 ∧ ¬𝐆𝐋 ≤ₛ 𝐊𝟒
Theorem: LO.Modal.Standard.strictReducible_K4_GL
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ≤ₛ 𝐆𝐋 ∧ ¬𝐆𝐋 ≤ₛ 𝐊𝟒
Tactic:
constructor
Proof state after:
case left
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ≤ₛ 𝐆𝐋

case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐆𝐋 ≤ₛ 𝐊𝟒
Theorem: LO.Modal.Standard.strictReducible_K4_GL
Proof state before:
case left
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ≤ₛ 𝐆𝐋

case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐆𝐋 ≤ₛ 𝐊𝟒
Tactic:
. apply reducible_K4_GL;
Proof state after:
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐆𝐋 ≤ₛ 𝐊𝟒
Theorem: LO.Modal.Standard.strictReducible_K4_GL
Proof state before:
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐆𝐋 ≤ₛ 𝐊𝟒
Tactic:
. simp [System.not_reducible_iff];
  existsi (Axioms.L (atom default))
  constructor;
  . exact axiomL!;
  . exact unprovable_AxiomL_K4;
Proof state after:
no goals
Theorem: LO.Modal.Standard.strictReducible_K4_GL
Proof state before:
case left
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ≤ₛ 𝐆𝐋
Tactic:
apply reducible_K4_GL
Proof state after:
no goals
Theorem: LO.Modal.Standard.strictReducible_K4_GL
Proof state before:
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐆𝐋 ≤ₛ 𝐊𝟒
Tactic:
simp [System.not_reducible_iff]
Proof state after:
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ f, 𝐆𝐋 ⊢! f ∧ 𝐊𝟒 ⊬! f
Theorem: LO.Modal.Standard.strictReducible_K4_GL
Proof state before:
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ f, 𝐆𝐋 ⊢! f ∧ 𝐊𝟒 ⊬! f
Tactic:
existsi (Axioms.L (atom default))
Proof state after:
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐆𝐋 ⊢! Axioms.L (atom default) ∧ 𝐊𝟒 ⊬! Axioms.L (atom default)
Theorem: LO.Modal.Standard.strictReducible_K4_GL
Proof state before:
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐆𝐋 ⊢! Axioms.L (atom default) ∧ 𝐊𝟒 ⊬! Axioms.L (atom default)
Tactic:
constructor
Proof state after:
case right.left
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐆𝐋 ⊢! Axioms.L (atom default)

case right.right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ⊬! Axioms.L (atom default)
Theorem: LO.Modal.Standard.strictReducible_K4_GL
Proof state before:
case right.left
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐆𝐋 ⊢! Axioms.L (atom default)

case right.right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ⊬! Axioms.L (atom default)
Tactic:
. exact axiomL!;
Proof state after:
case right.right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ⊬! Axioms.L (atom default)
Theorem: LO.Modal.Standard.strictReducible_K4_GL
Proof state before:
case right.right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ⊬! Axioms.L (atom default)
Tactic:
. exact unprovable_AxiomL_K4;
Proof state after:
no goals
Theorem: LO.Modal.Standard.strictReducible_K4_GL
Proof state before:
case right.left
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐆𝐋 ⊢! Axioms.L (atom default)
Tactic:
exact axiomL!
Proof state after:
no goals
Theorem: LO.Modal.Standard.strictReducible_K4_GL
Proof state before:
case right.right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ⊬! Axioms.L (atom default)
Tactic:
exact unprovable_AxiomL_K4
Proof state after:
no goals
Theorem: LO.Modal.Standard.unprovable_AxiomT_GL
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐆𝐋 ⊬! Axioms.T (atom default)
Tactic:
apply not_imp_not.mpr verTranslated_of_GL
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐂𝐥 ⊢! (Axioms.T (atom default)ⱽᴾ) ⋯
Theorem: LO.Modal.Standard.unprovable_AxiomT_GL
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐂𝐥 ⊢! (Axioms.T (atom default)ⱽᴾ) ⋯
Tactic:
apply unprovable_classical_of_exists_ClassicalValuation
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ V, ¬V ⊧ (Axioms.T (atom default)ⱽᴾ) ⋯
Theorem: LO.Modal.Standard.unprovable_AxiomT_GL
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ V, ¬V ⊧ (Axioms.T (atom default)ⱽᴾ) ⋯
Tactic:
simp [Axioms.T, VerTranslation, toPropFormula]
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ V, ¬V default
Theorem: LO.Modal.Standard.unprovable_AxiomT_GL
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ V, ¬V default
Tactic:
use (λ _ => False)
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬False
Theorem: LO.Modal.Standard.unprovable_AxiomT_GL
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬False
Tactic:
trivial
Proof state after:
no goals
Theorem: LO.Modal.Standard.notReducible_S4_GL
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐒𝟒 ≤ₛ 𝐆𝐋
Tactic:
apply System.not_reducible_iff.mpr
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ f, 𝐒𝟒 ⊢! f ∧ 𝐆𝐋 ⊬! f
Theorem: LO.Modal.Standard.notReducible_S4_GL
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ f, 𝐒𝟒 ⊢! f ∧ 𝐆𝐋 ⊬! f
Tactic:
existsi (Axioms.T (atom default))
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐒𝟒 ⊢! Axioms.T (atom default) ∧ 𝐆𝐋 ⊬! Axioms.T (atom default)
Theorem: LO.Modal.Standard.notReducible_S4_GL
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐒𝟒 ⊢! Axioms.T (atom default) ∧ 𝐆𝐋 ⊬! Axioms.T (atom default)
Tactic:
constructor
Proof state after:
case left
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐒𝟒 ⊢! Axioms.T (atom default)

case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐆𝐋 ⊬! Axioms.T (atom default)
Theorem: LO.Modal.Standard.notReducible_S4_GL
Proof state before:
case left
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐒𝟒 ⊢! Axioms.T (atom default)

case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐆𝐋 ⊬! Axioms.T (atom default)
Tactic:
. exact axiomT!;
Proof state after:
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐆𝐋 ⊬! Axioms.T (atom default)
Theorem: LO.Modal.Standard.notReducible_S4_GL
Proof state before:
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐆𝐋 ⊬! Axioms.T (atom default)
Tactic:
. exact unprovable_AxiomT_GL;
Proof state after:
no goals
Theorem: LO.Modal.Standard.notReducible_S4_GL
Proof state before:
case left
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐒𝟒 ⊢! Axioms.T (atom default)
Tactic:
exact axiomT!
Proof state after:
no goals
Theorem: LO.Modal.Standard.notReducible_S4_GL
Proof state before:
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐆𝐋 ⊬! Axioms.T (atom default)
Tactic:
exact unprovable_AxiomT_GL
Proof state after:
no goals
Theorem: Qq.List.mem_of_eq
Proof state before:
α : Type u
a b : α
l : List α
h : a = b
⊢ a ∈ b :: l
Tactic:
simp[h]
Proof state after:
no goals
Theorem: Qq.List.mem_of_mem
Proof state before:
α : Type u
a b : α
l : List α
h : a ∈ l
⊢ a ∈ b :: l
Tactic:
simp[h]
Proof state after:
no goals
Theorem: Qq.List.cases_of_mem_cons
Proof state before:
α : Type u
p : α → Prop
a a' : α
l : List α
h : a' ∈ a :: l
hl : ∀ a' ∈ l, p a'
ha : p a
⊢ p a'
Tactic:
rcases List.mem_cons.mp h with (h | h)
Proof state after:
case inl
α : Type u
p : α → Prop
a a' : α
l : List α
h✝ : a' ∈ a :: l
hl : ∀ a' ∈ l, p a'
ha : p a
h : a' = a
⊢ p a'

case inr
α : Type u
p : α → Prop
a a' : α
l : List α
h✝ : a' ∈ a :: l
hl : ∀ a' ∈ l, p a'
ha : p a
h : a' ∈ l
⊢ p a'
Theorem: Qq.List.cases_of_mem_cons
Proof state before:
case inl
α : Type u
p : α → Prop
a a' : α
l : List α
h✝ : a' ∈ a :: l
hl : ∀ a' ∈ l, p a'
ha : p a
h : a' = a
⊢ p a'
Tactic:
simpa[h]
Proof state after:
no goals
Theorem: Qq.List.cases_of_mem_cons
Proof state before:
case inr
α : Type u
p : α → Prop
a a' : α
l : List α
h✝ : a' ∈ a :: l
hl : ∀ a' ∈ l, p a'
ha : p a
h : a' ∈ l
⊢ p a'
Tactic:
exact hl _ h
Proof state after:
no goals
Theorem: Qq.compVecEmpty
Proof state before:
α : Type u
β : Type v
f : α → β
⊢ f ∘ ![] = ![]
Tactic:
simp
Proof state after:
no goals
Theorem: Qq.compVecCons
Proof state before:
α : Type u
β : Type v
f : α → β
n : ℕ
a : α
as : Fin n → α
b : β
bs : Fin n → β
hb : f a = b
hbs : f ∘ as = bs
⊢ f ∘ (a :> as) = b :> bs
Tactic:
simp[Function.comp, Matrix.comp_vecCons, hb, ←hbs]
Proof state after:
no goals
Theorem: Qq.eq_cons_app_succ_of_eq
Proof state before:
n : ℕ
α : Type u
a b : α
as : Fin n → α
i : Fin n
has : as i = b
⊢ (a :> as) i.succ = b
Tactic:
simp[has]
Proof state after:
no goals
Theorem: Qq.vecCons_assoc_eq
Proof state before:
α : Type u_1
n : ℕ
t : Fin n.succ → α
a b : α
s : Fin n → α
h : s <: b = t
⊢ (a :> s) <: b = a :> t
Tactic:
simp[←h, Matrix.vecCons_assoc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof state before:
L : Language
Δ : List (SyntacticFormula L)
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ℕ 0
M : Type u_1
s : Structure L M
ε : ℕ → M
⊢ ∃ p ∈ rel r v :: nrel r v :: Δ, (Evalfm M ε) p
Tactic:
by_cases h : s.rel r (Semiterm.valm M ![] ε ∘ v)
Proof state after:
case pos
L : Language
Δ : List (SyntacticFormula L)
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ℕ 0
M : Type u_1
s : Structure L M
ε : ℕ → M
h : Structure.rel r (Semiterm.valm M ![] ε ∘ v)
⊢ ∃ p ∈ rel r v :: nrel r v :: Δ, (Evalfm M ε) p

case neg
L : Language
Δ : List (SyntacticFormula L)
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ℕ 0
M : Type u_1
s : Structure L M
ε : ℕ → M
h : ¬Structure.rel r (Semiterm.valm M ![] ε ∘ v)
⊢ ∃ p ∈ rel r v :: nrel r v :: Δ, (Evalfm M ε) p
Theorem: LO.FirstOrder.Derivation.sound
Proof state before:
case pos
L : Language
Δ : List (SyntacticFormula L)
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ℕ 0
M : Type u_1
s : Structure L M
ε : ℕ → M
h : Structure.rel r (Semiterm.valm M ![] ε ∘ v)
⊢ ∃ p ∈ rel r v :: nrel r v :: Δ, (Evalfm M ε) p
Tactic:
exact ⟨rel r v, by simp, h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof state before:
L : Language
Δ : List (SyntacticFormula L)
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ℕ 0
M : Type u_1
s : Structure L M
ε : ℕ → M
h : Structure.rel r (Semiterm.valm M ![] ε ∘ v)
⊢ rel r v ∈ rel r v :: nrel r v :: Δ
Tactic:
simp
Proof state after:
no goals