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
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
@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?
ais the initial value before the computation. The accumulator's role is played by the third argument of
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
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
This lemma is easy to prove by well-founded induction on list length (with the help of
Last updated: Feb 09 2023 at 00:03 UTC