Defining a fold left induction principle · Coq users

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

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):

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, ais 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).

Stream: Coq users

Topic: Defining a fold left induction principle

Daniel Hilst Selli (Aug 02 2022 at 00:07):