From cf692701443d1ea7f7d2c1b06dea56d6052bd58d Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 6 Aug 2012 14:25:50 +0000 Subject: MSetRBT: a tail-recursive plength git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15685 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/MSets/MSetRBT.v | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) (limited to 'theories/MSets') 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. -- cgit v1.2.3