Skip to content

Commit

Permalink
rename
Browse files Browse the repository at this point in the history
  • Loading branch information
SnO2WMaN committed Dec 5, 2024
1 parent db06b20 commit 39a140a
Show file tree
Hide file tree
Showing 9 changed files with 16 additions and 15 deletions.
4 changes: 4 additions & 0 deletions LabelledSystem.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
import LabelledSystem.Basic

import LabelledSystem.Gentzen.Basic
import LabelledSystem.Gentzen.Soundness
File renamed without changes.
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import Foundation.Modal.Kripke.Basic
import ModalTableau.Basic
import LabelledSystem.Basic

namespace LO.Modal

Expand All @@ -15,7 +15,7 @@ structure SequentPart where

namespace SequentPart

def isFreshLabel (x : Label) (Γ : SequentPart) : Prop := (x ∉ Γ.fmls.map LabelledFormula.label) ∧ (∀ y, (x, y) ∉ Γ.rels) ∧ (∀ y, (y, x) ∉ Γ.rels)
@[simp] def isFreshLabel (x : Label) (Γ : SequentPart) : Prop := (x ∉ Γ.fmls.map LabelledFormula.label) ∧ (∀ y, (x, y) ∉ Γ.rels) ∧ (∀ y, (y, x) ∉ Γ.rels)

abbrev replaceLabel (σ : Label → Label) (Γ : SequentPart) : SequentPart :=
⟨Γ.fmls.map (LabelledFormula.labelReplace σ), Γ.rels.map (LabelTerm.replace σ)⟩
Expand Down Expand Up @@ -126,7 +126,7 @@ def axiomK : ⊢ᵍ ⟨⟨∅, ∅⟩, ⟨{x ∶ □(φ ➝ ψ) ➝ □φ ➝
letI y : Label := x + 1;
apply impR (Δ := ⟨_, _⟩);
apply impR;
apply boxR (y := y) (by simp [y]) (by simp [SequentPart.isFreshLabel]) (by simp [SequentPart.isFreshLabel]);
apply boxR (y := y) (by simp [y]) (by simp) (by simp);
suffices ⊢ᵍ (⟨(x ∶ □φ) ::ₘ {x ∶ □(φ ➝ ψ)}, {(x, y)}⟩ ⟹ ⟨{y ∶ ψ}, ∅⟩) by simpa;
apply boxL (Γ := ⟨_, _⟩);
suffices ⊢ᵍ (⟨(x ∶ □(φ ➝ ψ)) ::ₘ (y ∶ φ) ::ₘ {(x ∶ □φ)}, {(x, y)}⟩ ⟹ ⟨{y ∶ ψ}, ∅⟩) by
Expand Down Expand Up @@ -175,7 +175,7 @@ end Weakening

def necessitation (d : ⊢ᵍ ⟨⟨∅, ∅⟩, ⟨{x ∶ φ}, ∅⟩⟩) : ⊢ᵍ ⟨⟨∅, ∅⟩, ⟨{x ∶ □φ}, ∅⟩⟩ := by
letI y : Label := x + 1;
apply boxR (Δ := ⟨∅, ∅⟩) (y := y) (by simp [y]) (by simp [SequentPart.isFreshLabel]) (by simp [SequentPart.isFreshLabel]);
apply boxR (Δ := ⟨∅, ∅⟩) (y := y) (by simp [y]) (by simp) (by simp);
apply wkRelL';
simpa [SequentPart.replaceLabel, LabelledFormula.labelReplace, LabelReplace.specific] using replaceLabel' d (x ⧸ y);

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ModalTableau.Gentzen.Basic
import LabelledSystem.Gentzen.Basic

namespace LO.Modal.Labelled.Gentzen

Expand Down
2 changes: 1 addition & 1 deletion Main.lean
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import ModalTableau
import LabelledSystem

def main : IO Unit :=
IO.println s!"Hello, {hello}!"
4 changes: 0 additions & 4 deletions ModalTableau.lean

This file was deleted.

2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
@@ -1 +1 @@
# ModalTableau
# Labelled Systems for Modal Logic
2 changes: 1 addition & 1 deletion lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -101,5 +101,5 @@
"inputRev": "master",
"inherited": false,
"configFile": "lakefile.toml"}],
"name": "ModalTableau",
"name": "LabelledSystem",
"lakeDir": ".lake"}
7 changes: 4 additions & 3 deletions lakefile.toml
Original file line number Diff line number Diff line change
@@ -1,9 +1,10 @@
name = "ModalTableau"
name = "LabelledSystem"
version = "0.1.0"
defaultTargets = ["ModalTableau"]
defaultTargets = ["LabelledSystem"]
description = "Labelled Systems for Modal Logic"

[[lean_lib]]
name = "ModalTableau"
name = "LabelledSystem"

[[lean_exe]]
name = "modaltableau"
Expand Down

0 comments on commit 39a140a

Please sign in to comment.