feat(Foundations/Relation/Confluence): generalize results from confluence to commutation

[thomaskwaring]

This PR generalises many results from confluent to commuting relations, and obtains the classical case as a specialisation. We add HJoin and MHJoin — heterogenous versions of Join and MJoin — and associated API for them and related relational constructions.

NB: the theorem confluent_equivalents is now public, and the TFAE has been extended with certain other properties which generalise better to the heterogenous case.

[chenson2018]

Some minor organization comments:

[lengyijun]

Why is DiamondCommute defined with def, while the others are defined with abbrev?

[lengyijun]

Could we add this theorem to the PR?

theorem diamond_commute_reflTransGen
    (h : DiamondCommute r₂ r₁) :
    DiamondCommute r₂ (Relation.ReflTransGen r₁) := by
  intro q p r hB hA
  induction hA generalizing p with
  | refl => exact ⟨p, .refl, hB⟩
  | tail _ a_step ih =>
    obtain ⟨s, hs₁, hs₂⟩ := ih hB
    obtain ⟨w, hw₁, hw₂⟩ := h hs₂ a_step
    exact ⟨w, hs₁.tail hw₁, hw₂⟩

[thomaskwaring]

Nice catch @lengyijun — your theorem is a direct generalisation of DiamondCommute.extend with almost the same proof, & I've made DiamondCommute an abbrev for consistency.

[lengyijun]

@thomaskwaring @chenson2018 Shall we group the definitions into those involving one relation and those involving two relations?

[lengyijun]

lemma DiamondCommute.extend (h : DiamondCommute r₁ r₂) : SemiCommute r₂ r₁ := by
  intros _ c _ h₂ h₁
  induction h₁ using ReflTransGen.head_induction_on generalizing c with
  | refl => exact Join₂.single_right (.single h₂)
  | head ha _ ih =>
    obtain ⟨d, had, hcd⟩ := h ha h₂
    obtain ⟨d', hbd', hdd'⟩ := ih had
    exact ⟨d', .head hcd hbd', hdd'⟩

/-- Extending a multistep reduction by a single step preserves multi-joinability. -/
lemma Diamond.extend (h : Diamond r) : SemiConfluent r := DiamondCommute.extend h

lemma DiamondCommute.to_commute (h : DiamondCommute r₁ r₂) : Commute r₁ r₂ := by
  intro a b₁ b₂ hab₁ hab₂
  induction hab₂ using ReflTransGen.head_induction_on generalizing b₁ with
  | refl => exact Join₂.single_right hab₁
  | @head a a' ha hab₂ ih =>
    obtain ⟨c, hb₁c, hac⟩ := h.extend ha hab₁
    obtain ⟨d, hcd, hb₂d⟩ := ih hb₁c
    exact ⟨d, hac.trans hcd, hb₂d⟩