The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hi. You can have a look at the Coq library on rewriting and termination 
CoLoR on https://github.com/fblanqui/color/. See in particular 
https://github.com/fblanqui/color/tree/master/Util/Relation and 
https://github.com/fblanqui/color/blob/master/Util/Relation/NotSN_IS.v . 
Best regards, Frédéric.

Le 18/02/2023 à 21:54, mukesh tiwari a écrit :
> Hi everyone,
>
> Recently, I stumbled across the book ML for the Working Programmer [1]
>   and saw this text,
>
> "Infinite decreasing chains are intuitively appealing, but other
> definitions of well-foundedness permit simpler proofs. For instance, ≺
> is well-founded just if every non-empty set contains a ≺-minimal
> element. There also exist definitions suited for constructive logic."
> (see page 246 of[1]).
>
> In all my formalisation, and the ones that I have seen on GitHub, all
> of them have used infinite decrease chains, defined in Coq library
> [2]. My question is: are there any other Coq formalisations that use
> other definitions of well-foundedness, not the Acc one [2].
>
> Best,
> Mukesh
>
> [1] https://www.cl.cam.ac.uk/~lp15/MLbook/PDF/chapter6.pdf
> [2] https://coq.inria.fr/library/Coq.Init.Wf.html