From 0325e10aefcc4025554b4c188d268cd3d830ba21 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?SnO=E2=82=82WMaN?= Date: Thu, 2 Jan 2025 08:41:56 +0900 Subject: [PATCH] refactor: Remove duplicate definition of `Antisymmetric` (#183) --- Foundation/IntProp/Kripke/Basic.lean | 2 +- Foundation/Logic/Kripke/Basic.lean | 2 +- Foundation/Modal/Boxdot/GL_Grz.lean | 4 ++-- Foundation/Modal/Kripke/Grz/Completeness.lean | 6 +++--- Foundation/Modal/Kripke/Grz/Definability.lean | 12 ++++++------ Foundation/Vorspiel/BinaryRelations.lean | 14 ++++++-------- 6 files changed, 19 insertions(+), 21 deletions(-) diff --git a/Foundation/IntProp/Kripke/Basic.lean b/Foundation/IntProp/Kripke/Basic.lean index c641ce94..729d00e8 100644 --- a/Foundation/IntProp/Kripke/Basic.lean +++ b/Foundation/IntProp/Kripke/Basic.lean @@ -36,7 +36,7 @@ lemma rel_trans' : Transitive F.Rel := by apply rel_trans; lemma rel_refl' : Reflexive F.Rel := by apply rel_refl @[simp] lemma rel_antisymm {x y : F.World} : x ≺ y → y ≺ x → x = y := IsAntisymm.antisymm x y -lemma rel_antisymm' : Antisymmetric F.Rel := by apply rel_antisymm +lemma rel_antisymm' : AntiSymmetric F.Rel := by apply rel_antisymm end Frame diff --git a/Foundation/Logic/Kripke/Basic.lean b/Foundation/Logic/Kripke/Basic.lean index 95496978..b74fca50 100644 --- a/Foundation/Logic/Kripke/Basic.lean +++ b/Foundation/Logic/Kripke/Basic.lean @@ -124,7 +124,7 @@ abbrev TransitiveIrreflexiveFrameClass : FrameClass := { F | Transitive F ∧ Ir abbrev ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass : FrameClass := { F | Reflexive F.Rel ∧ Transitive F ∧ WeaklyConverseWellFounded F } /-- FrameClass for `𝐆𝐫𝐳` (Finite version) -/ -abbrev ReflexiveTransitiveAntisymmetricFrameClass : FrameClass := { F | Reflexive F.Rel ∧ Transitive F ∧ Antisymmetric F } +abbrev ReflexiveTransitiveAntiSymmetricFrameClass : FrameClass := { F | Reflexive F.Rel ∧ Transitive F ∧ AntiSymmetric F } end diff --git a/Foundation/Modal/Boxdot/GL_Grz.lean b/Foundation/Modal/Boxdot/GL_Grz.lean index f744413f..5b26c16f 100644 --- a/Foundation/Modal/Boxdot/GL_Grz.lean +++ b/Foundation/Modal/Boxdot/GL_Grz.lean @@ -47,7 +47,7 @@ namespace Kripke open Relation (ReflGen) open Formula.Kripke -lemma mem_reflClosure_GrzFiniteFrameClass_of_mem_GLFiniteFrameClass (hF : F ∈ TransitiveIrreflexiveFiniteFrameClass) : ⟨F.toFrame^=⟩ ∈ ReflexiveTransitiveAntisymmetricFiniteFrameClass := by +lemma mem_reflClosure_GrzFiniteFrameClass_of_mem_GLFiniteFrameClass (hF : F ∈ TransitiveIrreflexiveFiniteFrameClass) : ⟨F.toFrame^=⟩ ∈ ReflexiveTransitiveAntiSymmetricFiniteFrameClass := by obtain ⟨F_trans, F_irrefl⟩ := hF; refine ⟨?F_refl, ?F_trans, ?F_antisymm⟩; . intro x; apply ReflGen.refl; @@ -65,7 +65,7 @@ lemma mem_reflClosure_GrzFiniteFrameClass_of_mem_GLFiniteFrameClass (hF : F ∈ have := F_irrefl x; contradiction; -lemma mem_irreflClosure_GLFiniteFrameClass_of_mem_GrzFiniteFrameClass (hF : F ∈ ReflexiveTransitiveAntisymmetricFiniteFrameClass) : ⟨F.toFrame^≠⟩ ∈ TransitiveIrreflexiveFiniteFrameClass := by +lemma mem_irreflClosure_GLFiniteFrameClass_of_mem_GrzFiniteFrameClass (hF : F ∈ ReflexiveTransitiveAntiSymmetricFiniteFrameClass) : ⟨F.toFrame^≠⟩ ∈ TransitiveIrreflexiveFiniteFrameClass := by obtain ⟨_, F_trans, F_antisymm⟩ := hF; refine ⟨?F_trans, ?F_irrefl⟩; . rintro x y z ⟨nexy, Rxy⟩ ⟨_, Ryz⟩; diff --git a/Foundation/Modal/Kripke/Grz/Completeness.lean b/Foundation/Modal/Kripke/Grz/Completeness.lean index 124670dc..00648efd 100644 --- a/Foundation/Modal/Kripke/Grz/Completeness.lean +++ b/Foundation/Modal/Kripke/Grz/Completeness.lean @@ -76,7 +76,7 @@ lemma transitive : Transitive (miniCanonicalFrame φ).Rel := by subst_vars; tauto; -lemma antisymm : Antisymmetric (miniCanonicalFrame φ).Rel := by +lemma antisymm : AntiSymmetric (miniCanonicalFrame φ).Rel := by rintro X Y ⟨_, h₁⟩ ⟨h₂, _⟩; exact h₁ h₂; @@ -257,7 +257,7 @@ lemma truthlemma {X : (miniCanonicalModel φ).World} (q_sub : ψ ∈ φ.subformu open Modal.Kripke -instance complete : Complete (Hilbert.Grz ℕ) (ReflexiveTransitiveAntisymmetricFiniteFrameClass) := ⟨by +instance complete : Complete (Hilbert.Grz ℕ) (ReflexiveTransitiveAntiSymmetricFiniteFrameClass) := ⟨by intro φ; contrapose; intro h; @@ -278,7 +278,7 @@ instance complete : Complete (Hilbert.Grz ℕ) (ReflexiveTransitiveAntisymmetric tauto; ⟩ -instance : Kripke.FiniteFrameProperty (Hilbert.Grz ℕ) ReflexiveTransitiveAntisymmetricFiniteFrameClass where +instance : Kripke.FiniteFrameProperty (Hilbert.Grz ℕ) ReflexiveTransitiveAntiSymmetricFiniteFrameClass where complete := complete sound := finite_sound diff --git a/Foundation/Modal/Kripke/Grz/Definability.lean b/Foundation/Modal/Kripke/Grz/Definability.lean index bf953b0b..efcf2c9e 100644 --- a/Foundation/Modal/Kripke/Grz/Definability.lean +++ b/Foundation/Modal/Kripke/Grz/Definability.lean @@ -13,7 +13,7 @@ open Formula.Kripke open Relation (IrreflGen) abbrev ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass : FrameClass := { F | Reflexive F.Rel ∧ Transitive F.Rel ∧ WeaklyConverseWellFounded F.Rel } -abbrev ReflexiveTransitiveAntisymmetricFiniteFrameClass : FiniteFrameClass := { F | Reflexive F.Rel ∧ Transitive F.Rel ∧ Antisymmetric F.Rel } +abbrev ReflexiveTransitiveAntiSymmetricFiniteFrameClass : FiniteFrameClass := { F | Reflexive F.Rel ∧ Transitive F.Rel ∧ AntiSymmetric F.Rel } variable {F : Kripke.Frame} @@ -172,7 +172,7 @@ lemma ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass.is_defined_by_Grz : . rintro h; refine ⟨refl_of_Grz h, trans_of_Grz h, WCWF_of_Grz h⟩; -lemma ReflexiveTransitiveAntisymmetricFiniteFrameClass.is_defined_by_Grz : ReflexiveTransitiveAntisymmetricFiniteFrameClass.DefinedBy 𝗚𝗿𝘇 := by +lemma ReflexiveTransitiveAntiSymmetricFiniteFrameClass.is_defined_by_Grz : ReflexiveTransitiveAntiSymmetricFiniteFrameClass.DefinedBy 𝗚𝗿𝘇 := by intro F; constructor; . rintro ⟨hRefl, hTrans, hAntisymm⟩; @@ -196,12 +196,12 @@ open Hilbert.Kripke instance Grz.Kripke.sound : Sound (Hilbert.Grz ℕ) (ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass) := instSound_of_frameClass_definedBy ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass.is_defined_by_Grz rfl -instance Grz.Kripke.finite_sound : Sound (Hilbert.Grz ℕ) (ReflexiveTransitiveAntisymmetricFiniteFrameClass) := - instSound_of_finiteFrameClass_definedBy ReflexiveTransitiveAntisymmetricFiniteFrameClass.is_defined_by_Grz rfl +instance Grz.Kripke.finite_sound : Sound (Hilbert.Grz ℕ) (ReflexiveTransitiveAntiSymmetricFiniteFrameClass) := + instSound_of_finiteFrameClass_definedBy ReflexiveTransitiveAntiSymmetricFiniteFrameClass.is_defined_by_Grz rfl -instance Grz.consistent : System.Consistent (Hilbert.Grz ℕ) := Kripke.instConsistent_of_nonempty_finiteFrameclass (FC := ReflexiveTransitiveAntisymmetricFiniteFrameClass) $ by +instance Grz.consistent : System.Consistent (Hilbert.Grz ℕ) := Kripke.instConsistent_of_nonempty_finiteFrameclass (FC := ReflexiveTransitiveAntiSymmetricFiniteFrameClass) $ by use reflexivePointFrame; - simp [Transitive, Reflexive, Antisymmetric]; + simp [Transitive, Reflexive, AntiSymmetric]; end Hilbert diff --git a/Foundation/Vorspiel/BinaryRelations.lean b/Foundation/Vorspiel/BinaryRelations.lean index d404c0c2..db6a31b6 100644 --- a/Foundation/Vorspiel/BinaryRelations.lean +++ b/Foundation/Vorspiel/BinaryRelations.lean @@ -25,8 +25,6 @@ def Coreflexive := ∀ ⦃x y⦄, x ≺ y → x = y def Equality := ∀ ⦃x y⦄, x ≺ y ↔ x = y -def Antisymmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x → x = y - def Isolated := ∀ ⦃x y⦄, ¬(x ≺ y) def Assymetric := ∀ ⦃x y⦄, (x ≺ y) → ¬(y ≺ x) @@ -72,7 +70,7 @@ lemma refl_of_symm_serial_eucl (hSymm : Symmetric rel) (hSerial : Serial rel) (h have Ryx := hSymm Rxy; exact trans_of_symm_eucl hSymm hEucl Rxy Ryx; -lemma corefl_of_refl_assym_eucl (hRefl : Reflexive rel) (hAntisymm : Antisymmetric rel) (hEucl : Euclidean rel) : Coreflexive rel := by +lemma corefl_of_refl_assym_eucl (hRefl : Reflexive rel) (hAntisymm : AntiSymmetric rel) (hEucl : Euclidean rel) : Coreflexive rel := by intro x y Rxy; have Ryx := hEucl (hRefl x) Rxy; exact hAntisymm Rxy Ryx; @@ -83,7 +81,7 @@ lemma equality_of_refl_corefl (hRefl : Reflexive rel) (hCorefl : Coreflexive rel . apply hCorefl; . rintro rfl; apply hRefl; -lemma equality_of_refl_assym_eucl (hRefl : Reflexive rel) (hAntisymm : Antisymmetric rel) (hEucl : Euclidean rel) : Equality rel := by +lemma equality_of_refl_assym_eucl (hRefl : Reflexive rel) (hAntisymm : AntiSymmetric rel) (hEucl : Euclidean rel) : Equality rel := by apply equality_of_refl_corefl; . assumption; . exact corefl_of_refl_assym_eucl hRefl hAntisymm hEucl; @@ -163,9 +161,9 @@ lemma Finite.exists_ne_map_eq_of_infinite_lt {α β} [LinearOrder α] [Infinite . contradiction; . use j, i; simp [hij, e]; -lemma antisymm_of_WCWF {R : α → α → Prop} : WCWF R → Antisymmetric R := by +lemma antisymm_of_WCWF {R : α → α → Prop} : WCWF R → AntiSymmetric R := by contrapose; - simp [Antisymmetric]; + simp [AntiSymmetric]; intro x y Rxy Ryz hxy; apply ConverseWellFounded.iff_has_max.not.mpr; push_neg; @@ -178,7 +176,7 @@ lemma antisymm_of_WCWF {R : α → α → Prop} : WCWF R → Antisymmetric R := . use x; simp_all [Relation.IrreflGen]; lemma WCWF_of_finite_trans_antisymm {R : α → α → Prop} (hFin : Finite α) (R_trans : Transitive R) - : Antisymmetric R → WCWF R := by + : AntiSymmetric R → WCWF R := by contrapose; intro hWCWF; replace hWCWF := ConverseWellFounded.iff_has_max.not.mp hWCWF; @@ -186,7 +184,7 @@ lemma WCWF_of_finite_trans_antisymm {R : α → α → Prop} (hFin : Finite α) obtain ⟨f, hf⟩ := dependent_choice hWCWF; clear hWCWF; simp [Relation.IrreflGen] at hf; - simp [Antisymmetric]; + simp [AntiSymmetric]; obtain ⟨i, j, hij, e⟩ := Finite.exists_ne_map_eq_of_infinite_lt f; use (f i), (f (i + 1)); have ⟨hi₁, hi₂⟩ := hf i;