From 48446179118a9786e6197075f3931e8efc60d224 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Fri, 6 Dec 2024 12:53:34 +0900 Subject: [PATCH] fix --- LabelledSystem.lean | 1 + LabelledSystem/Gentzen/Hilbert.lean | 4 ++-- LabelledSystem/Gentzen/Soundness.lean | 4 ++-- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/LabelledSystem.lean b/LabelledSystem.lean index ad1370c..7acb209 100644 --- a/LabelledSystem.lean +++ b/LabelledSystem.lean @@ -2,3 +2,4 @@ import LabelledSystem.Basic import LabelledSystem.Gentzen.Basic import LabelledSystem.Gentzen.Soundness +import LabelledSystem.Gentzen.Hilbert diff --git a/LabelledSystem/Gentzen/Hilbert.lean b/LabelledSystem/Gentzen/Hilbert.lean index 3228f71..41f617d 100644 --- a/LabelledSystem/Gentzen/Hilbert.lean +++ b/LabelledSystem/Gentzen/Hilbert.lean @@ -56,8 +56,8 @@ def axiomK : ⊢ᵍ ⟨∅, ∅⟩ ⟹ ⟨{x ∶ □(φ ➝ ψ) ➝ □φ ➝ have e : (x ∶ □(φ ➝ ψ)) ::ₘ (y ∶ φ ➝ ψ) ::ₘ (y ∶ φ) ::ₘ {x ∶ □φ} = (y ∶ φ ➝ ψ) ::ₘ {y ∶ φ, x ∶ □φ, x ∶ □(φ ➝ ψ)} := by sorry; simpa [e]; apply impL (Γ := ⟨_, _⟩); - . simpa using initFml (Γ := ⟨_, _⟩) (Δ := ⟨_, _⟩); - . simpa using initFml (Γ := ⟨_, _⟩) (Δ := ⟨_, _⟩); + . exact initFml' y φ (by simp) (by simp); + . exact initFml' y ψ (by simp) (by simp); def mdp (d₁ : ⊢ᵍ ⟨∅, ∅⟩ ⟹ ⟨{x ∶ φ ➝ ψ}, ∅⟩) (d₂ : ⊢ᵍ ⟨∅, ∅⟩ ⟹ ⟨{x ∶ φ}, ∅⟩) : ⊢ᵍ ⟨∅, ∅⟩ ⟹ ⟨{x ∶ ψ}, ∅⟩ := by simpa using cutFml (Δ₁ := ⟨∅, ∅⟩) (Δ₂ := ⟨{x ∶ ψ}, ∅⟩) d₂ $ implyRInv (Δ := ⟨∅, ∅⟩) d₁; diff --git a/LabelledSystem/Gentzen/Soundness.lean b/LabelledSystem/Gentzen/Soundness.lean index 4bf7abf..4faa41d 100644 --- a/LabelledSystem/Gentzen/Soundness.lean +++ b/LabelledSystem/Gentzen/Soundness.lean @@ -5,10 +5,10 @@ namespace LO.Modal.Labelled.Gentzen theorem soundness {S : Sequent} : ⊢ᵍ S → ∀ (M : Kripke.Model), ∀ (f : Assignment M), S.Satisfies M f := by intro d; induction d with - | axA => + | initAtom => rintro M f ⟨hΓ, hX⟩; simp_all; - | axBot => + | initBot => rintro M f ⟨hΓ, hX⟩; simp at hΓ; | @impL Γ Δ x φ ψ d₁ d₂ ih₁ ih₂ =>