The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Mukesh,

Actually, Acc is not about "infinite decreasing chains" if
you think of chains as in the type nat -> X, because
those are chains given by laws and Acc captures chains
beyond those given by a law (ie a program).

I did write this to explain some aspects of the accessibility
predicates and how it compares with chain based definitions
here: 

https://github.com/DmxLarchey/Accessibility/blob/main/acc.v

This was for Raj at first but I see no reason not to
share ;-)

Best regards,

Dominique


----- Mail original -----
> De: "mukesh tiwari" <mukeshtiwari.iiitm AT gmail.com>
> À: "coq-club" <coq-club AT inria.fr>
> Envoyé: Samedi 18 Février 2023 21:54:20
> Objet: [Coq-Club] Alternate Definition of Well-Foundedness

> 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