Skip to content

Commit

Permalink
wkRelLₕ
Browse files Browse the repository at this point in the history
  • Loading branch information
@SnO2WMaN
SnO2WMaN committed Dec 18, 2024
1 parent 0661eba commit f4d39a9
Show file tree
Hide file tree
Showing 2 changed files with 227 additions and 3 deletions.
18 changes: 17 additions & 1 deletion LabelledSystem/Gentzen/Basic.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -523,7 +523,7 @@ end
section

variable {S : Sequent}
variable {x y z : Label} {φ ψ ξ : Formula PropVar}
variable {x y z w : Label} {φ ψ ξ : Formula PropVar}

def exchangeFmlLₕ :
(⊢ᵍ[k] (⟨(x ∶ φ) ::ₘ (y ∶ ψ) ::ₘ Φ, X⟩ ⟹ Δ)) →
Expand Down Expand Up @@ -556,6 +556,22 @@ def exchangeFml₃L
: ⊢ᵍ (⟨(y ∶ ψ) ::ₘ (z ∶ ξ) ::ₘ (x ∶ φ) ::ₘ Φ, X⟩ ⟹ Δ)
:= exchangeFml₃Lₕ (k := d.height) ⟨d, by simp⟩ |>.drv


def exchangeRelLₕ :
(⊢ᵍ[k] (⟨Φ, (x, y) ::ₘ (z, w) ::ₘ X⟩ ⟹ ⟨Ψ, Y⟩)) →
(⊢ᵍ[k] (⟨Φ, (z, w) ::ₘ (x, y) ::ₘ X⟩ ⟹ ⟨Ψ, Y⟩))
:= by
suffices (x, y) ::ₘ (z, w) ::ₘ X = (z, w) ::ₘ (x, y) ::ₘ X by
rw [this];
tauto;
simp_rw [←Multiset.singleton_add];
abel;

def exchangeRelL
(d : ⊢ᵍ (⟨Φ, (x, y) ::ₘ (z, w) ::ₘ X⟩ ⟹ ⟨Ψ, Y⟩))
: ⊢ᵍ (⟨Φ, (z, w) ::ₘ (x, y) ::ₘ X⟩ ⟹ ⟨Ψ, Y⟩)
:= exchangeRelLₕ (k := d.height) ⟨d, by simp⟩ |>.drv

end


Expand Down
212 changes: 210 additions & 2 deletions LabelledSystem/Gentzen/Weakening.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -126,9 +126,217 @@ noncomputable def wkFmlLₐ (x φ) :
:= wkFmlL


