diff options
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 20 | ||||
| -rw-r--r-- | theories/FSets/FMapFullAVL.v | 4 | ||||
| -rw-r--r-- | theories/FSets/FMapPositive.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FSetBridge.v | 148 | ||||
| -rw-r--r-- | theories/FSets/FSetEqProperties.v | 8 | ||||
| -rw-r--r-- | theories/FSets/FSetFacts.v | 6 | ||||
| -rw-r--r-- | theories/FSets/FSetProperties.v | 2 |
7 files changed, 94 insertions, 96 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index c761e2a7..980cfeac 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -32,9 +32,9 @@ Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. preservation *) Module Raw (Import I:Int)(X: OrderedType). -Open Local Scope pair_scope. -Open Local Scope lazy_bool_scope. -Open Local Scope Int_scope. +Local Open Scope pair_scope. +Local Open Scope lazy_bool_scope. +Local Open Scope Int_scope. Definition key := X.t. Hint Transparent key. @@ -603,12 +603,12 @@ Qed. Lemma lt_leaf : forall x, lt_tree x (Leaf elt). Proof. - unfold lt_tree in |- *; intros; intuition_in. + unfold lt_tree; intros; intuition_in. Qed. Lemma gt_leaf : forall x, gt_tree x (Leaf elt). Proof. - unfold gt_tree in |- *; intros; intuition_in. + unfold gt_tree; intros; intuition_in. Qed. Lemma lt_tree_node : forall x y l r e h, @@ -1388,8 +1388,8 @@ Lemma fold_equiv_aux : L.fold f (elements_aux acc s) a = L.fold f acc (fold f s a). Proof. simple induction s. - simpl in |- *; intuition. - simpl in |- *; intros. + simpl; intuition. + simpl; intros. rewrite H. simpl. apply H0. @@ -1399,11 +1399,11 @@ Lemma fold_equiv : forall (A : Type) (s : t elt) (f : key -> elt -> A -> A) (a : A), fold f s a = fold' f s a. Proof. - unfold fold', elements in |- *. - simple induction s; simpl in |- *; auto; intros. + unfold fold', elements. + simple induction s; simpl; auto; intros. rewrite fold_equiv_aux. rewrite H0. - simpl in |- *; auto. + simpl; auto. Qed. Lemma fold_1 : diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index 774bcd9b..e1c60351 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -34,8 +34,8 @@ Module AvlProofs (Import I:Int)(X: OrderedType). Module Import Raw := Raw I X. Module Import II:=MoreInt(I). Import Raw.Proofs. -Open Local Scope pair_scope. -Open Local Scope Int_scope. +Local Open Scope pair_scope. +Local Open Scope Int_scope. Ltac omega_max := i2z_refl; romega with Z. diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 2e2eb166..c59f7c22 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -11,7 +11,7 @@ Require Import Bool ZArith OrderedType OrderedTypeEx FMapInterface. Set Implicit Arguments. -Open Local Scope positive_scope. +Local Open Scope positive_scope. Local Unset Elimination Schemes. Local Unset Case Analysis Schemes. diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 25ce5577..1ac544e1 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -44,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. @@ -131,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. @@ -147,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. @@ -162,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. @@ -183,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. @@ -212,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. @@ -308,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 : @@ -318,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. @@ -360,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 := @@ -368,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. @@ -382,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. @@ -398,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. @@ -412,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. @@ -429,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. @@ -453,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. @@ -478,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. @@ -486,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. @@ -506,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. @@ -514,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. @@ -530,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. @@ -551,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''. @@ -582,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. @@ -646,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. @@ -673,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. @@ -681,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. @@ -689,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. @@ -703,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. @@ -712,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. @@ -725,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. @@ -733,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. @@ -745,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). @@ -763,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). diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index 755bc7dd..ac495c04 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -206,7 +206,7 @@ intros. generalize (@choose_1 s) (@choose_2 s). destruct (choose s);intros. exists e;auto with set. -generalize (H1 (refl_equal None)); clear H1. +generalize (H1 Logic.eq_refl); clear H1. intros; rewrite (is_empty_1 H1) in H; discriminate. Qed. @@ -631,7 +631,7 @@ destruct (choose (filter f s)). intros H0 _; apply exists_1; auto. exists e; generalize (H0 e); rewrite filter_iff; auto. intros _ H0. -rewrite (is_empty_1 (H0 (refl_equal None))) in H; auto; discriminate. +rewrite (is_empty_1 (H0 Logic.eq_refl)) in H; auto; discriminate. Qed. Lemma partition_filter_1: @@ -881,8 +881,8 @@ generalize (@add_filter_1 f Hf s0 (add x s0) x) (@add_filter_2 f Hf s0 (add x s0 assert (~ In x (filter f s0)). intro H1; rewrite (mem_1 (filter_1 Hf H1)) in H; discriminate H. case (f x); simpl; intros. -rewrite (MP.cardinal_2 H1 (H2 (refl_equal true) (MP.Add_add s0 x))); auto. -rewrite <- (MP.Equal_cardinal (H3 (refl_equal false) (MP.Add_add s0 x))); auto. +rewrite (MP.cardinal_2 H1 (H2 Logic.eq_refl (MP.Add_add s0 x))); auto. +rewrite <- (MP.Equal_cardinal (H3 Logic.eq_refl (MP.Add_add s0 x))); auto. intros; rewrite fold_empty;auto. rewrite MP.cardinal_1; auto. unfold Empty; intros. diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index f473b334..b240ede4 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -315,11 +315,11 @@ symmetry. rewrite <- H1; intros a Ha. rewrite <- (H a) in Ha. destruct H0 as (_,H0). -exact (H0 (refl_equal true) _ Ha). +exact (H0 Logic.eq_refl _ Ha). rewrite <- H0; intros a Ha. rewrite (H a) in Ha. destruct H1 as (_,H1). -exact (H1 (refl_equal true) _ Ha). +exact (H1 Logic.eq_refl _ Ha). Qed. Instance Empty_m : Proper (Equal ==> iff) Empty. @@ -489,5 +489,3 @@ End WFacts_fun. Module WFacts (M:WS) := WFacts_fun M.E M. Module Facts := WFacts. - - diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index 1bad8061..d53ce0c8 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -823,7 +823,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). rewrite (inter_subset_equal H). generalize (@cardinal_inv_1 (diff s' s)). destruct (cardinal (diff s' s)). - intro H2; destruct (H2 (refl_equal _) x). + intro H2; destruct (H2 Logic.eq_refl x). set_iff; auto. intros _. change (0 + cardinal s < S n + cardinal s). |