`Acc`

, `well_founded`

, and `well_founded_induction`

makes zero sense to me, I understand the very high level idea that well founded recursion induction is one that is structurally decreasing, but I cannot link that high level idea to those three definitions.

Well it is the constructive counterpart of no infinite decreasing sequence: an element is accessible if all the smaller elements are accessible. The base elements are accessible because there are no smaller ones, and then basically you say that for an accessible element, all decreasing paths reach one of the base elements eventually.

So no infinite decreasing sequence becomes all decreasing sequences are finite.

I understand what you said but I still feel lost.

```
Inductive Acc (x: A) : Prop :=
Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x.
```

nothing here says that the size of `y`

is less than the size of `x`

First, do you agree that Théo's definition "an element is accessible if all the smaller elements are accessible" is exactly what the type of the `Acc_intro`

constructor means? Second, by definition of inductive types in Coq, any object of type `Acc R x`

looks like a finitely deep tree (though possibly infinitely branching). If you combine both parts, then you get the usual meaning of a well-founded order.

consider something like

```
Fixpoint foorec {A} (l:list A) n (H:length l = n) {struct n} := ... (* eg recurse on "remove x l" knowing that x was in l *)
Definition foo {A} l := @foorec A l (length l) eq_refl.
```

ie recursion based on the size of the list

the relation given to Acc (ie `R`

) is a generalized version of "the first one is smaller than the second one"

walker said:

nothing here says that the size of

`y`

is less than the size of`x`

It is not the size; it is `y`

itself that is smaller than `x`

. And "smaller" is just a word used to shorten "in relation with respect to `R`

".

alright I kind of understand to some degree. but is there good reading material on this ?

I tried to explain it in Chapter 21 of my PhD thesis. I'll let you judge whether it's a good reading material or not.

One important thing to understand is that the *finiteness* @Théo Winterhalter is talking about is **build in** the `Inductive`

keyword. There is no notion of *size* in well foundedness in the sense of something that (computably) mesures values in `A`

. The mesure lies instead in the tree that is the proof of the `Acc R x`

predicate which live in `Prop`

.

You should read the code of both `Acc_rect`

and `Fix_F`

in the `Wf`

module of the standard library. Notice that `Acc_rect`

is auto-generated so you can just `Print Acc_rect`

. They both proceed by structural induction on the proof of the `Acc R _`

predicate.

Also notice that the `Acc`

predicate captures **more** than just the impossibility of infinite decreasing `R`

-sequences. It captures the finite termination of **any process** that unfolds along `R`

, not just those given by a *law* (eg decreasing *sequences in nat -> A*). I am quoting Th. Coquand here.

Last updated: Jan 29 2023 at 03:28 UTC