Add a fold operation over finite maps, and associated lemmas

theories/algebra/Bigop.eca

@@ -589,3 +589,49 @@ have: forall (i : int), exists j, i = 2 * j \/ i = 2 * j + 1 by smt().
 - case/(_ x) => y [] ->>; [left | right]; apply/mapP=> /=;
     by exists y; (split; first apply/mem_range); smt().
 qed.
+
+(* -------------------------------------------------------------------- *)
+require import FSet.
+
+(* -------------------------------------------------------------------- *)
+abbrev bigs ['a] (P : 'a -> bool) (F : 'a -> t) (s : 'a fset) =
+  big P F (elems s).
+
+(* -------------------------------------------------------------------- *)
+section BigFSet.
+declare type a.
+
+lemma bigs0 (P : a -> bool) (F : a -> t) : bigs P F fset0 = idm.
+proof. by rewrite elems_fset0 big_nil. qed.
+
+lemma bigs1 (F : a -> t) (x : a) : bigs predT F (fset1 x) = F x.
+proof. by rewrite elems_fset1 big_seq1. qed.
+
+lemma bigsU (P : a -> bool) (F : a -> t) (s1 s2 : a fset) : disjoint s1 s2 =>
+  bigs P F (s1 `|` s2) = (bigs P F s1) + (bigs P F s2).
+proof.
+move=> djt; rewrite -big_cat &(eq_big_perm) &(uniq_perm_eq).
+- by apply: uniq_elems.
+- rewrite uniq_catC &(cat_uniq) !uniq_elems /=.
+  by apply/hasPn=> x; rewrite -!memE &(disjointP).
+- by move=> x; rewrite mem_cat -!memE in_fsetU.
+qed.
+
+lemma bigsU1 (F : a -> t) (x : a) (s : a fset) :
+  x \notin s => bigs predT F (s `|` fset1 x) = F x + bigs predT F s.
+proof.
+move=> x_notin_s; rewrite bigsU.
+- by rewrite fsetIC; apply/disjointP=> a /in_fset1 ->.
+- by rewrite bigs1 addmC.
+qed.
+
+lemma bigsD1 (F : a -> t) (x : a) (s : a fset) :
+  x \in s => bigs predT F s = F x + bigs predT F (s `\` fset1 x).
+proof.
+move=> x_in_s; suff {1}->: s = (s `\` fset1 x) `|` fset1 x.
+- rewrite bigsU; last by rewrite bigs1 addmC.
+  by apply/disjointP=> a; rewrite in_fsetD1 in_fset1.
+by apply/fsetP=> a; rewrite in_fsetU1 in_fsetD1 /#.
+qed.
+
+end section BigFSet.

theories/datatypes/FMap.ec

@@ -958,3 +958,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

@@ -723,6 +723,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.
 
@@ -733,18 +734,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

@@ -2881,6 +2881,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 =>