MSetRBT: a tail-recursive plength

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15685 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 13 insertions, 4 deletions

diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
index 7724e30cf..b838495f9 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -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 => Pos.succ (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).
 
@@ -1008,9 +1010,16 @@ Proof.
  - 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.