Exemples d'utilisation de MSets dans Coq

Question

MSets semblent être la voie à suivre pour les jeux finis de type OCaml. Malheureusement, je ne peux pas trouver des exemples d'utilisation. Comment puis-je définir un MSet vide ou un singleton MSet? Comment puis-je union deux MSets ensemble?

Answer 1

Laissez-moi vous montrer un exemple simple pour des ensembles finis de nombres naturels:

From Coq 
Require Import MSets Arith. 

(* We can make a set out of an ordered type *) 
Module S := Make Nat_as_OT. 

Definition test := S.union (S.singleton 42) 
          (S.empty). 

(* membership *) 
Compute S.mem 0 test. (* evaluates to `false` *) 
Compute S.mem 42 test. (* evaluates to `true` *) 

Compute S.is_empty test.  (* evaluates to `false` *) 
Compute S.is_empty S.empty. (* evaluates to `true` *) 

Vous pouvez lire Coq.MSets.MSetInterface pour découvrir les opérations et les spécifications MSet s fournissent.