term rewriting

Stream: CSLib

[Chris Henson]

I have opened cslib#230 proving some more properties of relations. I wanted to discuss a few design decisions here. First is the definition

abbrev Terminating (r : α → α → Prop) := WellFounded (fun a b => Relation.TransGen r b a)

I was able to write some proofs exactly as I expected, but I wanted to double check that this makes sense, is the right generality, etc. Cc @Bhavik Mehta who suggested reusing WellFounded.

The second is the addition of commuting relations. You could for instance define confluence as a relation commuting with itself and similarly for other definitions. I chose not to do so, as it seemed a bit harder to work with. I instead just added rfl theorems showing their equivalence. Does this seem okay?

Lastly I added

abbrev Relation.Union (r₁ r₂ : α → α → Prop) (a₁ a₂) := r₁ a₁ a₂ ∨ r₂ a₁ a₂

which I was somewhat surprised didn't exist already. Did I miss some other equivalent formulation?

[Eric Wieser]

The second one is r₁ ⊔ r₂

[Chris Henson]

Eric Wieser said:

The second one is r₁ ⊔ r₂

Thanks!

[Malvin Gattinger]

Is "terminating" used in this way in the literature with the TransGen included? It is equivalent to a version without that, right?

abbrev Terminating {α : Type} (r : α → α → Prop) := WellFounded (fun a b => Relation.TransGen r b a)
abbrev Terminating' {α : Type} (r : α → α → Prop) := WellFounded (fun a b => r b a)

equivalence proof

Sorry for the messy code, this is based on stuff I already had here.

import Mathlib.Order.WellFounded

lemma Relation.TransGen.flip_iff (α : Type) {r : α → α → Prop} {a b : α} :
    (Relation.TransGen (flip r)) a b ↔ (Relation.TransGen r) b a := by
  exact @Relation.transGen_swap α r a b

/-- If the transitive closure of `r` is wellfounded, then `r` itself is wellfounded.
This was for example proven in https://www.cs.utexas.edu/~EWD/ewd12xx/EWD1241.PDF (page 2 aka 3)
(but here we prove it via `WellFounded.wellFounded_iff_has_min` instead. -/
lemma wf_of_trans_wf {α : Type} {r : α → α → Prop} (trans_wf : WellFounded (Relation.TransGen r)) :
    WellFounded r := by
  rw [WellFounded.wellFounded_iff_has_min]
  rw [WellFounded.wellFounded_iff_has_min] at trans_wf
  intro s s_nE
  specialize trans_wf s s_nE
  rcases trans_wf with ⟨m, m_in_s, m_is_min⟩
  refine ⟨m, m_in_s, fun x x_in_s hyp => ?_⟩
  absurd m_is_min x x_in_s
  exact Relation.TransGen.single hyp

theorem same_help {α : Type} (r : α → α → Prop) :
    WellFounded (fun a b => Relation.TransGen r b a) ↔ WellFounded (fun a b => r b a) := by
  constructor
  · convert @wf_of_trans_wf α (flip r) using 2
    grind [Relation.TransGen.flip_iff]
  · intro r_wf
    convert WellFounded.transGen r_wf using 1
    have := @Relation.TransGen.flip_iff α r
    grind [flip]

abbrev Terminating {α : Type} (r : α → α → Prop) := WellFounded (fun a b => Relation.TransGen r b a)

abbrev Terminating' {α : Type} (r : α → α → Prop) := WellFounded (fun a b => r b a)

theorem same {α : Type} {r : α → α → Prop} : Terminating r ↔ Terminating' r := by
  apply same_help

[Chris Henson]

The reference I am primarily working from is Term Rewriting and All That, where "terminating" is defined as there being no infinite descending chain, i.e. docs#wellFounded_iff_isEmpty_descending_chain

My thought process was simply that to match up with the induction principle
Screenshot_20251219-060912.png
they presented, that it seemed I needed to both flip and take the transitive closure. I knew about docs#WellFounded.transGen, but had trouble with the other direction of your proof. (And then questioned if it held since it wasn't in core already)

It would be nice to have this, can I adapt it into my PR?

[Chris Henson]

This can be written pretty compactly with grind, I think I'd just add this:

import Mathlib.Order.WellFounded

variable {α : Type*} {r : α → α → Prop}

theorem WellFounded.ofTransGen (trans_wf : WellFounded (Relation.TransGen r)) : WellFounded r := by
  grind [WellFounded.wellFounded_iff_has_min, Relation.TransGen]

[Malvin Gattinger]

Oh, nice. Maybe that one should even be in Mathlib Core already? And yes, feel free to use any of my code above in any way you want.

[Thomas Waring]

Malvin Gattinger said:

Oh, nice. Maybe that one should even be in Mathlib Core already? And yes, feel free to use any of my code above in any way you want.

It's not there but the version for Acc is: docs#acc_transGen_iff meaning this works too

theorem WellFounded.ofTransGen (trans_wf : WellFounded (Relation.TransGen r)) : WellFounded r :=
  ⟨fun x => acc_transGen_iff.mp <| trans_wf.apply x⟩

[Thomas Waring]

Terminating as you've defined it would often be called "strongly normalising" right? No need to change the name but perhaps you could mention that in the docstring. In eg untyped lambda calculi we also want to talk about particular terms that are strongly normalising, which would be equivalent to them being Acc, might be nice to have that as well.

[Eric Wieser]

I think you should rather add the Iff version, WellFounded (Relation.TransGen r) ↔ WellFounded r, as a simp lemma

[Chris Henson]

Thomas Waring said:

Terminating as you've defined it would often be called "strongly normalising" right? No need to change the name but perhaps you could mention that in the docstring. In eg untyped lambda calculi we also want to talk about particular terms that are strongly normalising, which would be equivalent to them being Acc, might be nice to have that as well.

Yes, SN and terminating (also Noetherian) are sometimes used as synonyms. I can add a note in the docstring. I agree that there are situations where it is useful to talk about this property on a subset of terms, I'd not thought about this yet.

[Thomas Waring]

great, thanks— ive been looking at intersection types a bit (on paper), so possibly down the track i can add the term-by-term version