diff options
Diffstat (limited to 'theories/FSets/FSetBridge.v')
| -rw-r--r-- | theories/FSets/FSetBridge.v | 150 |
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). |