## Stream: Coq users

### Topic: How to prove Acc for some relation?

#### Daniel Hilst Selli (Feb 09 2022 at 14:55):

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.

#### Guillaume Melquiond (Feb 09 2022 at 14:57):

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

#### Guillaume Melquiond (Feb 09 2022 at 14:58):

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

#### Kenji Maillard (Feb 09 2022 at 14:58):

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 `<`.

#### Daniel Hilst Selli (Feb 09 2022 at 14:59):

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?

#### Daniel Hilst Selli (Feb 09 2022 at 14:59):

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

#### Karl Palmskog (Feb 09 2022 at 15:00):

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)

#### Kenji Maillard (Feb 09 2022 at 15:00):

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 ...`

#### Daniel Hilst Selli (Feb 09 2022 at 15:00):

Changing to `<` I got `H : 0 < len` in my context, yay!

#### Daniel Hilst Selli (Feb 09 2022 at 15:03):

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 :)

#### Daniel Hilst Selli (Feb 09 2022 at 15:05):

Thanks Kenji, the `a0 >> a1 >> a2 >> ...` example make everything much cleaner, now it's obvious why `<=` will not work

#### Pierre Castéran (Feb 09 2022 at 16:06):

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.

#### Daniel Hilst Selli (Feb 12 2022 at 22:14):

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`

#### Karl Palmskog (Feb 12 2022 at 22:28):

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.
``````

#### Karl Palmskog (Feb 12 2022 at 22:31):

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

#### Gaëtan Gilbert (Feb 12 2022 at 22:33):

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

#### Karl Palmskog (Feb 12 2022 at 22:36):

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.

#### Gaëtan Gilbert (Feb 12 2022 at 22:39):

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

#### Karl Palmskog (Feb 12 2022 at 22:43):

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

#### Karl Palmskog (Feb 12 2022 at 22:48):

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

#### Pierre Castéran (Feb 13 2022 at 06:58):

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: Feb 01 2023 at 11:04 UTC