## Stream: Coq users

### Topic: Defining a fold left induction principle

#### 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?

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

#### 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?

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

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

#### 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

#### 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?

#### Pierre Castéran (Aug 02 2022 at 12:11):

No, `a`is just the initial value of the accumulator 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.

#### 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

#### 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: Jun 24 2024 at 14:01 UTC