proposition: Lemma fold_left_comm: forall {A B} (f: A -> B -> A) l1 l2 init, (forall a b1 b2, f (f a b1) b2 = f (f a b2) b1) -> Permutation l1 l2 -> fold_left f l1 init = fold_left f l2 init.
proof: Proof. intros. remember (length l1). assert (length l1 <= n) by lia. clear Heqn. revert init l1 l2 H1 H0. induction n; intros; destruct l1. - apply Permutation_nil in H0. subst l2. simpl. reflexivity. - simpl in H1; exfalso; lia. - apply Permutation_nil in H0. subst l2. simpl. reflexivity. - simpl in H1. assert (length l1 <= n) by lia. clear H1. assert (In b l2) by (apply Permutation_in with (x := b) in H0; [assumption | left; reflexivity]). apply in_split in H1. destruct H1 as [l3 [l4 ?]]. subst l2. apply Permutation_cons_app_inv in H0. simpl. rewrite IHn with (l2 := l3 ++ l4) by assumption. rewrite !fold_left_app. simpl. f_equal. clear -H. revert b init. rev_induction l3; simpl. 1: reflexivity. rewrite !fold_left_app. simpl. rewrite H. f_equal. apply H0. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver