Timings for MSetToFiniteSet.v
- /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-stdlib.dev/_build/default/theories//./MSets/MSetToFiniteSet.timing
- /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-stdlib.dev/_build/default/theories//./MSets/MSetToFiniteSet.timing
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** * Finite sets library : conversion to old [Finite_sets] *)
Require Import Ensembles Finite_sets.
Require Import MSetInterface MSetProperties OrdersEx.
(** * Going from [MSets] with usual Leibniz equality
to the good old [Ensembles] and [Finite_sets] theory. *)
Module WS_to_Finite_set (U:UsualDecidableType)(M: WSetsOn U).
Module MP:= WPropertiesOn U M.
Import M MP FM Ensembles Finite_sets.
Definition mkEns : M.t -> Ensemble M.elt :=
fun s x => M.In x s.
Notation " !! " := mkEns.
Lemma In_In : forall s x, M.In x s <-> In _ (!!s) x.
unfold In; compute; auto with extcore.
Lemma Subset_Included : forall s s', s[<=]s' <-> Included _ (!!s) (!!s').
unfold Subset, Included, In, mkEns; intuition.
Notation " a === b " := (Same_set M.elt a b) (at level 70, no associativity).
Lemma Equal_Same_set : forall s s', s[=]s' <-> !!s === !!s'.
rewrite double_inclusion.
unfold Subset, Included, Same_set, In, mkEns; intuition.
Lemma empty_Empty_Set : !!M.empty === Empty_set _.
unfold Same_set, Included, mkEns, In.
split; intro; set_iff; inversion 1.
Lemma Empty_Empty_set : forall s, Empty s -> !!s === Empty_set _.
unfold Same_set, Included, mkEns, In.
Lemma singleton_Singleton : forall x, !!(M.singleton x) === Singleton _ x .
unfold Same_set, Included, mkEns, In.
split; intro; set_iff; inversion 1; try constructor; auto.
Lemma union_Union : forall s s', !!(union s s') === Union _ (!!s) (!!s').
unfold Same_set, Included, mkEns, In.
split; intro; set_iff; inversion 1; [ constructor 1 | constructor 2 | | ]; auto.
Lemma inter_Intersection : forall s s', !!(inter s s') === Intersection _ (!!s) (!!s').
unfold Same_set, Included, mkEns, In.
split; intro; set_iff; inversion 1; try constructor; auto.
Lemma add_Add : forall x s, !!(add x s) === Add _ (!!s) x.
unfold Same_set, Included, mkEns, In.
split; intro; set_iff; inversion 1; auto with sets.
constructor 2; constructor.
Lemma Add_Add : forall x s s', MP.Add x s s' -> !!s' === Add _ (!!s) x.
unfold Same_set, Included, mkEns, In.
red in H; rewrite H in H0.
constructor 2; constructor.
Lemma remove_Subtract : forall x s, !!(remove x s) === Subtract _ (!!s) x.
unfold Same_set, Included, mkEns, In.
split; intro; set_iff; inversion 1; auto with sets.
Lemma mkEns_Finite : forall s, Finite _ (!!s).
intro s; pattern s; apply set_induction; clear s; intros.
intros; replace (!!s) with (Empty_set elt); auto with sets.
symmetry; apply Extensionality_Ensembles.
apply Empty_Empty_set; auto.
replace (!!s') with (Add _ (!!s) x).
symmetry; apply Extensionality_Ensembles.
Lemma mkEns_cardinal : forall s, cardinal _ (!!s) (M.cardinal s).
intro s; pattern s; apply set_induction; clear s; intros.
intros; replace (!!s) with (Empty_set elt); auto with sets.
rewrite MP.cardinal_1; auto with sets.
symmetry; apply Extensionality_Ensembles.
apply Empty_Empty_set; auto.
replace (!!s') with (Add _ (!!s) x).
rewrite (cardinal_2 H0 H1); auto with sets.
symmetry; apply Extensionality_Ensembles.
(** we can even build a function from Finite Ensemble to MSet
... at least in Prop. *)
Lemma Ens_to_MSet : forall e : Ensemble M.elt, Finite _ e ->
exists s:M.t, !!s === e.
destruct IHFinite as (s,Hs).
apply Extensionality_Ensembles in Hs.
Module S_to_Finite_set (U:UsualOrderedType)(M: SetsOn U) :=
WS_to_Finite_set U M.