summaryrefslogtreecommitdiff
path: root/theories/FSets/FSetPositive.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets/FSetPositive.v')
-rw-r--r--theories/FSets/FSetPositive.v95
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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 03:03:12 +0000