I'm trying to understand well-founded relations and recursion. I know that there are easier ways to define non-trivial recursive functions but I want to get a better intuition on `Acc`

and well-fondness I have this lemma, an simplification on the CPDT chapter

```
Require Import Coq.Lists.List.
Set Implicit Arguments.
Definition length_order {A : Type} (a b : list A) :=
length a <= length b.
Lemma length_order_acc : forall {A : Type} (l : list A) len,
length l <= len -> Acc length_order l.
intros.
unfold length_order. induction l.
{ simpl in *.
refine (@Acc_intro (list A) length_order nil (fun y =>
fun _ => _)).
(* and we are back to the beginning *)
```

After induction I have this goal `Acc (fun a b : list A => length a <= length b) nil`

but I have zero ideas on how to attack it. I tried constructor but I go in a loop, introducing a variable and getting back to the same goal. I searched for a way to do induction on `Acc`

instead because of this loop thing but didn't find anything.

Usually, you will get a contradiction in your context, which you can use to break out of the loop.

(And if you don't have one, you are missing some information, because this is basically the only way to build `Acc`

.)

Your relation `length_order`

is reflexive, it cannot be well-founded, so you'll probably have some difficulties trying to prove that it is. You should probably change `<=`

to `<`

.

So I follow the loop until I got a contradiction on the context, on the base case of induction I think the first iteration or the second would reach the contradiction right?

Oh, I didn't know about that, it makes sense, thanks Kanji!

I usually find it helpful to go back to the slogan about "no infinite descending chains". If at a high level it looks convincing that there aren't any descending chain, then one can start doing the `Acc`

proof, but indirect proofs are usually most convenient (see: `wf_inverse_image`

and the like)

The idea of a well-founded relation `>>`

is that any chain `a0 >> a1 >> a2 >> ...`

has to be finite, so if there is an `a`

such that `a >> a`

then you get the infinite chain `a >> a >> a >> a ...`

Changing to `<`

I got `H : 0 < len`

in my context, yay!

I know that there are more convenient ways (besides not knowing how to use them yet) Karl, but I want to build intuition first, then go to other alternatives. You know that programming tutorial maximum, in chapter 3 you learn that you don't need chapters 1 and 2, it's something like that :)

Thanks Kenji, the `a0 >> a1 >> a2 >> ...`

example make everything much cleaner, now it's obvious why `<=`

will not work

A convenient way to be at ease with `Acc`

is to re-invent the wheel, i.e.. to prove as an exercise a few lemmas of the Standard Library, e.g. that the order `<`

on `nat`

is well-founded, that no reflexive relation (on a non-empty type) is well-founded, and some closure properties (simple lexicographic product, inverse image, etc.) Proving that a well-founded relation (in Coq's meaning) has no descending chain is a good exercise too.

Hello folks

I get the weekend to study this, the base case was easy to do but I can't find a way to finish the inductive case I have this so far

```
Require Import Coq.Lists.List.
Require Import Lia.
Import ListNotations.
From Hammer Require Import Tactics.
Set Implict Arguments.
Definition lenord {A : Type} (l1 l2 : list A) :=
length l1 < length l2.
Lemma lenord_acc : forall {A : Type} (l : list A) len,
length l < len -> Acc lenord l.
assert (length_pos : forall {A} (ll : list A),
length ll < 0 -> ll = []) by (induction ll; simpl; [easy|lia]).
intros. unfold lenord. constructor.
intros. induction l; [easy|].
apply IHl; [simpl in H; lia|].
simpl in *.
unfold lt in H0.
apply le_S_n in H0.
(* goal *)
1 subgoal
length_pos : forall (A : Type) (ll : list A), length ll < 0 -> ll = []
A : Type
a : A
l : list A
len : nat
H : S (length l) < len
y : list A
H0 : length y <= length l
IHl : length l < len ->
length y < length l ->
Acc (fun l1 l2 : list A => length l1 < length l2) y
========================= (1 / 1)
length y < length l
```

I'm starting to think that I got the wrong path on the proof. Any advice to point me to the right direction is welcome :)

At that point I have ` length y <= length l`

in my context this implies that `length y = length l \/ length y < length l`

I was trying to prove that `length y = length l -> False`

so that I can keep with the right side of `\/`

and finish my goal, but can't find a way to prove `length y = length l -> False`

why prove this explicitly using `Acc`

, when you have stuff like `well_founded_lt_compat`

?

```
From Coq Require Import List.
From Coq Require Import Wf_nat.
Import ListNotations.
Definition lenord {A : Type} (l1 l2 : list A) :=
length l1 < length l2.
Lemma wf_lenord A : well_founded (@lenord A).
Proof. apply (well_founded_lt_compat _ (fun l => length l)); auto. Qed.
```

here, `well_founded (@lenord A)`

is definitionally equal to `forall l, Acc (@lenord A) l`

well_founded_ltof is even more direct (no need for auto, and no need for explicit arguments)

the whole `len, length l < len`

is superfluous, since `len`

is not used in the conclusion, and in fact all lists have some natural number that is greater than their length, so no need to pass that as an argument/premise.

no, that's basically how the proof of well_founded_ltof works (induction on a bigger n)

of course if you use the lemma you don't need to reprove it

but that would be some intra-proof construction (prove something more contrived to be able to apply induction), not something you put in the statement of the lemma

I think the situation overall with automation for well-foundedness proofs is pretty terrible though, although CoLoR and Rainbow has some

Another point of view (learning Coq) is given by the decomposition of a proof of lemmas like `le_nord_acc`

into an application of `lt_wf`

, `Wellfounded.Inclusion.Acc_incl`

and `Wellfounded.Inverse_Image.Acc_inverse_image`

.

For each argument in the proof of `le_nord_acc`

, you can see to which of the three lemmas it belongs. The combination of `wf_incl`

and `wf_inverse_image`

gives you a generic way to prove accessibility by reduction to an already known well-founded relation (by a measure), which may be used with much more complex order types than omega.

Last updated: Dec 01 2023 at 06:01 UTC