From 8e5cae9a9f8edbedc2fb2451d32dc18af89cfa40 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 2 Nov 2010 15:10:50 +0000 Subject: NZLog : since spec is complete, no need for morphism axiom log2_wd git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13608 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Integer/Binary/ZBinary.v | 2 -- theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 2 -- theories/Numbers/NatInt/NZLog.v | 12 +++++++++++- theories/Numbers/Natural/Binary/NBinary.v | 1 - theories/Numbers/Natural/Peano/NPeano.v | 1 - theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 2 -- 6 files changed, 11 insertions(+), 9 deletions(-) (limited to 'theories') diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index bdaa748e4..d4796d106 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -159,8 +159,6 @@ Definition sqrt := Zsqrt. (** Log2 *) -Program Instance log2_wd : Proper (eq==>eq) Zlog2. - Definition log2_spec := Zlog2_spec. Definition log2_nonpos := Zlog2_nonpos. Definition log2 := Zlog2. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index 96f243fa6..69feb9315 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -295,8 +295,6 @@ Qed. (** Log2 *) -Program Instance log2_wd : Proper (eq==>eq) log2. - Lemma log2_spec : forall n, 0 2^(log2 n) <= n /\ n < 2^(succ (log2 n)). Proof. diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v index 34c57aad9..4c8dcc8f3 100644 --- a/theories/Numbers/NatInt/NZLog.v +++ b/theories/Numbers/NatInt/NZLog.v @@ -18,7 +18,6 @@ End Log2. Module Type NZLog2Spec (A : NZOrdAxiomsSig')(B : Pow' A)(C : Log2 A). Import A B C. - Declare Instance log2_wd : Proper (eq==>eq) log2. Axiom log2_spec : forall a, 0 2^(log2 a) <= a < 2^(S (log2 a)). Axiom log2_nonpos : forall a, a<=0 -> log2 a == 0. End NZLog2Spec. @@ -74,6 +73,17 @@ Proof. order. Qed. +(** Hence log2 is a morphism. *) + +Instance log2_wd : Proper (eq==>eq) log2. +Proof. + intros x x' Hx. + destruct (le_gt_cases x 0). + rewrite 2 log2_nonpos; trivial. reflexivity. now rewrite <- Hx. + apply log2_unique. apply log2_nonneg. + rewrite Hx in *. now apply log2_spec. +Qed. + (** An alternate specification *) Lemma log2_spec_alt : forall a, 0 exists r, diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index 97e7b3678..34b44d3c6 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -160,7 +160,6 @@ Proof. destruct b; discriminate. Qed. (** Log2 *) -Program Instance log2_wd : Proper (eq==>eq) Nlog2. Definition log2_spec := Nlog2_spec. Definition log2_nonpos := Nlog2_nonpos. diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 3255fda68..6502cfa55 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -444,7 +444,6 @@ Definition pow_succ_r := pow_succ_r. Lemma pow_neg_r : forall a b, b<0 -> a^b = 0. inversion 1. Qed. Definition pow := pow. -Program Instance log2_wd : Proper (eq==>eq) log2. Definition log2_spec := log2_spec. Definition log2_nonpos := log2_nonpos. Definition log2 := log2. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 64dcd1967..3620045d1 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -245,8 +245,6 @@ Qed. (** Log2 *) -Program Instance log2_wd : Proper (eq==>eq) log2. - Lemma log2_spec : forall n, 0 2^(log2 n) <= n /\ n < 2^(succ (log2 n)). Proof. -- cgit v1.2.3