add new MSet theory (#722)

Author: oskgo

theories/algebra/Number.ec

@@ -1291,6 +1291,15 @@ qed.
 lemma maxrC (x y : t) : maxr x y = maxr y x.
 proof. by rewrite !maxrE lerNgt ler_eqVlt; case: (x = y); case: (x < y). qed.
 
+lemma maxrA (x y z: t): maxr (maxr x y) z = maxr x (maxr y z).
+proof. 
+rewrite !maxrE.
+case (y <= x); case (z <= y); case (z <= x) => //
+  [/#||/#|/#|].
+- smt(ler_trans).
+- smt(ltr_trans ltrNge).
+qed.
+
 lemma maxrl (x y : t) : x <= maxr x y.
 proof. by rewrite maxrE; case: (y <= x) => [_|/ltrNge/ltrW]. qed.
 
@@ -1347,6 +1356,15 @@ qed.
 lemma minrC (x y : t) : minr x y = minr y x.
 proof. by rewrite !minrE lerNgt ler_eqVlt; case: (y = x); case: (y < x). qed.
 
+lemma minrA (x y z: t): minr (minr x y) z = minr x (minr y z).
+proof. 
+rewrite !minrE.
+case (x <= y); case (y <= z); case (x <= z) => //
+  [/#||/#|/#|].
+- smt(ler_trans).
+- smt(ltr_trans ltrNge).
+qed.
+
 lemma minrl (x y : t) : minr x y <= x.
 proof. by rewrite minrE; case: (x <= y) => [_|/ltrNge/ltrW]. qed.
 

theories/datatypes/FMap.ec

@@ -200,6 +200,9 @@ lemma remE ['a 'b] (m : ('a, 'b) fmap) x y :
   (rem m x).[y] = if y = x then None else m.[y].
 proof. by rewrite /rem /"_.[_]" rem_valE SmtMap.get_setE. qed.
 
+lemma rem_set (m: ('a, 'b) fmap) x: x \in m => (rem m x).[x <- oget m.[x]] = m.
+proof. move => x_in; apply fmap_eqP => y; rewrite get_setE remE /#. qed.
+
 (* -------------------------------------------------------------------- *)
 lemma mem_rem ['a 'b] (m : ('a, 'b) fmap) x y :
   y \in (rem m x) <=> (y \in m /\ y <> x).
@@ -529,6 +532,44 @@ lemma mem_fdom_rem ['a 'b] (m : ('a, 'b) fmap) x y :
   y \in fdom (rem m x) <=> (y \in fdom m /\ y <> x).
 proof. by rewrite fdom_rem in_fsetD1. qed.
 
+(* ==================================================================== *)
+op offset (s: 'a fset): ('a, unit) fmap = 
+  ofmap (offun (fun e => if e \in s then Some () else None)).
+
+lemma mem_offset (s: 'a fset) x: x \in (offset s) <=> x \in s.
+proof.
+rewrite /dom getE ofmapK.
+- move: (FSet.finite_mem s).
+  apply/eq_ind/fun_ext => y.
+  rewrite offunE /#.
+rewrite offunE /#.
+qed.
+
+lemma offset_get s (e: 'a): (offset s).[e] = if e \in s then Some () else None.
+proof.
+rewrite getE /ofset ofmapK.
+- move: (FSet.finite_mem s).
+  apply/eq_ind/fun_ext => y.
+  rewrite offunE /#.
+rewrite offunE /#.
+qed.
+
+lemma offsetK: cancel offset fdom<:'a, unit>.
+proof. move => s; rewrite fsetP => x; by rewrite mem_fdom mem_offset. qed.
+
+(* ==================================================================== *)
+op offsetmap (f: 'a -> 'b) (s: 'a fset) : ('a, 'b) fmap = 
+  map (fun x y => f x) (offset s).
+
+lemma offsetmapT (s: 'a fset) (f: 'a -> 'b) e: e \in s => (offsetmap f s).[e] = Some (f e).
+proof. by move => e_in; rewrite /offsetmap mapE offset_get e_in. qed.
+
+lemma offsetmapN (s: 'a fset) (f: 'a -> 'b) e: e \notin s => (offsetmap f s).[e] = None.
+proof. by move => e_in; rewrite /offsetmap mapE offset_get e_in. qed.
+
+lemma mem_offsetmap s (f: 'a -> 'b) e: e \in offsetmap f s <=> e \in s.
+proof. by rewrite /offsetmap mem_map mem_offset. qed.
+
 (* ==================================================================== *)
 op [opaque] frng ['a 'b] (m : ('a, 'b) fmap) = oflist (to_seq (rng m)).
 lemma frngE (m : ('a, 'b) fmap): frng m = oflist (to_seq (rng m)).
@@ -741,6 +782,16 @@ lemma fsize_set (m : ('a, 'b) fmap) k v :
   fsize m.[k <- v] = b2i (k \notin m) + fsize m.
 proof. by rewrite /fsize fdom_set fcardU1 mem_fdom. qed.
 
+lemma fsize0_empty (m: ('a, 'b) fmap): fsize m = 0 => m = empty.
+proof.
+move: m; apply fmapW => [//| /= m k v].
+rewrite mem_fdom fsize_set =>->_/=. 
+smt(ge0_fsize).
+qed.
+
+lemma fsize_map m (f: 'a -> 'b -> 'c): fsize (map f m) = fsize m.
+proof. by rewrite /fsize fdom_map. qed.
+
 (* ==================================================================== *)
 
 (* f-collisions (i.e. collisions under some function f) *)

theories/datatypes/FSet.ec

@@ -1,5 +1,5 @@
 (* -------------------------------------------------------------------- *)
-require import Core Int List StdRing StdOrder.
+require import Core Int List StdRing StdOrder Finite.
 (*---*) import IntOrder.
 
 (* -------------------------------------------------------------------- *)
@@ -84,6 +84,9 @@ split=> // h; apply/fset_eq/uniq_perm_eq; 1,2: exact/uniq_elems.
 by move=> x; rewrite -!memE h.
 qed.
 
+lemma finite_mem (s: 'a fset): is_finite (mem s).
+proof. apply mkfinite; exists (elems s) => /#. qed.
+
 (* -------------------------------------------------------------------- *)
 op [opaque] fset0 ['a] = oflist [<:'a>]. 
 lemma set0E: fset0<:'a> = oflist [<:'a>] by rewrite/fset0.

theories/datatypes/List.ec

@@ -224,6 +224,14 @@ proof. by rewrite /nseq iter1. qed.
 lemma nseqS n (x : 'a) : 0 <= n => nseq (n+1) x = x :: nseq n x.
 proof. by move=> le0_n; rewrite /nseq iterS. qed.
 
+lemma nseq_eq (x y: 'a) n m: 
+  nseq n x = nseq m y => (x = y /\ n = m) \/ (n <= 0 /\ m <= 0).
+proof. 
+move => nseq_eq; have: max 0 n = max 0 m by smt(size_nseq).
+case (n <= 0) => [/#|]; case (m <= 0) => [/#|/=]/ltzNge mgt0/ltzNge ngt0 max_eq.
+move: nseq_eq; rewrite (nseqS (n-1)) 2:(nseqS (m-1)); smt(ltzW).
+qed.
+
 lemma nseqSr n (x : 'a): 0 <= n => nseq (n+1) x = rcons (nseq n x) x.
 proof.
 elim: n=> /= [|i ge0_i ih]; first by rewrite nseq0 nseq1.
@@ -694,6 +702,13 @@ elim: s=> /= [|y s ih @/pred1]; first by rewrite nseq0.
 by case: (y = x)=> //; rewrite addzC nseqS ?count_ge0.
 qed.
 
+lemma count_nseq (x: 'a) n p: count p (nseq n x) = if p x then max 0 n else 0.
+proof.
+move: n; apply natind => n n_bound /=.
+- rewrite nseq0_le //= /#. 
+move => IH; rewrite nseqS //= lez_maxr /#.
+qed.
+
 lemma has_nseq a n (x : 'a) : has a (nseq n x) <=> (0 < n) /\ a x.
 proof.
 elim/natind: n => /= [n ^le0_n /lezNgt->|n ge0_n]; 1: by rewrite nseq0_le.
@@ -1263,6 +1278,13 @@ qed.
 lemma all_rem p (x : 'a) (s : 'a list): all p s => all p (rem x s).
 proof. by move=> /allP h; apply/allP=> y /mem_rem /h. qed.
 
+lemma count_remP ['a] (p : 'a -> bool) (s : 'a list) x :
+  count p (rem x s) = count p s - b2i (p x /\ x \in s).
+proof. 
+case (x \in s) => [/perm_to_rem/perm_eqP/(_ p)->/#|x_in].
+by rewrite rem_id.
+qed.
+
 lemma count_rem ['a] (p : 'a -> bool) (s : 'a list) x : x \in s =>
   count p s = b2i (p x) + count p (rem x s).
 proof. by move/perm_to_rem/perm_eqP/(_ p)=> ->. qed.