diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-02 15:10:52 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-02 15:10:52 +0000 |
| commit | cce4c64a95e5f835cfd28bb3589c535903cbd011 (patch) | |
| tree | 23d4dfb0f7c2a504c57d5c7be50ba59f5b06768d /theories/Numbers/NatInt | |
| parent | 8e5cae9a9f8edbedc2fb2451d32dc18af89cfa40 (diff) | |
NZSqrt : since spec is complete, no need for morphism axiom sqrt_wd
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13609 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/NatInt')
| -rw-r--r-- | theories/Numbers/NatInt/NZSqrt.v | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v index 276c5e9c6..4cdf322fd 100644 --- a/theories/Numbers/NatInt/NZSqrt.v +++ b/theories/Numbers/NatInt/NZSqrt.v @@ -23,7 +23,6 @@ End SqrtNotation. Module Type Sqrt' (A : Typ) := Sqrt A <+ SqrtNotation A. Module Type NZSqrtSpec (Import A : NZOrdAxiomsSig')(Import B : Sqrt' A). - Declare Instance sqrt_wd : Proper (eq==>eq) sqrt. Axiom sqrt_spec : forall a, 0<=a -> √a * √a <= a < S (√a) * S (√a). Axiom sqrt_neg : forall a, a<0 -> √a == 0. End NZSqrtSpec. @@ -78,6 +77,17 @@ Proof. order. Qed. +(** Hence sqrt is a morphism *) + +Instance sqrt_wd : Proper (eq==>eq) sqrt. +Proof. + intros x x' Hx. + destruct (lt_ge_cases x 0) as [H|H]. + rewrite 2 sqrt_neg; trivial. reflexivity. + now rewrite <- Hx. + apply sqrt_unique. rewrite Hx in *. now apply sqrt_spec. +Qed. + (** An alternate specification *) Lemma sqrt_spec_alt : forall a, 0<=a -> exists r, |