diff options
author | Stephane Glondu <steph@glondu.net> | 2012-08-20 18:27:01 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-08-20 18:27:01 +0200 |
commit | e0d682ec25282a348d35c5b169abafec48555690 (patch) | |
tree | 1a46f0142a85df553388c932110793881f3af52f /theories/MSets | |
parent | 86535d84cc3cffeee1dcd8545343f234e7285530 (diff) |
Imported Upstream version 8.4dfsgupstream/8.4dfsg
Diffstat (limited to 'theories/MSets')
-rw-r--r-- | theories/MSets/MSetEqProperties.v | 8 | ||||
-rw-r--r-- | theories/MSets/MSetInterface.v | 2 | ||||
-rw-r--r-- | theories/MSets/MSetList.v | 6 | ||||
-rw-r--r-- | theories/MSets/MSetPositive.v | 4 | ||||
-rw-r--r-- | theories/MSets/MSetProperties.v | 2 | ||||
-rw-r--r-- | theories/MSets/MSetRBT.v | 104 | ||||
-rw-r--r-- | theories/MSets/MSetWeakList.v | 6 |
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. |