def wkRelLₕ (d : ⊢ᵍ[h] S) : ⊢ᵍ[h] ⟨S.Γ.fmls, (x, y) ::ₘ S.Γ.rels⟩ ⟹ Δ := by sorry
noncomputable def wkRelLₕ (d : ⊢ᵍ[h] S) : ⊢ᵍ[h] ⟨S.Γ.fmls, (x, y) ::ₘ S.Γ.rels⟩ ⟹ S.Δ := by
induction d using DerivationWithHeight.rec' generalizing x y with
| hAtom z a => exact initAtom_memₕ z a (by simp) (by simp);
| hBot z => exact initBot_memₕ z (by simp);
| @hImpR S z φ ψ k d ih =>
suffices ⊢ᵍ[k + 1] ⟨S.Γ.fmls, (x, y) ::ₘ S.Γ.rels⟩ ⟹ ⟨(z ∶ φ ➝ ψ) ::ₘ S.Δ.fmls, S.Δ.rels⟩ by simpa;
exact impRₕ (S := ⟨S.Γ.fmls, (x, y) ::ₘ S.Γ.rels⟩ ⟹ S.Δ) z φ ψ $ ih;
| @hImpL S z φ ψ k₁ k₂ d₁ d₂ ih₁ ih₂ =>
suffices ⊢ᵍ[max k₁ k₂ + 1] ⟨(z ∶ φ ➝ ψ) ::ₘ S.Γ.fmls, (x, y) ::ₘ S.Γ.rels⟩ ⟹ S.Δ by simpa;
exact impLₕ (S := ⟨S.Γ.fmls, (x, y) ::ₘ S.Γ.rels⟩ ⟹ S.Δ) z φ ψ ih₁ ih₂;
| @hBoxL S z w φ k d ih =>
suffices ⊢ᵍ[k + 1] ⟨(z ∶ □φ) ::ₘ S.Γ.fmls, (x, y) ::ₘ (z, w) ::ₘ S.Γ.rels⟩ ⟹ S.Δ by simpa;
refine exchangeRelLₕ $ @boxLₕ (S := ⟨S.Γ.fmls, (x, y) ::ₘ S.Γ.rels⟩ ⟹ S.Δ) k z w φ ?_;
exact exchangeRelLₕ ih;
| @hBoxR S z w hzw hΓw hΔw φ k d ih =>
by_cases ewx : w = x <;> by_cases ewy : w = y
. subst ewx; subst ewy;
let v : Label := ((⟨S.Γ.fmls, (w, z) ::ₘ S.Γ.rels⟩) ⟹ S.Δ).getFreshLabel;
have := boxRₕ
(S := ⟨S.Γ.fmls, (v, v) ::ₘ S.Γ.rels⟩ ⟹ S.Δ)
(k := k) z w φ hzw ?_ hΔw (exchangeRelLₕ ih);
have := @replaceLabelₕ
(x := v) (y := w) (k := k + 1)
(S := ⟨S.Γ.fmls, (v, v) ::ₘ S.Γ.rels⟩ ⟹ ⟨(z ∶ □φ) ::ₘ S.Δ.fmls, S.Δ.rels ⟩)
this;
have e₁ : S.Γ.fmls⟦v ↦ w⟧ = S.Γ.fmls := by
apply Multiset.map_id_domain;
rintro ⟨l, ξ⟩ hlξ;
apply LabelledFormula.labelReplace_specific_not;
rintro rfl;
refine not_include_labelledFml_of_isFreshLabel ?_ ξ hlξ;
apply getFreshLabel_mono (Δ := ⟨S.Γ.fmls, (v, v) ::ₘ S.Γ.rels⟩);
. rfl;
. simp [Multiset.subset_cons];
have e₂ : S.Δ.fmls⟦v ↦ w⟧ = S.Δ.fmls := by
apply Multiset.map_id_domain;
rintro ⟨l, ξ⟩ hlξ;
apply LabelledFormula.labelReplace_specific_not;
rintro rfl;
refine not_include_labelledFml_of_isFreshLabel ?_ ξ hlξ;
exact Sequent.getFreshLabel_isFreshLabel₂;
have e₃ : S.Γ.rels⟦v ↦ w⟧ = S.Γ.rels := by
apply Multiset.map_id_domain;
rintro ⟨l₁, l₂⟩ hl;
apply LabelTerm.labelReplace_specific_not_both;
. rintro rfl;
exact not_include_relTerm_of_isFreshLabel₁ Sequent.getFreshLabel_isFreshLabel₁ l₂ hl;
. rintro rfl;
exact not_include_relTerm_of_isFreshLabel₂ Sequent.getFreshLabel_isFreshLabel₁ l₁ hl;
have e₄ : S.Δ.rels⟦v ↦ w⟧ = S.Δ.rels := by
apply Multiset.map_id_domain;
rintro ⟨l₁, l₂⟩ hl;
apply LabelTerm.labelReplace_specific_not_both;
. rintro rfl;
exact not_include_relTerm_of_isFreshLabel₁ Sequent.getFreshLabel_isFreshLabel₂ l₂ hl;
. rintro rfl;
exact not_include_relTerm_of_isFreshLabel₂ Sequent.getFreshLabel_isFreshLabel₂ l₁ hl;
have e₅ : (v ↦ w) w = w := by simp; -- TODO: this should be a lemma
have e₆ : (v ↦ w) z = z := by
suffices v ≠ z by simp; tauto;
exact Sequent.getFreshLabel_relΓ₂ (x := w) (y := z) (by simp);
simpa [e₁, e₂, e₃, e₄, e₅, e₆] using this;
. apply of_isFreshLabel;
. apply not_include_labelledFml_of_isFreshLabel hΓw;
. intro l;
suffices (v ≠ w) ∧ (w, l) ∉ S.Γ.rels by simp; constructor <;> tauto;
constructor;
. apply Sequent.getFreshLabel_relΓ₁ (y := z) (by simp);
. apply not_include_relTerm_of_isFreshLabel₁ hΓw;
. intro l;
suffices (v ≠ w) ∧ (l, w) ∉ S.Γ.rels by simp; constructor <;> tauto;
constructor;
. apply Sequent.getFreshLabel_relΓ₁ (y := z) (by simp);
. apply not_include_relTerm_of_isFreshLabel₂ hΓw;
. subst ewx;
let v : Label := ((⟨S.Γ.fmls, (w, y) ::ₘ (w, z) ::ₘ S.Γ.rels⟩) ⟹ S.Δ).getFreshLabel;
have := boxRₕ
(S := ⟨S.Γ.fmls, (v, y) ::ₘ S.Γ.rels⟩ ⟹ S.Δ)
(k := k) z w φ hzw ?_ hΔw (exchangeRelLₕ ih);
have := @replaceLabelₕ
(x := v) (y := w) (k := k + 1)
(S := ⟨S.Γ.fmls, (v, y) ::ₘ S.Γ.rels⟩ ⟹ ⟨(z ∶ □φ) ::ₘ S.Δ.fmls, S.Δ.rels ⟩)
this;
have e₁ : S.Γ.fmls⟦v ↦ w⟧ = S.Γ.fmls := by
apply Multiset.map_id_domain;
rintro ⟨l, ξ⟩ hlξ;
apply LabelledFormula.labelReplace_specific_not;
rintro rfl;
refine not_include_labelledFml_of_isFreshLabel ?_ ξ hlξ;
apply getFreshLabel_mono (Δ := ⟨S.Γ.fmls, (v, y) ::ₘ S.Γ.rels⟩);
. rfl;
. simp [Multiset.subset_cons];
have e₂ : S.Δ.fmls⟦v ↦ w⟧ = S.Δ.fmls := by
apply Multiset.map_id_domain;
rintro ⟨l, ξ⟩ hlξ;
apply LabelledFormula.labelReplace_specific_not;
rintro rfl;
refine not_include_labelledFml_of_isFreshLabel ?_ ξ hlξ;
exact Sequent.getFreshLabel_isFreshLabel₂;
have e₃ : S.Γ.rels⟦v ↦ w⟧ = S.Γ.rels := by
apply Multiset.map_id_domain;
rintro ⟨l₁, l₂⟩ hl;
apply LabelTerm.labelReplace_specific_not_both;
. rintro rfl;
exact not_include_relTerm_of_isFreshLabel₁ Sequent.getFreshLabel_isFreshLabel₁ l₂ hl;
. rintro rfl;
exact not_include_relTerm_of_isFreshLabel₂ Sequent.getFreshLabel_isFreshLabel₁ l₁ hl;
have e₄ : S.Δ.rels⟦v ↦ w⟧ = S.Δ.rels := by
apply Multiset.map_id_domain;
rintro ⟨l₁, l₂⟩ hl;
apply LabelTerm.labelReplace_specific_not_both;
. rintro rfl;
exact not_include_relTerm_of_isFreshLabel₁ Sequent.getFreshLabel_isFreshLabel₂ l₂ hl;
. rintro rfl;
exact not_include_relTerm_of_isFreshLabel₂ Sequent.getFreshLabel_isFreshLabel₂ l₁ hl;
have e₅ : (v ↦ w) y = y := by
suffices v ≠ y by simp; tauto;
exact Sequent.getFreshLabel_relΓ₂ (x := w) (y := y) (by simp);
have e₆ : (v ↦ w) z = z := by
suffices v ≠ z by simp; tauto;
exact Sequent.getFreshLabel_relΓ₂ (x := w) (y := z) (by simp);
simpa [e₁, e₂, e₃, e₄, e₅, e₆] using this;
. apply of_isFreshLabel;
. apply not_include_labelledFml_of_isFreshLabel hΓw;
. intro l;
suffices (v ≠ w) ∧ (w, l) ∉ S.Γ.rels by simp; constructor <;> tauto;
constructor;
. apply Sequent.getFreshLabel_relΓ₁ (y := y); simp;
. apply not_include_relTerm_of_isFreshLabel₁ hΓw;
. intro l;
suffices (v ≠ w) ∧ (l, w) ∉ S.Γ.rels by simp; constructor <;> tauto;
constructor;
. apply Sequent.getFreshLabel_relΓ₁ (y := y); simp;
. apply not_include_relTerm_of_isFreshLabel₂ hΓw;
. subst ewy;
let v : Label := ((⟨S.Γ.fmls, (x, w) ::ₘ (w, z) ::ₘ S.Γ.rels⟩) ⟹ S.Δ).getFreshLabel;
have := boxRₕ
(S := ⟨S.Γ.fmls, (x, v) ::ₘ S.Γ.rels⟩ ⟹ S.Δ)
(k := k) z w φ hzw ?_ hΔw (exchangeRelLₕ ih);
have := @replaceLabelₕ
(x := v) (y := w) (k := k + 1)
(S := ⟨S.Γ.fmls, (x, v) ::ₘ S.Γ.rels⟩ ⟹ ⟨(z ∶ □φ) ::ₘ S.Δ.fmls, S.Δ.rels ⟩)
this;
have e₁ : S.Γ.fmls⟦v ↦ w⟧ = S.Γ.fmls := by
apply Multiset.map_id_domain;
rintro ⟨l, ξ⟩ hlξ;
apply LabelledFormula.labelReplace_specific_not;
rintro rfl;
refine not_include_labelledFml_of_isFreshLabel ?_ ξ hlξ;
apply getFreshLabel_mono (Δ := ⟨S.Γ.fmls, (x, v) ::ₘ S.Γ.rels⟩);
. rfl;
. simp [Multiset.subset_cons];
have e₂ : S.Δ.fmls⟦v ↦ w⟧ = S.Δ.fmls := by
apply Multiset.map_id_domain;
rintro ⟨l, ξ⟩ hlξ;
apply LabelledFormula.labelReplace_specific_not;
rintro rfl;
refine not_include_labelledFml_of_isFreshLabel ?_ ξ hlξ;
exact Sequent.getFreshLabel_isFreshLabel₂;
have e₃ : S.Γ.rels⟦v ↦ w⟧ = S.Γ.rels := by
apply Multiset.map_id_domain;
rintro ⟨l₁, l₂⟩ hl;
apply LabelTerm.labelReplace_specific_not_both;
. rintro rfl;
exact not_include_relTerm_of_isFreshLabel₁ Sequent.getFreshLabel_isFreshLabel₁ l₂ hl;
. rintro rfl;
exact not_include_relTerm_of_isFreshLabel₂ Sequent.getFreshLabel_isFreshLabel₁ l₁ hl;
have e₄ : S.Δ.rels⟦v ↦ w⟧ = S.Δ.rels := by
apply Multiset.map_id_domain;
rintro ⟨l₁, l₂⟩ hl;
apply LabelTerm.labelReplace_specific_not_both;
. rintro rfl;
exact not_include_relTerm_of_isFreshLabel₁ Sequent.getFreshLabel_isFreshLabel₂ l₂ hl;
. rintro rfl;
exact not_include_relTerm_of_isFreshLabel₂ Sequent.getFreshLabel_isFreshLabel₂ l₁ hl;
have e₅ : (v ↦ w) x = x := by
suffices v ≠ x by simp; tauto;
exact Sequent.getFreshLabel_relΓ₁ (x := x) (y := w) (by simp);
have e₆ : (v ↦ w) z = z := by
suffices v ≠ z by simp; tauto;
exact Sequent.getFreshLabel_relΓ₂ (x := w) (y := z) (by simp);
simpa [e₁, e₂, e₃, e₄, e₅, e₆] using this;
. apply of_isFreshLabel;
. apply not_include_labelledFml_of_isFreshLabel hΓw;
. intro l;
suffices (v ≠ w) ∧ (w, l) ∉ S.Γ.rels by simp; constructor <;> tauto;
constructor;
. apply Sequent.getFreshLabel_relΓ₁ (y := z); simp;
. apply not_include_relTerm_of_isFreshLabel₁ hΓw;
. intro l;
suffices (v ≠ w) ∧ (l, w) ∉ S.Γ.rels by simp; constructor <;> tauto;
constructor;
. apply Sequent.getFreshLabel_relΓ₁ (y := z); simp;
. apply not_include_relTerm_of_isFreshLabel₂ hΓw;
. suffices ⊢ᵍ[k + 1] ⟨S.Γ.fmls, (x, y) ::ₘ S.Γ.rels⟩ ⟹ ⟨(z ∶ □φ) ::ₘ S.Δ.fmls, S.Δ.rels⟩ by simpa;
refine @boxRₕ (S := ⟨S.Γ.fmls, (x, y) ::ₘ S.Γ.rels⟩ ⟹ S.Δ) k z w φ hzw ?_ hΔw ?_;
. apply of_isFreshLabel;
. apply not_include_labelledFml_of_isFreshLabel hΓw;
. intro v;
suffices (w ≠ x) ∧ (w, v) ∉ S.Γ.rels by simp; constructor <;> tauto;
constructor;
. assumption;
. apply not_include_relTerm_of_isFreshLabel₁ hΓw;
. intro v;
suffices (w ≠ x) ∧ (v, w) ∉ S.Γ.rels by simp; constructor <;> tauto;
constructor;
. assumption;
. apply not_include_relTerm_of_isFreshLabel₂ hΓw;
. exact exchangeRelLₕ ih;

def wkRelL (d : ⊢ᵍ S) : ⊢ᵍ ⟨S.Γ.fmls, (x, y) ::ₘ S.Γ.rels⟩ ⟹ S.Δ := wkRelLₕ (d := .ofDerivation d) |>.drv
noncomputable def wkRelL (d : ⊢ᵍ S) : ⊢ᵍ ⟨S.Γ.fmls, (x, y) ::ₘ S.Γ.rels⟩ ⟹ S.Δ := wkRelLₕ (d := .ofDerivation d) |>.drv

noncomputable def wkRelLₐ (x y) :
⊢ᵍ (⟨Φ, X⟩ ⟹ ⟨Ψ, Y⟩) →
Expand Down

0 comments on commit f4d39a9

Please sign in to comment.