diff options
Diffstat (limited to 'theories/FSets/FSetPositive.v')
| -rw-r--r-- | theories/FSets/FSetPositive.v | 1173 |
1 files changed, 1173 insertions, 0 deletions
diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v new file mode 100644 index 00000000..e5d55ac5 --- /dev/null +++ b/theories/FSets/FSetPositive.v @@ -0,0 +1,1173 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(** Efficient implementation of [FSetInterface.S] for positive keys, + inspired from the [FMapPositive] module. + + This module was adapted by Alexandre Ren, Damien Pous, and Thomas + Braibant (2010, LIG, CNRS, UMR 5217), from the [FMapPositive] + module of Pierre Letouzey and Jean-Christophe Filliâtre, which in + turn comes from the [FMap] framework of a work by Xavier Leroy and + Sandrine Blazy (used for building certified compilers). +*) + +Require Import Bool BinPos OrderedType OrderedTypeEx FSetInterface. + +Set Implicit Arguments. + +Local Open Scope lazy_bool_scope. +Local Open Scope positive_scope. + +Local Unset Elimination Schemes. +Local Unset Case Analysis Schemes. +Local Unset Boolean Equality Schemes. + + +Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. + + Module E:=PositiveOrderedTypeBits. + + Definition elt := positive. + + Inductive tree := + | Leaf : tree + | Node : tree -> bool -> tree -> tree. + + Scheme tree_ind := Induction for tree Sort Prop. + + Definition t := tree. + + Definition empty := Leaf. + + Fixpoint is_empty (m : t) : bool := + match m with + | Leaf => true + | Node l b r => negb b &&& is_empty l &&& is_empty r + end. + + Fixpoint mem (i : positive) (m : t) : bool := + match m with + | Leaf => false + | Node l o r => + match i with + | 1 => o + | i~0 => mem i l + | i~1 => mem i r + end + end. + + Fixpoint add (i : positive) (m : t) : t := + match m with + | Leaf => + match i with + | 1 => Node Leaf true Leaf + | i~0 => Node (add i Leaf) false Leaf + | i~1 => Node Leaf false (add i Leaf) + end + | Node l o r => + match i with + | 1 => Node l true r + | i~0 => Node (add i l) o r + | i~1 => Node l o (add i r) + end + end. + + Definition singleton i := add i empty. + + (** helper function to avoid creating empty trees that are not leaves *) + + Definition node l (b: bool) r := + if b then Node l b r else + match l,r with + | Leaf,Leaf => Leaf + | _,_ => Node l false r end. + + Fixpoint remove (i : positive) (m : t) : t := + match m with + | Leaf => Leaf + | Node l o r => + match i with + | 1 => node l false r + | i~0 => node (remove i l) o r + | i~1 => node l o (remove i r) + end + end. + + Fixpoint union (m m': t) := + match m with + | Leaf => m' + | Node l o r => + match m' with + | Leaf => m + | Node l' o' r' => Node (union l l') (o||o') (union r r') + end + end. + + Fixpoint inter (m m': t) := + match m with + | Leaf => Leaf + | Node l o r => + match m' with + | Leaf => Leaf + | Node l' o' r' => node (inter l l') (o&&o') (inter r r') + end + end. + + Fixpoint diff (m m': t) := + match m with + | Leaf => Leaf + | Node l o r => + match m' with + | Leaf => m + | Node l' o' r' => node (diff l l') (o&&negb o') (diff r r') + end + end. + + Fixpoint equal (m m': t): bool := + match m with + | Leaf => is_empty m' + | Node l o r => + match m' with + | Leaf => is_empty m + | Node l' o' r' => eqb o o' &&& equal l l' &&& equal r r' + end + end. + + Fixpoint subset (m m': t): bool := + match m with + | Leaf => true + | Node l o r => + match m' with + | Leaf => is_empty m + | Node l' o' r' => (negb o ||| o') &&& subset l l' &&& subset r r' + end + end. + + (** reverses [y] and concatenate it with [x] *) + + Fixpoint rev_append y x := + match y with + | 1 => x + | y~1 => rev_append y x~1 + | y~0 => rev_append y x~0 + end. + Infix "@" := rev_append (at level 60). + Definition rev x := x@1. + + Section Fold. + + Variables B : Type. + Variable f : positive -> B -> B. + + (** the additional argument, [i], records the current path, in + reverse order (this should be more efficient: we reverse this argument + only at present nodes only, rather than at each node of the tree). + we also use this convention in all functions below + *) + + Fixpoint xfold (m : t) (v : B) (i : positive) := + match m with + | Leaf => v + | Node l true r => + xfold r (f (rev i) (xfold l v i~0)) i~1 + | Node l false r => + xfold r (xfold l v i~0) i~1 + end. + Definition fold m i := xfold m i 1. + + End Fold. + + Section Quantifiers. + + Variable f : positive -> bool. + + Fixpoint xforall (m : t) (i : positive) := + match m with + | Leaf => true + | Node l o r => + (negb o ||| f (rev i)) &&& xforall r i~1 &&& xforall l i~0 + end. + Definition for_all m := xforall m 1. + + Fixpoint xexists (m : t) (i : positive) := + match m with + | Leaf => false + | Node l o r => (o &&& f (rev i)) ||| xexists r i~1 ||| xexists l i~0 + end. + Definition exists_ m := xexists m 1. + + Fixpoint xfilter (m : t) (i : positive) := + match m with + | Leaf => Leaf + | Node l o r => node (xfilter l i~0) (o &&& f (rev i)) (xfilter r i~1) + end. + Definition filter m := xfilter m 1. + + Fixpoint xpartition (m : t) (i : positive) := + match m with + | Leaf => (Leaf,Leaf) + | Node l o r => + let (lt,lf) := xpartition l i~0 in + let (rt,rf) := xpartition r i~1 in + if o then + let fi := f (rev i) in + (node lt fi rt, node lf (negb fi) rf) + else + (node lt false rt, node lf false rf) + end. + Definition partition m := xpartition m 1. + + End Quantifiers. + + (** uses [a] to accumulate values rather than doing a lot of concatenations *) + + Fixpoint xelements (m : t) (i : positive) (a: list positive) := + match m with + | Leaf => a + | Node l false r => xelements l i~0 (xelements r i~1 a) + | Node l true r => xelements l i~0 (rev i :: xelements r i~1 a) + end. + + Definition elements (m : t) := xelements m 1 nil. + + Fixpoint cardinal (m : t) : nat := + match m with + | Leaf => O + | Node l false r => (cardinal l + cardinal r)%nat + | Node l true r => S (cardinal l + cardinal r) + end. + + Definition omap (f: elt -> elt) x := + match x with + | None => None + | Some i => Some (f i) + end. + + (** would it be more efficient to use a path like in the above functions ? *) + + Fixpoint choose (m: t) := + match m with + | Leaf => None + | Node l o r => if o then Some 1 else + match choose l with + | None => omap xI (choose r) + | Some i => Some i~0 + end + end. + + Fixpoint min_elt (m: t) := + match m with + | Leaf => None + | Node l o r => + match min_elt l with + | None => if o then Some 1 else omap xI (min_elt r) + | Some i => Some i~0 + end + end. + + Fixpoint max_elt (m: t) := + match m with + | Leaf => None + | Node l o r => + match max_elt r with + | None => if o then Some 1 else omap xO (max_elt l) + | Some i => Some i~1 + end + end. + + (** lexicographic product, defined using a notation to keep things lazy *) + + Notation lex u v := match u with Eq => v | Lt => Lt | Gt => Gt end. + + Definition compare_bool a b := + match a,b with + | false, true => Lt + | true, false => Gt + | _,_ => Eq + end. + + Fixpoint compare_fun (m m': t): comparison := + match m,m' with + | Leaf,_ => if is_empty m' then Eq else Lt + | _,Leaf => if is_empty m then Eq else Gt + | Node l o r,Node l' o' r' => + lex (compare_bool o o') (lex (compare_fun l l') (compare_fun r r')) + end. + + + Definition In i t := mem i t = true. + Definition Equal s s' := forall a : elt, In a s <-> In a s'. + Definition Subset s s' := forall a : elt, In a s -> In a s'. + Definition Empty s := forall a : elt, ~ In a s. + Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x. + Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x. + + Notation "s [=] t" := (Equal s t) (at level 70, no associativity). + Notation "s [<=] t" := (Subset s t) (at level 70, no associativity). + + Definition eq := Equal. + Definition lt m m' := compare_fun m m' = Lt. + + (** Specification of [In] *) + + Lemma In_1: forall s x y, E.eq x y -> In x s -> In y s. + Proof. intros s x y ->. trivial. Qed. + + (** Specification of [eq] *) + + Lemma eq_refl: forall s, eq s s. + Proof. unfold eq, Equal. reflexivity. Qed. + + Lemma eq_sym: forall s s', eq s s' -> eq s' s. + Proof. unfold eq, Equal. intros. symmetry. trivial. Qed. + + Lemma eq_trans: forall s s' s'', eq s s' -> eq s' s'' -> eq s s''. + Proof. unfold eq, Equal. intros ? ? ? H ? ?. rewrite H. trivial. Qed. + + (** Specification of [mem] *) + + Lemma mem_1: forall s x, In x s -> mem x s = true. + Proof. unfold In. trivial. Qed. + + Lemma mem_2: forall s x, mem x s = true -> In x s. + Proof. unfold In. trivial. Qed. + + (** Additional lemmas for mem *) + + Lemma mem_Leaf: forall x, mem x Leaf = false. + Proof. destruct x; trivial. Qed. + + (** Specification of [empty] *) + + Lemma empty_1 : Empty empty. + Proof. unfold Empty, In. intro. rewrite mem_Leaf. discriminate. Qed. + + (** Specification of node *) + + Lemma mem_node: forall x l o r, mem x (node l o r) = mem x (Node l o r). + Proof. + intros x l o r. + case o; trivial. + destruct l; trivial. + destruct r; trivial. + symmetry. destruct x. + apply mem_Leaf. + apply mem_Leaf. + reflexivity. + Qed. + Local Opaque node. + + (** Specification of [is_empty] *) + + Lemma is_empty_spec: forall s, Empty s <-> is_empty s = true. + Proof. + unfold Empty, In. + induction s as [|l IHl o r IHr]; simpl. + setoid_rewrite mem_Leaf. firstorder. + rewrite <- 2andb_lazy_alt, 2andb_true_iff, <- IHl, <- IHr. clear IHl IHr. + destruct o; simpl; split. + intro H. elim (H 1). reflexivity. + intuition discriminate. + intro H. split. split. reflexivity. + intro a. apply (H a~0). + intro a. apply (H a~1). + intros H [a|a|]; apply H || intro; discriminate. + Qed. + + Lemma is_empty_1: forall s, Empty s -> is_empty s = true. + Proof. intro. rewrite is_empty_spec. trivial. Qed. + + Lemma is_empty_2: forall s, is_empty s = true -> Empty s. + Proof. intro. rewrite is_empty_spec. trivial. Qed. + + (** Specification of [subset] *) + + Lemma subset_Leaf_s: forall s, Leaf [<=] s. + Proof. intros s i Hi. elim (empty_1 Hi). Qed. + + Lemma subset_spec: forall s s', s [<=] s' <-> subset s s' = true. + Proof. + induction s as [|l IHl o r IHr]; intros [|l' o' r']; simpl. + split; intros. reflexivity. apply subset_Leaf_s. + + split; intros. reflexivity. apply subset_Leaf_s. + + rewrite <- 2andb_lazy_alt, 2andb_true_iff, <- 2is_empty_spec. + destruct o; simpl. + split. + intro H. elim (@empty_1 1). apply H. reflexivity. + intuition discriminate. + split; intro H. + split. split. reflexivity. + unfold Empty. intros a H1. apply (@empty_1 (a~0)). apply H. assumption. + unfold Empty. intros a H1. apply (@empty_1 (a~1)). apply H. assumption. + destruct H as [[_ Hl] Hr]. + intros [i|i|] Hi. + elim (Hr i Hi). + elim (Hl i Hi). + discriminate. + + rewrite <- 2andb_lazy_alt, 2andb_true_iff, <- IHl, <- IHr. clear. + destruct o; simpl. + split; intro H. + split. split. + destruct o'; trivial. + specialize (H 1). unfold In in H. simpl in H. apply H. reflexivity. + intros i Hi. apply (H i~0). apply Hi. + intros i Hi. apply (H i~1). apply Hi. + destruct H as [[Ho' Hl] Hr]. rewrite Ho'. + intros i Hi. destruct i. + apply (Hr i). assumption. + apply (Hl i). assumption. + assumption. + split; intros. + split. split. reflexivity. + intros i Hi. apply (H i~0). apply Hi. + intros i Hi. apply (H i~1). apply Hi. + intros i Hi. destruct i; destruct H as [[H Hl] Hr]. + apply (Hr i). assumption. + apply (Hl i). assumption. + discriminate Hi. + Qed. + + + Lemma subset_1: forall s s', Subset s s' -> subset s s' = true. + Proof. intros s s'. apply -> subset_spec; trivial. Qed. + + Lemma subset_2: forall s s', subset s s' = true -> Subset s s'. + Proof. intros s s'. apply <- subset_spec; trivial. Qed. + + (** Specification of [equal] (via subset) *) + + Lemma equal_subset: forall s s', equal s s' = subset s s' && subset s' s. + Proof. + induction s as [|l IHl o r IHr]; intros [|l' o' r']; simpl; trivial. + destruct o. reflexivity. rewrite andb_comm. reflexivity. + rewrite <- 6andb_lazy_alt. rewrite eq_iff_eq_true. + rewrite 7andb_true_iff, eqb_true_iff. + rewrite IHl, IHr, 2andb_true_iff. clear IHl IHr. intuition subst. + destruct o'; reflexivity. + destruct o'; reflexivity. + destruct o; auto. destruct o'; trivial. + Qed. + + Lemma equal_spec: forall s s', Equal s s' <-> equal s s' = true. + Proof. + intros. rewrite equal_subset. rewrite andb_true_iff. + rewrite <- 2subset_spec. unfold Equal, Subset. firstorder. + Qed. + + Lemma equal_1: forall s s', Equal s s' -> equal s s' = true. + Proof. intros s s'. apply -> equal_spec; trivial. Qed. + + Lemma equal_2: forall s s', equal s s' = true -> Equal s s'. + Proof. intros s s'. apply <- equal_spec; trivial. Qed. + + Lemma eq_dec : forall s s', { eq s s' } + { ~ eq s s' }. + Proof. + unfold eq. + intros. case_eq (equal s s'); intro H. + left. apply equal_2, H. + right. abstract (intro H'; rewrite (equal_1 H') in H; discriminate). + Defined. + + (** (Specified) definition of [compare] *) + + Lemma lex_Opp: forall u v u' v', u = CompOpp u' -> v = CompOpp v' -> + lex u v = CompOpp (lex u' v'). + Proof. intros ? ? u' ? -> ->. case u'; reflexivity. Qed. + + Lemma compare_bool_inv: forall b b', + compare_bool b b' = CompOpp (compare_bool b' b). + Proof. intros [|] [|]; reflexivity. Qed. + + Lemma compare_inv: forall s s', compare_fun s s' = CompOpp (compare_fun s' s). + Proof. + induction s as [|l IHl o r IHr]; destruct s' as [|l' o' r']; trivial. + unfold compare_fun. case is_empty; reflexivity. + unfold compare_fun. case is_empty; reflexivity. + simpl. rewrite compare_bool_inv. + case compare_bool; simpl; trivial; apply lex_Opp; auto. + Qed. + + Lemma lex_Eq: forall u v, lex u v = Eq <-> u=Eq /\ v=Eq. + Proof. intros u v; destruct u; intuition discriminate. Qed. + + Lemma compare_bool_Eq: forall b1 b2, + compare_bool b1 b2 = Eq <-> eqb b1 b2 = true. + Proof. intros [|] [|]; intuition discriminate. Qed. + + Lemma compare_equal: forall s s', compare_fun s s' = Eq <-> equal s s' = true. + Proof. + induction s as [|l IHl o r IHr]; destruct s' as [|l' o' r']. + simpl. tauto. + unfold compare_fun, equal. case is_empty; intuition discriminate. + unfold compare_fun, equal. case is_empty; intuition discriminate. + simpl. rewrite <- 2andb_lazy_alt, 2andb_true_iff. + rewrite <- IHl, <- IHr, <- compare_bool_Eq. clear IHl IHr. + rewrite and_assoc. rewrite <- 2lex_Eq. reflexivity. + Qed. + + + Lemma compare_gt: forall s s', compare_fun s s' = Gt -> lt s' s. + Proof. + unfold lt. intros s s'. rewrite compare_inv. + case compare_fun; trivial; intros; discriminate. + Qed. + + Lemma compare_eq: forall s s', compare_fun s s' = Eq -> eq s s'. + Proof. + unfold eq. intros s s'. rewrite compare_equal, equal_spec. trivial. + Qed. + + Lemma compare : forall s s' : t, Compare lt eq s s'. + Proof. + intros. case_eq (compare_fun s s'); intro H. + apply EQ. apply compare_eq, H. + apply LT. assumption. + apply GT. apply compare_gt, H. + Defined. + + Section lt_spec. + + Inductive ct: comparison -> comparison -> comparison -> Prop := + | ct_xxx: forall x, ct x x x + | ct_xex: forall x, ct x Eq x + | ct_exx: forall x, ct Eq x x + | ct_glx: forall x, ct Gt Lt x + | ct_lgx: forall x, ct Lt Gt x. + + Lemma ct_cxe: forall x, ct (CompOpp x) x Eq. + Proof. destruct x; constructor. Qed. + + Lemma ct_xce: forall x, ct x (CompOpp x) Eq. + Proof. destruct x; constructor. Qed. + + Lemma ct_lxl: forall x, ct Lt x Lt. + Proof. destruct x; constructor. Qed. + + Lemma ct_gxg: forall x, ct Gt x Gt. + Proof. destruct x; constructor. Qed. + + Lemma ct_xll: forall x, ct x Lt Lt. + Proof. destruct x; constructor. Qed. + + Lemma ct_xgg: forall x, ct x Gt Gt. + Proof. destruct x; constructor. Qed. + + Local Hint Constructors ct: ct. + Local Hint Resolve ct_cxe ct_xce ct_lxl ct_xll ct_gxg ct_xgg: ct. + Ltac ct := trivial with ct. + + Lemma ct_lex: forall u v w u' v' w', + ct u v w -> ct u' v' w' -> ct (lex u u') (lex v v') (lex w w'). + Proof. + intros u v w u' v' w' H H'. + inversion_clear H; inversion_clear H'; ct; destruct w; ct; destruct w'; ct. + Qed. + + Lemma ct_compare_bool: + forall a b c, ct (compare_bool a b) (compare_bool b c) (compare_bool a c). + Proof. + intros [|] [|] [|]; constructor. + Qed. + + Lemma compare_x_Leaf: forall s, + compare_fun s Leaf = if is_empty s then Eq else Gt. + Proof. + intros. rewrite compare_inv. simpl. case (is_empty s); reflexivity. + Qed. + + Lemma compare_empty_x: forall a, is_empty a = true -> + forall b, compare_fun a b = if is_empty b then Eq else Lt. + Proof. + induction a as [|l IHl o r IHr]; trivial. + destruct o. intro; discriminate. + simpl is_empty. rewrite <- andb_lazy_alt, andb_true_iff. + intros [Hl Hr]. + destruct b as [|l' [|] r']; simpl compare_fun; trivial. + rewrite Hl, Hr. trivial. + rewrite (IHl Hl), (IHr Hr). simpl. + case (is_empty l'); case (is_empty r'); trivial. + Qed. + + Lemma compare_x_empty: forall a, is_empty a = true -> + forall b, compare_fun b a = if is_empty b then Eq else Gt. + Proof. + setoid_rewrite <- compare_x_Leaf. + intros. rewrite 2(compare_inv b), (compare_empty_x _ H). reflexivity. + Qed. + + Lemma ct_compare_fun: + forall a b c, ct (compare_fun a b) (compare_fun b c) (compare_fun a c). + Proof. + induction a as [|l IHl o r IHr]; intros s' s''. + destruct s' as [|l' o' r']; destruct s'' as [|l'' o'' r'']; ct. + rewrite compare_inv. ct. + unfold compare_fun at 1. case_eq (is_empty (Node l' o' r')); intro H'. + rewrite (compare_empty_x _ H'). ct. + unfold compare_fun at 2. case_eq (is_empty (Node l'' o'' r'')); intro H''. + rewrite (compare_x_empty _ H''), H'. ct. + ct. + + destruct s' as [|l' o' r']; destruct s'' as [|l'' o'' r'']. + ct. + unfold compare_fun at 2. rewrite compare_x_Leaf. + case_eq (is_empty (Node l o r)); intro H. + rewrite (compare_empty_x _ H). ct. + case_eq (is_empty (Node l'' o'' r'')); intro H''. + rewrite (compare_x_empty _ H''), H. ct. + ct. + + rewrite 2 compare_x_Leaf. + case_eq (is_empty (Node l o r)); intro H. + rewrite compare_inv, (compare_x_empty _ H). ct. + case_eq (is_empty (Node l' o' r')); intro H'. + rewrite (compare_x_empty _ H'), H. ct. + ct. + + simpl compare_fun. apply ct_lex. apply ct_compare_bool. + apply ct_lex; trivial. + Qed. + + End lt_spec. + + Lemma lt_trans: forall s s' s'', lt s s' -> lt s' s'' -> lt s s''. + Proof. + unfold lt. intros a b c. assert (H := ct_compare_fun a b c). + inversion_clear H; trivial; intros; discriminate. + Qed. + + Lemma lt_not_eq: forall s s', lt s s' -> ~ eq s s'. + Proof. + unfold lt, eq. intros s s' H H'. + rewrite equal_spec, <- compare_equal in H'. congruence. + Qed. + + (** Specification of [add] *) + + Lemma add_spec: forall x y s, In y (add x s) <-> x=y \/ In y s. + Proof. + unfold In. induction x; intros [y|y|] [|l o r]; simpl mem; + try (rewrite IHx; clear IHx); rewrite ?mem_Leaf; intuition congruence. + Qed. + + Lemma add_1: forall s x y, x = y -> In y (add x s). + Proof. intros. apply <- add_spec. left. assumption. Qed. + + Lemma add_2: forall s x y, In y s -> In y (add x s). + Proof. intros. apply <- add_spec. right. assumption. Qed. + + Lemma add_3: forall s x y, x<>y -> In y (add x s) -> In y s. + Proof. + intros s x y H. rewrite add_spec. intros [->|?]; trivial. elim H; trivial. + Qed. + + (** Specification of [remove] *) + + Lemma remove_spec: forall x y s, In y (remove x s) <-> x<>y /\ In y s. + Proof. + unfold In. + induction x; intros [y|y|] [|l o r]; simpl remove; rewrite ?mem_node; + simpl mem; try (rewrite IHx; clear IHx); rewrite ?mem_Leaf; + intuition congruence. + Qed. + + Lemma remove_1: forall s x y, x=y -> ~ In y (remove x s). + Proof. intros. rewrite remove_spec. tauto. Qed. + + Lemma remove_2: forall s x y, x<>y -> In y s -> In y (remove x s). + Proof. intros. rewrite remove_spec. split; assumption. Qed. + + Lemma remove_3: forall s x y, In y (remove x s) -> In y s. + Proof. intros s x y. rewrite remove_spec. tauto. Qed. + + (** Specification of [singleton] *) + + Lemma singleton_1: forall x y, In y (singleton x) -> x=y. + Proof. + unfold singleton. intros x y. rewrite add_spec. + unfold In. rewrite mem_Leaf. intuition discriminate. + Qed. + + Lemma singleton_2: forall x y, x = y -> In y (singleton x). + Proof. + unfold singleton. intros. apply add_1. assumption. + Qed. + + (** Specification of [union] *) + + Lemma union_spec: forall x s s', In x (union s s') <-> In x s \/ In x s'. + Proof. + unfold In. + induction x; destruct s; destruct s'; simpl union; simpl mem; + try (rewrite IHx; clear IHx); try intuition congruence. + apply orb_true_iff. + Qed. + + Lemma union_1: forall s s' x, In x (union s s') -> In x s \/ In x s'. + Proof. intros. apply -> union_spec. assumption. Qed. + + Lemma union_2: forall s s' x, In x s -> In x (union s s'). + Proof. intros. apply <- union_spec. left. assumption. Qed. + + Lemma union_3: forall s s' x, In x s' -> In x (union s s'). + Proof. intros. apply <- union_spec. right. assumption. Qed. + + (** Specification of [inter] *) + + Lemma inter_spec: forall x s s', In x (inter s s') <-> In x s /\ In x s'. + Proof. + unfold In. + induction x; destruct s; destruct s'; simpl inter; rewrite ?mem_node; + simpl mem; try (rewrite IHx; clear IHx); try intuition congruence. + apply andb_true_iff. + Qed. + + Lemma inter_1: forall s s' x, In x (inter s s') -> In x s. + Proof. intros s s' x. rewrite inter_spec. tauto. Qed. + + Lemma inter_2: forall s s' x, In x (inter s s') -> In x s'. + Proof. intros s s' x. rewrite inter_spec. tauto. Qed. + + Lemma inter_3: forall s s' x, In x s -> In x s' -> In x (inter s s'). + Proof. intros. rewrite inter_spec. split; assumption. Qed. + + (** Specification of [diff] *) + + Lemma diff_spec: forall x s s', In x (diff s s') <-> In x s /\ ~ In x s'. + Proof. + unfold In. + induction x; destruct s; destruct s' as [|l' o' r']; simpl diff; + rewrite ?mem_node; simpl mem; + try (rewrite IHx; clear IHx); try intuition congruence. + rewrite andb_true_iff. destruct o'; intuition discriminate. + Qed. + + Lemma diff_1: forall s s' x, In x (diff s s') -> In x s. + Proof. intros s s' x. rewrite diff_spec. tauto. Qed. + + Lemma diff_2: forall s s' x, In x (diff s s') -> ~ In x s'. + Proof. intros s s' x. rewrite diff_spec. tauto. Qed. + + Lemma diff_3: forall s s' x, In x s -> ~ In x s' -> In x (diff s s'). + Proof. intros. rewrite diff_spec. split; assumption. Qed. + + (** Specification of [fold] *) + + Lemma fold_1: forall s (A : Type) (i : A) (f : elt -> A -> A), + fold f s i = fold_left (fun a e => f e a) (elements s) i. + Proof. + unfold fold, elements. intros s A i f. revert s i. + set (f' := fun a e => f e a). + assert (H: forall s i j acc, + fold_left f' acc (xfold f s i j) = + fold_left f' (xelements s j acc) i). + + induction s as [|l IHl o r IHr]; intros; trivial. + destruct o; simpl xelements; simpl xfold. + rewrite IHr, <- IHl. reflexivity. + rewrite IHr. apply IHl. + + intros. exact (H s i 1 nil). + Qed. + + (** Specification of [cardinal] *) + + Lemma cardinal_1: forall s, cardinal s = length (elements s). + Proof. + unfold elements. + assert (H: forall s j acc, + (cardinal s + length acc)%nat = length (xelements s j acc)). + + induction s as [|l IHl b r IHr]; intros j acc; simpl; trivial. destruct b. + rewrite <- IHl. simpl. rewrite <- IHr. + rewrite <- plus_n_Sm, Plus.plus_assoc. reflexivity. + rewrite <- IHl, <- IHr. rewrite Plus.plus_assoc. reflexivity. + + intros. rewrite <- H. simpl. rewrite Plus.plus_comm. reflexivity. + Qed. + + (** Specification of [filter] *) + + Lemma xfilter_spec: forall f s x i, + In x (xfilter f s i) <-> In x s /\ f (i@x) = true. + Proof. + intro f. unfold In. + induction s as [|l IHl o r IHr]; intros x i; simpl xfilter. + rewrite mem_Leaf. intuition discriminate. + rewrite mem_node. destruct x; simpl. + rewrite IHr. reflexivity. + rewrite IHl. reflexivity. + rewrite <- andb_lazy_alt. apply andb_true_iff. + Qed. + + Lemma filter_1 : forall s x f, compat_bool E.eq f -> + In x (filter f s) -> In x s. + Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed. + + Lemma filter_2 : forall s x f, compat_bool E.eq f -> + In x (filter f s) -> f x = true. + Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed. + + Lemma filter_3 : forall s x f, compat_bool E.eq f -> In x s -> + f x = true -> In x (filter f s). + Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed. + + + (** Specification of [for_all] *) + + Lemma xforall_spec: forall f s i, + xforall f s i = true <-> For_all (fun x => f (i@x) = true) s. + Proof. + unfold For_all, In. intro f. + induction s as [|l IHl o r IHr]; intros i; simpl. + setoid_rewrite mem_Leaf. intuition discriminate. + rewrite <- 2andb_lazy_alt, <- orb_lazy_alt, 2 andb_true_iff. + rewrite IHl, IHr. clear IHl IHr. + split. + intros [[Hi Hr] Hl] x. destruct x; simpl; intro H. + apply Hr, H. + apply Hl, H. + rewrite H in Hi. assumption. + intro H; intuition. + specialize (H 1). destruct o. apply H. reflexivity. reflexivity. + apply H. assumption. + apply H. assumption. + Qed. + + Lemma for_all_1 : forall s f, 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. rewrite xforall_spec. trivial. Qed. + + Lemma for_all_2 : forall s f, 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. rewrite xforall_spec. trivial. Qed. + + + (** Specification of [exists] *) + + Lemma xexists_spec: forall f s i, + xexists f s i = true <-> Exists (fun x => f (i@x) = true) s. + Proof. + unfold Exists, In. intro f. + induction s as [|l IHl o r IHr]; intros i; simpl. + setoid_rewrite mem_Leaf. firstorder. + rewrite <- 2orb_lazy_alt, 2orb_true_iff, <- andb_lazy_alt, andb_true_iff. + rewrite IHl, IHr. clear IHl IHr. + split. + intros [[Hi|[x Hr]]|[x Hl]]. + exists 1. exact Hi. + exists x~1. exact Hr. + exists x~0. exact Hl. + intros [[x|x|] H]; eauto. + Qed. + + Lemma exists_1 : forall s f, compat_bool E.eq f -> + Exists (fun x => f x = true) s -> exists_ f s = true. + Proof. intros s f _. unfold exists_. rewrite xexists_spec. trivial. Qed. + + Lemma exists_2 : forall s f, compat_bool E.eq f -> + exists_ f s = true -> Exists (fun x => f x = true) s. + Proof. intros s f _. unfold exists_. rewrite xexists_spec. trivial. Qed. + + + (** Specification of [partition] *) + + Lemma partition_filter : forall s f, + partition f s = (filter f s, filter (fun x => negb (f x)) s). + Proof. + unfold partition, filter. intros s f. generalize 1 as j. + induction s as [|l IHl o r IHr]; intro j. + reflexivity. + destruct o; simpl; rewrite IHl, IHr; reflexivity. + Qed. + + Lemma partition_1 : forall s f, compat_bool E.eq f -> + Equal (fst (partition f s)) (filter f s). + Proof. intros. rewrite partition_filter. apply eq_refl. Qed. + + Lemma partition_2 : forall s f, compat_bool E.eq f -> + Equal (snd (partition f s)) (filter (fun x => negb (f x)) s). + Proof. intros. rewrite partition_filter. apply eq_refl. Qed. + + + (** Specification of [elements] *) + + Notation InL := (InA E.eq). + + Lemma xelements_spec: forall s j acc y, + InL y (xelements s j acc) + <-> + InL y acc \/ exists x, y=(j@x) /\ mem x s = true. + Proof. + induction s as [|l IHl o r IHr]; simpl. + intros. split; intro H. + left. assumption. + destruct H as [H|[x [Hx Hx']]]. assumption. elim (empty_1 Hx'). + + intros j acc y. case o. + rewrite IHl. rewrite InA_cons. rewrite IHr. clear IHl IHr. split. + intros [[H|[H|[x [-> H]]]]|[x [-> H]]]; eauto. + right. exists x~1. auto. + right. exists x~0. auto. + intros [H|[x [-> H]]]. + eauto. + destruct x. + left. right. right. exists x; auto. + right. exists x; auto. + left. left. reflexivity. + + rewrite IHl, IHr. clear IHl IHr. split. + intros [[H|[x [-> H]]]|[x [-> H]]]. + eauto. + right. exists x~1. auto. + right. exists x~0. auto. + intros [H|[x [-> H]]]. + eauto. + destruct x. + left. right. exists x; auto. + right. exists x; auto. + discriminate. + Qed. + + Lemma elements_1: forall s x, In x s -> InL x (elements s). + Proof. + unfold elements, In. intros. + rewrite xelements_spec. right. exists x. auto. + Qed. + + Lemma elements_2: forall s x, InL x (elements s) -> In x s. + Proof. + unfold elements, In. intros s x H. + rewrite xelements_spec in H. destruct H as [H|[y [H H']]]. + inversion_clear H. + rewrite H. assumption. + Qed. + + Lemma lt_rev_append: forall j x y, E.lt x y -> E.lt (j@x) (j@y). + Proof. induction j; intros; simpl; auto. Qed. + + Lemma elements_3: forall s, sort E.lt (elements s). + Proof. + unfold elements. + assert (H: forall s j acc, + sort E.lt acc -> + (forall x y, In x s -> InL y acc -> E.lt (j@x) y) -> + sort E.lt (xelements s j acc)). + + induction s as [|l IHl o r IHr]; simpl; trivial. + intros j acc Hacc Hsacc. destruct o. + apply IHl. constructor. + apply IHr. apply Hacc. + intros x y Hx Hy. apply Hsacc; assumption. + case_eq (xelements r j~1 acc). constructor. + intros z q H. constructor. + assert (H': InL z (xelements r j~1 acc)). + rewrite H. constructor. reflexivity. + clear H q. rewrite xelements_spec in H'. destruct H' as [Hy|[x [-> Hx]]]. + apply (Hsacc 1 z); trivial. reflexivity. + simpl. apply lt_rev_append. exact I. + intros x y Hx Hy. inversion_clear Hy. + rewrite H. simpl. apply lt_rev_append. exact I. + rewrite xelements_spec in H. destruct H as [Hy|[z [-> Hy]]]. + apply Hsacc; assumption. + simpl. apply lt_rev_append. exact I. + + apply IHl. apply IHr. apply Hacc. + intros x y Hx Hy. apply Hsacc; assumption. + intros x y Hx Hy. rewrite xelements_spec in Hy. + destruct Hy as [Hy|[z [-> Hy]]]. + apply Hsacc; assumption. + simpl. apply lt_rev_append. exact I. + + intros. apply H. constructor. + intros x y _ H'. inversion H'. + Qed. + + Lemma elements_3w: forall s, NoDupA E.eq (elements s). + Proof. + intro. apply SortA_NoDupA with E.lt. + constructor. + intro. apply E.eq_refl. + intro. apply E.eq_sym. + intro. apply E.eq_trans. + constructor. + intros x H. apply E.lt_not_eq in H. apply H. reflexivity. + intro. apply E.lt_trans. + intros ? ? <- ? ? <-. reflexivity. + apply elements_3. + Qed. + + + (** Specification of [choose] *) + + Lemma choose_1: forall s x, choose s = Some x -> In x s. + Proof. + induction s as [| l IHl o r IHr]; simpl. + intros. discriminate. + destruct o. + intros x H. injection H; intros; subst. reflexivity. + revert IHl. case choose. + intros p Hp x H. injection H; intros; subst; clear H. apply Hp. + reflexivity. + intros _ x. revert IHr. case choose. + intros p Hp H. injection H; intros; subst; clear H. apply Hp. + reflexivity. + intros. discriminate. + Qed. + + Lemma choose_2: forall s, choose s = None -> Empty s. + Proof. + unfold Empty, In. intros s H. + induction s as [|l IHl o r IHr]. + intro. apply empty_1. + destruct o. + discriminate. + simpl in H. destruct (choose l). + discriminate. + destruct (choose r). + discriminate. + intros [a|a|]. + apply IHr. reflexivity. + apply IHl. reflexivity. + discriminate. + Qed. + + Lemma choose_empty: forall s, is_empty s = true -> choose s = None. + Proof. + intros s Hs. case_eq (choose s); trivial. + intros p Hp. apply choose_1 in Hp. apply is_empty_2 in Hs. elim (Hs _ Hp). + Qed. + + Lemma choose_3': forall s s', Equal s s' -> choose s = choose s'. + Proof. + setoid_rewrite equal_spec. + induction s as [|l IHl o r IHr]. + intros. symmetry. apply choose_empty. assumption. + + destruct s' as [|l' o' r']. + generalize (Node l o r) as s. simpl. intros. apply choose_empty. + rewrite <- equal_spec in H. apply eq_sym in H. rewrite equal_spec in H. + assumption. + + simpl. rewrite <- 2andb_lazy_alt, 2andb_true_iff, eqb_true_iff. + intros [[<- Hl] Hr]. rewrite (IHl _ Hl), (IHr _ Hr). reflexivity. + Qed. + + Lemma choose_3: forall s s' x y, + choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y. + Proof. intros s s' x y Hx Hy H. apply choose_3' in H. congruence. Qed. + + + (** Specification of [min_elt] *) + + Lemma min_elt_1: forall s x, min_elt s = Some x -> In x s. + Proof. + unfold In. + induction s as [| l IHl o r IHr]; simpl. + intros. discriminate. + intros x. destruct (min_elt l); intros. + injection H. intros <-. apply IHl. reflexivity. + destruct o; simpl. + injection H. intros <-. reflexivity. + destruct (min_elt r); simpl in *. + injection H. intros <-. apply IHr. reflexivity. + discriminate. + Qed. + + Lemma min_elt_3: forall s, min_elt s = None -> Empty s. + Proof. + unfold Empty, In. intros s H. + induction s as [|l IHl o r IHr]. + intro. apply empty_1. + intros [a|a|]. + apply IHr. revert H. clear. simpl. destruct (min_elt r); trivial. + case min_elt; intros; try discriminate. destruct o; discriminate. + apply IHl. revert H. clear. simpl. destruct (min_elt l); trivial. + intro; discriminate. + revert H. clear. simpl. case min_elt; intros; try discriminate. + destruct o; discriminate. + Qed. + + Lemma min_elt_2: forall s x y, min_elt s = Some x -> In y s -> ~ E.lt y x. + Proof. + unfold In. + induction s as [|l IHl o r IHr]; intros x y H H'. + discriminate. + simpl in H. case_eq (min_elt l). + intros p Hp. rewrite Hp in H. injection H; intros <-. + destruct y as [z|z|]; simpl; intro; trivial. apply (IHl p z); trivial. + intro Hp; rewrite Hp in H. apply min_elt_3 in Hp. + destruct o. + injection H. intros <- Hl. clear H. + destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). + + destruct (min_elt r). + injection H. intros <-. clear H. + destruct y as [z|z|]. + apply (IHr p z); trivial. + elim (Hp _ H'). + discriminate. + discriminate. + Qed. + + + (** Specification of [max_elt] *) + + Lemma max_elt_1: forall s x, max_elt s = Some x -> In x s. + Proof. + unfold In. + induction s as [| l IHl o r IHr]; simpl. + intros. discriminate. + intros x. destruct (max_elt r); intros. + injection H. intros <-. apply IHr. reflexivity. + destruct o; simpl. + injection H. intros <-. reflexivity. + destruct (max_elt l); simpl in *. + injection H. intros <-. apply IHl. reflexivity. + discriminate. + Qed. + + Lemma max_elt_3: forall s, max_elt s = None -> Empty s. + Proof. + unfold Empty, In. intros s H. + induction s as [|l IHl o r IHr]. + intro. apply empty_1. + intros [a|a|]. + apply IHr. revert H. clear. simpl. destruct (max_elt r); trivial. + intro; discriminate. + apply IHl. revert H. clear. simpl. destruct (max_elt l); trivial. + case max_elt; intros; try discriminate. destruct o; discriminate. + revert H. clear. simpl. case max_elt; intros; try discriminate. + destruct o; discriminate. + Qed. + + Lemma max_elt_2: forall s x y, max_elt s = Some x -> In y s -> ~ E.lt x y. + Proof. + unfold In. + induction s as [|l IHl o r IHr]; intros x y H H'. + discriminate. + simpl in H. case_eq (max_elt r). + intros p Hp. rewrite Hp in H. injection H; intros <-. + destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial. + intro Hp; rewrite Hp in H. apply max_elt_3 in Hp. + destruct o. + injection H. intros <- Hl. clear H. + destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). + + destruct (max_elt l). + injection H. intros <-. clear H. + destruct y as [z|z|]. + elim (Hp _ H'). + apply (IHl p z); trivial. + discriminate. + discriminate. + Qed. + +End PositiveSet. |