proposition: Lemma fold_progress : forall (A B: Type) (conv: B -> A) g l (a init: A) (f := fun r el => match el with None => r | Some e => g r (conv e) end), (forall a b c, g (g a b) c = g a (g b c)) -> (forall a, g a init = g init a) -> g a (fold_left f l init) = fold_left f l (g init a).
proof: Proof. induction l. simpl; auto. intros a' init f g_assoc g_init_comm; destruct a. simpl. rewrite g_assoc. unfold f. rewrite <- (IHl (conv b) init); trivial. rewrite <- (IHl (g a' (conv b)) init); trivial. fold f. rewrite g_assoc; trivial. apply (IHl a' init); trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)