diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /theories/FSets/FSetBridge.v | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'theories/FSets/FSetBridge.v')
-rw-r--r-- | theories/FSets/FSetBridge.v | 104 |
1 files changed, 84 insertions, 20 deletions
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 08985cfc..0622451f 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: FSetBridge.v 8834 2006-05-20 00:41:35Z letouzey $ *) +(* $Id: FSetBridge.v 10601 2008-02-28 00:20:33Z letouzey $ *) (** * Finite sets library *) @@ -27,7 +27,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E. Definition empty : {s : t | Empty s}. Proof. - exists empty; auto. + exists empty; auto with set. Qed. Definition is_empty : forall s : t, {Empty s} + {~ Empty s}. @@ -66,12 +66,12 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E. {s' : t | forall y : elt, In y s' <-> ~ E.eq x y /\ In y s}. Proof. intros; exists (remove x s); intuition. - absurd (In x (remove x s)); auto. + absurd (In x (remove x s)); auto with set. apply In_1 with y; auto. elim (ME.eq_dec x y); intros; auto. - absurd (In x (remove x s)); auto. + absurd (In x (remove x s)); auto with set. apply In_1 with y; auto. - eauto. + eauto with set. Qed. Definition union : @@ -83,14 +83,14 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E. Definition inter : forall s s' : t, {s'' : t | forall x : elt, In x s'' <-> In x s /\ In x s'}. Proof. - intros; exists (inter s s'); intuition; eauto. + intros; exists (inter s s'); intuition; eauto with set. Qed. Definition diff : forall s s' : t, {s'' : t | forall x : elt, In x s'' <-> In x s /\ ~ In x s'}. Proof. - intros; exists (diff s s'); intuition; eauto. - absurd (In x s'); eauto. + intros; exists (diff s s'); intuition; eauto with set. + absurd (In x s'); eauto with set. Qed. Definition equal : forall s s' : t, {Equal s s'} + {~ Equal s s'}. @@ -115,7 +115,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E. Defined. Definition fold : - forall (A : Set) (f : elt -> A -> A) (s : t) (i : A), + forall (A : Type) (f : elt -> A -> A) (s : t) (i : A), {r : A | let (l,_) := elements s in r = fold_left (fun a e => f e a) l i}. Proof. @@ -150,7 +150,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E. exists (filter (fdec Pdec) s). intro H; assert (compat_bool E.eq (fdec Pdec)); auto. intuition. - eauto. + eauto with set. generalize (filter_2 H0 H1). unfold fdec in |- *. case (Pdec x); intuition. @@ -226,7 +226,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E. generalize H4; unfold For_all, Equal in |- *; intuition. elim (H0 x); intros. assert (fdec Pdec x = true). - eauto. + eapply filter_2; eauto with set. generalize H8; unfold fdec in |- *; case (Pdec x); intuition. inversion H9. generalize H; unfold For_all, Equal in |- *; intuition. @@ -238,8 +238,8 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E. set (b := fdec Pdec x) in *; generalize (refl_equal b); pattern b at -1 in |- *; case b; unfold b in |- *; [ left | right ]. - elim (H4 x); intros _ B; apply B; auto. - elim (H x); intros _ B; apply B; auto. + elim (H4 x); intros _ B; apply B; auto with set. + elim (H x); intros _ B; apply B; auto with set. apply filter_3; auto. rewrite H5; auto. eapply (filter_1 (s:=s) (x:=x) H2); elim (H4 x); intros B _; apply B; @@ -247,12 +247,63 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E. eapply (filter_1 (s:=s) (x:=x) H3); elim (H x); intros B _; apply B; auto. Qed. + Definition choose_aux: forall s : t, + { x : elt | M.choose s = Some x } + { M.choose s = None }. + Proof. + intros. + destruct (M.choose s); [left | right]; auto. + exists e; auto. + Qed. + Definition choose : forall s : t, {x : elt | In x s} + {Empty s}. - Proof. - intros. - generalize (choose_1 (s:=s)) (choose_2 (s:=s)). - case (choose s); [ left | right ]; auto. - exists e; auto. + Proof. + intros; destruct (choose_aux s) as [(x,Hx)|H]. + left; exists x; apply choose_1; auto. + right; apply choose_2; auto. + Defined. + + Lemma choose_ok1 : + forall s x, M.choose s = Some x <-> exists H:In x s, + choose s = inleft _ (exist (fun x => In x s) x H). + Proof. + intros s x. + unfold choose; split; intros. + destruct (choose_aux s) as [(y,Hy)|H']; try congruence. + replace x with y in * by congruence. + exists (choose_1 Hy); auto. + destruct H. + destruct (choose_aux s) as [(y,Hy)|H']; congruence. + Qed. + + Lemma choose_ok2 : + forall s, M.choose s = None <-> exists H:Empty s, + choose s = inright _ H. + Proof. + intros s. + unfold choose; split; intros. + destruct (choose_aux s) as [(y,Hy)|H']; try congruence. + exists (choose_2 H'); auto. + destruct H. + destruct (choose_aux s) as [(y,Hy)|H']; congruence. + Qed. + + Lemma choose_equal : forall s s', Equal s s' -> + match choose s, choose s' with + | inleft (exist x _), inleft (exist x' _) => E.eq x x' + | inright _, inright _ => True + | _, _ => False + end. + Proof. + intros. + generalize (@M.choose_1 s)(@M.choose_2 s) + (@M.choose_1 s')(@M.choose_2 s')(@M.choose_3 s s') + (choose_ok1 s)(choose_ok2 s)(choose_ok1 s')(choose_ok2 s'). + destruct (choose s) as [(x,Hx)|Hx]; destruct (choose s') as [(x',Hx')|Hx']; auto; intros. + apply H4; auto. + rewrite H5; exists Hx; auto. + rewrite H7; exists Hx'; auto. + apply Hx' with x; unfold Equal in H; rewrite <-H; auto. + apply Hx with x'; unfold Equal in H; rewrite H; auto. Qed. Definition min_elt : @@ -391,6 +442,15 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. intro s; unfold choose in |- *; case (M.choose s); auto. simple destruct s0; intros; discriminate H. Qed. + + Lemma choose_3 : forall s s' x x', + choose s = Some x -> choose s' = Some x' -> Equal s s' -> E.eq x x'. + Proof. + unfold choose; intros. + generalize (M.choose_equal H1); clear H1. + destruct (M.choose s) as [(?,?)|?]; destruct (M.choose s') as [(?,?)|?]; + simpl; auto; congruence. + Qed. Definition elements (s : t) : list elt := let (l, _) := elements s in l. @@ -408,6 +468,10 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Proof. intros; unfold elements in |- *; case (M.elements s); firstorder. Qed. + Hint Resolve elements_3. + + Lemma elements_3w : forall s : t, NoDupA E.eq (elements s). + Proof. auto. Qed. Definition min_elt (s : t) : option elt := match min_elt s with @@ -578,11 +642,11 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. destruct (M.elements s); auto. Qed. - Definition fold (B : Set) (f : elt -> B -> B) (i : t) + Definition fold (B : Type) (f : elt -> B -> B) (i : t) (s : B) : B := let (fold, _) := fold f i s in fold. Lemma fold_1 : - forall (s : t) (A : Set) (i : A) (f : elt -> A -> A), + 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 *; |