Stream: Coq users

Topic: Defining a fold left induction principle


view this post on Zulip Daniel Hilst Selli (Aug 02 2022 at 00:07):

Doing induction in fold_left is a problem because of the accumulator, I was wondering if it's possible to define a inductive principle for left folds to make proofs easier, I came up with this but I don't know if it's correct or if is provable in general

Axiom fold_left_ind : forall (A B : Set) (P : A -> Prop) (f : A -> B -> A),
 (forall acc, P (fold_left f nil acc)) ->
 (forall acc l hd, P (fold_left f (hd :: l) acc) -> P (fold_left f l (f acc hd))) ->
 forall acc l, P (fold_left f l acc).

Is this correct/reasonable?

view this post on Zulip Guillaume Melquiond (Aug 02 2022 at 04:30):

This cannot be correct. Your second antecedent is definitionally true, while the first one trivially implies the consequent.

view this post on Zulip Guillaume Melquiond (Aug 02 2022 at 04:32):

Usually, in presence of fold_left, you rewrite it into fold_right and then perform an induction on the reverted list. Maybe it would help to find a proper induction principle?

view this post on Zulip Li-yao (Aug 02 2022 at 07:37):

You could try using Function or Equations to define fold_left and derive an induction principle for it.

view this post on Zulip Pierre Castéran (Aug 02 2022 at 11:36):

You can also prove a forward induction scheme like:

Lemma  fold_left_ind  (A B : Set)
  (P : A -> list B -> A ->Prop)
  (f : A -> B -> A) (a:A):
    P a nil a ->
    (forall  b l x, P a l x -> P a (l++[b]) (f x b)) ->
    forall l, P a l (fold_left f l a).

view this post on Zulip Daniel Hilst Selli (Aug 02 2022 at 11:52):

@Guillaume Melquiond does this always hold?,
@Li-yao I'm looking into Function thanks
@Pierre Castéran I'm still trying to understand the lemma

view this post on Zulip Daniel Hilst Selli (Aug 02 2022 at 11:55):

@Pierre Castéran I see I think this was what I was trying to state, thanks. I see that you fixed (a : A) this is the accumulator?

view this post on Zulip Pierre Castéran (Aug 02 2022 at 12:11):

No ais the initial value before the computation. The accumulator's role is played by the third argument of P.
Intuitively, this lemma reflects the way how fold_left runs left-to-right along l. It should be interesting to compare it with the lemma you will obtain with Function.

Note that, if you re-define fold_left, but you still want to apply some Standard Library lemmas about this function, you will probably have to prove that your function and Stdlib's are extensionally equivalent.

view this post on Zulip Daniel Hilst Selli (Aug 02 2022 at 22:12):

Thank you, Pierre, I'll spend some time studying the lemma that you stated, never used Function also, it would be worth learning it

view this post on Zulip Pierre Castéran (Aug 03 2022 at 05:14):

Hi, Daniel,
This lemma is easy to prove by well-founded induction on list length (with the help of List.fold_left_app).


Last updated: Feb 09 2023 at 00:03 UTC