Improvements to `Relation.Binary.Rewriting`?

[jamesmckinna]

Issue #2075 draws attention to the lack of a definition of StronglyNormalising (SN) of a relation R, defined by

StronglyNormalising (R : Rel A ℓ) = WellFounded (flip R)

One fix might be to add such a definition to PR #2077...
... but a better one might be to add a new module Induction.Normalising defining both the above, and

data WeaklyNormalising (N : Pred A ℓ₁) (R : Rel A ℓ₂) : Pred A _ where
  norm : ∀ {x} → N x → WeaklyNormalising N R x
  step : ∀ {x y} → R x y → WeaklyNormalising N R y → WeaklyNormalising N R x

such that ... suitable properties hold on the basis of suitable assumptions about N and R... (to be continued)

Ooops! I hadn't previously been aware of Relation.Binary.Rewriting!

[jamesmckinna]

Similarly: 'almost full' (AF) relations, aka 'well-quasi-order's (WQOs) ... based on this paper from 2012 ITP by Vytiniotis, Coquand and Wahlstedt

[gallais]

FTR, I have some of AF formalised in Idris: https://github.com/gallais/potpourri/blob/main/idris/papers/almostfull21/src/AlmostFull.idr

[jwaldmann]

Re: Relation.Binary.Rewriting (just bike-shedding the name)

it claims "Concepts from rewriting theory" while it actually is about "abstract reduction systems" (e.g., Baader/Nipkow Chapter 2, https://www21.in.tum.de/~nipkow/TRaAT/toc.html; TeReSe Chapter 1) That's fine to have, but "rewriting" also suggests concrete instances (rewriting on strings, terms, graphs, ...; see other chapters of cited books).