feat: more lemmas on Euclidean relations

Cslib/Foundations/Data/Relation.lean

@@ -11,18 +11,22 @@ public import Mathlib.Data.List.TFAE
 public import Mathlib.Order.Comparable
 public import Mathlib.Order.WellFounded
 public import Mathlib.Order.BooleanAlgebra.Basic
+public import Mathlib.Data.Fintype.EquivFin
 
 /-! # Relations
 
 ## References
 
 * [*Term Rewriting and All That*][Baader1998]
+* [*Simple Laws about Nonprominent Properties of Binary Relations*][Burghardt2018]
 
 -/
 
 @[expose] public section
 
-variable {α : Type*} {r : α → α → Prop}
+open Relator
+
+variable {α : Type*} {r r₁ r₂ : α → α → Prop}
 
 theorem WellFounded.ofTransGen (trans_wf : WellFounded (Relation.TransGen r)) : WellFounded r := by
   grind [WellFounded.wellFounded_iff_has_min, Relation.TransGen]
@@ -37,6 +41,78 @@ namespace Relation
 @[nolint unusedArguments]
 def emptyHRelation {α : Sort u} {β : Sort v} (_ : α) (_ : β) := False
 
+@[simp, grind =]
+theorem emptyHRelation_emptyRelation : (emptyHRelation : α → α → Prop) = emptyRelation := rfl
+
+@[simp, grind =]
+theorem emptyHrelation_apply (a : α) (b : β) : emptyHRelation a b ↔ False := .rfl
+
+section dom_cod
+
+variable {β : Type*} {r : α → β → Prop}
+
+/-- Domain of a relation. -/
+def dom (r : α → β → Prop) : Set α := {a | ∃ b, r a b}
+
+/-- Codomain of a relation, aka range. -/
+def cod (r : α → β → Prop) : Set β := {b | ∃ a, r a b}
+
+@[simp, grind =] lemma mem_dom : a ∈ dom r ↔ ∃ b, r a b := .rfl
+@[simp, grind =] lemma mem_cod : b ∈ cod r ↔ ∃ a, r a b := .rfl
+
+@[gcongr] lemma dom_mono (h : r₁ ≤ r₂) : dom r₁ ⊆ dom r₂ := fun a ⟨b, hab⟩ => ⟨b, h a b hab⟩
+@[gcongr] lemma cod_mono (h : r₁ ≤ r₂) : cod r₁ ⊆ cod r₂ := fun b ⟨a, hab⟩ => ⟨a, h a b hab⟩
+
+@[simp, grind =]
+lemma dom_empty : dom (emptyHRelation : α → β → Prop) = ∅ := by grind
+
+@[simp, grind =]
+lemma cod_empty : cod (emptyHRelation : α → β → Prop) = ∅ := by grind
+
+@[simp, grind =]
+lemma dom_eq_empty_iff : dom r = ∅ ↔ r = emptyHRelation where
+  mp h := by
+    ext a b
+    simp
+    grind => have : a ∈ dom r; finish
+  mpr := by grind
+
+@[simp, grind =]
+lemma cod_eq_empty_iff : cod r = ∅ ↔ r = emptyHRelation where
+  mp h := by
+    ext a b
+    simp
+    grind => have : b ∈ cod r; finish
+  mpr h := by grind
+
+@[simp]
+lemma cod_inv : cod (fun a b => r b a) = dom r := rfl
+
+@[simp]
+lemma dom_inv : dom (fun a b => r b a) = cod r := rfl
+
+end dom_cod
+
+instance : CoeDep (α → α → Prop) r (dom r → dom r → Prop) where
+  coe a b := r a b
+
+instance : CoeDep (α → α → Prop) r (cod r → cod r → Prop) where
+  coe a b := r a b
+
+theorem _root_.Std.Trichotomous.subsingleton_cod [Std.Trichotomous r] :
+    Subsingleton ((cod r)ᶜ : Set α) := by
+  constructor
+  rintro ⟨b₁, _⟩ ⟨b₂, _⟩
+  have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ b₁ b₂
+  grind
+
+theorem _root_.Std.Trichotomous.subsingleton_dom [Std.Trichotomous r] :
+    Subsingleton ((dom r)ᶜ : Set α) := by
+  constructor
+  rintro ⟨a₁, _⟩ ⟨a₂, _⟩
+  have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a₁ a₂
+  grind
+
 attribute [scoped grind] ReflGen TransGen ReflTransGen EqvGen CompRel
 
 theorem ReflGen.to_eqvGen (h : ReflGen r a b) : EqvGen r a b := by
