summaryrefslogtreecommitdiff
path: root/theories/FSets/FSetBridge.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets/FSetBridge.v')
-rw-r--r--theories/FSets/FSetBridge.v150
1 files changed, 74 insertions, 76 deletions
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index c2d921be..1ac544e1 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetBridge.v 13253 2010-07-07 08:39:30Z letouzey $ *)
-
(** * Finite sets library *)
(** This module implements bridges (as functors) from dependent
@@ -46,7 +44,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
Definition add : forall (x : elt) (s : t), {s' : t | Add x s s'}.
Proof.
intros; exists (add x s); auto.
- unfold Add in |- *; intuition.
+ unfold Add; intuition.
elim (E.eq_dec x y); auto.
intros; right.
eapply add_3; eauto.
@@ -133,7 +131,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x}),
compat_P E.eq P -> compat_bool E.eq (fdec Pdec).
Proof.
- unfold compat_P, compat_bool, Proper, respectful, fdec in |- *; intros.
+ unfold compat_P, compat_bool, Proper, respectful, fdec; intros.
generalize (E.eq_sym H0); case (Pdec x); case (Pdec y); firstorder.
Qed.
@@ -149,11 +147,11 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
intuition.
eauto with set.
generalize (filter_2 H0 H1).
- unfold fdec in |- *.
+ unfold fdec.
case (Pdec x); intuition.
inversion H2.
apply filter_3; auto.
- unfold fdec in |- *; simpl in |- *.
+ unfold fdec; simpl.
case (Pdec x); intuition.
Qed.
@@ -164,17 +162,17 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
intros.
generalize (for_all_1 (s:=s) (f:=fdec Pdec))
(for_all_2 (s:=s) (f:=fdec Pdec)).
- case (for_all (fdec Pdec) s); unfold For_all in |- *; [ left | right ];
+ case (for_all (fdec Pdec) s); unfold For_all; [ left | right ];
intros.
assert (compat_bool E.eq (fdec Pdec)); auto.
- generalize (H0 H3 (refl_equal _) _ H2).
- unfold fdec in |- *.
+ generalize (H0 H3 Logic.eq_refl _ H2).
+ unfold fdec.
case (Pdec x); intuition.
inversion H4.
intuition.
absurd (false = true); [ auto with bool | apply H; auto ].
intro.
- unfold fdec in |- *.
+ unfold fdec.
case (Pdec x); intuition.
Qed.
@@ -185,19 +183,19 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
intros.
generalize (exists_1 (s:=s) (f:=fdec Pdec))
(exists_2 (s:=s) (f:=fdec Pdec)).
- case (exists_ (fdec Pdec) s); unfold Exists in |- *; [ left | right ];
+ case (exists_ (fdec Pdec) s); unfold Exists; [ left | right ];
intros.
elim H0; auto; intros.
exists x; intuition.
generalize H4.
- unfold fdec in |- *.
+ unfold fdec.
case (Pdec x); intuition.
inversion H2.
intuition.
elim H2; intros.
absurd (false = true); [ auto with bool | apply H; auto ].
exists x; intuition.
- unfold fdec in |- *.
+ unfold fdec.
case (Pdec x); intuition.
Qed.
@@ -214,26 +212,26 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
exists (partition (fdec Pdec) s).
generalize (partition_1 s (f:=fdec Pdec)) (partition_2 s (f:=fdec Pdec)).
case (partition (fdec Pdec) s).
- intros s1 s2; simpl in |- *.
+ intros s1 s2; simpl.
intros; assert (compat_bool E.eq (fdec Pdec)); auto.
intros; assert (compat_bool E.eq (fun x => negb (fdec Pdec x))).
- generalize H2; unfold compat_bool, Proper, respectful in |- *; intuition;
+ generalize H2; unfold compat_bool, Proper, respectful; intuition;
apply (f_equal negb); auto.
intuition.
- generalize H4; unfold For_all, Equal in |- *; intuition.
+ generalize H4; unfold For_all, Equal; intuition.
elim (H0 x); intros.
assert (fdec Pdec x = true).
eapply filter_2; eauto with set.
- generalize H8; unfold fdec in |- *; case (Pdec x); intuition.
+ generalize H8; unfold fdec; case (Pdec x); intuition.
inversion H9.
- generalize H; unfold For_all, Equal in |- *; intuition.
+ generalize H; unfold For_all, Equal; intuition.
elim (H0 x); intros.
cut ((fun x => negb (fdec Pdec x)) x = true).
- unfold fdec in |- *; case (Pdec x); intuition.
- change ((fun x => negb (fdec Pdec x)) x = true) in |- *.
+ unfold fdec; case (Pdec x); intuition.
+ change ((fun x => negb (fdec Pdec x)) x = true).
apply (filter_2 (s:=s) (x:=x)); auto.
- set (b := fdec Pdec x) in *; generalize (refl_equal b);
- pattern b at -1 in |- *; case b; unfold b in |- *;
+ set (b := fdec Pdec x) in *; generalize (Logic.eq_refl b);
+ pattern b at -1; case b; unfold b;
[ left | right ].
elim (H4 x); intros _ B; apply B; auto with set.
elim (H x); intros _ B; apply B; auto with set.
@@ -310,7 +308,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
intros;
generalize (min_elt_1 (s:=s)) (min_elt_2 (s:=s)) (min_elt_3 (s:=s)).
case (min_elt s); [ left | right ]; auto.
- exists e; unfold For_all in |- *; eauto.
+ exists e; unfold For_all; eauto.
Qed.
Definition max_elt :
@@ -320,7 +318,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
intros;
generalize (max_elt_1 (s:=s)) (max_elt_2 (s:=s)) (max_elt_3 (s:=s)).
case (max_elt s); [ left | right ]; auto.
- exists e; unfold For_all in |- *; eauto.
+ exists e; unfold For_all; eauto.
Qed.
Definition elt := elt.
@@ -362,7 +360,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
Lemma empty_1 : Empty empty.
Proof.
- unfold empty in |- *; case M.empty; auto.
+ unfold empty; case M.empty; auto.
Qed.
Definition is_empty (s : t) : bool :=
@@ -370,12 +368,12 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
Lemma is_empty_1 : forall s : t, Empty s -> is_empty s = true.
Proof.
- intros; unfold is_empty in |- *; case (M.is_empty s); auto.
+ intros; unfold is_empty; case (M.is_empty s); auto.
Qed.
Lemma is_empty_2 : forall s : t, is_empty s = true -> Empty s.
Proof.
- intro s; unfold is_empty in |- *; case (M.is_empty s); auto.
+ intro s; unfold is_empty; case (M.is_empty s); auto.
intros; discriminate H.
Qed.
@@ -384,12 +382,12 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
Lemma mem_1 : forall (s : t) (x : elt), In x s -> mem x s = true.
Proof.
- intros; unfold mem in |- *; case (M.mem x s); auto.
+ intros; unfold mem; case (M.mem x s); auto.
Qed.
Lemma mem_2 : forall (s : t) (x : elt), mem x s = true -> In x s.
Proof.
- intros s x; unfold mem in |- *; case (M.mem x s); auto.
+ intros s x; unfold mem; case (M.mem x s); auto.
intros; discriminate H.
Qed.
@@ -400,12 +398,12 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
Lemma equal_1 : forall s s' : t, Equal s s' -> equal s s' = true.
Proof.
- intros; unfold equal in |- *; case M.equal; intuition.
+ intros; unfold equal; case M.equal; intuition.
Qed.
Lemma equal_2 : forall s s' : t, equal s s' = true -> Equal s s'.
Proof.
- intros s s'; unfold equal in |- *; case (M.equal s s'); intuition;
+ intros s s'; unfold equal; case (M.equal s s'); intuition;
inversion H.
Qed.
@@ -414,12 +412,12 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
Lemma subset_1 : forall s s' : t, Subset s s' -> subset s s' = true.
Proof.
- intros; unfold subset in |- *; case M.subset; intuition.
+ intros; unfold subset; case M.subset; intuition.
Qed.
Lemma subset_2 : forall s s' : t, subset s s' = true -> Subset s s'.
Proof.
- intros s s'; unfold subset in |- *; case (M.subset s s'); intuition;
+ intros s s'; unfold subset; case (M.subset s s'); intuition;
inversion H.
Qed.
@@ -431,14 +429,14 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
Lemma choose_1 : forall (s : t) (x : elt), choose s = Some x -> In x s.
Proof.
- intros s x; unfold choose in |- *; case (M.choose s).
+ intros s x; unfold choose; case (M.choose s).
simple destruct s0; intros; injection H; intros; subst; auto.
intros; discriminate H.
Qed.
Lemma choose_2 : forall s : t, choose s = None -> Empty s.
Proof.
- intro s; unfold choose in |- *; case (M.choose s); auto.
+ intro s; unfold choose; case (M.choose s); auto.
simple destruct s0; intros; discriminate H.
Qed.
@@ -455,17 +453,17 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
Lemma elements_1 : forall (s : t) (x : elt), In x s -> InA E.eq x (elements s).
Proof.
- intros; unfold elements in |- *; case (M.elements s); firstorder.
+ intros; unfold elements; case (M.elements s); firstorder.
Qed.
Lemma elements_2 : forall (s : t) (x : elt), InA E.eq x (elements s) -> In x s.
Proof.
- intros s x; unfold elements in |- *; case (M.elements s); firstorder.
+ intros s x; unfold elements; case (M.elements s); firstorder.
Qed.
Lemma elements_3 : forall s : t, sort E.lt (elements s).
Proof.
- intros; unfold elements in |- *; case (M.elements s); firstorder.
+ intros; unfold elements; case (M.elements s); firstorder.
Qed.
Hint Resolve elements_3.
@@ -480,7 +478,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
Lemma min_elt_1 : forall (s : t) (x : elt), min_elt s = Some x -> In x s.
Proof.
- intros s x; unfold min_elt in |- *; case (M.min_elt s).
+ intros s x; unfold min_elt; case (M.min_elt s).
simple destruct s0; intros; injection H; intros; subst; intuition.
intros; discriminate H.
Qed.
@@ -488,15 +486,15 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
Lemma min_elt_2 :
forall (s : t) (x y : elt), min_elt s = Some x -> In y s -> ~ E.lt y x.
Proof.
- intros s x y; unfold min_elt in |- *; case (M.min_elt s).
- unfold For_all in |- *; simple destruct s0; intros; injection H; intros;
+ intros s x y; unfold min_elt; case (M.min_elt s).
+ unfold For_all; simple destruct s0; intros; injection H; intros;
subst; firstorder.
intros; discriminate H.
Qed.
Lemma min_elt_3 : forall s : t, min_elt s = None -> Empty s.
Proof.
- intros s; unfold min_elt in |- *; case (M.min_elt s); auto.
+ intros s; unfold min_elt; case (M.min_elt s); auto.
simple destruct s0; intros; discriminate H.
Qed.
@@ -508,7 +506,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
Lemma max_elt_1 : forall (s : t) (x : elt), max_elt s = Some x -> In x s.
Proof.
- intros s x; unfold max_elt in |- *; case (M.max_elt s).
+ intros s x; unfold max_elt; case (M.max_elt s).
simple destruct s0; intros; injection H; intros; subst; intuition.
intros; discriminate H.
Qed.
@@ -516,15 +514,15 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
Lemma max_elt_2 :
forall (s : t) (x y : elt), max_elt s = Some x -> In y s -> ~ E.lt x y.
Proof.
- intros s x y; unfold max_elt in |- *; case (M.max_elt s).
- unfold For_all in |- *; simple destruct s0; intros; injection H; intros;
+ intros s x y; unfold max_elt; case (M.max_elt s).
+ unfold For_all; simple destruct s0; intros; injection H; intros;
subst; firstorder.
intros; discriminate H.
Qed.
Lemma max_elt_3 : forall s : t, max_elt s = None -> Empty s.
Proof.
- intros s; unfold max_elt in |- *; case (M.max_elt s); auto.
+ intros s; unfold max_elt; case (M.max_elt s); auto.
simple destruct s0; intros; discriminate H.
Qed.
@@ -532,20 +530,20 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
Lemma add_1 : forall (s : t) (x y : elt), E.eq x y -> In y (add x s).
Proof.
- intros; unfold add in |- *; case (M.add x s); unfold Add in |- *;
+ intros; unfold add; case (M.add x s); unfold Add;
firstorder.
Qed.
Lemma add_2 : forall (s : t) (x y : elt), In y s -> In y (add x s).
Proof.
- intros; unfold add in |- *; case (M.add x s); unfold Add in |- *;
+ intros; unfold add; case (M.add x s); unfold Add;
firstorder.
Qed.
Lemma add_3 :
forall (s : t) (x y : elt), ~ E.eq x y -> In y (add x s) -> In y s.
Proof.
- intros s x y; unfold add in |- *; case (M.add x s); unfold Add in |- *;
+ intros s x y; unfold add; case (M.add x s); unfold Add;
firstorder.
Qed.
@@ -553,30 +551,30 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
Lemma remove_1 : forall (s : t) (x y : elt), E.eq x y -> ~ In y (remove x s).
Proof.
- intros; unfold remove in |- *; case (M.remove x s); firstorder.
+ intros; unfold remove; case (M.remove x s); firstorder.
Qed.
Lemma remove_2 :
forall (s : t) (x y : elt), ~ E.eq x y -> In y s -> In y (remove x s).
Proof.
- intros; unfold remove in |- *; case (M.remove x s); firstorder.
+ intros; unfold remove; case (M.remove x s); firstorder.
Qed.
Lemma remove_3 : forall (s : t) (x y : elt), In y (remove x s) -> In y s.
Proof.
- intros s x y; unfold remove in |- *; case (M.remove x s); firstorder.
+ intros s x y; unfold remove; case (M.remove x s); firstorder.
Qed.
Definition singleton (x : elt) : t := let (s, _) := singleton x in s.
Lemma singleton_1 : forall x y : elt, In y (singleton x) -> E.eq x y.
Proof.
- intros x y; unfold singleton in |- *; case (M.singleton x); firstorder.
+ intros x y; unfold singleton; case (M.singleton x); firstorder.
Qed.
Lemma singleton_2 : forall x y : elt, E.eq x y -> In y (singleton x).
Proof.
- intros x y; unfold singleton in |- *; case (M.singleton x); firstorder.
+ intros x y; unfold singleton; case (M.singleton x); firstorder.
Qed.
Definition union (s s' : t) : t := let (s'', _) := union s s' in s''.
@@ -584,60 +582,60 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
Lemma union_1 :
forall (s s' : t) (x : elt), In x (union s s') -> In x s \/ In x s'.
Proof.
- intros s s' x; unfold union in |- *; case (M.union s s'); firstorder.
+ intros s s' x; unfold union; case (M.union s s'); firstorder.
Qed.
Lemma union_2 : forall (s s' : t) (x : elt), In x s -> In x (union s s').
Proof.
- intros s s' x; unfold union in |- *; case (M.union s s'); firstorder.
+ intros s s' x; unfold union; case (M.union s s'); firstorder.
Qed.
Lemma union_3 : forall (s s' : t) (x : elt), In x s' -> In x (union s s').
Proof.
- intros s s' x; unfold union in |- *; case (M.union s s'); firstorder.
+ intros s s' x; unfold union; case (M.union s s'); firstorder.
Qed.
Definition inter (s s' : t) : t := let (s'', _) := inter s s' in s''.
Lemma inter_1 : forall (s s' : t) (x : elt), In x (inter s s') -> In x s.
Proof.
- intros s s' x; unfold inter in |- *; case (M.inter s s'); firstorder.
+ intros s s' x; unfold inter; case (M.inter s s'); firstorder.
Qed.
Lemma inter_2 : forall (s s' : t) (x : elt), In x (inter s s') -> In x s'.
Proof.
- intros s s' x; unfold inter in |- *; case (M.inter s s'); firstorder.
+ intros s s' x; unfold inter; case (M.inter s s'); firstorder.
Qed.
Lemma inter_3 :
forall (s s' : t) (x : elt), In x s -> In x s' -> In x (inter s s').
Proof.
- intros s s' x; unfold inter in |- *; case (M.inter s s'); firstorder.
+ intros s s' x; unfold inter; case (M.inter s s'); firstorder.
Qed.
Definition diff (s s' : t) : t := let (s'', _) := diff s s' in s''.
Lemma diff_1 : forall (s s' : t) (x : elt), In x (diff s s') -> In x s.
Proof.
- intros s s' x; unfold diff in |- *; case (M.diff s s'); firstorder.
+ intros s s' x; unfold diff; case (M.diff s s'); firstorder.
Qed.
Lemma diff_2 : forall (s s' : t) (x : elt), In x (diff s s') -> ~ In x s'.
Proof.
- intros s s' x; unfold diff in |- *; case (M.diff s s'); firstorder.
+ intros s s' x; unfold diff; case (M.diff s s'); firstorder.
Qed.
Lemma diff_3 :
forall (s s' : t) (x : elt), In x s -> ~ In x s' -> In x (diff s s').
Proof.
- intros s s' x; unfold diff in |- *; case (M.diff s s'); firstorder.
+ intros s s' x; unfold diff; case (M.diff s s'); firstorder.
Qed.
Definition cardinal (s : t) : nat := let (f, _) := cardinal s in f.
Lemma cardinal_1 : forall s, cardinal s = length (elements s).
Proof.
- intros; unfold cardinal in |- *; case (M.cardinal s); unfold elements in *;
+ intros; unfold cardinal; case (M.cardinal s); unfold elements in *;
destruct (M.elements s); auto.
Qed.
@@ -648,7 +646,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
forall (s : t) (A : Type) (i : A) (f : elt -> A -> A),
fold f s i = fold_left (fun a e => f e a) (elements s) i.
Proof.
- intros; unfold fold in |- *; case (M.fold f s i); unfold elements in *;
+ intros; unfold fold; case (M.fold f s i); unfold elements in *;
destruct (M.elements s); auto.
Qed.
@@ -675,7 +673,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
forall (s : t) (x : elt) (f : elt -> bool),
compat_bool E.eq f -> In x (filter f s) -> In x s.
Proof.
- intros s x f; unfold filter in |- *; case M.filter; intuition.
+ intros s x f; unfold filter; case M.filter; intuition.
generalize (i (compat_P_aux H)); firstorder.
Qed.
@@ -683,7 +681,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
forall (s : t) (x : elt) (f : elt -> bool),
compat_bool E.eq f -> In x (filter f s) -> f x = true.
Proof.
- intros s x f; unfold filter in |- *; case M.filter; intuition.
+ intros s x f; unfold filter; case M.filter; intuition.
generalize (i (compat_P_aux H)); firstorder.
Qed.
@@ -691,7 +689,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
forall (s : t) (x : elt) (f : elt -> bool),
compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s).
Proof.
- intros s x f; unfold filter in |- *; case M.filter; intuition.
+ intros s x f; unfold filter; case M.filter; intuition.
generalize (i (compat_P_aux H)); firstorder.
Qed.
@@ -705,7 +703,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
compat_bool E.eq f ->
For_all (fun x => f x = true) s -> for_all f s = true.
Proof.
- intros s f; unfold for_all in |- *; case M.for_all; intuition; elim n;
+ intros s f; unfold for_all; case M.for_all; intuition; elim n;
auto.
Qed.
@@ -714,7 +712,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
compat_bool E.eq f ->
for_all f s = true -> For_all (fun x => f x = true) s.
Proof.
- intros s f; unfold for_all in |- *; case M.for_all; intuition;
+ intros s f; unfold for_all; case M.for_all; intuition;
inversion H0.
Qed.
@@ -727,7 +725,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
forall (s : t) (f : elt -> bool),
compat_bool E.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true.
Proof.
- intros s f; unfold exists_ in |- *; case M.exists_; intuition; elim n;
+ intros s f; unfold exists_; case M.exists_; intuition; elim n;
auto.
Qed.
@@ -735,7 +733,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
forall (s : t) (f : elt -> bool),
compat_bool E.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s.
Proof.
- intros s f; unfold exists_ in |- *; case M.exists_; intuition;
+ intros s f; unfold exists_; case M.exists_; intuition;
inversion H0.
Qed.
@@ -747,10 +745,10 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
forall (s : t) (f : elt -> bool),
compat_bool E.eq f -> Equal (fst (partition f s)) (filter f s).
Proof.
- intros s f; unfold partition in |- *; case M.partition.
+ intros s f; unfold partition; case M.partition.
intro p; case p; clear p; intros s1 s2 H C.
generalize (H (compat_P_aux C)); clear H; intro H.
- simpl in |- *; unfold Equal in |- *; intuition.
+ simpl; unfold Equal; intuition.
apply filter_3; firstorder.
elim (H2 a); intros.
assert (In a s).
@@ -765,13 +763,13 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
forall (s : t) (f : elt -> bool),
compat_bool E.eq f -> Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
Proof.
- intros s f; unfold partition in |- *; case M.partition.
+ intros s f; unfold partition; case M.partition.
intro p; case p; clear p; intros s1 s2 H C.
generalize (H (compat_P_aux C)); clear H; intro H.
assert (D : compat_bool E.eq (fun x => negb (f x))).
generalize C; unfold compat_bool, Proper, respectful; intros; apply (f_equal negb);
auto.
- simpl in |- *; unfold Equal in |- *; intuition.
+ simpl; unfold Equal; intuition.
apply filter_3; firstorder.
elim (H2 a); intros.
assert (In a s).