summaryrefslogtreecommitdiff
path: root/theories/MSets
diff options
context:
space:
mode:
Diffstat (limited to 'theories/MSets')
-rw-r--r--theories/MSets/MSetAVL.v5
-rw-r--r--theories/MSets/MSetDecide.v6
-rw-r--r--theories/MSets/MSetEqProperties.v5
-rw-r--r--theories/MSets/MSetGenTree.v24
-rw-r--r--theories/MSets/MSetInterface.v1
-rw-r--r--theories/MSets/MSetList.v21
-rw-r--r--theories/MSets/MSetPositive.v62
-rw-r--r--theories/MSets/MSetRBT.v21
-rw-r--r--theories/MSets/MSetWeakList.v18
9 files changed, 75 insertions, 88 deletions
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index db12ee31..e1fc454a 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -38,7 +38,6 @@ Unset Strict Implicit.
(* for nicer extraction, we create inductive principles
only when needed *)
Local Unset Elimination Schemes.
-Local Unset Case Analysis Schemes.
(** * Ops : the pure functions *)
@@ -307,13 +306,13 @@ Include MSetGenTree.Props X I.
Local Hint Immediate MX.eq_sym.
Local Hint Unfold In lt_tree gt_tree Ok.
Local Hint Constructors InT bst.
-Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok.
Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
Local Hint Resolve elements_spec2.
(* Sometimes functional induction will expose too much of
- a tree structure. The following tactic allows to factor back
+ a tree structure. The following tactic allows factoring back
a Node whose internal parts occurs nowhere else. *)
(* TODO: why Ltac instead of Tactic Notation don't work ? why clear ? *)
diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v
index eefd2951..f2555791 100644
--- a/theories/MSets/MSetDecide.v
+++ b/theories/MSets/MSetDecide.v
@@ -15,7 +15,7 @@
(** This file implements a decision procedure for a certain
class of propositions involving finite sets. *)
-Require Import Decidable DecidableTypeEx MSetFacts.
+Require Import Decidable Setoid DecidableTypeEx MSetFacts.
(** First, a version for Weak Sets in functorial presentation *)
@@ -115,8 +115,8 @@ the above form:
not affect the namespace if you import the enclosing
module [Decide]. *)
Module MSetLogicalFacts.
- Require Export Decidable.
- Require Export Setoid.
+ Export Decidable.
+ Export Setoid.
(** ** Lemmas and Tactics About Decidable Propositions *)
diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v
index 4f0d93fb..ae20edc8 100644
--- a/theories/MSets/MSetEqProperties.v
+++ b/theories/MSets/MSetEqProperties.v
@@ -819,8 +819,7 @@ Proof.
intros.
rewrite for_all_exists in H; auto.
rewrite negb_true_iff in H.
-elim (@for_all_mem_4 (fun x =>negb (f x)) Comp' s);intros;auto.
-elim p;intros.
+destruct (@for_all_mem_4 (fun x =>negb (f x)) Comp' s) as (x,[]); auto.
exists x;split;auto.
rewrite <-negb_false_iff; auto.
Qed.
@@ -856,7 +855,7 @@ intros.
rewrite <- (fold_equal _ _ _ _ fc ft 0 _ _ H).
rewrite <- (fold_equal _ _ _ _ gc gt 0 _ _ H).
rewrite <- (fold_equal _ _ _ _ fgc fgt 0 _ _ H); auto.
-intros; do 3 (rewrite fold_add; auto with *).
+intros. do 3 (rewrite fold_add; auto with *).
do 3 rewrite fold_empty;auto.
Qed.
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index 704ff31b..154c2384 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -27,14 +27,13 @@
- min_elt max_elt choose
*)
-Require Import Orders OrdersFacts MSetInterface NPeano.
+Require Import Orders OrdersFacts MSetInterface PeanoNat.
Local Open Scope list_scope.
Local Open Scope lazy_bool_scope.
(* For nicer extraction, we create induction principles
only when needed *)
Local Unset Elimination Schemes.
-Local Unset Case Analysis Schemes.
Module Type InfoTyp.
Parameter t : Set.
@@ -341,7 +340,7 @@ Module Import MX := OrderedTypeFacts X.
Scheme tree_ind := Induction for tree Sort Prop.
Scheme bst_ind := Induction for bst Sort Prop.
-Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok.
Local Hint Immediate MX.eq_sym.
Local Hint Unfold In lt_tree gt_tree.
Local Hint Constructors InT bst.
@@ -378,7 +377,7 @@ Ltac invtree f :=
Ltac inv := inv_ok; invtree InT.
-Ltac intuition_in := repeat progress (intuition; inv).
+Ltac intuition_in := repeat (intuition; inv).
(** Helper tactic concerning order of elements. *)
@@ -963,13 +962,16 @@ Proof. firstorder. Qed.
Lemma eq_Leq : forall s s', eq s s' <-> L.eq (elements s) (elements s').
Proof.
unfold eq, Equal, L.eq; intros.
- setoid_rewrite elements_spec1; firstorder.
+ setoid_rewrite elements_spec1.
+ firstorder.
Qed.
Definition lt (s1 s2 : tree) : Prop :=
exists s1' s2', Ok s1' /\ Ok s2' /\ eq s1 s1' /\ eq s2 s2'
/\ L.lt (elements s1') (elements s2').
+Declare Equivalent Keys L.eq equivlistA.
+
Instance lt_strorder : StrictOrder lt.
Proof.
split.
@@ -1017,7 +1019,7 @@ Lemma flatten_e_elements :
forall l x r c e,
elements l ++ flatten_e (More x r e) = elements (Node c l x r) ++ flatten_e e.
Proof.
- intros; simpl. now rewrite elements_node, app_ass.
+ intros. now rewrite elements_node, app_ass.
Qed.
Lemma cons_1 : forall s e,
@@ -1051,7 +1053,7 @@ Lemma compare_cont_Cmp : forall s1 cont e2 l,
(forall e, Cmp (cont e) l (flatten_e e)) ->
Cmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2).
Proof.
- induction s1 as [|c1 l1 Hl1 x1 r1 Hr1]; simpl; intros; auto.
+ induction s1 as [|c1 l1 Hl1 x1 r1 Hr1]; intros; auto.
rewrite elements_node, app_ass; simpl.
apply Hl1; auto. clear e2. intros [|x2 r2 e2].
simpl; auto.
@@ -1063,9 +1065,9 @@ Lemma compare_Cmp : forall s1 s2,
Cmp (compare s1 s2) (elements s1) (elements s2).
Proof.
intros; unfold compare.
- rewrite (app_nil_end (elements s1)).
+ rewrite <- (app_nil_r (elements s1)).
replace (elements s2) with (flatten_e (cons s2 End)) by
- (rewrite cons_1; simpl; rewrite <- app_nil_end; auto).
+ (rewrite cons_1; simpl; rewrite app_nil_r; auto).
apply compare_cont_Cmp; auto.
intros.
apply compare_end_Cmp; auto.
@@ -1129,14 +1131,14 @@ Proof.
Qed.
Lemma maxdepth_log_cardinal s : s <> Leaf ->
- log2 (cardinal s) < maxdepth s.
+ Nat.log2 (cardinal s) < maxdepth s.
Proof.
intros H.
apply Nat.log2_lt_pow2. destruct s; simpl; intuition.
apply maxdepth_cardinal.
Qed.
-Lemma mindepth_log_cardinal s : mindepth s <= log2 (S (cardinal s)).
+Lemma mindepth_log_cardinal s : mindepth s <= Nat.log2 (S (cardinal s)).
Proof.
apply Nat.log2_le_pow2. auto with arith.
apply mindepth_cardinal.
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index 6778deff..bd881168 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -431,7 +431,6 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E.
(** We avoid creating induction principles for the Record *)
Local Unset Elimination Schemes.
- Local Unset Case Analysis Schemes.
Definition elt := E.t.
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index d9b1fd9b..fb0d1ad9 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -56,7 +56,7 @@ Module Ops (X:OrderedType) <: WOps X.
Definition singleton (x : elt) := x :: nil.
- Fixpoint remove x s :=
+ Fixpoint remove x s : t :=
match s with
| nil => nil
| y :: l =>
@@ -228,16 +228,14 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
Notation Inf := (lelistA X.lt).
Notation In := (InA X.eq).
- (* TODO: modify proofs in order to avoid these hints *)
- Hint Resolve (@Equivalence_Reflexive _ _ X.eq_equiv).
- Hint Immediate (@Equivalence_Symmetric _ _ X.eq_equiv).
- Hint Resolve (@Equivalence_Transitive _ _ X.eq_equiv).
+ Existing Instance X.eq_equiv.
+ Hint Extern 20 => solve [order].
Definition IsOk s := Sort s.
Class Ok (s:t) : Prop := ok : Sort s.
- Hint Resolve @ok.
+ Hint Resolve ok.
Hint Unfold Ok.
Instance Sort_Ok s `(Hs : Sort s) : Ok s := { ok := Hs }.
@@ -343,7 +341,6 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
induction s; simpl; intros.
intuition. inv; auto.
elim_compare x a; inv; rewrite !InA_cons, ?IHs; intuition.
- left; order.
Qed.
Lemma remove_inf :
@@ -402,8 +399,8 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
Global Instance union_ok s s' : forall `(Ok s, Ok s'), Ok (union s s').
Proof.
repeat rewrite <- isok_iff; revert s s'.
- induction2; constructors; try apply @ok; auto.
- apply Inf_eq with x'; auto; apply union_inf; auto; apply Inf_eq with x; auto.
+ induction2; constructors; try apply @ok; auto.
+ apply Inf_eq with x'; auto; apply union_inf; auto; apply Inf_eq with x; auto; order.
change (Inf x' (union (x :: l) l')); auto.
Qed.
@@ -412,7 +409,6 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
In x (union s s') <-> In x s \/ In x s'.
Proof.
induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto.
- left; order.
Qed.
Lemma inter_inf :
@@ -440,7 +436,6 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
Proof.
induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto;
try sort_inf_in; try order.
- left; order.
Qed.
Lemma diff_inf :
@@ -477,7 +472,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
equal s s' = true <-> Equal s s'.
Proof.
induction s as [ | x s IH]; intros [ | x' s'] Hs Hs'; simpl.
- intuition.
+ intuition reflexivity.
split; intros H. discriminate. assert (In x' nil) by (rewrite H; auto). inv.
split; intros H. discriminate. assert (In x nil) by (rewrite <-H; auto). inv.
inv.
@@ -825,7 +820,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
Lemma compare_spec_aux : forall s s', CompSpec eq L.lt s s' (compare s s').
Proof.
- induction s as [|x s IH]; intros [|x' s']; simpl; intuition.
+ induction s as [|x s IH]; intros [|x' s']; simpl; intuition.
elim_compare x x'; auto.
Qed.
diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v
index e500602f..25a8c162 100644
--- a/theories/MSets/MSetPositive.v
+++ b/theories/MSets/MSetPositive.v
@@ -19,14 +19,9 @@
Require Import Bool BinPos Orders MSetInterface.
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.
-
(** Even if [positive] can be seen as an ordered type with respect to the
usual order (see above), we can also use a lexicographic order over bits
@@ -98,7 +93,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
Module E:=PositiveOrderedTypeBits.
- Definition elt := positive.
+ Definition elt := positive : Type.
Inductive tree :=
| Leaf : tree
@@ -106,9 +101,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
@@ -116,7 +111,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 : positive) (m : t) {struct m} : bool :=
match m with
| Leaf => false
| Node l o r =>
@@ -147,13 +142,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 : positive) (m : t) {struct m} : t :=
match m with
| Leaf => Leaf
| Node l o r =>
@@ -164,7 +159,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 =>
@@ -174,7 +169,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 =>
@@ -184,7 +179,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 =>
@@ -216,7 +211,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
@@ -267,14 +262,14 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
end.
Definition exists_ m := xexists m 1.
- Fixpoint xfilter (m : t) (i : positive) :=
+ Fixpoint xfilter (m : t) (i : positive) : 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 : positive) : t * t :=
match m with
| Leaf => (Leaf,Leaf)
| Node l o r =>
@@ -316,7 +311,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
@@ -326,7 +321,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 =>
@@ -336,7 +331,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 =>
@@ -414,10 +409,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.
+ destruct x; reflexivity.
Qed.
Local Opaque node.
@@ -427,7 +419,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
Proof.
unfold Empty, In.
induction s as [|l IHl o r IHr]; simpl.
- setoid_rewrite mem_Leaf. firstorder.
+ firstorder.
rewrite <- 2andb_lazy_alt, 2andb_true_iff, IHl, IHr. clear IHl IHr.
destruct o; simpl; split.
intuition discriminate.
@@ -813,7 +805,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
rewrite <- andb_lazy_alt. apply andb_true_iff.
Qed.
- Lemma filter_spec: forall s x f, compat_bool E.eq f ->
+ Lemma filter_spec: forall s x f, @compat_bool elt E.eq f ->
(In x (filter f s) <-> In x s /\ f x = true).
Proof. intros. apply xfilter_spec. Qed.
@@ -824,7 +816,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
Proof.
unfold For_all, In. intro f.
induction s as [|l IHl o r IHr]; intros i; simpl.
- setoid_rewrite mem_Leaf. intuition discriminate.
+ intuition discriminate.
rewrite <- 2andb_lazy_alt, <- orb_lazy_alt, 2 andb_true_iff.
rewrite IHl, IHr. clear IHl IHr.
split.
@@ -838,7 +830,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
apply H. assumption.
Qed.
- Lemma for_all_spec: forall s f, compat_bool E.eq f ->
+ Lemma for_all_spec: forall s f, @compat_bool elt E.eq f ->
(for_all f s = true <-> For_all (fun x => f x = true) s).
Proof. intros. apply xforall_spec. Qed.
@@ -849,7 +841,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.
+ firstorder.
rewrite <- 2orb_lazy_alt, 2orb_true_iff, <- andb_lazy_alt, andb_true_iff.
rewrite IHl, IHr. clear IHl IHr.
split.
@@ -860,7 +852,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
intros [[x|x|] H]; eauto.
Qed.
- Lemma exists_spec : forall s f, compat_bool E.eq f ->
+ Lemma exists_spec : forall s f, @compat_bool elt E.eq f ->
(exists_ f s = true <-> Exists (fun x => f x = true) s).
Proof. intros. apply xexists_spec. Qed.
@@ -876,11 +868,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
destruct o; simpl; rewrite IHl, IHr; reflexivity.
Qed.
- Lemma partition_spec1 : forall s f, compat_bool E.eq f ->
+ Lemma partition_spec1 : forall s f, @compat_bool elt E.eq f ->
Equal (fst (partition f s)) (filter f s).
Proof. intros. rewrite partition_filter. reflexivity. Qed.
- Lemma partition_spec2 : forall s f, compat_bool E.eq f ->
+ Lemma partition_spec2 : 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. reflexivity. Qed.
@@ -897,7 +889,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_spec 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.
@@ -1087,7 +1079,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.
@@ -1141,7 +1133,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.
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
index b838495f..751d4f35 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -31,13 +31,12 @@ Additional suggested reading:
*)
Require MSetGenTree.
-Require Import Bool List BinPos Pnat Setoid SetoidList NPeano.
+Require Import Bool List BinPos Pnat Setoid SetoidList PeanoNat.
Local Open Scope list_scope.
(* For nicer extraction, we create induction principles
only when needed *)
Local Unset Elimination Schemes.
-Local Unset Case Analysis Schemes.
(** An extra function not (yet?) in MSetInterface.S *)
@@ -399,7 +398,7 @@ Definition skip_black t :=
Fixpoint compare_height (s1x s1 s2 s2x: tree) : comparison :=
match skip_red s1x, skip_red s1, skip_red s2, skip_red s2x with
| Node _ s1x' _ _, Node _ s1' _ _, Node _ s2' _ _, Node _ s2x' _ _ =>
- compare_height (skip_black s2x') s1' s2' (skip_black s2x')
+ compare_height (skip_black s1x') s1' s2' (skip_black s2x')
| _, Leaf, _, Node _ _ _ _ => Lt
| Node _ _ _ _, _, Leaf, _ => Gt
| Node _ s1x' _ _, Node _ s1' _ _, Node _ s2' _ _, Leaf =>
@@ -452,7 +451,7 @@ Local Notation Bk := (Node Black).
Local Hint Immediate MX.eq_sym.
Local Hint Unfold In lt_tree gt_tree Ok.
Local Hint Constructors InT bst.
-Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok.
Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
Local Hint Resolve elements_spec2.
@@ -980,7 +979,7 @@ Proof.
{ transitivity size; trivial. subst. auto with arith. }
destruct acc1 as [|x acc1].
{ exfalso. revert LE. apply Nat.lt_nge. subst.
- rewrite <- app_nil_end, <- elements_cardinal; auto with arith. }
+ rewrite app_nil_r, <- elements_cardinal; auto with arith. }
specialize (Hg acc1).
destruct (g acc1) as (t2,acc2).
destruct Hg as (Hg1,Hg2).
@@ -988,7 +987,7 @@ Proof.
rewrite app_length, <- elements_cardinal. simpl.
rewrite Nat.add_succ_r, <- Nat.succ_le_mono.
apply Nat.add_le_mono_l. }
- simpl. rewrite elements_node, app_ass. now subst.
+ rewrite elements_node, app_ass. now subst.
Qed.
Lemma treeify_aux_spec n (p:bool) :
@@ -1013,7 +1012,7 @@ Qed.
Lemma plength_aux_spec l p :
Pos.to_nat (plength_aux l p) = length l + Pos.to_nat p.
Proof.
- revert p. induction l; simpl; trivial.
+ revert p. induction l; trivial. simpl plength_aux.
intros. now rewrite IHl, Pos2Nat.inj_succ, Nat.add_succ_r.
Qed.
@@ -1059,7 +1058,7 @@ Lemma filter_aux_elements s f acc :
filter_aux f s acc = List.filter f (elements s) ++ acc.
Proof.
revert acc.
- induction s as [|c l IHl x r IHr]; simpl; trivial.
+ induction s as [|c l IHl x r IHr]; trivial.
intros acc.
rewrite elements_node, filter_app. simpl.
destruct (f x); now rewrite IHl, IHr, app_ass.
@@ -1197,7 +1196,7 @@ Lemma INV_rev l1 l2 acc :
Proof.
intros. rewrite rev_append_rev.
apply SortA_app with X.eq; eauto with *.
- intros x y. inA. eapply l1_lt_acc; eauto.
+ intros x y. inA. eapply @l1_lt_acc; eauto.
Qed.
(** ** union *)
@@ -1567,7 +1566,7 @@ Proof.
Qed.
Lemma maxdepth_upperbound s : Rbt s ->
- maxdepth s <= 2 * log2 (S (cardinal s)).
+ maxdepth s <= 2 * Nat.log2 (S (cardinal s)).
Proof.
intros (n,H).
eapply Nat.le_trans; [eapply rb_maxdepth; eauto|].
@@ -1582,7 +1581,7 @@ Proof.
Qed.
Lemma maxdepth_lowerbound s : s<>Leaf ->
- log2 (cardinal s) < maxdepth s.
+ Nat.log2 (cardinal s) < maxdepth s.
Proof.
apply maxdepth_log_cardinal.
Qed.
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index fd4114cd..372acd56 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -56,8 +56,8 @@ Module Ops (X: DecidableType) <: WOps X.
if X.eq_dec x y then l else y :: remove x l
end.
- Definition fold (B : Type) (f : elt -> B -> B) (s : t) (i : B) : B :=
- fold_left (flip f) s i.
+ Definition fold (B : Type) (f : elt -> B -> B) : t -> B -> B :=
+ fold_left (flip f).
Definition union (s : t) : t -> t := fold add s.
@@ -118,16 +118,18 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
Notation In := (InA X.eq).
(* TODO: modify proofs in order to avoid these hints *)
- Hint Resolve (@Equivalence_Reflexive _ _ X.eq_equiv).
- Hint Immediate (@Equivalence_Symmetric _ _ X.eq_equiv).
- Hint Resolve (@Equivalence_Transitive _ _ X.eq_equiv).
+ Let eqr:= (@Equivalence_Reflexive _ _ X.eq_equiv).
+ Let eqsym:= (@Equivalence_Symmetric _ _ X.eq_equiv).
+ Let eqtrans:= (@Equivalence_Transitive _ _ X.eq_equiv).
+ Hint Resolve eqr eqtrans.
+ Hint Immediate eqsym.
Definition IsOk := NoDup.
Class Ok (s:t) : Prop := ok : NoDup s.
Hint Unfold Ok.
- Hint Resolve @ok.
+ Hint Resolve ok.
Instance NoDup_Ok s (nd : NoDup s) : Ok s := { ok := nd }.
@@ -215,10 +217,10 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
Proof.
induction s; simpl; intros.
intuition; inv; auto.
- destruct X.eq_dec; inv; rewrite !InA_cons, ?IHs; intuition.
+ destruct X.eq_dec as [|Hnot]; inv; rewrite !InA_cons, ?IHs; intuition.
elim H. setoid_replace a with y; eauto.
elim H3. setoid_replace x with y; eauto.
- elim n. eauto.
+ elim Hnot. eauto.
Qed.
Global Instance remove_ok s x `(Ok s) : Ok (remove x s).
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 21:46:29 +0000