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: Oct 13 2024 at 01:02 UTC