diff options
Diffstat (limited to 'theories/NArith/Nsqrt_def.v')
-rw-r--r-- | theories/NArith/Nsqrt_def.v | 48 |
1 files changed, 8 insertions, 40 deletions
diff --git a/theories/NArith/Nsqrt_def.v b/theories/NArith/Nsqrt_def.v index 375ed0f90..edb6b2895 100644 --- a/theories/NArith/Nsqrt_def.v +++ b/theories/NArith/Nsqrt_def.v @@ -6,45 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Definition of a square root function for N. *) +Require Import BinNat. -Require Import BinPos BinNat. +(** Obsolete file, see [BinNat] now, + only compatibility notations remain here. *) -Local Open Scope N_scope. - -Definition Nsqrtrem n := - match n with - | N0 => (N0, N0) - | Npos p => - match Pos.sqrtrem p with - | (s, IsPos r) => (Npos s, Npos r) - | (s, _) => (Npos s, N0) - end - end. - -Definition Nsqrt n := - match n with - | N0 => N0 - | Npos p => Npos (Pos.sqrt p) - end. - -Lemma Nsqrtrem_spec : forall n, - let (s,r) := Nsqrtrem n in n = s*s + r /\ r <= 2*s. -Proof. - destruct n. now split. - generalize (Pos.sqrtrem_spec p). simpl. - destruct 1; simpl; subst; now split. -Qed. - -Lemma Nsqrt_spec : forall n, - let s := Nsqrt n in s*s <= n < (Nsucc s)*(Nsucc s). -Proof. - destruct n. now split. apply (Pos.sqrt_spec p). -Qed. - -Lemma Nsqrtrem_sqrt : forall n, fst (Nsqrtrem n) = Nsqrt n. -Proof. - destruct n. reflexivity. - unfold Nsqrtrem, Nsqrt, Pos.sqrt. - destruct (Pos.sqrtrem p) as (s,r). now destruct r. -Qed.
\ No newline at end of file +Notation Nsqrtrem := N.sqrtrem (only parsing). +Notation Nsqrt := N.sqrt (only parsing). +Notation Nsqrtrem_spec := N.sqrtrem_spec (only parsing). +Notation Nsqrt_spec := (fun n => N.sqrt_spec n (N.le_0_l n)) (only parsing). +Notation Nsqrtrem_sqrt := N.sqrtrem_sqrt (only parsing). |