diff --git a/LabelledSystem/Basic.lean b/LabelledSystem/Basic.lean index c3a6bfa..22b7a77 100644 --- a/LabelledSystem/Basic.lean +++ b/LabelledSystem/Basic.lean @@ -9,6 +9,9 @@ namespace Labelled abbrev Label := ℕ +abbrev PropVar := ℕ + + def Assignment (M : Kripke.Model) := Label → M.World @@ -70,7 +73,7 @@ end LabelTerm structure LabelledFormula where label : Label - formula : Formula ℕ + formula : Formula PropVar deriving DecidableEq, Repr namespace LabelledFormula @@ -83,7 +86,7 @@ notation lφ "⟦" σ "⟧" => labelReplace σ lφ section -variable {x y z : Label} {φ ψ : Formula ℕ} {σ : LabelReplace} +variable {x y z : Label} {φ ψ : Formula PropVar} {σ : LabelReplace} @[simp] lemma def_labelReplace : (x ∶ φ).labelReplace σ = (σ x ∶ φ) := by rfl @@ -106,7 +109,7 @@ protected instance semantics {M : Kripke.Model} : Semantics (LabelledFormula) (A variable {M : Kripke.Model} {f : Assignment M} variable {x y : Label} -variable {φ ψ : Formula ℕ} {xφ: LabelledFormula} +variable {φ ψ : Formula PropVar} {xφ: LabelledFormula} @[simp] protected lemma iff_models : f ⊧ (x ∶ φ) ↔ f x ⊧ φ := by tauto; @@ -121,7 +124,7 @@ end LabelledFormula structure LabelledNNFormula where label : Label - formula : NNFormula ℕ + formula : NNFormula PropVar deriving DecidableEq, Repr end Labelled diff --git a/LabelledSystem/Gentzen/Basic.lean b/LabelledSystem/Gentzen/Basic.lean index b1012a7..42e076a 100644 --- a/LabelledSystem/Gentzen/Basic.lean +++ b/LabelledSystem/Gentzen/Basic.lean @@ -61,12 +61,19 @@ lemma getFreshLabel_isFreshLabel : Γ.isFreshLabel (Γ.getFreshLabel) := by sorr lemma getFreshLabel_ne (h : (x ∶ φ) ∈ Γ.fmls) : Γ.getFreshLabel ≠ x := by rintro rfl; - have := not_include_labelledFml_of_isFreshLabel getFreshLabel_isFreshLabel (Γ := Γ) φ; - contradiction; + exact not_include_labelledFml_of_isFreshLabel getFreshLabel_isFreshLabel φ h; + +lemma getFreshLabel_rel₁ (h : (x, y) ∈ Γ.rels) : Γ.getFreshLabel ≠ x := by + rintro rfl; + exact not_include_relTerm_of_isFreshLabel₁ getFreshLabel_isFreshLabel y h; + +lemma getFreshLabel_rel₂ (h : (x, y) ∈ Γ.rels) : Γ.getFreshLabel ≠ y := by + rintro rfl; + exact not_include_relTerm_of_isFreshLabel₂ getFreshLabel_isFreshLabel x h; lemma getFreshLabel_mono (hFmls : Γ.fmls ⊆ Δ.fmls) (hRels : Γ.rels ⊆ Δ.rels) : Γ.isFreshLabel Δ.getFreshLabel := by apply of_isFreshLabel; - . suffices ∀ (φ : Formula ℕ), (Δ.getFreshLabel ∶ φ) ∉ Δ.fmls by + . suffices ∀ (φ : Formula PropVar), (Δ.getFreshLabel ∶ φ) ∉ Δ.fmls by intro φ; exact Multiset.not_mem_mono hFmls $ this φ; apply not_include_labelledFml_of_isFreshLabel; @@ -107,8 +114,8 @@ infix:50 " ⟹ " => Sequent.mk namespace Sequent -abbrev ofFormula (φ : Formula ℕ) : Sequent := ⟨∅, ∅⟩ ⟹ ⟨{0 ∶ φ}, ∅⟩ -instance : Coe (Formula ℕ) Sequent := ⟨Sequent.ofFormula⟩ +abbrev ofFormula (φ : Formula PropVar) : Sequent := ⟨∅, ∅⟩ ⟹ ⟨{0 ∶ φ}, ∅⟩ +instance : Coe (Formula PropVar) Sequent := ⟨Sequent.ofFormula⟩ abbrev replaceLabel (σ : Label → Label) (S : Sequent) : Sequent := ⟨S.Γ⟦σ⟧, S.Δ⟦σ⟧⟩ @@ -145,18 +152,36 @@ lemma getFreshLabel_isFreshLabel₂ : S.Δ.isFreshLabel (S.getFreshLabel) := get lemma getFreshLabel_ne₁ (h : (x ∶ φ) ∈ S.Γ.fmls) : S.getFreshLabel ≠ x := by rintro rfl; - have : (S.getFreshLabel ∶ φ) ∉ S.Γ.fmls := SequentPart.not_include_labelledFml_of_isFreshLabel getFreshLabel_isFreshLabel₁ φ; - contradiction; + exact SequentPart.not_include_labelledFml_of_isFreshLabel getFreshLabel_isFreshLabel₁ φ h; lemma getFreshLabel_ne₂ (h : (x ∶ φ) ∈ S.Δ.fmls) : S.getFreshLabel ≠ x := by rintro rfl; - have : (S.getFreshLabel ∶ φ) ∉ S.Δ.fmls := SequentPart.not_include_labelledFml_of_isFreshLabel getFreshLabel_isFreshLabel₂ φ; - contradiction; + exact SequentPart.not_include_labelledFml_of_isFreshLabel getFreshLabel_isFreshLabel₂ φ h; + + +lemma getFreshLabel_relΓ₁ (h : (x, y) ∈ S.Γ.rels) : S.getFreshLabel ≠ x := by + rintro rfl; + exact SequentPart.not_include_relTerm_of_isFreshLabel₁ getFreshLabel_isFreshLabel₁ y h; + +lemma getFreshLabel_relΓ₂ (h : (x, y) ∈ S.Γ.rels) : S.getFreshLabel ≠ y := by + rintro rfl; + exact SequentPart.not_include_relTerm_of_isFreshLabel₂ getFreshLabel_isFreshLabel₁ x h; + +lemma getFreshLabel_relΔ₁ (h : (x, y) ∈ S.Δ.rels) : S.getFreshLabel ≠ x := by + rintro rfl; + exact SequentPart.not_include_relTerm_of_isFreshLabel₁ getFreshLabel_isFreshLabel₂ y h; + +lemma getFreshLabel_relΔ₂ (h : (x, y) ∈ S.Δ.rels) : S.getFreshLabel ≠ y := by + rintro rfl; + exact SequentPart.not_include_relTerm_of_isFreshLabel₂ getFreshLabel_isFreshLabel₂ x h; + end end Sequent +-- variable {S : Sequent} +-- variable {Γ Γ₁ Γ₂ Δ Δ₁ Δ₂ : SequentPart} inductive Derivation : Sequent → Type _ | initAtom {S : Sequent} (x) (a) : Derivation (⟨(x ∶ atom a) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ ⟨(x ∶ atom a) ::ₘ S.Δ.fmls, S.Δ.rels⟩) @@ -183,8 +208,6 @@ abbrev Derivable (S : Sequent) : Prop := Nonempty (⊢ᵍ S) prefix:40 "⊢ᵍ! " => Derivable -section Height - namespace Derivation def height {S : Sequent} : ⊢ᵍ S → ℕ @@ -231,39 +254,55 @@ lemma ofZero (d : ⊢ᵍ[0] Γ ⟹ Δ) : (∃ x a, (x ∶ .atom a) ∈ Γ.fmls | initBot y => right; use y; simp; | _ => simp [Derivation.height] at height_le; -noncomputable def induc - (motive : ∀ S k, (⊢ᵍ[k] S) → Sort*) - : ∀ S k, (d : ⊢ᵍ[k] S) → motive S k d - := by - rintro S h ⟨d, h_le⟩; - induction d with - | initAtom x a => - sorry; - | initBot => - sorry; - | impL d₁ d₂ ih₁ ih₂ => - sorry; - | impR d ih => - sorry; - | boxL d ih => - sorry; - | boxR _ _ _ d ih => - sorry; - end DerivationWithHeight - abbrev DerivableWithHeight (S : Sequent) (h : ℕ) : Prop := Nonempty (⊢ᵍ[h] S) notation:80 "⊢ᵍ[" h "]! " S => DerivableWithHeight S h -end Height +section variable {S : Sequent} -variable {Γ Γ₁ Γ₂ Δ Δ₁ Δ₂ : SequentPart} -open SequentPart +def initAtomₕ (x a) : ⊢ᵍ[k] (⟨(x ∶ atom a) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ ⟨(x ∶ atom a) ::ₘ S.Δ.fmls, S.Δ.rels⟩) := ⟨initAtom x a, by simp⟩ + +def initBotₕ (x) : ⊢ᵍ[k] (⟨(x ∶ ⊥) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ) := ⟨initBot x, by simp⟩ + +def impRₕ (x φ ψ) : + (⊢ᵍ[h] (⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ ⟨(x ∶ ψ) ::ₘ S.Δ.fmls, S.Δ.rels⟩)) → + (⊢ᵍ[h + 1] (S.Γ ⟹ ⟨(x ∶ φ ➝ ψ) ::ₘ S.Δ.fmls, S.Δ.rels⟩)) := by + rintro ⟨d, hk⟩; + exact ⟨impR x φ ψ d, by simpa [impR]⟩ + +def impLₕ (x φ ψ) : + (⊢ᵍ[k₁] (S.Γ ⟹ ⟨(x ∶ φ) ::ₘ S.Δ.fmls, S.Δ.rels⟩)) → + (⊢ᵍ[k₂] (⟨(x ∶ ψ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ)) → + (⊢ᵍ[max k₁ k₂ + 1] (⟨(x ∶ φ ➝ ψ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ)) := by + rintro ⟨d₁, hk₁⟩ ⟨d₂, hk₂⟩; + exact ⟨ + @impL S x φ ψ d₁ d₂, + by simp [impL]; omega; + ⟩; + +def boxLₕ (x y φ) : + (⊢ᵍ[k] (⟨(x ∶ □φ) ::ₘ (y ∶ φ) ::ₘ S.Γ.fmls, (x, y) ::ₘ S.Γ.rels⟩ ⟹ S.Δ)) → + (⊢ᵍ[k + 1] (⟨(x ∶ □φ) ::ₘ S.Γ.fmls, (x, y) ::ₘ S.Γ.rels⟩ ⟹ S.Δ)) := by + rintro ⟨d, hk⟩; + exact ⟨boxL x y φ d, by simpa [boxL]⟩ + +def boxRₕ (x y φ) + (h₁ : x ≠ y) + (h₂ : S.Γ.isFreshLabel y) + (h₃ : S.Δ.isFreshLabel y) : + (⊢ᵍ[k] (⟨S.Γ.fmls, (x, y) ::ₘ S.Γ.rels⟩ ⟹ ⟨(y ∶ φ) ::ₘ S.Δ.fmls, S.Δ.rels⟩)) → + (⊢ᵍ[k + 1] (S.Γ ⟹ ⟨(x ∶ □φ) ::ₘ S.Δ.fmls, S.Δ.rels⟩)) := by + rintro ⟨d, hk⟩; + exact ⟨boxR x y φ h₁ h₂ h₃ d, by simpa [boxR]⟩ + +end + +/- section def initAtomₕ' {k : ℕ} (x a) (h₁ : (x ∶ atom a) ∈ S.Γ.fmls) (h₂ : (x ∶ atom a) ∈ S.Δ.fmls) : ⊢ᵍ[k] S := by @@ -332,60 +371,194 @@ def boxRₕ (hxy : x ≠ y) (hΓ : Γ.isFreshLabel y) (hΔ : Δ.isFreshLabel y) exact ⟨boxR₂ hxy hΓ hΔ d, by simpa [boxR₂]⟩ end +-/ + + +namespace DerivationWithHeight + +#check Derivation.rec +#check DerivationWithHeight.rec + +noncomputable def rec' + (motive : ∀ (S k), (⊢ᵍ[k] S) → Sort*) + (hAtom : + {S : Sequent} → + (x : Label) → + (a : PropVar) → + (k : ℕ) → + motive (⟨(x ∶ atom a) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ ⟨(x ∶ atom a) ::ₘ S.Δ.fmls, S.Δ.rels⟩) k (initAtomₕ x a) + ) + (hBot : + {S : Sequent} → + (x : Label) → + (k : ℕ) → + motive (⟨(x ∶ ⊥) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ) k (initBotₕ x) + ) + (hImpR : + {S : Sequent} → + (x : Label) → + (φ ψ : Formula PropVar) → + (k : ℕ) → + (d : ⊢ᵍ[k] ⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ ⟨(x ∶ ψ) ::ₘ S.Δ.fmls, S.Δ.rels⟩) → + motive _ k d → + motive _ (k + 1) (impRₕ x φ ψ d) + ) + (hImpL : + {S : Sequent} → + (x : Label) → + (φ ψ : Formula PropVar) → + (k₁ k₂ : ℕ) → + (d₁ : ⊢ᵍ[k₁] S.Γ ⟹ ⟨(x ∶ φ) ::ₘ S.Δ.fmls, S.Δ.rels⟩) → + (d₂ : ⊢ᵍ[k₂] ⟨(x ∶ ψ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ) → + motive _ k₁ d₁ → + motive _ k₂ d₂ → + motive _ (max k₁ k₂ + 1) (impLₕ x φ ψ d₁ d₂) + ) + (hBoxL : + {S : Sequent} → + (x y : Label) → + (φ : Formula PropVar) → + (k : ℕ) → + (d : ⊢ᵍ[k] ⟨(x ∶ □φ) ::ₘ (y ∶ φ) ::ₘ S.Γ.fmls, (x, y) ::ₘ S.Γ.rels⟩ ⟹ S.Δ) → + motive _ k d → + motive _ (k + 1) (boxLₕ x y φ d) + ) + (hBoxR : + {S : Sequent} → + (x y : Label) → + (hxy : x ≠ y) → + (hΓ : S.Γ.isFreshLabel y) → + (hΔ : S.Δ.isFreshLabel y) → + (φ : Formula PropVar) → + (k : ℕ) → + (d : ⊢ᵍ[k] ⟨S.Γ.fmls, (x, y) ::ₘ S.Γ.rels⟩ ⟹ ⟨(y ∶ φ) ::ₘ S.Δ.fmls, S.Δ.rels⟩) → + motive _ k d → + motive _ (k + 1) (boxRₕ x y φ hxy hΓ hΔ d) + ) + : ∀ {S k}, (d : ⊢ᵍ[k] S) → motive S k d + := by + rintro S k ⟨d, hk⟩; + induction d generalizing k with + | @initAtom S x a => + exact @hAtom S x a k; + | @initBot S x => + exact @hBot S x k; + | impR x φ ψ d ih => + by_cases k = 0; + . simp at hk; + omega; + . convert hImpR x φ ψ (k - 1) ⟨d, by simp at hk; omega⟩ ?_; + . omega; + . exact ih $ by simp at hk; omega; + | impL x φ ψ d₁ d₂ ih₁ ih₂ => + by_cases k = 0; + . simp at hk; + omega; + . convert hImpL x φ ψ (k - 1) (k - 1) ⟨d₁, by simp at hk; omega⟩ ⟨d₂, by simp at hk; omega⟩ ?_ ?_; + . omega; + . exact ih₁ $ by simp at hk; omega; + . exact ih₂ $ by simp at hk; omega; + | boxL x y φ d ih => + by_cases k = 0; + . simp at hk; + omega; + . convert hBoxL x y φ (k - 1) ⟨d, by simp at hk; omega⟩ ?_; + . omega; + . exact ih $ by simp at hk; omega; + | boxR x y φ hxy hΓy hΔy d ih => + by_cases k = 0; + . simp at hk; + omega; + . convert hBoxR x y hxy hΓy hΔy φ (k - 1) ⟨d, by simp at hk; omega⟩ ?_; + . omega; + . exact ih $ by simp at hk; omega; + +end DerivationWithHeight + + +open SequentPart + + +section + +def initAtom_memₕ {k : ℕ} (x a) (h₁ : (x ∶ atom a) ∈ S.Γ.fmls) (h₂ : (x ∶ atom a) ∈ S.Δ.fmls) + : ⊢ᵍ[k] S := by + suffices ⊢ᵍ[k] (⟨S.Γ.fmls, S.Γ.rels⟩ ⟹ ⟨S.Δ.fmls, S.Δ.rels⟩) by simpa; + rw [←(Multiset.cons_erase h₁), ←(Multiset.cons_erase h₂)]; + exact ⟨initAtom (S := ⟨S.Γ.fmls.erase (x ∶ .atom a), S.Γ.rels⟩ ⟹ ⟨S.Δ.fmls.erase (x ∶ .atom a), S.Δ.rels⟩) x a, by simp⟩ + +def initAtom_mem (x a) (h₁ : (x ∶ atom a) ∈ S.Γ.fmls) (h₂ : (x ∶ atom a) ∈ S.Δ.fmls) + : ⊢ᵍ S := initAtom_memₕ (k := 0) x a h₁ h₂ |>.drv + + +def initBot_memₕ {k : ℕ} (x) (h : (x ∶ ⊥) ∈ S.Γ.fmls) + : ⊢ᵍ[k] S := by + suffices ⊢ᵍ[k] (⟨S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ) by simpa; + rw [←(Multiset.cons_erase h)]; + exact ⟨initBot (S := ⟨S.Γ.fmls.erase (x ∶ ⊥), S.Γ.rels⟩ ⟹ S.Δ) x, by simp⟩ + +def initBot_mem (x) (h : (x ∶ ⊥) ∈ S.Γ.fmls) + : ⊢ᵍ S := initBot_memₕ (k := 0) x h |>.drv + +end + section open Sequent -def initFml₂ : ⊢ᵍ (⟨(x ∶ φ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ ⟨(x ∶ φ) ::ₘ Δ.fmls, Δ.rels⟩) := by - induction φ using Formula.rec' generalizing Γ Δ x with - | hatom a => apply initAtom' x a (by simp) (by simp); - | hfalsum => apply initBot' x (by simp); +variable {S : Sequent} + +def initFml (x φ) + : ⊢ᵍ (⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ ⟨(x ∶ φ) ::ₘ S.Δ.fmls, S.Δ.rels⟩) := by + induction φ using Formula.rec' generalizing S x with + | hatom a => apply initAtom_mem x a (by simp) (by simp); + | hfalsum => apply initBot_mem x (by simp); | himp φ ψ ihφ ihψ => - apply impR₂; + apply impR (S := ⟨(x ∶ φ ➝ ψ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ); rw [Multiset.cons_swap]; - apply impL₂ (Γ := ⟨(x ∶ φ) ::ₘ Γ.fmls, Γ.rels⟩) (Δ := ⟨(x ∶ ψ) ::ₘ Δ.fmls, Δ.rels⟩); - . simpa using ihφ (Δ := ⟨(x ∶ ψ) ::ₘ Δ.fmls, Δ.rels⟩); - . simpa using ihψ (Γ := ⟨(x ∶ φ) ::ₘ Γ.fmls, Γ.rels⟩); + apply impL (S := ⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ ⟨(x ∶ ψ) ::ₘ S.Δ.fmls, S.Δ.rels⟩); + . simpa using ihφ (S := S.Γ ⟹ ⟨(x ∶ ψ) ::ₘ S.Δ.fmls, S.Δ.rels⟩) x; + . simpa using ihψ (S := ⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ) x; | hbox φ ih => - apply boxR₂ (y := (⟨(x ∶ □φ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ Δ).getFreshLabel) - (getFreshLabel_ne₁ (x := x) (φ := □φ) (by simp)).symm - getFreshLabel_isFreshLabel₁ - getFreshLabel_isFreshLabel₂; - apply boxL₂; - simpa [Multiset.cons_swap] using ih (Γ := ⟨(x ∶ □φ) ::ₘ Γ.fmls, _ ::ₘ Γ.rels⟩); - -def initFml₂' (x φ) (hΓ : (x ∶ φ) ∈ Γ.fmls) (hΔ : (x ∶ φ) ∈ Δ.fmls) : ⊢ᵍ Γ ⟹ Δ := by - suffices ⊢ᵍ (⟨Γ.fmls, Γ.rels⟩ ⟹ ⟨Δ.fmls, Δ.rels⟩) by simpa; + let y := (⟨(x ∶ □φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ).getFreshLabel; + apply boxR (φ := φ) (x := x) (y := y) (S := ⟨(x ∶ □φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ) ?_ ?_ ?_; + apply boxL (S := ⟨S.Γ.fmls, S.Γ.rels⟩ ⟹ ⟨(y ∶ φ) ::ₘ S.Δ.fmls, S.Δ.rels⟩); + rw [Multiset.cons_swap]; + exact ih (S := ⟨(x ∶ □φ) ::ₘ S.Γ.fmls, (x, y) ::ₘ S.Γ.rels⟩ ⟹ S.Δ) y; + . exact (getFreshLabel_ne₁ (x := x) (φ := □φ) (by simp)).symm + . exact getFreshLabel_isFreshLabel₁; + . exact getFreshLabel_isFreshLabel₂; + +def initFml_mem (x φ) (hΓ : (x ∶ φ) ∈ S.Γ.fmls) (hΔ : (x ∶ φ) ∈ S.Δ.fmls) + : ⊢ᵍ S := by + suffices ⊢ᵍ (⟨S.Γ.fmls, S.Γ.rels⟩ ⟹ ⟨S.Δ.fmls, S.Δ.rels⟩) by simpa; rw [←(Multiset.cons_erase hΓ), ←(Multiset.cons_erase hΔ)]; - simpa using initFml₂ (Γ := ⟨Γ.fmls.erase (x ∶ φ), _⟩) (Δ := ⟨Δ.fmls.erase (x ∶ φ), _⟩); - -def initFml (x φ) : ⊢ᵍ (⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ ⟨(x ∶ φ) ::ₘ S.Δ.fmls, S.Δ.rels⟩) := initFml₂ - -def initFml' (x φ) (h₁ : (x ∶ φ) ∈ S.Γ.fmls) (h₂ : (x ∶ φ) ∈ S.Δ.fmls) : ⊢ᵍ S := initFml₂' x φ h₁ h₂ + exact initFml (S := ⟨S.Γ.fmls.erase (x ∶ φ), S.Γ.rels⟩ ⟹ ⟨S.Δ.fmls.erase (x ∶ φ), S.Δ.rels⟩) x φ; end section -variable {x y z : Label} {φ ψ ξ : Formula ℕ} +variable {S : Sequent} +variable {x y z : Label} {φ ψ ξ : Formula PropVar} def exchangeFmlLₕ : - (⊢ᵍ[k] (⟨(x ∶ φ) ::ₘ (y ∶ ψ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ Δ)) → - (⊢ᵍ[k] (⟨(y ∶ ψ) ::ₘ (x ∶ φ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ Δ)) + (⊢ᵍ[k] (⟨(x ∶ φ) ::ₘ (y ∶ ψ) ::ₘ Φ, X⟩ ⟹ Δ)) → + (⊢ᵍ[k] (⟨(y ∶ ψ) ::ₘ (x ∶ φ) ::ₘ Φ, X⟩ ⟹ Δ)) := by - suffices (x ∶ φ) ::ₘ (y ∶ ψ) ::ₘ Γ.fmls = (y ∶ ψ) ::ₘ (x ∶ φ) ::ₘ Γ.fmls by + suffices (x ∶ φ) ::ₘ (y ∶ ψ) ::ₘ Φ = (y ∶ ψ) ::ₘ (x ∶ φ) ::ₘ Φ by rw [this]; tauto; - simp_rw [←Multiset.singleton_add] + simp_rw [←Multiset.singleton_add]; abel; def exchangeFml₃Lₕ : - (⊢ᵍ[k] (⟨(x ∶ φ) ::ₘ (y ∶ ψ) ::ₘ (z ∶ ξ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ Δ)) → - (⊢ᵍ[k] (⟨(y ∶ ψ) ::ₘ (z ∶ ξ) ::ₘ (x ∶ φ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ Δ)) + (⊢ᵍ[k] (⟨(x ∶ φ) ::ₘ (y ∶ ψ) ::ₘ (z ∶ ξ) ::ₘ Φ, X⟩ ⟹ Δ)) → + (⊢ᵍ[k] (⟨(y ∶ ψ) ::ₘ (z ∶ ξ) ::ₘ (x ∶ φ) ::ₘ Φ, X⟩ ⟹ Δ)) := by - suffices (x ∶ φ) ::ₘ (y ∶ ψ) ::ₘ (z ∶ ξ) ::ₘ Γ.fmls = (y ∶ ψ) ::ₘ (z ∶ ξ) ::ₘ (x ∶ φ) ::ₘ Γ.fmls by + suffices (x ∶ φ) ::ₘ (y ∶ ψ) ::ₘ (z ∶ ξ) ::ₘ Φ = (y ∶ ψ) ::ₘ (z ∶ ξ) ::ₘ (x ∶ φ) ::ₘ Φ by rw [this]; tauto; simp_rw [←Multiset.singleton_add]; diff --git a/LabelledSystem/Gentzen/Hilbert.lean b/LabelledSystem/Gentzen/Hilbert.lean index 8e7d0c4..3f0ab0f 100644 --- a/LabelledSystem/Gentzen/Hilbert.lean +++ b/LabelledSystem/Gentzen/Hilbert.lean @@ -8,7 +8,7 @@ namespace Labelled.Gentzen open SequentPart -variable {x : Label} {φ ψ χ : Formula ℕ} +variable {x : Label} {φ ψ χ : Formula PropVar} def imply₁ : ⊢ᵍ ↑(φ ➝ ψ ➝ φ) := by apply impR₂ (Δ := ⟨_, _⟩); diff --git a/LabelledSystem/Gentzen/ReplaceLabel.lean b/LabelledSystem/Gentzen/ReplaceLabel.lean index 37ebf2a..6627518 100644 --- a/LabelledSystem/Gentzen/ReplaceLabel.lean +++ b/LabelledSystem/Gentzen/ReplaceLabel.lean @@ -2,118 +2,82 @@ import LabelledSystem.Gentzen.Basic namespace LO.Modal.Labelled.Gentzen +open Formula open SequentPart open DerivationWithHeight -noncomputable def replaceLabelₕAux (d : ⊢ᵍ[k] S) (σ : Label → Label) : ⊢ᵍ[k] S⟦σ⟧ := by - obtain ⟨d, kh⟩ := d; - induction d generalizing k with - | initAtom y a => exact initAtomₕ' (σ y) a (by simp) (by simp); - | initBot y => exact initBotₕ' (σ y) (by simp); - | @impL S x φ ψ d₁ d₂ ih₁ ih₂ => - by_cases k = 0; - . simp at kh; omega; - . suffices ⊢ᵍ[k] - ⟨(σ x ∶ φ ➝ ψ) ::ₘ S.Γ.fmls.map (.labelReplace σ), S.Γ.rels.map (.labelReplace σ)⟩ ⟹ - ⟨S.Δ.fmls.map (.labelReplace σ), S.Δ.rels.map (.labelReplace σ)⟩ - by simpa; - have := @impLₕ - (Γ := ⟨S.Γ.fmls.map (.labelReplace σ), S.Γ.rels.map (.labelReplace σ)⟩) - (Δ := ⟨S.Δ.fmls.map (.labelReplace σ), S.Δ.rels.map (.labelReplace σ)⟩) - (x := (σ x)) (φ := φ) (ψ := ψ) (k₁ := (k - 1)) (k₂ := (k - 1)) ?_ ?_; - rwa [(show max (k - 1) (k - 1) + 1 = k by omega)] at this; - . simpa using @ih₁ (k - 1) (by simp at kh; omega); - . simpa using @ih₂ (k - 1) (by simp at kh; omega); - | @impR S x φ ψ d ih => - by_cases k = 0; - . simp at kh; omega; - . suffices ⊢ᵍ[k] - ⟨S.Γ.fmls.map (.labelReplace σ), S.Γ.rels.map (.labelReplace σ)⟩ ⟹ - ⟨(σ x ∶ φ ➝ ψ) ::ₘ S.Δ.fmls.map (.labelReplace σ), S.Δ.rels.map (.labelReplace σ)⟩ - by simpa; - have := @impRₕ - (Γ := ⟨S.Γ.fmls.map (.labelReplace σ), S.Γ.rels.map (.labelReplace σ)⟩) - (Δ := ⟨S.Δ.fmls.map (.labelReplace σ), S.Δ.rels.map (.labelReplace σ)⟩) - (x := (σ x)) (φ := φ) (ψ := ψ) (h := (k - 1)) ?_; - rwa [(show k - 1 + 1 = k by omega)] at this; - . simpa using @ih (k - 1) (by simp at kh; omega); - | @boxL S x y φ d ih => - by_cases k = 0; - . simp at kh; omega; - . suffices ⊢ᵍ[k] - ⟨(σ x ∶ □φ) ::ₘ S.Γ.fmls.map (.labelReplace σ), (σ x, σ y) ::ₘ S.Γ.rels.map (.labelReplace σ)⟩ ⟹ - ⟨S.Δ.fmls.map (.labelReplace σ), S.Δ.rels.map (.labelReplace σ)⟩ - by simpa; - have := @boxLₕ - (Γ := ⟨S.Γ.fmls.map (.labelReplace σ), S.Γ.rels.map (.labelReplace σ)⟩) - (Δ := ⟨S.Δ.fmls.map (.labelReplace σ), S.Δ.rels.map (.labelReplace σ)⟩) - (x := (σ x)) (y := (σ y)) (φ := φ) (k := k - 1) ?_; - rwa [(show k - 1 + 1 = k by omega)] at this; - . simpa using @ih (k - 1) (by simp at kh; omega); - | @boxR S x y φ hxy hΓ hΔ d ih => - by_cases k = 0; - . simp at kh; omega; - . suffices ⊢ᵍ[k] - ⟨S.Γ.fmls.map (.labelReplace σ), S.Γ.rels.map (.labelReplace σ)⟩ ⟹ - ⟨(σ x ∶ □φ) ::ₘ S.Δ.fmls.map (.labelReplace σ), S.Δ.rels.map (.labelReplace σ)⟩ - by simpa; - by_cases e : y = σ x; - . subst e; - have := @boxRₕ - (Γ := ⟨S.Γ.fmls.map (.labelReplace σ), S.Γ.rels.map (.labelReplace σ)⟩) - (Δ := ⟨S.Δ.fmls.map (.labelReplace σ), S.Δ.rels.map (.labelReplace σ)⟩) - (x := σ x) (y := x) (φ := φ) (h := k - 1) ?_ ?_ ?_ ?_; - rwa [(show k - 1 + 1 = k by omega)] at this; - . sorry; - . refine ⟨?_, ?_, ?_⟩; - . sorry; - . sorry; - . sorry; - . refine ⟨?_, ?_, ?_⟩; - . simp; - rintro ⟨z, ψ⟩ hψ; - simp; - sorry; - . simp; - rintro z w v h₁ h₂ rfl; - have := (not_include_relTerm_of_isFreshLabel₁ hΔ) (σ w); - sorry; - . simp; - rintro z w v h₁ h₂ rfl; - sorry; - . simp - -- have := @ih Γ Δ (k - 1) (by simp at kh; omega); - sorry; - -- simpa using ih (k := k - 1) (by simp at kh; omega); - . have := @boxRₕ - (Γ := ⟨S.Γ.fmls.map (.labelReplace σ), S.Γ.rels.map (.labelReplace σ)⟩) - (Δ := ⟨S.Δ.fmls.map (.labelReplace σ), S.Δ.rels.map (.labelReplace σ)⟩) - (x := σ x) (y := σ y) (φ := φ) (h := k - 1) ?_ ?_ ?_ ?_; - rwa [(show k - 1 + 1 = k by omega)] at this; - . by_contra hC; +noncomputable def replaceLabelₕAux' (x y) (d : ⊢ᵍ[k] S) : ⊢ᵍ[k] S⟦x ↦ y⟧ := by + induction d using DerivationWithHeight.rec' with + | hAtom z a k => exact initAtom_memₕ ((x ↦ y) z) a (by simp) (by simp); + | hBot z => exact initBot_memₕ ((x ↦ y) z) (by simp); + | @hImpR S z φ ψ k d ih => + suffices ⊢ᵍ[k + 1] + ⟨S.Γ.fmls.map (.labelReplace _), S.Γ.rels.map (.labelReplace _)⟩ ⟹ + ⟨((x ↦ y) z ∶ φ ➝ ψ) ::ₘ S.Δ.fmls.map (.labelReplace _), S.Δ.rels.map (.labelReplace _)⟩ + by simpa; + apply impRₕ + (S := (⟨S.Γ.fmls.map (.labelReplace (x ↦ y)), S.Γ.rels.map (.labelReplace (x ↦ y))⟩ ⟹ ⟨S.Δ.fmls.map (.labelReplace (x ↦ y)), S.Δ.rels.map (.labelReplace (x ↦ y))⟩)) + ((x ↦ y) z) φ ψ ?_; + . simpa using ih; + | @hImpL S z φ ψ k₁ k₂ d₁ d₂ ih₁ ih₂ => + suffices ⊢ᵍ[(max k₁ k₂ + 1)] + ⟨((x ↦ y) z ∶ φ ➝ ψ) ::ₘ S.Γ.fmls.map (.labelReplace (x ↦ y)), S.Γ.rels.map (.labelReplace (x ↦ y))⟩ ⟹ + ⟨S.Δ.fmls.map (.labelReplace (x ↦ y)), S.Δ.rels.map (.labelReplace (x ↦ y))⟩ + by simpa; + apply impLₕ + (S := (⟨S.Γ.fmls.map (.labelReplace (x ↦ y)), S.Γ.rels.map (.labelReplace (x ↦ y))⟩ ⟹ ⟨S.Δ.fmls.map (.labelReplace (x ↦ y)), S.Δ.rels.map (.labelReplace (x ↦ y))⟩)) + ((x ↦ y) z) φ ψ ?_ ?_; + . simpa using ih₁; + . simpa using ih₂; + | @hBoxL S z w φ k d ih => + suffices ⊢ᵍ[k + 1] + ⟨((x ↦ y) z ∶ □φ) ::ₘ S.Γ.fmls.map (.labelReplace (x ↦ y)), ((x ↦ y) z, (x ↦ y) w) ::ₘ S.Γ.rels.map (.labelReplace (x ↦ y))⟩ ⟹ + ⟨S.Δ.fmls.map (.labelReplace (x ↦ y)), S.Δ.rels.map (.labelReplace (x ↦ y))⟩ + by simpa; + apply boxLₕ + (S := (⟨S.Γ.fmls.map (.labelReplace (x ↦ y)), S.Γ.rels.map (.labelReplace (x ↦ y))⟩ ⟹ ⟨S.Δ.fmls.map (.labelReplace (x ↦ y)), S.Δ.rels.map (.labelReplace (x ↦ y))⟩)) + ((x ↦ y) z) ((x ↦ y) w) φ ?_; + . simpa using ih; + | @hBoxR S z w hyz hΓ hΔ φ k d ih => + suffices ⊢ᵍ[k + 1] + ⟨S.Γ.fmls.map (.labelReplace (x ↦ y)), S.Γ.rels.map (.labelReplace (x ↦ y))⟩ ⟹ + ⟨((x ↦ y) z ∶ □φ) ::ₘ S.Δ.fmls.map (.labelReplace (x ↦ y)), S.Δ.rels.map (.labelReplace (x ↦ y))⟩ + by simpa; + sorry; + /- + by_cases e : x = z; + . subst e; + apply @boxRₕ + (S := (⟨S.Γ.fmls.map (.labelReplace (x ↦ y)), S.Γ.rels.map (.labelReplace (x ↦ y))⟩ ⟹ ⟨S.Δ.fmls.map (.labelReplace (x ↦ y)), S.Δ.rels.map (.labelReplace (x ↦ y))⟩)) + (x := y) (y := (x ↦ y) w) (k := k) φ ?_ ?_ ?_ ?_; + . exact hyz.symm; + . simp; + sorry; + . simp; + sorry; + . simp; + sorry; + . apply @boxRₕ + (S := (⟨S.Γ.fmls.map (.labelReplace (x ↦ y)), S.Γ.rels.map (.labelReplace (x ↦ y))⟩ ⟹ ⟨S.Δ.fmls.map (.labelReplace (x ↦ y)), S.Δ.rels.map (.labelReplace (x ↦ y))⟩)) + (x := (x ↦ y) z) (y := (x ↦ y) w) (k := k) φ ?_ ?_ ?_ ?_; + . simp; + sorry; + . apply SequentPart.of_isFreshLabel; + . simp; sorry; - . have ⟨hΓ₁, hΓ₂, hΓ₃⟩ := hΓ; - sorry; - . refine ⟨?_, ?_, ?_⟩; - . have := not_include_labelledFml_of_isFreshLabel hΔ; - simp; - rintro ⟨z, ψ⟩ hψ; - simp; - sorry; - . simp; - rintro z w v h₁ h₂ rfl; - have := (not_include_relTerm_of_isFreshLabel₁ hΔ) (σ w); - sorry; - . simp; - rintro z w v h₁ h₂ h₃; - have := (not_include_relTerm_of_isFreshLabel₂ hΔ) (σ w); - sorry; - . simpa using @ih (k := k - 1) (by simp at kh; omega); + . sorry; + . sorry; + . apply SequentPart.of_isFreshLabel; + . sorry; + . sorry; + . sorry; + . simpa using ih; + -/ -noncomputable def replaceLabelₕ (d : ⊢ᵍ[h] Γ ⟹ Δ) (σ : LabelReplace) : ⊢ᵍ[h] Γ⟦σ⟧ ⟹ Δ⟦σ⟧ := by - simpa using replaceLabelₕAux d σ; +noncomputable def replaceLabelₕ (x y) (d : ⊢ᵍ[h] Γ ⟹ Δ) : ⊢ᵍ[h] Γ⟦x ↦ y⟧ ⟹ Δ⟦x ↦ y⟧ := by + simpa using replaceLabelₕAux' x y d; -noncomputable def replaceLabel (d : ⊢ᵍ Γ ⟹ Δ) (σ : LabelReplace) : ⊢ᵍ Γ⟦σ⟧ ⟹ Δ⟦σ⟧ := - replaceLabelₕ (.ofDerivation d) σ |>.drv +noncomputable def replaceLabel (x y) (d : ⊢ᵍ Γ ⟹ Δ) : ⊢ᵍ Γ⟦x ↦ y⟧ ⟹ Δ⟦x ↦ y⟧ := + replaceLabelₕ x y (.ofDerivation d) |>.drv end LO.Modal.Labelled.Gentzen diff --git a/LabelledSystem/Gentzen/Soundness.lean b/LabelledSystem/Gentzen/Soundness.lean index d5d55ad..e3d2cb8 100644 --- a/LabelledSystem/Gentzen/Soundness.lean +++ b/LabelledSystem/Gentzen/Soundness.lean @@ -132,7 +132,7 @@ theorem soundness {S : Sequent} (d : ⊢ᵍ S) : ∀ (M : Kripke.Model), ∀ (f have : ¬(f a) ≺ (f b) := hΔ₁ a b h₁; contradiction; -theorem soundness_fml {φ : Formula ℕ} : ⊢ᵍ! ↑φ → ∀ (M : Kripke.Model), ∀ (f : Assignment M), f 0 ⊧ φ := by +theorem soundness_fml {φ : Formula PropVar} : ⊢ᵍ! ↑φ → ∀ (M : Kripke.Model), ∀ (f : Assignment M), f 0 ⊧ φ := by rintro ⟨d⟩ M f; simpa [Sequent.Satisfies] using soundness d M f diff --git a/LabelledSystem/Gentzen/Weakening.lean b/LabelledSystem/Gentzen/Weakening.lean index 9dd3e72..adb101f 100644 --- a/LabelledSystem/Gentzen/Weakening.lean +++ b/LabelledSystem/Gentzen/Weakening.lean @@ -9,151 +9,126 @@ namespace LO.Modal.Labelled.Gentzen open SequentPart open DerivationWithHeight -noncomputable def wkFmlLₕAux (d : ⊢ᵍ[k] S) : ⊢ᵍ[k] ⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ := by - obtain ⟨d, kh⟩ := d; - induction d generalizing k x with - | initAtom y a => exact initAtomₕ' y a (by simp) (by simp); - | initBot y => exact initBotₕ' y (by simp); - | @impR S y ψ χ d ih => - by_cases k = 0; - . simp at kh; omega; - . suffices ⊢ᵍ[k] - ⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ ⟨(y ∶ ψ ➝ χ) ::ₘ S.Δ.fmls, S.Δ.rels⟩ - by simpa; - have := impRₕ - (Γ := ⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩) - (Δ := S.Δ) - (x := y) (φ := ψ) (ψ := χ) (h := (k - 1)) ?_; - simpa [(show k - 1 + 1 = k by omega)] using this; - . exact exchangeFmlLₕ $ ih $ by simp at kh; omega; - | @impL S y ψ ξ dψ dξ ihψ ihξ => - by_cases k = 0; - . simp at kh; omega; - . suffices ⊢ᵍ[k] - (⟨(x ∶ φ) ::ₘ (y ∶ ψ ➝ ξ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ) - by simpa; - have := exchangeFmlLₕ $ @impLₕ - (Γ := ⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩) - (Δ := S.Δ) - (x := y) (φ := ψ) (ψ := ξ) (k₁ := (k - 1)) (k₂ := (k - 1)) ?_ ?_; - simpa [(show k - 1 + 1 = k by omega)] using this; - . exact ihψ (by simp at kh; omega); - . exact exchangeFmlLₕ $ ihξ $ by simp at kh; omega; - | @boxL S y z ψ d ih => - by_cases k = 0; - . simp at kh; omega; - . suffices ⊢ᵍ[k] - (⟨(x ∶ φ) ::ₘ (y ∶ □ψ) ::ₘ S.Γ.fmls, (y, z) ::ₘ S.Γ.rels⟩ ⟹ S.Δ) - by simpa; - have := @boxLₕ - (Γ := ⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩) - (Δ := S.Δ) - (x := y) (y := z) (φ := ψ) (k := k - 1) ?_; - apply exchangeFmlLₕ (Γ := ⟨S.Γ.fmls, (y, z) ::ₘ S.Γ.rels⟩); - simpa [(show k - 1 + 1 = k by omega)] using this; - . apply exchangeFml₃Lₕ (Γ := ⟨S.Γ.fmls, (y, z) ::ₘ S.Γ.rels⟩); - exact ih $ by simp at kh; omega; - | @boxR S y z ψ hyz hΓz hΔz d ih => - by_cases k = 0; - . simp at kh; omega; - . suffices ⊢ᵍ[k] - (⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ ⟨(y ∶ □ψ) ::ₘ S.Δ.fmls, S.Δ.rels⟩) - by simpa; - by_cases hzx : z = x; - . subst hzx; - let w : Label := ((⟨(z ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩) ⟹ S.Δ).getFreshLabel; - have := @boxRₕ - (Γ := ⟨(w ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩) - (Δ := S.Δ) - (x := y) (y := z) (φ := ψ) (h := k - 1) hyz ?_ ?_ ?_; - have := @replaceLabelₕ (Γ := ⟨(w ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩) (Δ := ⟨(y ∶ □ψ) ::ₘ S.Δ.fmls, S.Δ.rels⟩) _ this (w ↦ z); - have e₁ : S.Γ.fmls.map (.labelReplace (w ↦ z)) = S.Γ.fmls := by - apply Multiset.map_id_domain; - intro ⟨l, ξ⟩ hlξ; - apply LabelledFormula.labelReplace_specific_not; - rintro rfl; - have : (w ∶ ξ) ∉ S.Γ.fmls := not_include_labelledFml_of_isFreshLabel ?_ ξ; +noncomputable def wkFmlLₕ (d : ⊢ᵍ[k] S) : ⊢ᵍ[k] ⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ := by + induction d using DerivationWithHeight.rec' generalizing x with + | hAtom y a => exact initAtom_memₕ y a (by simp) (by simp); + | hBot y => exact initBot_memₕ y (by simp); + | @hImpR S y ψ χ k d ih => + suffices ⊢ᵍ[k + 1] + ⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ ⟨(y ∶ ψ ➝ χ) ::ₘ S.Δ.fmls, S.Δ.rels⟩ + by simpa; + refine impRₕ + (S := ⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ) + (x := y) (φ := ψ) (ψ := χ) $ ?_; + . exact exchangeFmlLₕ $ ih; + | @hImpL S y ψ ξ k₁ k₂ d₁ d₂ ih₁ ih₂ => + suffices ⊢ᵍ[max k₁ k₂ + 1] + ⟨(x ∶ φ) ::ₘ (y ∶ ψ ➝ ξ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ + by simpa; + refine exchangeFmlLₕ $ impLₕ + (S := ⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ) + (x := y) (φ := ψ) (ψ := ξ) ?_ ?_; + . exact ih₁; + . exact exchangeFmlLₕ $ ih₂; + | @hBoxL S y z ψ k d ih => + suffices ⊢ᵍ[k + 1] + ⟨(x ∶ φ) ::ₘ (y ∶ □ψ) ::ₘ S.Γ.fmls, (y, z) ::ₘ S.Γ.rels⟩ ⟹ S.Δ + by simpa; + refine exchangeFmlLₕ $ @boxLₕ + (S := ⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ) + (x := y) (y := z) (φ := ψ) (k := k) ?_; + . exact exchangeFml₃Lₕ $ ih; + | @hBoxR S y z hyz hΓz hΔz ψ k d ih => + suffices ⊢ᵍ[k + 1] + ⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ ⟨(y ∶ □ψ) ::ₘ S.Δ.fmls, S.Δ.rels⟩ + by simpa; + by_cases e : z = x; + . subst e; + let w : Label := ((⟨(z ∶ φ) ::ₘ S.Γ.fmls, (y, z) ::ₘ S.Γ.rels⟩) ⟹ S.Δ).getFreshLabel; + have := boxRₕ + (S := ⟨(w ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ) + (k := k) y z ψ hyz ?_ ?_ $ by simpa using @ih w; + have := @replaceLabelₕAux' + (x := w) (y := z) (k := k + 1) + (S := { fmls := (w ∶ φ) ::ₘ S.Γ.fmls, rels := S.Γ.rels } ⟹ { fmls := (y ∶ □ψ) ::ₘ S.Δ.fmls, rels := S.Δ.rels }) + this; + simp at this; + have e₁ : S.Γ.fmls.map (.labelReplace (w ↦ z)) = S.Γ.fmls := by + apply Multiset.map_id_domain; + rintro ⟨l, ξ⟩ hlξ; + apply LabelledFormula.labelReplace_specific_not; + have : (w ∶ ξ) ∉ S.Γ.fmls := not_include_labelledFml_of_isFreshLabel ?_ ξ; + rintro rfl; + contradiction; + apply getFreshLabel_mono (Δ := ⟨(w ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩); + . simp [Multiset.subset_cons]; + . rfl; + have e₂ : S.Δ.fmls.map (.labelReplace (w ↦ z)) = S.Δ.fmls := by + apply Multiset.map_id_domain; + intro ⟨l, ξ⟩ hlξ; + apply LabelledFormula.labelReplace_specific_not; + rintro rfl; + have : (w ∶ ξ) ∉ S.Δ.fmls := not_include_labelledFml_of_isFreshLabel ?_ ξ; + contradiction; + exact Sequent.getFreshLabel_isFreshLabel₂; + have e₃ : S.Γ.rels.map (.labelReplace (w ↦ z)) = S.Γ.rels := by + apply Multiset.map_id_domain; + intro ⟨l₁, l₂⟩ hl; + apply LabelTerm.labelReplace_specific_not_both; + . rintro rfl; + have : (w, l₂) ∉ S.Γ.rels := not_include_relTerm_of_isFreshLabel₁ ?_ l₂; contradiction; - apply getFreshLabel_mono (Δ := ⟨(w ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩); - . simp [Multiset.subset_cons]; - . rfl; - have e₂ : S.Δ.fmls.map (.labelReplace (w ↦ z)) = S.Δ.fmls := by - apply Multiset.map_id_domain; - intro ⟨l, ξ⟩ hlξ; - apply LabelledFormula.labelReplace_specific_not; - rintro rfl; - have : (w ∶ ξ) ∉ S.Δ.fmls := not_include_labelledFml_of_isFreshLabel ?_ ξ; + exact Sequent.getFreshLabel_isFreshLabel₁; + . rintro rfl; + have : (l₁, w) ∉ S.Γ.rels := not_include_relTerm_of_isFreshLabel₂ ?_ l₁; + contradiction; + exact Sequent.getFreshLabel_isFreshLabel₁; + have e₄ : S.Δ.rels.map (.labelReplace (w ↦ z)) = S.Δ.rels := by + apply Multiset.map_id_domain; + intro ⟨l₁, l₂⟩ hl; + apply LabelTerm.labelReplace_specific_not_both; + . rintro rfl; + have : (w, l₂) ∉ S.Δ.rels := not_include_relTerm_of_isFreshLabel₁ ?_ l₂; contradiction; exact Sequent.getFreshLabel_isFreshLabel₂; - have e₃ : S.Γ.rels.map (.labelReplace (w ↦ z)) = S.Γ.rels := by - apply Multiset.map_id_domain; - intro ⟨l₁, l₂⟩ hl; - apply LabelTerm.labelReplace_specific_not_both; - . rintro rfl; - have : (w, l₂) ∉ S.Γ.rels := not_include_relTerm_of_isFreshLabel₁ ?_ l₂; - contradiction; - exact Sequent.getFreshLabel_isFreshLabel₁; - . rintro rfl; - have : (l₁, w) ∉ S.Γ.rels := not_include_relTerm_of_isFreshLabel₂ ?_ l₁; - contradiction; - exact Sequent.getFreshLabel_isFreshLabel₁; - have e₄ : S.Δ.rels.map (.labelReplace (w ↦ z)) = S.Δ.rels := by - apply Multiset.map_id_domain; - intro ⟨l₁, l₂⟩ hl; - apply LabelTerm.labelReplace_specific_not_both; - . rintro rfl; - have : (w, l₂) ∉ S.Δ.rels := not_include_relTerm_of_isFreshLabel₁ ?_ l₂; - contradiction; - exact Sequent.getFreshLabel_isFreshLabel₂; - . rintro rfl; - have : (l₁, w) ∉ S.Δ.rels := not_include_relTerm_of_isFreshLabel₂ ?_ l₁; - contradiction; - exact Sequent.getFreshLabel_isFreshLabel₂; - have e₅ : (y ∶ □ψ)⟦w ↦ z⟧ = (y ∶ □ψ) := LabelledFormula.labelReplace_specific_not $ by - sorry; - simpa [ - e₁, - e₂, - e₃, - e₄, - e₅, - (show k - 1 + 1 = k by omega) - ] using this; - . refine ⟨?_, ?_, ?_⟩; - . suffices z ≠ w ∧ ∀ x ∈ S.Γ.fmls, ¬x.label = z by simpa; - constructor; - . apply @SequentPart.getFreshLabel_ne ({ fmls := (z ∶ φ) ::ₘ S.Γ.fmls, rels := S.Γ.rels }) z φ (by simp) |>.symm; - . rintro ⟨w, ψ⟩ h rfl; - have := not_include_labelledFml_of_isFreshLabel hΓz ψ; - contradiction; - . exact hΓz.2.1; - . exact hΓz.2.2; - . exact hΔz; - . simpa using @ih (k - 1) w (by simp at kh; omega); - . have := @boxRₕ - (Γ := ⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩) - (Δ := ⟨S.Δ.fmls, S.Δ.rels⟩) - (x := y) (y := z) (φ := ψ) (h := k - 1) hyz ?_ hΔz ?_; - simpa [(show k - 1 + 1 = k by omega)] using this; - . refine ⟨?_, ?_, ?_⟩; - . suffices z ≠ x ∧ ∀ x ∈ S.Γ.fmls, ¬x.label = z by simpa; - constructor; - . assumption; - . rintro ⟨w, ψ⟩ h rfl; - have := not_include_labelledFml_of_isFreshLabel hΓz ψ; - contradiction; - . exact hΓz.2.1; - . exact hΓz.2.2; - . exact ih (by simp at kh; omega); - -def wkFmlLₕ (d : ⊢ᵍ[k] Γ ⟹ Δ) : ⊢ᵍ[k] ⟨(x ∶ φ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ Δ := by - obtain ⟨d, kh⟩ := d; - cases d with - | initAtom y a => exact initAtomₕ' y a (by simp) (by simp); - | initBot y => exact initBotₕ' y (by simp); - | _ => sorry; - -def wkFmlL (d : ⊢ᵍ Γ ⟹ Δ) : ⊢ᵍ ⟨(x ∶ φ) ::ₘ Γ.fmls, Γ.rels⟩ ⟹ Δ := wkFmlLₕ (d := .ofDerivation d) |>.drv + . rintro rfl; + have : (l₁, w) ∉ S.Δ.rels := not_include_relTerm_of_isFreshLabel₂ ?_ l₁; + contradiction; + exact Sequent.getFreshLabel_isFreshLabel₂; + have e₅ : ((w ↦ z) y ∶ □ψ) = (y ∶ □ψ) := by + apply LabelledFormula.labelReplace_specific_not; + apply Ne.symm; + apply Sequent.getFreshLabel_relΓ₁ (y := z); + simp; + simpa [e₁, e₂, e₃, e₄, e₅] using this; + . apply of_isFreshLabel; + . intro ξ; + suffices (w ≠ z) ∧ (z ∶ ξ) ∉ S.Γ.fmls by simp; constructor <;> tauto; + constructor; + . apply Sequent.getFreshLabel_ne₁ (φ := φ) (by simp); + . apply not_include_labelledFml_of_isFreshLabel hΓz ξ; + . apply not_include_relTerm_of_isFreshLabel₁ hΓz; + . apply not_include_relTerm_of_isFreshLabel₂ hΓz; + . apply of_isFreshLabel; + . apply not_include_labelledFml_of_isFreshLabel hΔz; + . apply not_include_relTerm_of_isFreshLabel₁ hΔz; + . apply not_include_relTerm_of_isFreshLabel₂ hΔz; + . refine boxRₕ (S := ⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ) (k := k) y z ψ hyz ?_ ?_ ?_; + . apply of_isFreshLabel; + . intro ξ; + suffices (z = x → ¬ξ = φ) ∧ (z ∶ ξ) ∉ S.Γ.fmls by simpa; + constructor; + . tauto; + . exact not_include_labelledFml_of_isFreshLabel hΓz ξ; + . apply not_include_relTerm_of_isFreshLabel₁ hΓz; + . apply not_include_relTerm_of_isFreshLabel₂ hΓz; + . apply of_isFreshLabel; + . apply not_include_labelledFml_of_isFreshLabel hΔz; + . apply not_include_relTerm_of_isFreshLabel₁ hΔz; + . apply not_include_relTerm_of_isFreshLabel₂ hΔz; + . exact ih; + +noncomputable def wkFmlL (d : ⊢ᵍ S) : ⊢ᵍ ⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ := wkFmlLₕ (d := .ofDerivation d) |>.drv def wkRelLₕ (d : ⊢ᵍ[h] Γ ⟹ Δ) : ⊢ᵍ[h] ⟨Γ.fmls, (x, y) ::ₘ Γ.rels⟩ ⟹ Δ := by sorry