aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-07-05 16:56:41 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-07-05 16:56:41 +0000
commit884274998a0b7f3daad47ec77a82f295538c3f81 (patch)
treeafb02a678b5891da9355be70bb283278c923c3eb
parentffb64d16132dd80f72ecb619ef87e3eee1fa8bda (diff)
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
-rw-r--r--theories/MSets/MSetRBT.v87
1 files changed, 56 insertions, 31 deletions
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.