Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \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.forall (s : t) (x : elt), M.In x s <-> In elt (!! s) x
 Proof.forall (s : t) (x : elt), M.In x s <-> In elt (!! s) x
 unfold In; compute; auto with extcore.
 Qed.

 Lemma Subset_Included : forall s s',  s[<=]s'  <-> Included _ (!!s) (!!s').forall s s' : t,
s [<=] s' <-> Included elt (!! s) (!! s')
 Proof.forall s s' : t,
s [<=] s' <-> Included elt (!! s) (!! s')
 unfold Subset, Included, In, mkEns; intuition.
 Qed.

 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'.forall s s' : t, s [=] s' <-> !! s === !! s'
 Proof.forall s s' : t, s [=] s' <-> !! s === !! s'
 intros.s, s':t
s [=] s' <-> !! s === !! s'
 rewrite double_inclusion.s, s':t
s [<=] s' /\ s' [<=] s <-> !! s === !! s'
 unfold Subset, Included, Same_set, In, mkEns; intuition.
 Qed.

 Lemma empty_Empty_Set : !!M.empty === Empty_set _.!! empty === Empty_set elt
 Proof.!! empty === Empty_set elt
 unfold Same_set, Included, mkEns, In.(forall x : elt, M.In x empty -> Empty_set elt x) /\
(forall x : elt, Empty_set elt x -> M.In x empty)
 split; intro; set_iff; inversion 1.
 Qed.

 Lemma Empty_Empty_set : forall s, Empty s -> !!s === Empty_set _.forall s : t, Empty s -> !! s === Empty_set elt
 Proof.forall s : t, Empty s -> !! s === Empty_set elt
 unfold Same_set, Included, mkEns, In.forall s : t,
Empty s ->
(forall x : elt, M.In x s -> Empty_set elt x) /\
(forall x : elt, Empty_set elt x -> M.In x s)
 split; intros.s:t
H:Empty s
x:elt
H0:M.In x s
Empty_set elt x
s:t
H:Empty s
x:elt
H0:Empty_set elt x
M.In x s
 destruct(H x H0).s:t
H:Empty s
x:elt
H0:Empty_set elt x
M.In x s
 inversion H0.
 Qed.

 Lemma singleton_Singleton : forall x, !!(M.singleton x) === Singleton _ x .forall x : elt, !! (singleton x) === Singleton elt x
 Proof.forall x : elt, !! (singleton x) === Singleton elt x
 unfold Same_set, Included, mkEns, In.forall x : elt,
(forall x0 : elt,
 M.In x0 (singleton x) -> Singleton elt x x0) /\