@@ -82,7 +158,9 @@ namespace RightEuclidean
 variable [RightEuclidean r]
 
 /-- A `RightEuclidean` relation is reflexive on its range -/
-theorem refl_range (ab : r a b) : r b b := rightEuclidean ab ab
+theorem refl_cod (ab : r a b) : r b b := rightEuclidean ab ab
+
+theorem refl_cod' : b ∈ cod r → r b b := fun ⟨_, ab⟩ ↦ refl_cod ab
 
 /-- The converse of a `RightEuclidean` relation is `LeftEuclidean` -/
 theorem leftEuclidean_swap : LeftEuclidean (fun a b => r b a) where
@@ -94,7 +172,7 @@ instance [Std.Refl r] : Std.Symm r where
 theorem trichotomous_trans [Std.Trichotomous r] : IsTrans α r where
   trans a b c ab bc := by
     have := Std.Trichotomous.trichotomous (r := r) a c
-    have cc := refl_range bc
+    have cc := refl_cod bc
     have (ca : r c a) := rightEuclidean ca cc
     grind
 
@@ -103,7 +181,63 @@ theorem antisymm_rightUnique [Std.Antisymm r] : Relator.RightUnique r := by
   exact antisymm (rightEuclidean ab ac) (rightEuclidean ac ab)
 
 theorem rightUnique_antisymm (h : Relator.RightUnique r) : Std.Antisymm r where
