summaryrefslogtreecommitdiff
path: root/theories/MSets
diff options
context:
space:
mode:
Diffstat (limited to 'theories/MSets')
-rw-r--r--theories/MSets/MSetEqProperties.v8
-rw-r--r--theories/MSets/MSetInterface.v2
-rw-r--r--theories/MSets/MSetList.v6
-rw-r--r--theories/MSets/MSetPositive.v4
-rw-r--r--theories/MSets/MSetProperties.v2
-rw-r--r--theories/MSets/MSetRBT.v104
-rw-r--r--theories/MSets/MSetWeakList.v6
7 files changed, 83 insertions, 49 deletions
diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v
index 2e7da404..4f0d93fb 100644
--- a/theories/MSets/MSetEqProperties.v
+++ b/theories/MSets/MSetEqProperties.v
@@ -206,7 +206,7 @@ intros.
generalize (@choose_1 s) (@choose_2 s).
destruct (choose s);intros.
exists e;auto with set.
-generalize (H1 (refl_equal None)); clear H1.
+generalize (H1 (eq_refl None)); clear H1.
intros; rewrite (is_empty_1 H1) in H; discriminate.
Qed.
@@ -631,7 +631,7 @@ destruct (choose (filter f s)).
intros H0 _; apply exists_1; auto.
exists e; generalize (H0 e); rewrite filter_iff; auto.
intros _ H0.
-rewrite (is_empty_1 (H0 (refl_equal None))) in H; auto; discriminate.
+rewrite (is_empty_1 (H0 (eq_refl None))) in H; auto; discriminate.
Qed.
Lemma partition_filter_1:
@@ -879,8 +879,8 @@ generalize (@add_filter_1 f Hf s0 (add x s0) x) (@add_filter_2 f Hf s0 (add x s0
assert (~ In x (filter f s0)).
intro H1; rewrite (mem_1 (filter_1 Hf H1)) in H; discriminate H.
case (f x); simpl; intros.
-rewrite (MP.cardinal_2 H1 (H2 (refl_equal true) (MP.Add_add s0 x))); auto.
-rewrite <- (MP.Equal_cardinal (H3 (refl_equal false) (MP.Add_add s0 x))); auto.
+rewrite (MP.cardinal_2 H1 (H2 (eq_refl true) (MP.Add_add s0 x))); auto.
+rewrite <- (MP.Equal_cardinal (H3 (eq_refl false) (MP.Add_add s0 x))); auto.
intros; rewrite fold_empty;auto.
rewrite MP.cardinal_1; auto.
unfold Empty; intros.
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index f2b908af..6778deff 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -480,7 +480,7 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E.
Proof.
intros (s,Hs) (s',Hs').
change ({M.Equal s s'}+{~M.Equal s s'}).
- destruct (M.equal s s') as [ ]_eqn:H; [left|right];
+ destruct (M.equal s s') eqn:H; [left|right];
rewrite <- M.equal_spec; congruence.
Defined.
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index bcf68f1d..d9b1fd9b 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -662,7 +662,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
Proof.
induction s; simpl; intros.
split; intuition; inv.
- destruct (f a) as [ ]_eqn:F; rewrite !InA_cons, ?IHs; intuition.
+ destruct (f a) eqn:F; rewrite !InA_cons, ?IHs; intuition.
setoid_replace x with a; auto.
setoid_replace a with x in F; auto; congruence.
Qed.
@@ -674,7 +674,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
Proof.
unfold For_all; induction s; simpl; intros.
split; intros; auto. inv.
- destruct (f a) as [ ]_eqn:F.
+ destruct (f a) eqn:F.
rewrite IHs; auto. firstorder. inv; auto.
setoid_replace x with a; auto.
split; intros H'. discriminate.
@@ -688,7 +688,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
Proof.
unfold Exists; induction s; simpl; intros.
firstorder. discriminate. inv.
- destruct (f a) as [ ]_eqn:F.
+ destruct (f a) eqn:F.
firstorder.
rewrite IHs; auto.
firstorder.
diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v
index e83ac27d..e500602f 100644
--- a/theories/MSets/MSetPositive.v
+++ b/theories/MSets/MSetPositive.v
@@ -36,8 +36,8 @@ Local Unset Boolean Equality Schemes.
Module PositiveOrderedTypeBits <: UsualOrderedType.
Definition t:=positive.
Include HasUsualEq <+ UsualIsEq.
- Definition eqb := Peqb.
- Definition eqb_eq := Peqb_eq.
+ Definition eqb := Pos.eqb.
+ Definition eqb_eq := Pos.eqb_eq.
Include HasEqBool2Dec.
Fixpoint bits_lt (p q:positive) : Prop :=
diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v
index 0f24d76a..396067b5 100644
--- a/theories/MSets/MSetProperties.v
+++ b/theories/MSets/MSetProperties.v
@@ -831,7 +831,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
rewrite (inter_subset_equal H).
generalize (@cardinal_inv_1 (diff s' s)).
destruct (cardinal (diff s' s)).
- intro H2; destruct (H2 (refl_equal _) x).
+ intro H2; destruct (H2 (eq_refl _) x).
set_iff; auto.
intros _.
change (0 + cardinal s < S n + cardinal s).
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
index b53c0392..b838495f 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -31,7 +31,7 @@ Additional suggested reading:
*)
Require MSetGenTree.
-Require Import Bool List BinPos Pnat Setoid SetoidList NPeano Psatz.
+Require Import Bool List BinPos Pnat Setoid SetoidList NPeano.
Local Open Scope list_scope.
(* For nicer extraction, we create induction principles
@@ -280,11 +280,13 @@ Fixpoint treeify_aux (pred:bool)(n: positive) : treeify_t :=
| xI n => treeify_cont (treeify_aux false n) (treeify_aux pred n)
end.
-Fixpoint plength (l:list elt) := match l with
- | nil => 1%positive
- | _::l => Psucc (plength l)
+Fixpoint plength_aux (l:list elt)(p:positive) := match l with
+ | nil => p
+ | _::l => plength_aux l (Pos.succ p)
end.
+Definition plength l := plength_aux l 1.
+
Definition treeify (l:list elt) :=
fst (treeify_aux true (plength l) l).
@@ -975,18 +977,18 @@ Proof.
specialize (Hf acc).
destruct (f acc) as (t1,acc1).
destruct Hf as (Hf1,Hf2).
- { lia. }
+ { transitivity size; trivial. subst. auto with arith. }
destruct acc1 as [|x acc1].
- { exfalso. subst acc.
- rewrite <- app_nil_end, <- elements_cardinal in LE. lia. }
+ { exfalso. revert LE. apply Nat.lt_nge. subst.
+ rewrite <- app_nil_end, <- elements_cardinal; auto with arith. }
specialize (Hg acc1).
destruct (g acc1) as (t2,acc2).
destruct Hg as (Hg1,Hg2).
- { subst acc. rewrite app_length, <- elements_cardinal in LE.
- simpl in LE. unfold elt in *. lia. }
- simpl. split.
- * lia.
- * rewrite elements_node, app_ass. simpl. unfold elt in *; congruence.
+ { revert LE. subst.
+ 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.
Qed.
Lemma treeify_aux_spec n (p:bool) :
@@ -995,17 +997,29 @@ Proof.
revert p.
induction n as [n|n|]; intros p; simpl treeify_aux.
- eapply treeify_cont_spec; [ apply (IHn false) | apply (IHn p) | ].
- rewrite Pos2Nat.inj_xI. generalize (Pos2Nat.is_pos n).
- destruct p; simpl; lia.
+ rewrite Pos2Nat.inj_xI.
+ assert (H := Pos2Nat.is_pos n). apply Nat.neq_0_lt_0 in H.
+ destruct p; simpl; intros; rewrite Nat.add_0_r; trivial.
+ now rewrite <- Nat.add_succ_r, Nat.succ_pred; trivial.
- eapply treeify_cont_spec; [ apply (IHn p) | apply (IHn true) | ].
- rewrite Pos2Nat.inj_xO. generalize (Pos2Nat.is_pos n).
- destruct p; simpl; lia.
+ rewrite Pos2Nat.inj_xO.
+ assert (H := Pos2Nat.is_pos n). apply Nat.neq_0_lt_0 in H.
+ rewrite <- Nat.add_succ_r, Nat.succ_pred by trivial.
+ destruct p; simpl; intros; rewrite Nat.add_0_r; trivial.
+ symmetry. now apply Nat.add_pred_l.
- destruct p; [ apply treeify_zero_spec | apply treeify_one_spec ].
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.
+ intros. now rewrite IHl, Pos2Nat.inj_succ, Nat.add_succ_r.
+Qed.
+
Lemma plength_spec l : Pos.to_nat (plength l) = S (length l).
Proof.
- induction l; simpl; now rewrite ?Pos2Nat.inj_succ, ?IHl.
+ unfold plength. rewrite plength_aux_spec. apply Nat.add_1_r.
Qed.
Lemma treeify_elements l : elements (treeify l) = l.
@@ -1016,7 +1030,9 @@ Proof.
subst l. rewrite plength_spec, app_length, <- elements_cardinal in *.
destruct acc.
* now rewrite app_nil_r.
- * simpl in H. lia.
+ * exfalso. revert H. simpl.
+ rewrite Nat.add_succ_r, Nat.add_comm.
+ apply Nat.succ_add_discr.
Qed.
Lemma treeify_spec x l : InT x (treeify l) <-> InA X.eq x l.
@@ -1531,10 +1547,10 @@ Proof.
simpl maxdepth. simpl redcarac.
rewrite Nat.add_succ_r, <- Nat.succ_le_mono.
now apply Nat.max_lub.
- - simpl. Nat.nzsimpl. rewrite <- Nat.succ_le_mono.
- apply Nat.max_lub; eapply Nat.le_trans; eauto.
- destree l; simpl; lia.
- destree r; simpl; lia.
+ - simpl. rewrite <- Nat.succ_le_mono.
+ apply Nat.max_lub; eapply Nat.le_trans; eauto;
+ [destree l | destree r]; simpl;
+ rewrite !Nat.add_0_r, ?Nat.add_1_r; auto with arith.
Qed.
Lemma rb_mindepth s n : rbt n s -> n + redcarac s <= mindepth s.
@@ -1546,7 +1562,8 @@ Proof.
replace (redcarac l) with 0 in * by now destree l.
replace (redcarac r) with 0 in * by now destree r.
now apply Nat.min_glb.
- - apply -> Nat.succ_le_mono. apply Nat.min_glb; lia.
+ - apply -> Nat.succ_le_mono. rewrite Nat.add_0_r.
+ apply Nat.min_glb; eauto with arith.
Qed.
Lemma maxdepth_upperbound s : Rbt s ->
@@ -1554,8 +1571,14 @@ Lemma maxdepth_upperbound s : Rbt s ->
Proof.
intros (n,H).
eapply Nat.le_trans; [eapply rb_maxdepth; eauto|].
- generalize (rb_mindepth s n H).
- generalize (mindepth_log_cardinal s). lia.
+ transitivity (2*(n+redcarac s)).
+ - rewrite Nat.mul_add_distr_l. apply Nat.add_le_mono_l.
+ rewrite <- Nat.mul_1_l at 1. apply Nat.mul_le_mono_r.
+ auto with arith.
+ - apply Nat.mul_le_mono_l.
+ transitivity (mindepth s).
+ + now apply rb_mindepth.
+ + apply mindepth_log_cardinal.
Qed.
Lemma maxdepth_lowerbound s : s<>Leaf ->
@@ -1792,12 +1815,18 @@ Proof.
unfold treeify_cont.
specialize (Hf acc).
destruct (f acc) as (l, acc1). simpl in *.
- destruct Hf as (Hf1, Hf2). { lia. }
- destruct acc1 as [|x acc2]; simpl in *. { lia. }
- specialize (Hg acc2).
- destruct (g acc2) as (r, acc3). simpl in *.
- destruct Hg as (Hg1, Hg2). { lia. }
- split; [auto | lia].
+ destruct Hf as (Hf1, Hf2). { subst. eauto with arith. }
+ destruct acc1 as [|x acc2]; simpl in *.
+ - exfalso. revert Hacc. apply Nat.lt_nge. rewrite H, <- Hf2.
+ auto with arith.
+ - specialize (Hg acc2).
+ destruct (g acc2) as (r, acc3). simpl in *.
+ destruct Hg as (Hg1, Hg2).
+ { revert Hacc.
+ rewrite H, <- Hf2, Nat.add_succ_r, <- Nat.succ_le_mono.
+ apply Nat.add_le_mono_l. }
+ split; auto.
+ now rewrite H, <- Hf2, <- Hg2, Nat.add_succ_r, Nat.add_assoc.
Qed.
Lemma treeify_aux_rb n :
@@ -1807,12 +1836,17 @@ Proof.
induction n as [n (d,IHn)|n (d,IHn)| ].
- exists (S d). intros b.
eapply treeify_cont_rb; [ apply (IHn false) | apply (IHn b) | ].
- rewrite Pos2Nat.inj_xI. generalize (Pos2Nat.is_pos n).
- destruct b; simpl; lia.
+ rewrite Pos2Nat.inj_xI.
+ assert (H := Pos2Nat.is_pos n). apply Nat.neq_0_lt_0 in H.
+ destruct b; simpl; intros; rewrite Nat.add_0_r; trivial.
+ now rewrite <- Nat.add_succ_r, Nat.succ_pred; trivial.
- exists (S d). intros b.
eapply treeify_cont_rb; [ apply (IHn b) | apply (IHn true) | ].
- rewrite Pos2Nat.inj_xO. generalize (Pos2Nat.is_pos n).
- destruct b; simpl; lia.
+ rewrite Pos2Nat.inj_xO.
+ assert (H := Pos2Nat.is_pos n). apply Nat.neq_0_lt_0 in H.
+ rewrite <- Nat.add_succ_r, Nat.succ_pred by trivial.
+ destruct b; simpl; intros; rewrite Nat.add_0_r; trivial.
+ symmetry. now apply Nat.add_pred_l.
- exists 0; destruct b;
[ apply treeify_zero_rb | apply treeify_one_rb ].
Qed.
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index 76f09c76..fd4114cd 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -396,7 +396,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
induction s; simpl.
intuition; inv.
intros.
- destruct (f a) as [ ]_eqn:E; rewrite ?InA_cons, IHs; intuition.
+ destruct (f a) eqn:E; rewrite ?InA_cons, IHs; intuition.
setoid_replace x with a; auto.
setoid_replace a with x in E; auto. congruence.
Qed.
@@ -420,7 +420,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
unfold For_all; induction s; simpl.
intuition. inv.
intros; inv.
- destruct (f a) as [ ]_eqn:F.
+ destruct (f a) eqn:F.
rewrite IHs; intuition. inv; auto.
setoid_replace x with a; auto.
split; intros H'; try discriminate.
@@ -436,7 +436,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
unfold Exists; induction s; simpl.
split; [discriminate| intros (x & Hx & _); inv].
intros.
- destruct (f a) as [ ]_eqn:F.
+ destruct (f a) eqn:F.
split; auto.
exists a; auto.
rewrite IHs; firstorder.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 12:31:20 +0000