Stream: Coq users

Topic: How to prove Acc for some relation?


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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 <.

view this post on Zulip 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?

view this post on Zulip Daniel Hilst Selli (Feb 09 2022 at 14:59):

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

view this post on Zulip 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)

view this post on Zulip 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 ...

view this post on Zulip Daniel Hilst Selli (Feb 09 2022 at 15:00):

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

view this post on Zulip 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 :)

view this post on Zulip 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

view this post on Zulip Pierre Castéran (Feb 09 2022 at 16:06):

A convenient way to be at ease with Accis 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 natis 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Feb 12 2022 at 22:31):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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_accinto an application of lt_wf, Wellfounded.Inclusion.Acc_incland 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_incland 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: Mar 29 2024 at 10:01 UTC