(forall x0 : elt,
 Singleton elt x x0 -> M.In x0 (singleton x))
 split; intro; set_iff; inversion 1; try constructor; auto.
 Qed.

 Lemma union_Union : forall s s', !!(union s s') === Union _ (!!s) (!!s').forall s s' : t,
!! (union s s') === Union elt (!! s) (!! s')
 Proof.forall s s' : t,
!! (union s s') === Union elt (!! s) (!! s')
 unfold Same_set, Included, mkEns, In.forall s s' : t,
(forall x : elt,
 M.In x (union s s') ->
 Union elt (fun x0 : elt => M.In x0 s)
   (fun x0 : elt => M.In x0 s') x) /\
(forall x : elt,
 Union elt (fun x0 : elt => M.In x0 s)
   (fun x0 : elt => M.In x0 s') x ->
 M.In x (union s s'))
 split; intro; set_iff; inversion 1; [ constructor 1 | constructor 2 | | ]; auto.
 Qed.

 Lemma inter_Intersection : forall s s', !!(inter s s') === Intersection _ (!!s) (!!s').forall s s' : t,
!! (inter s s') === Intersection elt (!! s) (!! s')
 Proof.forall s s' : t,
!! (inter s s') === Intersection elt (!! s) (!! s')
 unfold Same_set, Included, mkEns, In.forall s s' : t,
(forall x : elt,
 M.In x (inter s s') ->
 Intersection elt (fun x0 : elt => M.In x0 s)
   (fun x0 : elt => M.In x0 s') x) /\
(forall x : elt,
 Intersection elt (fun x0 : elt => M.In x0 s)
   (fun x0 : elt => M.In x0 s') x ->
 M.In x (inter s s'))
 split; intro; set_iff; inversion 1; try constructor; auto.
 Qed.

 Lemma add_Add : forall x s, !!(add x s) === Add _ (!!s) x.forall (x : elt) (s : t),
!! (add x s) === Add elt (!! s) x
 Proof.forall (x : elt) (s : t),
!! (add x s) === Add elt (!! s) x
 unfold Same_set, Included, mkEns, In.forall (x : elt) (s : t),
(forall x0 : elt,
 M.In x0 (add x s) ->
 Add elt (fun x1 : elt => M.In x1 s) x x0) /\
(forall x0 : elt,
 Add elt (fun x1 : elt => M.In x1 s) x x0 ->
 M.In x0 (add x s))
 split; intro; set_iff; inversion 1; auto with sets.x:elt
s:t
x0:elt
H:x = x0 \/ M.In x0 s
H0:x = x0
Add elt (fun x1 : elt => M.In x1 s) x x0
x:elt
s:t
x0:elt
H:x = x0 \/ M.In x0 s
H0:M.In x0 s
Add elt (fun x1 : elt => M.In x1 s) x x0
 inversion H0.x:elt
s:t
x0:elt
H:x = x0 \/ M.In x0 s
H0, H1:x = x0
Add elt (fun x1 : elt => M.In x1 s) x0 x0
x:elt
s:t
x0:elt
H:x = x0 \/ M.In x0 s
H0:M.In x0 s
Add elt (fun x1 : elt => M.In x1 s) x x0
 constructor 2; constructor.x:elt
s:t
x0:elt
H:x = x0 \/ M.In x0 s
H0:M.In x0 s
Add elt (fun x1 : elt => M.In x1 s) x x0
 constructor 1; auto.
 Qed.

 Lemma Add_Add : forall x s s', MP.Add x s s' -> !!s' === Add _ (!!s) x.forall (x : U.t) (s s' : t),
MP.Add x s s' -> !! s' === Add elt (!! s) x
 Proof.forall (x : U.t) (s s' : t),
MP.Add x s s' -> !! s' === Add elt (!! s) x
 unfold Same_set, Included, mkEns, In.forall (x : U.t) (s s' : t),
MP.Add x s s' ->
(forall x0 : elt,
 M.In x0 s' ->
 Add elt (fun x1 : elt => M.In x1 s) x x0) /\
(forall x0 : elt,
 Add elt (fun x1 : elt => M.In x1 s) x x0 ->
 M.In x0 s')
 split; intros.x:U.t
s, s':t
H:MP.Add x s s'
x0:elt
H0:M.In x0 s'
Add elt (fun x1 : elt => M.In x1 s) x x0
x:U.t
s, s':t
H:MP.Add x s s'
x0:elt
H0:Add elt (fun x1 : elt => M.In x1 s) x x0
M.In x0 s'
 red in H; rewrite H in H0.x:U.t
s, s':t
H:forall y : elt, M.In y s' <-> x = y \/ M.In y s
x0:elt
H0:x = x0 \/ M.In x0 s
Add elt (fun x1 : elt => M.In x1 s) x x0
x:U.t
s, s':t
H:MP.Add x s s'
x0:elt
H0:Add elt (fun x1 : elt => M.In x1 s) x x0
M.In x0 s'
 destruct H0.x:U.t
s, s':t
H:forall y : elt, M.In y s' <-> x = y \/ M.In y s
x0:elt
H0:x = x0
Add elt (fun x1 : elt => M.In x1 s) x x0
x:U.t
s, s':t
H:forall y : elt, M.In y s' <-> x = y \/ M.In y s
x0:elt
H0:M.In x0 s
Add elt (fun x1 : elt => M.In x1 s) x x0
x:U.t
s, s':t
H:MP.Add x s s'
x0:elt
H0:Add elt (fun x1 : elt => M.In x1 s) x x0
M.In x0 s'
 inversion H0.x:U.t
s, s':t
H:forall y : elt, M.In y s' <-> x = y \/ M.In y s
x0:elt
H0, H1:x = x0
Add elt (fun x1 : elt => M.In x1 s) x0 x0
x:U.t
s, s':t
H:forall y : elt, M.In y s' <-> x = y \/ M.In y s
x0:elt
H0:M.In x0 s
Add elt (fun x1 : elt => M.In x1 s) x x0
x:U.t
s, s':t
H:MP.Add x s s'
x0:elt
H0:Add elt (fun x1 : elt => M.In x1 s) x x0
M.In x0 s'
 constructor 2; constructor.x:U.t
s, s':t
H:forall y : elt, M.In y s' <-> x = y \/ M.In y s
x0:elt
H0:M.In x0 s
Add elt (fun x1 : elt => M.In x1 s) x x0
x:U.t
s, s':t
H:MP.Add x s s'
x0:elt
H0:Add elt (fun x1 : elt => M.In x1 s) x x0
M.In x0 s'
 constructor 1; auto.x:U.t
s, s':t
H:MP.Add x s s'
x0:elt
H0:Add elt (fun x1 : elt => M.In x1 s) x x0
M.In x0 s'
 red in H; rewrite H.x:U.t
s, s':t
H:forall y : elt, M.In y s' <-> x = y \/ M.In y s
x0:elt
H0:Add elt (fun x1 : elt => M.In x1 s) x x0
x = x0 \/ M.In x0 s
 inversion H0; auto.x:U.t
s, s':t
H:forall y : elt, M.In y s' <-> x = y \/ M.In y s
x0:elt
H0:Add elt (fun x2 : elt => M.In x2 s) x x0
x1:elt
H1:In elt (Singleton elt x) x0
H2:x1 = x0
x = x0 \/ M.In x0 s
 inversion H1; auto.
 Qed.

 Lemma remove_Subtract : forall x s, !!(remove x s) === Subtract _ (!!s) x.forall (x : elt) (s : t),
!! (remove x s) === Subtract elt (!! s) x
 Proof.forall (x : elt) (s : t),
!! (remove x s) === Subtract elt (!! s) x
 unfold Same_set, Included, mkEns, In.forall (x : elt) (s : t),
(forall x0 : elt,
 M.In x0 (remove x s) ->
 Subtract elt (fun x1 : elt => M.In x1 s) x x0) /\
(forall x0 : elt,
 Subtract elt (fun x1 : elt => M.In x1 s) x x0 ->
 M.In x0 (remove x s))
 split; intro; set_iff; inversion 1; auto with sets.x:elt
s:t
x0:elt
H:M.In x0 s /\ x <> x0
H0:M.In x0 s
H1:x <> x0
Subtract elt (fun x1 : elt => M.In x1 s) x x0
 split; auto.x:elt
s:t
x0:elt
H:M.In x0 s /\ x <> x0
H0:M.In x0 s
H1:x <> x0
~ In elt (Singleton elt x) x0
 contradict H1.x:elt
s:t
x0:elt
H:M.In x0 s /\ x <> x0
H0:M.In x0 s
H1:In elt (Singleton elt x) x0
x = x0
 inversion H1; auto.
 Qed.

 Lemma mkEns_Finite : forall s, Finite _ (!!s).forall s : t, Finite elt (!! s)
 Proof.forall s : t, Finite elt (!! s)
 intro s; pattern s; apply set_induction; clear s; intros.s:t
H:Empty s
Finite elt (!! s)
s, s':t
H:Finite elt (!! s)
x:elt
H0:~ M.In x s
H1:MP.Add x s s'
Finite elt (!! s')
 intros; replace (!!s) with (Empty_set elt); auto with sets.s:t
H:Empty s
Empty_set elt = !! s
s, s':t
H:Finite elt (!! s)
x:elt
H0:~ M.In x s
H1:MP.Add x s s'
Finite elt (!! s')
 symmetry; apply Extensionality_Ensembles.s:t
H:Empty s
!! s === Empty_set elt
s, s':t
H:Finite elt (!! s)
x:elt
H0:~ M.In x s
H1:MP.Add x s s'
Finite elt (!! s')
 apply Empty_Empty_set; auto.s, s':t
H:Finite elt (!! s)
x:elt
H0:~ M.In x s
H1:MP.Add x s s'
Finite elt (!! s')
 replace (!!s') with (Add _ (!!s) x).s, s':t
H:Finite elt (!! s)
x:elt
H0:~ M.In x s
H1:MP.Add x s s'
Finite elt (Add elt (!! s) x)
s, s':t
H:Finite elt (!! s)
x:elt
H0:~ M.In x s
H1:MP.Add x s s'
Add elt (!! s) x = !! s'
 constructor 2; auto.s, s':t
H:Finite elt (!! s)
x:elt
H0:~ M.In x s
H1:MP.Add x s s'
Add elt (!! s) x = !! s'
 symmetry; apply Extensionality_Ensembles.s, s':t
H:Finite elt (!! s)
x:elt
H0:~ M.In x s
H1:MP.Add x s s'
!! s' === Add elt (!! s) x
 apply Add_Add; auto.
 Qed.

 Lemma mkEns_cardinal : forall s, cardinal _ (!!s) (M.cardinal s).forall s : t, cardinal elt (!! s) (M.cardinal s)
 Proof.forall s : t, cardinal elt (!! s) (M.cardinal s)
 intro s; pattern s; apply set_induction; clear s; intros.s:t
H:Empty s
cardinal elt (!! s) (M.cardinal s)
s, s':t
H:cardinal elt (!! s) (M.cardinal s)
x:elt
H0:~ M.In x s
H1:MP.Add x s s'
cardinal elt (!! s') (M.cardinal s')
 intros; replace (!!s) with (Empty_set elt); auto with sets.s:t
H:Empty s
cardinal elt (Empty_set elt) (M.cardinal s)
s:t
H:Empty s
Empty_set elt = !! s
s, s':t
H:cardinal elt (!! s) (M.cardinal s)
x:elt
H0:~ M.In x s
H1:MP.Add x s s'
cardinal elt (!! s') (M.cardinal s')
 rewrite MP.cardinal_1; auto with sets.s:t
H:Empty s
Empty_set elt = !! s
s, s':t
H:cardinal elt (!! s) (M.cardinal s)
x:elt
H0:~ M.In x s
H1:MP.Add x s s'
cardinal elt (!! s') (M.cardinal s')
 symmetry; apply Extensionality_Ensembles.s:t
H:Empty s
!! s === Empty_set elt
s, s':t
H:cardinal elt (!! s) (M.cardinal s)
x:elt
H0:~ M.In x s
H1:MP.Add x s s'
cardinal elt (!! s') (M.cardinal s')
 apply Empty_Empty_set; auto.s, s':t
H:cardinal elt (!! s) (M.cardinal s)
x:elt
H0:~ M.In x s
H1:MP.Add x s s'
cardinal elt (!! s') (M.cardinal s')
 replace (!!s') with (Add _ (!!s) x).s, s':t
H:cardinal elt (!! s) (M.cardinal s)
x:elt
H0:~ M.In x s
H1:MP.Add x s s'
cardinal elt (Add elt (!! s) x) (M.cardinal s')
s, s':t
H:cardinal elt (!! s) (M.cardinal s)
x:elt
H0:~ M.In x s
H1:MP.Add x s s'
Add elt (!! s) x = !! s'
 rewrite (cardinal_2 H0 H1); auto with sets.s, s':t
H:cardinal elt (!! s) (M.cardinal s)
x:elt
H0:~ M.In x s
H1:MP.Add x s s'
Add elt (!! s) x = !! s'
 symmetry; apply Extensionality_Ensembles.s, s':t
H:cardinal elt (!! s) (M.cardinal s)
x:elt
H0:~ M.In x s
H1:MP.Add x s s'
!! s' === Add elt (!! s) x
 apply Add_Add; auto.
 Qed.

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.forall e : Ensemble elt,
Finite elt e -> exists s : t, !! s === e
 Proof.forall e : Ensemble elt,
Finite elt e -> exists s : t, !! s === e
 induction 1.exists s : t, !! s === Empty_set elt
A:Ensemble elt
H:Finite elt A
x:elt
H0:~ In elt A x
IHFinite:exists s : t, !! s === A
exists s : t, !! s === Add elt A x
 exists M.empty.!! empty === Empty_set elt
A:Ensemble elt
H:Finite elt A
x:elt
H0:~ In elt A x
IHFinite:exists s : t, !! s === A
exists s : t, !! s === Add elt A x
 apply empty_Empty_Set.A:Ensemble elt
H:Finite elt A
x:elt
H0:~ In elt A x
IHFinite:exists s : t, !! s === A
exists s : t, !! s === Add elt A x
 destruct IHFinite as (s,Hs).A:Ensemble elt
H:Finite elt A
x:elt
H0:~ In elt A x
s:t
Hs:!! s === A
exists s0 : t, !! s0 === Add elt A x
 exists (M.add x s).A:Ensemble elt
H:Finite elt A
x:elt
H0:~ In elt A x
s:t
Hs:!! s === A
!! (add x s) === Add elt A x
 apply Extensionality_Ensembles in Hs.A:Ensemble elt
H:Finite elt A
x:elt
H0:~ In elt A x
s:t
Hs:!! s = A
!! (add x s) === Add elt A x
 rewrite <- Hs.A:Ensemble elt
H:Finite elt A
x:elt
H0:~ In elt A x
s:t
Hs:!! s = A
!! (add x s) === Add elt (!! s) x
 apply add_Add.
 Qed.

End WS_to_Finite_set.


Module S_to_Finite_set (U:UsualOrderedType)(M: SetsOn U) :=
  WS_to_Finite_set U M.