Extend sets with filter and cartesian product
Looking at the modules inside set.mlw
, I'm wondering whether or not it is possible to extend some of them.
For the filter
function defined in module Fset
, can we also have it in SetApp
?
What about Set
? I understand that these are potentially infinite sets, is it an issue ?
Another operator on sets that I think would be nice to have is the cartesian product. For the finite sets, this can be added by:
let rec ghost function cartesian_product (s1 : fset 'a) (s2 : fset 'b)
variant { cardinal s1 }
ensures { forall x y. mem (x, y) result <-> mem x s1 /\ mem y s2 }
=
if is_empty s1 then empty
else let x1 = pick s1 in
union (map (fun y -> (x1, y)) s2)
(cartesian_product (remove x1 s1) s2)
Could we also add a cartesian product for all kinds of sets ?