aboutsummaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/FSets/FSetAVL.v46
-rw-r--r--theories/FSets/FSetBridge.v80
-rw-r--r--theories/FSets/FSetInterface.v17
-rw-r--r--theories/FSets/FSetList.v38
4 files changed, 174 insertions, 7 deletions
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index bbb29158df..8bd51abec3 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -2542,6 +2542,38 @@ Proof.
apply subset'_2; auto.
Qed.
+Lemma choose_equal: forall s s', bst s -> avl s -> bst s' -> avl s' ->
+ (equal' s s')=true ->
+ match choose s, choose s' with
+ | Some x, Some x' => X.eq x x'
+ | None, None => True
+ | _, _ => False
+ end.
+Proof.
+ unfold choose; intros s s' Hb Ha Hb' Ha' H.
+ generalize (equal'_2 s s' Hb Ha Hb' Ha' H); clear H; intros.
+ generalize (@min_elt_1 s) (@min_elt_2 s) (@min_elt_3 s).
+ generalize (@min_elt_1 s') (@min_elt_2 s') (@min_elt_3 s').
+ destruct (min_elt s) as [x|]; destruct (min_elt s') as [x'|]; auto.
+
+ intros H1 H2 _ H1' H2' _.
+ destruct (X.compare x x'); auto.
+ assert (In x s) by auto.
+ rewrite (H x) in H0.
+ destruct (H2 x' x); auto.
+ assert (In x' s') by auto.
+ rewrite <- (H x') in H0.
+ destruct (H2' x x'); auto.
+
+ intros _ _ H3 H1' _ _.
+ destruct (H3 (refl_equal _) x).
+ rewrite <- (H x); auto.
+
+ intros H1 _ _ _ _ H3'.
+ destruct (H3' (refl_equal _) x').
+ rewrite (H x'); auto.
+Qed.
+
End Raw.
(** * Encapsulation
@@ -2877,6 +2909,20 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
Lemma choose_2 : choose s = None -> Empty s.
Proof. exact (Raw.choose_2 s). Qed.
+ Lemma choose_equal: (equal s s')=true ->
+ match choose s, choose s' with
+ | Some x, Some x' => E.eq x x'
+ | None, None => True
+ | _, _ => False
+ end.
+ Proof.
+ intros.
+ unfold choose.
+ apply Raw.choose_equal; auto.
+ apply Raw.equal'_1; auto.
+ exact (equal_2 H).
+ Qed.
+
Lemma eq_refl : eq s s.
Proof. exact (Raw.eq_refl s). Qed.
Lemma eq_sym : eq s s' -> eq s' s.
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 9ac7b9c7cb..f517898e14 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -247,14 +247,71 @@ 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_equal (M.equal_1 H)); clear H; intros Heq.
+ generalize (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 H _ H' _; generalize (H x) (H' x'); clear H H'; intros H H'.
+ destruct H as (_,H); rewrite H in Heq; simpl in Heq; [|exists Hx]; auto.
+ destruct H' as (_,H'); rewrite H' in Heq; simpl in Heq; [|exists Hx']; auto.
+
+ intros H _ _ H'; generalize (H x); clear H; intros H.
+ destruct H as (_,H); rewrite H in Heq; simpl in Heq; [|exists Hx]; auto.
+ destruct H' as (_,H'); rewrite H' in Heq; simpl in Heq;[|exists Hx']; auto.
+
+ intros _ H H' _; generalize (H' x'); clear H'; intros H'.
+ destruct H as (_,H); rewrite H in Heq; simpl in Heq; [|exists Hx]; auto.
+ destruct H' as (_,H'); rewrite H' in Heq; simpl in Heq; [|exists Hx']; auto.
+ Qed.
+
Definition min_elt :
forall s : t,
{x : elt | In x s /\ For_all (fun y => ~ E.lt y x) s} + {Empty s}.
@@ -391,6 +448,19 @@ 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_equal: forall s s', (equal s s')=true ->
+ match choose s, choose s' with
+ | Some x, Some x' => E.eq x x'
+ | None, None => True
+ | _, _ => False
+ end.
+ Proof.
+ unfold choose; intros.
+ generalize (M.choose_equal (equal_2 H)); clear H.
+ destruct (M.choose s) as [(x,Hx)|Hx]; destruct (M.choose s') as [(x',Hx')|Hx'];
+ simpl; auto.
+ Qed.
Definition elements (s : t) : list elt := let (l, _) := elements s in l.
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index 9d5f2ad76f..50e6fb5395 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -274,8 +274,12 @@ Module Type S.
(** Specification of [choose] *)
Parameter choose_1 : choose s = Some x -> In x s.
Parameter choose_2 : choose s = None -> Empty s.
-(* Parameter choose_equal:
- (equal s s')=true -> E.eq (choose s) (choose s'). *)
+ Parameter choose_equal: (equal s s')=true ->
+ match choose s, choose s' with
+ | Some x, Some x' => E.eq x x'
+ | None, None => True
+ | _, _ => False
+ end.
End Spec.
@@ -418,4 +422,13 @@ Module Type Sdep.
Parameter choose : forall s : t, {x : elt | In x s} + {Empty s}.
+ (** The [choose_equal] specification of [S] cannot be packed
+ in the dependent version of [choose], so we leave it separate. *)
+ Parameter 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.
+
End Sdep.
diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
index 51771fc41c..a9f81008d2 100644
--- a/theories/FSets/FSetList.v
+++ b/theories/FSets/FSetList.v
@@ -718,6 +718,37 @@ Module Raw (X: OrderedType).
Definition choose_2 : forall s : t, choose s = None -> Empty s := min_elt_3.
+ Lemma choose_equal: forall s s', Sort s -> Sort s' -> (equal s s')=true ->
+ match choose s, choose s' with
+ | Some x, Some x' => X.eq x x'
+ | None, None => True
+ | _, _ => False
+ end.
+ Proof.
+ unfold choose; intros s s' Hs Hs' H.
+ generalize (equal_2 H); clear H; intros.
+ generalize (@min_elt_1 s) (@min_elt_2 _ Hs) (@min_elt_3 s).
+ generalize (@min_elt_1 s') (@min_elt_2 _ Hs') (@min_elt_3 s').
+ destruct (min_elt s) as [x|]; destruct (min_elt s') as [x'|]; auto.
+
+ intros H1 H2 _ H1' H2' _.
+ destruct (X.compare x x'); auto.
+ assert (In x s) by auto.
+ rewrite (H x) in H0.
+ destruct (H2 x' x); auto.
+ assert (In x' s') by auto.
+ rewrite <- (H x') in H0.
+ destruct (H2' x x'); auto.
+
+ intros _ _ H3 H1' _ _.
+ destruct (H3 (refl_equal _) x).
+ rewrite <- (H x); auto.
+
+ intros H1 _ _ _ _ H3'.
+ destruct (H3' (refl_equal _) x').
+ rewrite (H x'); auto.
+ Qed.
+
Lemma fold_1 :
forall (s : t) (Hs : Sort s) (A : Set) (i : A) (f : elt -> A -> A),
fold f s i = fold_left (fun a e => f e a) (elements s) i.
@@ -1221,6 +1252,13 @@ Module Make (X: OrderedType) <: S with Module E := X.
Proof. exact (fun H => Raw.choose_1 H). Qed.
Lemma choose_2 : choose s = None -> Empty s.
Proof. exact (fun H => Raw.choose_2 H). Qed.
+ Lemma choose_equal : (equal s s')=true ->
+ match choose s, choose s' with
+ | Some x, Some x' => E.eq x x'
+ | None, None => True
+ | _, _ => False
+ end.
+ Proof. exact (Raw.choose_equal s.(sorted) s'.(sorted)). Qed.
Lemma eq_refl : eq s s.
Proof. exact (Raw.eq_refl s). Qed.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 06:17:00 +0000