Commit 9a1a509f authored by Guillaume Melquiond's avatar Guillaume Melquiond

Define and prove a slightly faster version of Zdigits2.

parent 6b980516
......@@ -616,18 +616,6 @@ intros (m, r, s) Hm.
now destruct m as [|[m|m|]|m] ; try (now elim Hm) ; destruct r as [|] ; destruct s as [|].
Qed.
Definition Zdigits2 m :=
match m with Z0 => m | Zpos p => Z_of_nat (S (digits2_Pnat p)) | Zneg p => Z_of_nat (S (digits2_Pnat p)) end.
Theorem Zdigits2_Zdigits :
forall m,
Zdigits2 m = Zdigits radix2 m.
Proof.
unfold Zdigits2.
intros [|m|m] ; try apply Z_of_nat_S_digits2_Pnat.
easy.
Qed.
Definition shr_fexp m e l :=
shr (shr_record_of_loc m l) e (fexp (Zdigits2 m + e) - e).
......
......@@ -1142,4 +1142,37 @@ rewrite <- Zpower_nat_Z.
apply digits2_Pnat_correct.
Qed.
Fixpoint digits2_pos (n : positive) : positive :=
match n with
| xH => xH
| xO p => Psucc (digits2_pos p)
| xI p => Psucc (digits2_pos p)
end.
Theorem Zpos_digits2_pos :
forall m : positive,
Zpos (digits2_pos m) = Zdigits radix2 (Zpos m).
Proof.
intros m.
rewrite <- Z_of_nat_S_digits2_Pnat.
unfold Z.of_nat.
apply f_equal.
induction m ; simpl ; try easy ;
apply f_equal, IHm.
Qed.
Definition Zdigits2 n :=
match n with
| Z0 => n
| Zpos p => Zpos (digits2_pos p)
| Zneg p => Zpos (digits2_pos p)
end.
Lemma Zdigits2_Zdigits :
forall n, Zdigits2 n = Zdigits radix2 n.
Proof.
intros [|p|p] ; try easy ;
apply Zpos_digits2_pos.
Qed.
End Zdigits2.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment