Projects: Term Rewriting

Stream: ItaLean 2025

[Lorenzo Luccioli]

This thread is dedicated to the Term Rewriting project:

• Repository: ?
• Informal & Formal Manager: @Chris Henson

[Chris Henson]

Since there are just a few of us, I think we can easily work from a branch in my fork of CSLib: https://github.com/chenson2018/cslib/tree/italean-traat. I pushed a slightly cleaned up version of our discussion from this evening. For simplicity I'm just throwing everything in the Relation namespace at the top of Cslib/Foundations/Data/Relation.lean. I can clean up namespaces before anything is PR'd.

[Chris Henson]

@Alessandro D'Angelo Could you share you GitHub username and the proofs you wrote yesterday for (semi)confluence/Church-Rosser? I'll try to clean things up a bit before project work this afternoon.

[Alessandro D'Angelo]

@Chris Henson sorry yesterday I went back to my airbnb quite late. Here's the code:

theorem semiConfluent_to_confluent (h : SemiConfluent r) : Confluent r := by
  -- We need to show: ∀ x y1 y2, x ↠ y1 → x ↠ y2 → Join (ReflTransGen r) y1 y2
  intro x y1 y2 h_xy1 h_xy2
  -- Induction on the first reduction chain x ↠ y1
  induction h_xy1 with
  | refl =>
    exact ⟨y2, h_xy2, ReflTransGen.refl⟩
  | tail h_xz h_zy1 ih =>
    obtain ⟨u, h_zu, h_y2u⟩ := ih
    obtain ⟨v, h_y1v, h_uv⟩ := h h_zu h_zy1
    exact ⟨v, h_y1v, ReflTransGen.trans h_y2u h_uv⟩

theorem confluent_to_churchRosser (h : Confluent r) : ChurchRosser r := by
  intro x y h_eqv
  -- Induction on the structure of the equivalence x ≈ y
  induction h_eqv with
  | rel a b h_r =>
    exact ⟨b, ReflTransGen.single h_r, ReflTransGen.refl⟩
  | refl a =>
    exact ⟨a, ReflTransGen.refl, ReflTransGen.refl⟩
  | symm a b _ ih =>
    exact symmetric_join ih
  | trans a b c _ _ ih1 ih2 =>
    obtain ⟨u, hau, hbu⟩ := ih1
    obtain ⟨v, hbv, hcv⟩ := ih2
    obtain ⟨w, huw, hvw⟩ := h hbu hbv
    exists w
    refine ⟨?_, ?_⟩
    · exact ReflTransGen.trans hau huw
    · exact ReflTransGen.trans hcv hvw

/-- Theorem 2.1.5 (3 ⇒ 1): Semi-confluence implies the Church-Rosser property. -/
theorem SemiConfluent_toChurchRosser (h : SemiConfluent r) : ChurchRosser r :=
  confluent_to_churchRosser r (semiConfluent_to_confluent r h)

P.S. my github user name is a-dangelo

[Chris Henson]

I have pushed the SemiConfluent r ↔ ChurchRosser r ↔ Confluent r proofs with some cleaning done. With some help from grind we end up with pretty compact proofs.

[Chris Henson]

I have opened cslib#215

[Alessandro D'Angelo]

Great thanks!

[Chris Henson]

This is now merged, thank you all! I will be continuing work along these lines, please ping me in the CSLib channel for any further discussion.