From 884274998a0b7f3daad47ec77a82f295538c3f81 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 Jul 2012 16:56:41 +0000 Subject: MSetRBT : elementary arith proofs instead of calls to lia git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15519 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/MSets/MSetRBT.v | 87 +++++++++++++++++++++++++++++++----------------- 1 file changed, 56 insertions(+), 31 deletions(-) (limited to 'theories/MSets') diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index 35d8245a7..7724e30cf 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 @@ -975,18 +975,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,11 +995,16 @@ 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. @@ -1016,7 +1021,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 +1538,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 +1553,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 +1562,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 +1806,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 +1827,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. -- cgit v1.2.3