diff options
Diffstat (limited to 'theories/FSets/FSetPositive.v')
-rw-r--r-- | theories/FSets/FSetPositive.v | 95 |
1 files changed, 44 insertions, 51 deletions
diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v index e5d55ac5..7398c6d6 100644 --- a/theories/FSets/FSetPositive.v +++ b/theories/FSets/FSetPositive.v @@ -19,20 +19,15 @@ 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. + Definition elt := positive : Type. Inductive tree := | Leaf : tree @@ -40,9 +35,9 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Scheme tree_ind := Induction for tree Sort Prop. - Definition t := tree. + Definition t := tree : Type. - Definition empty := Leaf. + Definition empty : t := Leaf. Fixpoint is_empty (m : t) : bool := match m with @@ -50,7 +45,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. | Node l b r => negb b &&& is_empty l &&& is_empty r end. - Fixpoint mem (i : positive) (m : t) : bool := + Fixpoint mem (i : elt) (m : t) {struct m} : bool := match m with | Leaf => false | Node l o r => @@ -61,7 +56,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint add (i : positive) (m : t) : t := + Fixpoint add (i : elt) (m : t) : t := match m with | Leaf => match i with @@ -81,13 +76,13 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. (** helper function to avoid creating empty trees that are not leaves *) - Definition node l (b: bool) r := + Definition node (l : t) (b: bool) (r : t) : t := 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 := + Fixpoint remove (i : elt) (m : t) {struct m} : t := match m with | Leaf => Leaf | Node l o r => @@ -98,7 +93,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint union (m m': t) := + Fixpoint union (m m': t) : t := match m with | Leaf => m' | Node l o r => @@ -108,7 +103,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint inter (m m': t) := + Fixpoint inter (m m': t) : t := match m with | Leaf => Leaf | Node l o r => @@ -118,7 +113,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint diff (m m': t) := + Fixpoint diff (m m': t) : t := match m with | Leaf => Leaf | Node l o r => @@ -150,7 +145,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. (** reverses [y] and concatenate it with [x] *) - Fixpoint rev_append y x := + Fixpoint rev_append (y x : elt) : elt := match y with | 1 => x | y~1 => rev_append y x~1 @@ -161,8 +156,8 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Section Fold. - Variables B : Type. - Variable f : positive -> B -> B. + Variable B : Type. + Variable f : elt -> B -> B. (** the additional argument, [i], records the current path, in reverse order (this should be more efficient: we reverse this argument @@ -170,7 +165,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. we also use this convention in all functions below *) - Fixpoint xfold (m : t) (v : B) (i : positive) := + Fixpoint xfold (m : t) (v : B) (i : elt) := match m with | Leaf => v | Node l true r => @@ -184,9 +179,9 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Section Quantifiers. - Variable f : positive -> bool. + Variable f : elt -> bool. - Fixpoint xforall (m : t) (i : positive) := + Fixpoint xforall (m : t) (i : elt) := match m with | Leaf => true | Node l o r => @@ -194,21 +189,21 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end. Definition for_all m := xforall m 1. - Fixpoint xexists (m : t) (i : positive) := + Fixpoint xexists (m : t) (i : elt) := 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) := + Fixpoint xfilter (m : t) (i : elt) : t := 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) := + Fixpoint xpartition (m : t) (i : elt) : t * t := match m with | Leaf => (Leaf,Leaf) | Node l o r => @@ -226,7 +221,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. (** uses [a] to accumulate values rather than doing a lot of concatenations *) - Fixpoint xelements (m : t) (i : positive) (a: list positive) := + Fixpoint xelements (m : t) (i : elt) (a: list elt) := match m with | Leaf => a | Node l false r => xelements l i~0 (xelements r i~1 a) @@ -250,7 +245,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. (** would it be more efficient to use a path like in the above functions ? *) - Fixpoint choose (m: t) := + Fixpoint choose (m: t) : option elt := match m with | Leaf => None | Node l o r => if o then Some 1 else @@ -260,7 +255,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint min_elt (m: t) := + Fixpoint min_elt (m: t) : option elt := match m with | Leaf => None | Node l o r => @@ -270,7 +265,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint max_elt (m: t) := + Fixpoint max_elt (m: t) : option elt := match m with | Leaf => None | Node l o r => @@ -311,6 +306,9 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Notation "s [<=] t" := (Subset s t) (at level 70, no associativity). Definition eq := Equal. + + Declare Equivalent Keys Equal eq. + Definition lt m m' := compare_fun m m' = Lt. (** Specification of [In] *) @@ -355,10 +353,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. case o; trivial. destruct l; trivial. destruct r; trivial. - symmetry. destruct x. - apply mem_Leaf. - apply mem_Leaf. - reflexivity. + now destruct x. Qed. Local Opaque node. @@ -367,8 +362,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. 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. + induction s as [|l IHl o r IHr]; simpl. now split. rewrite <- 2andb_lazy_alt, 2andb_true_iff, <- IHl, <- IHr. clear IHl IHr. destruct o; simpl; split. intro H. elim (H 1). reflexivity. @@ -759,7 +753,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. 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. @@ -807,15 +801,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. rewrite <- andb_lazy_alt. apply andb_true_iff. Qed. - Lemma filter_1 : forall s x f, compat_bool E.eq f -> + Lemma filter_1 : forall s x f, @compat_bool elt 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 -> + Lemma filter_2 : forall s x f, @compat_bool elt 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 -> + Lemma filter_3 : forall s x f, @compat_bool elt 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. @@ -826,8 +820,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. 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. + induction s as [|l IHl o r IHr]; intros i; simpl. now split. rewrite <- 2andb_lazy_alt, <- orb_lazy_alt, 2 andb_true_iff. rewrite IHl, IHr. clear IHl IHr. split. @@ -841,11 +834,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. apply H. assumption. Qed. - Lemma for_all_1 : forall s f, compat_bool E.eq f -> + Lemma for_all_1 : forall s f, @compat_bool elt 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 -> + Lemma for_all_2 : forall s f, @compat_bool elt 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. @@ -857,7 +850,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Proof. unfold Exists, In. intro f. induction s as [|l IHl o r IHr]; intros i; simpl. - setoid_rewrite mem_Leaf. firstorder. + split; [ discriminate | now intros [ _ [? _]]]. rewrite <- 2orb_lazy_alt, 2orb_true_iff, <- andb_lazy_alt, andb_true_iff. rewrite IHl, IHr. clear IHl IHr. split. @@ -868,11 +861,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. intros [[x|x|] H]; eauto. Qed. - Lemma exists_1 : forall s f, compat_bool E.eq f -> + Lemma exists_1 : forall s f, @compat_bool elt 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 -> + Lemma exists_2 : forall s f, @compat_bool elt 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. @@ -888,11 +881,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. destruct o; simpl; rewrite IHl, IHr; reflexivity. Qed. - Lemma partition_1 : forall s f, compat_bool E.eq f -> + Lemma partition_1 : forall s f, @compat_bool elt 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 -> + Lemma partition_2 : forall s f, @compat_bool elt E.eq f -> Equal (snd (partition f s)) (filter (fun x => negb (f x)) s). Proof. intros. rewrite partition_filter. apply eq_refl. Qed. @@ -909,7 +902,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. 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'). + destruct H as [H|[x [Hx Hx']]]. assumption. discriminate. intros j acc y. case o. rewrite IHl. rewrite InA_cons. rewrite IHr. clear IHl IHr. split. @@ -1000,7 +993,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. constructor. intros x H. apply E.lt_not_eq in H. apply H. reflexivity. intro. apply E.lt_trans. - intros ? ? <- ? ? <-. reflexivity. + solve_proper. apply elements_3. Qed. @@ -1111,7 +1104,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. destruct (min_elt r). injection H. intros <-. clear H. destruct y as [z|z|]. - apply (IHr p z); trivial. + apply (IHr e z); trivial. elim (Hp _ H'). discriminate. discriminate. @@ -1165,7 +1158,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. injection H. intros <-. clear H. destruct y as [z|z|]. elim (Hp _ H'). - apply (IHl p z); trivial. + apply (IHl e z); trivial. discriminate. discriminate. Qed. |