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?

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

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?

You could try using `Function`

or `Equations`

to define `fold_left`

and derive an induction principle for it.

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

@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

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

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.

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

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