-  antisymm _ _ ab ba := h ba (refl_range ab)
+  antisymm _ _ ab ba := h ba (refl_cod ab)
+
+theorem rightUnique_trans (h : Relator.RightUnique r) : IsTrans α r where
+  trans a b c ab bc := by
+    have eq : c = b := h bc (refl_cod ab)
+    simpa [eq]
+
+theorem rightTotal_equiv (h : Relator.RightTotal r) : IsEquiv α r := by
+  have : Std.Refl r := ⟨fun a => refl_cod (h a).choose_spec⟩
+  exact {toIsTrans := ⟨fun _ _ _ ab bc => rightEuclidean (symm ab) bc⟩}
+
+omit [RightEuclidean r] in
+theorem leftTotal_rightUnique_trans (h₁ : LeftTotal r) (h₂ : RightUnique r) [IsTrans α r] :
+    RightEuclidean r where
+  rightEuclidean {a b c} ab ac := by
+    obtain ⟨d, dc⟩ := h₁ c
+    have : b = c := h₂ ab ac
+    have : d = c := h₂ (_root_.trans ac dc) ac
+    grind
+
+private theorem three_contra [Std.Trichotomous r] [Std.Antisymm r] :
+    ¬ ∃ (a b c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c := by
+  rintro ⟨a, b, c, _⟩
+  have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a b
+  have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a c
+  have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ b c
+  have := antisymm_rightUnique (r := r)
+  have := @refl_cod (r := r)
+  grind [Relator.RightUnique]
+
+theorem trichotomous_antisymm_finite [Std.Trichotomous r] [Std.Antisymm r] : Finite α := by
+  classical
+  by_contra! h
+  apply three_contra (r := r)
+  have ⟨_, hcard⟩ := Infinite.exists_subset_card_eq α 3
+  have ⟨a, b, c, _, _, _, _⟩ := Finset.card_eq_three.mp hcard
+  use a, b, c
+
+theorem trichotomous_antisymm_card [Std.Trichotomous r] [Std.Antisymm r] [Fintype α] :
+    Fintype.card α ≤ 2 := by
+  by_contra! h
+  apply three_contra (r := r)
+  have ⟨a, b, c, _⟩ := Fintype.two_lt_card_iff.mp h
+  use a, b, c
+
+theorem cod_subset_dom : cod r ⊆ dom r := fun b ⟨_, ab⟩ ↦ ⟨b, refl_cod ab⟩
+
+instance : RightEuclidean (α := cod r) r where
+  rightEuclidean := rightEuclidean
+
+instance : RightEuclidean (α := dom r) r where
+  rightEuclidean := rightEuclidean
+
+theorem rightTotal_cod : Relator.RightTotal (α := cod r) (β := cod r) r :=
+  fun ⟨_, _, h⟩ => ⟨_, refl_cod h⟩
+
+theorem equiv_cod : IsEquiv (cod r) r := rightTotal_equiv rightTotal_cod
 
 end RightEuclidean
 
@@ -114,6 +248,8 @@ variable [LeftEuclidean r]
 /-- A `LeftEuclidean` relation is reflexive on its domain -/
 theorem refl_dom (ab : r a b) : r a a := leftEuclidean ab ab
 
+theorem refl_dom' : a ∈ dom r → r a a := fun ⟨_, ab⟩ ↦ refl_dom ab
+
 /-- The converse of a `LeftEuclidean` relation is `RightEuclidean` -/
 theorem rightEuclidean_swap : RightEuclidean (fun a b => r b a) where
   rightEuclidean ab ac := leftEuclidean ac ab
@@ -135,6 +271,62 @@ theorem antisymm_leftUnique [Std.Antisymm r] : Relator.LeftUnique r := by
 theorem leftUnique_antisymm (h : Relator.LeftUnique r) : Std.Antisymm r where
   antisymm _ _ ab ba := h ab (refl_dom ba)
 
+theorem leftUnique_trans (h : Relator.LeftUnique r) : IsTrans α r where
+  trans a b c ab bc := by
+    have eq : a = b := h ab (refl_dom bc)
+    simpa [eq]
+
+theorem leftTotal_equiv (h : Relator.LeftTotal r) : IsEquiv α r := by
+  have : Std.Refl r := ⟨fun a => refl_dom (h a).choose_spec⟩
+  exact {toIsTrans := ⟨fun _ _ _ ab bc => leftEuclidean ab (symm bc)⟩}
+
+omit [LeftEuclidean r] in
+theorem rightTotal_leftUnique_trans (h₁ : RightTotal r) (h₂ : LeftUnique r) [IsTrans α r] :
+    LeftEuclidean r where
+  leftEuclidean {a b c} ac bc := by
+    obtain ⟨d, da⟩ := h₁ a
+    have : a = b := h₂ ac bc
+    have : a = d := h₂ ac (_root_.trans da ac)
+    grind
+
+private theorem three_contra [Std.Trichotomous r] [Std.Antisymm r] :
+    ¬ ∃ (a b c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c := by
+  rintro ⟨a, b, c, _⟩
+  have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a b
+  have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ a c
+  have := @Std.Trichotomous.rel_or_eq_or_rel_swap _ r _ b c
+  have := antisymm_leftUnique (r := r)
+  have := @refl_dom (r := r)
+  grind [Relator.LeftUnique]
+
+theorem trichotomous_antisymm_finite [Std.Trichotomous r] [Std.Antisymm r] : Finite α := by
+  classical
+  by_contra! h
+  apply three_contra (r := r)
+  have ⟨_, hcard⟩ := Infinite.exists_subset_card_eq α 3
+  have ⟨a, b, c, _, _, _, _⟩ := Finset.card_eq_three.mp hcard
+  use a, b, c
+
+theorem trichotomous_antisymm_card [Std.Trichotomous r] [Std.Antisymm r] [Fintype α] :
+    Fintype.card α ≤ 2 := by
+  by_contra! h
+  apply three_contra (r := r)
+  have ⟨a, b, c, _⟩ := Fintype.two_lt_card_iff.mp h
+  use a, b, c
+
+theorem dom_subset_cod : dom r ⊆ cod r := fun a ⟨_, ab⟩ ↦ ⟨a, refl_dom ab⟩
+
+instance : LeftEuclidean (α := cod r) r where
+  leftEuclidean := leftEuclidean
+
+instance : LeftEuclidean (α := dom r) r where
+  leftEuclidean := leftEuclidean
+
+theorem leftTotal_dom : Relator.LeftTotal (α := dom r) (β := dom r) r :=
+  fun ⟨_, _, h⟩ => ⟨_, refl_dom h⟩
+
+theorem equiv_dom : IsEquiv (dom r) r := leftTotal_equiv leftTotal_dom
+
 end LeftEuclidean
 
 section euclidean_symm
@@ -172,6 +364,31 @@ theorem symm_rightEuclidean_iff_trans : RightEuclidean r ↔ IsTrans α r :=
 
 end euclidean_symm
 
+theorem leftEuclidean_rightEuclidean_dom_cod_eq [LeftEuclidean r] [RightEuclidean r] :
+    dom r = cod r := by
+  have : dom r ⊆ cod r := LeftEuclidean.dom_subset_cod
+  have : cod r ⊆ dom r := RightEuclidean.cod_subset_dom
+  grind
+
+theorem dom_cod_leftEuclidean (eq : dom r = cod r) [equiv_dom : IsEquiv (dom r) r] :
+    LeftEuclidean r where
+  leftEuclidean {a b c} ac bc := by
+    have cb : r c b := equiv_dom.symm ⟨_, _, bc⟩ ⟨c, by grind⟩ bc
+    exact equiv_dom.trans ⟨_, _, ac⟩ ⟨_, _, cb⟩ ⟨_, by grind⟩ ac cb
+
+lemma dom_cod_rightEuclidean (eq : dom r = cod r) [equiv_dom : IsEquiv (dom r) r] :
+    RightEuclidean r where
+  rightEuclidean {a b c} ab ac := by
+    have ba : r b a := equiv_dom.symm ⟨a, _, ab⟩ ⟨b, by grind⟩ ab
+    exact equiv_dom.trans ⟨_, _, ba⟩ ⟨_, _, ac⟩ ⟨c, by grind⟩ ba ac
+
+/-- A relation is both left and right Euclidean if and only if the relation is an equivalence on
+  coinciding domain and codomain. -/
+theorem leftEuclidean_rightEuclidean_iff_dom_cod :
+    LeftEuclidean r ∧ RightEuclidean r ↔ dom r = cod r ∧ IsEquiv (dom r) r where
+  mp := fun ⟨_, _⟩ ↦ ⟨leftEuclidean_rightEuclidean_dom_cod_eq, LeftEuclidean.equiv_dom⟩
+  mpr := fun ⟨eq, _⟩ ↦ ⟨dom_cod_leftEuclidean eq, dom_cod_rightEuclidean eq⟩
+
 /-- A relation has the diamond property when all reductions with a common origin are joinable -/
 abbrev Diamond (r : α → α → Prop) := ∀ {a b c : α}, r a b → r a c → Join r b c
 
@@ -251,9 +468,9 @@ theorem Confluent_of_unique_end {x : α} (h : ∀ y : α, ReflTransGen r y x) :
 /-- An element is reducible with respect to a relation if there is a value it is related to. -/
 abbrev Reducible (r : α → α → Prop) (x : α) : Prop := ∃ y, r x y
 
-/-- A relation `r` is serial if every element is `Reducible`. -/
+/-- A relation `r` is serial if every element is `Reducible`, i.e. `Relator.LeftTotal`. -/
 class Serial (r : α → α → Prop) where
-  serial a : Reducible r a
+  serial : Relator.LeftTotal r
 
 @[scoped grind →]
 lemma refl_serial (r : α → α → Prop) (h : Std.Refl r) : Relation.Serial r where

references.bib

@@ -49,6 +49,18 @@ @book{Blackburn2001
   collection={Cambridge Tracts in Theoretical Computer Science}
 }
 
+@misc{Burghardt2018,
+	title = {Simple {Laws} about {Nonprominent} {Properties} of {Binary} {Relations}},
+	url = {https://arxiv.org/abs/1806.05036v2},
+	abstract = {We checked each binary relation on a 5-element set for a given set of properties, including usual ones like asymmetry and less known ones like Euclideanness. Using a poor man's Quine-McCluskey algorithm, we computed prime implicants of non-occurring property combinations, like "not irreflexive, but asymmetric". We considered the non-trivial laws obtained this way, and manually proved them true for binary relations on arbitrary sets, thus contributing to the encyclopedic knowledge about less known properties.},
+	language = {en},
+	urldate = {2026-05-19},
+	journal = {arXiv.org},
+	author = {Burghardt, Jochen},
+	month = jun,
+	year = {2018},
+}
+
 @inproceedings{Danielsson2008,
 author = {Danielsson, Nils Anders},
 title = {Lightweight semiformal time complexity analysis for purely functional data structures},