Add a fold operation over finite maps, and associated lemmas

theories/datatypes/FMap.ec

@@ -907,3 +907,49 @@ proof. by apply fmap_eqP=> z; rewrite mergeE // !get_setE mergeE // /#. qed.
 lemma mem_pair_map (m1: ('a, 'b1)fmap) (m2: ('a, 'b2)fmap) x:
   (x \in pair_map m1 m2) = (x \in m1 /\ x \in m2).
 proof. by rewrite /dom mergeE // /#. qed.
+
+(* -------------------------------------------------------------------- *)
+lemma fmap_ind (p : ('a, 'b) fmap -> bool):
+     p empty
+  => (forall m k v, p (rem m k) => p m.[k <- v])
+  => forall m, p m.
+proof.
+move=> p_empty pS; elim/fmapW=> //.
+by move=> m k v; rewrite mem_fdom=> /rem_id {1}<- /pS ->.
+qed.
+
+(* -------------------------------------------------------------------- *)
+op [opaque] fold (f : 'a -> 'b -> 'c -> 'c) z (m : ('a, 'b) fmap) =
+  fold (fun x s=> f x (oget m.[x]) s) z (fdom m).
+
+lemma foldE (f : 'a -> 'b -> 'c -> 'c) z m:
+  fold f z m = fold (fun x s=> f x (oget m.[x]) s) z (fdom m).
+proof. by rewrite /fold. qed.
+
+lemma fold0 (f : 'a -> 'b -> 'c -> 'c) z:
+  fold f z empty = z.
+proof. by rewrite foldE fdom0 fold0. qed.
+
+lemma fold1 (f : 'a -> 'b -> 'c -> 'c) z x y:
+  fold f z empty.[x <- y] = f x y z.
+proof. by rewrite foldE fdom_set fdom0 fset0U fold1 /= get_set_sameE. qed.
+
+lemma fold_set_neq (f : 'a -> 'b -> 'c -> 'c) z m x y:
+     (forall a a' z,
+           a \in m.[x <- y]
+        => a' \in m.[x <- y]
+        =>   f a (oget m.[x <- y].[a]) (f a' (oget m.[x <- y].[a']) z)
+           = f a' (oget m.[x <- y].[a']) (f a (oget m.[x <- y].[a]) z))
+  => x \notin m
+  => fold f z m.[x <- y] = f x y (fold f z m).
+proof.
+move=> fCA x_notin_m; rewrite foldE fdom_set.
+rewrite (foldC_in x) /=.
++ by move=> a a' b; smt(in_fsetU in_fset1 mem_set mem_fdom).
++ by move=> /=; rewrite in_fsetU in_fset1.
+rewrite get_set_sameE fsetDK /oget /=.
+rewrite -fdom_rem rem_id //.
+congr; rewrite foldE; apply: eq_in_fold.
+move=> a /mem_fdom a_in_m /=.
+by rewrite get_set_neqE // -negP=> <<-.
+qed.

theories/datatypes/FSet.ec

@@ -720,6 +720,7 @@ qed.
 (* -------------------------------------------------------------------- *)
 op [opaque] fold (f : 'a -> 'b -> 'b) (z : 'b) (A : 'a fset) : 'b =
   foldr f z (elems A).
+
 lemma foldE (f : 'a -> 'b -> 'b) z A: fold f z A = foldr f z (elems A).
 proof. by rewrite/fold. qed.
 
@@ -730,18 +731,35 @@ lemma fold1 (f : 'a -> 'b -> 'b) (z : 'b) (a : 'a):
   fold f z (fset1 a) = f a z.
 proof. by rewrite foldE elems_fset1. qed.
 
+lemma foldC_in (a : 'a) (f : 'a -> 'b -> 'b) (z : 'b) (A : 'a fset):
+  (forall a a' b, a \in A => a' \in A => f a (f a' b) = f a' (f a b)) =>
+  a \in A =>
+  fold f z A = f a (fold f z (A `\` fset1 a)).
+proof.
+move=> f_commutative a_in_A; rewrite !foldE (foldr_rem_in a) //.
++ by move=> z0 x y; rewrite -!memE; exact:f_commutative.
++ by rewrite -memE.
+congr; apply/foldr_perm_in=> //.
++ move=> z0 x y /mem_rem + /mem_rem; rewrite -!memE; exact:f_commutative.
+rewrite setDE rem_filter 1:uniq_elems//.
+have ->: predC (mem (fset1 a)) = predC1 a (* FIXME: views *)
+  by apply/fun_ext=> x; rewrite /predC /predC1 in_fset1.
+rewrite -{1}(undup_id (filter (predC1 a) (elems A))) 2:oflistK//.
+by apply/filter_uniq/uniq_elems.
+qed.
+
 lemma foldC (a : 'a) (f : 'a -> 'b -> 'b) (z : 'b) (A : 'a fset):
   (forall a a' b, f a (f a' b) = f a' (f a b)) =>
-  mem A a =>
+  a \in A =>
   fold f z A = f a (fold f z (A `\` fset1 a)).
+proof. by move=> f_commutative; apply: foldC_in=> + + + _ _. qed.
+
+lemma eq_in_fold (f g : 'a -> 'b -> 'b) (z : 'b) (A : 'a fset):
+  (forall a, a \in A => f a = g a) =>
+  fold f z A = fold g z A.
 proof.
-  move=> f_commutative a_in_A; rewrite !foldE (foldr_rem a)// 1:-memE//.
-  congr; apply/foldr_perm=> //.
-  rewrite setDE rem_filter 1:uniq_elems//.
-  have ->: predC (mem (fset1 a)) = predC1 a (* FIXME: views *)
-    by apply/fun_ext=> x; rewrite /predC /predC1 in_fset1.
-  rewrite -{1}(undup_id (filter (predC1 a) (elems A))) 2:oflistK//.
-  by apply/filter_uniq/uniq_elems.
+move=> f_eq_in; rewrite !foldE.
+by apply: eq_in_foldr=> // x; rewrite -memE=> /f_eq_in.
 qed.
 
 (* -------------------------------------------------------------------- *)

theories/datatypes/List.ec

@@ -2820,6 +2820,12 @@ proof.
   by rewrite Hlci.
 qed.
 
+lemma foldr_rem_in ['b 'a] x o z (s : 'a list) :
+  (forall (z : 'b) , left_commutative_in o z s) =>
+  x \in s =>
+  foldr o z s = o x (foldr o z (rem x s)).
+proof. by move=> fAC /perm_to_rem peq; rewrite (@foldr_perm_in o _ _ fAC peq z). qed.
+
 op right_commutative_in ['a 'b] o (x : 'a) (s : 'b list) =
   forall y z ,
     y \in s =>