feat(Relation): add TransGenCommute, SemiDiamondCommute

Cslib/Foundations/Relation/Confluence.lean

@@ -92,6 +92,47 @@ theorem Commute.isTrans_join₂_reflTransGen (h : Commute r₁ r₂) :
 theorem Confluent.isTrans_join_reflTransGen (h : Confluent r) : IsTrans α (Join (ReflTransGen r)) :=
   Commute.isTrans_join₂_reflTransGen h
 
+-- mirror of `SemiCommute.to_commute`
+theorem SemiDiamondCommute.to_diamond_commute (h : SemiDiamondCommute r₁ r₂) :
+  DiamondCommute (ReflTransGen r₁) (TransGen r₂) := by
+  intro a b₁ b₂ hab₁ hab₂
+  induction hab₁ with
+  | refl => use b₂
+  | tail hab hbb' ih =>
+    obtain ⟨d, hd, hd'⟩ := ih
+    obtain ⟨e, he, he'⟩ := h hbb' hd
+    use e, he, hd'.trans he'
+
+theorem semiDiamondCommute_iff_diamondCommute :
+    SemiDiamondCommute r₁ r₂ ↔ DiamondCommute (ReflTransGen r₁) (TransGen r₂) :=
+  ⟨fun h => h.to_diamond_commute, fun h => fun _ _ _ hxy₁ hxy₂ => h (.single hxy₁) hxy₂⟩
+
+theorem Commute.to_semiDiamondCommute (hc : Commute r₁ r₂) (h : TransGenCommute r₁ r₂) :
+  SemiDiamondCommute r₁ r₂ := by
+  intros x y z hxy hyz
+  induction hyz with
+  | single hyz => exact h hxy hyz
+  | tail h₁ h₂ h₃ =>
+    obtain ⟨w, hw₁, hw₂⟩ := h₃
+    obtain ⟨s, hs₁, hs₂⟩ := hc hw₂ (.single h₂)
+    exact ⟨s, hw₁.trans_left hs₁, hs₂⟩
+
+theorem SemiDiamondCommute.to_commute (h : SemiDiamondCommute r₁ r₂) : Commute r₁ r₂ := by
+  intro x y₁ y₂ hxy₁ hxy₂
+  rcases hxy₂.cases_head with rfl | ⟨c, hxc, hcy₂⟩
+  · exact ⟨y₁, .refl, hxy₁⟩
+  · obtain ⟨z, hz₁, hz₂⟩ := h.to_diamond_commute hxy₁ (TransGen.head' hxc hcy₂)
+    exact ⟨z, hz₁.to_reflTransGen, hz₂⟩
+
+theorem SemiDiamondCommute.to_transGenCommute (h : SemiDiamondCommute r₁ r₂) :
+    TransGenCommute r₁ r₂ :=
+  fun _ _ _ hxy₁ hxy₂ => h hxy₁ (.single hxy₂)
+
+theorem commute_and_transGenCommute_iff_semiDiamondCommute :
+    Commute r₁ r₂ ∧ TransGenCommute r₁ r₂ ↔ SemiDiamondCommute r₁ r₂ :=
+    ⟨fun ⟨hc, h⟩ => hc.to_semiDiamondCommute h,
+     fun h => ⟨h.to_commute, h.to_transGenCommute⟩⟩
+
 theorem SemiCommute.to_commute (h : SemiCommute r₁ r₂) : Commute r₁ r₂ := by
   intro a b₁ b₂ hab₁ hab₂
   induction hab₁ with

Cslib/Foundations/Relation/Defs.lean

@@ -92,6 +92,22 @@ abbrev StronglyConfluent (r : α → α → Prop) :=
 def StronglyCommute (r₁ r₂ : α → α → Prop) :=
   ∀ {x y₁ y₂}, r₁ x y₁ → r₂ x y₂ → ∃ z, ReflGen r₂ y₁ z ∧ ReflTransGen r₁ y₂ z
 
+/--
+`TransGenCommute r₁ r₂` states that a single step of `r₁` and a single step of `r₂`
+with the same source can be joined by a path along `r₂` from the first result and a
+reflexive-transitive path along `r₁` from the second result.
+-/
+abbrev TransGenCommute (r₁ r₂ : α → α → Prop) :=
+  ∀ ⦃x y₁ y₂⦄, r₁ x y₁ → r₂ x y₂ → ∃ z, TransGen r₂ y₁ z ∧ ReflTransGen r₁ y₂ z
+
+/--
+`SemiDiamondCommute r₁ r₂` is the asymmetric version of the commutation square where one
+branch takes a single `r₁`-step and the other takes a non-empty `r₂`-path. The two
+outcomes are then joinable by a further `r₂`-path and an `r₁`-reflexive-transitive path.
+-/
+abbrev SemiDiamondCommute (r₁ r₂ : α → α → Prop) :=
+  ∀ ⦃x y₁ y₂⦄, r₁ x y₁ → TransGen r₂ x y₂ → ∃ z, TransGen r₂ y₁ z ∧ ReflTransGen r₁ y₂ z
+
 /-! ### Normalization properties -/
 
 /-- An element is reducible with respect to a relation if there is a value it is related to. -/