From 157bee13827f9a616b6c82be4af110c8f2464c64 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 May 2011 15:12:23 +0000 Subject: Modularization of BinNat + fixes of stdlib A sub-module N in BinNat now contains functions add (ex-Nplus), mul (ex-Nmult), ... and properties. In particular, this sub-module N directly instantiates NAxiomsSig and includes all derived properties NProp. Files Ndiv_def and co are now obsolete and kept only for compat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14100 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Natural/Binary/NBinary.v | 227 +----------------------------- 1 file changed, 3 insertions(+), 224 deletions(-) (limited to 'theories/Numbers/Natural') diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index bd59ef494..43ca67dd3 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -8,236 +8,15 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -Require Import BinPos Ndiv_def Nsqrt_def Ngcd_def Ndigits. +Require Import BinPos. Require Export BinNat. Require Import NAxioms NProperties. Local Open Scope N_scope. -(** * Implementation of [NAxiomsSig] module type via [BinNat.N] *) +(** * [BinNat.N] already implements [NAxiomSig] *) -Module Type N - <: NAxiomsMiniSig <: UsualOrderedTypeFull <: TotalOrder <: DecidableTypeFull. - -(** Bi-directional induction. *) - -Theorem bi_induction : - forall A : N -> Prop, Proper (eq==>iff) A -> - A N0 -> (forall n, A n <-> A (Nsucc n)) -> forall n : N, A n. -Proof. -intros A A_wd A0 AS. apply Nrect. assumption. intros; now apply -> AS. -Qed. - -(** Basic operations. *) - -Definition eq_equiv : Equivalence (@eq N) := eq_equivalence. -Local Obligation Tactic := simpl_relation. -Program Instance succ_wd : Proper (eq==>eq) Nsucc. -Program Instance pred_wd : Proper (eq==>eq) Npred. -Program Instance add_wd : Proper (eq==>eq==>eq) Nplus. -Program Instance sub_wd : Proper (eq==>eq==>eq) Nminus. -Program Instance mul_wd : Proper (eq==>eq==>eq) Nmult. - -Definition pred_succ := Npred_succ. -Definition add_0_l := Nplus_0_l. -Definition add_succ_l := Nplus_succ. -Definition sub_0_r := Nminus_0_r. -Definition sub_succ_r := Nminus_succ_r. -Definition mul_0_l := Nmult_0_l. -Definition mul_succ_l n m := eq_trans (Nmult_Sn_m n m) (Nplus_comm _ _). - -Lemma one_succ : 1 = Nsucc 0. -Proof. -reflexivity. -Qed. - -Lemma two_succ : 2 = Nsucc 1. -Proof. -reflexivity. -Qed. - -(** Order *) - -Program Instance lt_wd : Proper (eq==>eq==>iff) Nlt. - -Definition lt_eq_cases := Nle_lteq. -Definition lt_irrefl := Nlt_irrefl. -Definition lt_succ_r := Nlt_succ_r. -Definition eqb_eq := Neqb_eq. - -Definition compare_spec := Ncompare_spec. - -Theorem min_l : forall n m, n <= m -> Nmin n m = n. -Proof. -unfold Nmin, Nle; intros n m H. -destruct (n ?= m); try reflexivity. now elim H. -Qed. - -Theorem min_r : forall n m, m <= n -> Nmin n m = m. -Proof. -unfold Nmin, Nle; intros n m H. -case_eq (n ?= m); intro H1; try reflexivity. -now apply Ncompare_eq_correct. -rewrite <- Ncompare_antisym, H1 in H; elim H; auto. -Qed. - -Theorem max_l : forall n m, m <= n -> Nmax n m = n. -Proof. -unfold Nmax, Nle; intros n m H. -case_eq (n ?= m); intro H1; try reflexivity. -symmetry; now apply Ncompare_eq_correct. -rewrite <- Ncompare_antisym, H1 in H; elim H; auto. -Qed. - -Theorem max_r : forall n m : N, n <= m -> Nmax n m = m. -Proof. -unfold Nmax, Nle; intros n m H. -destruct (n ?= m); try reflexivity. now elim H. -Qed. - -(** Part specific to natural numbers, not integers. *) - -Theorem pred_0 : Npred 0 = 0. -Proof. -reflexivity. -Qed. - -Definition recursion (A : Type) : A -> (N -> A -> A) -> N -> A := - Nrect (fun _ => A). -Implicit Arguments recursion [A]. - -Instance recursion_wd A (Aeq : relation A) : - Proper (Aeq==>(eq==>Aeq==>Aeq)==>eq==>Aeq) (@recursion A). -Proof. -intros a a' Eaa' f f' Eff'. -intro x; pattern x; apply Nrect. -intros x' H; now rewrite <- H. -clear x. -intros x IH x' H; rewrite <- H. -unfold recursion in *. do 2 rewrite Nrect_step. -now apply Eff'; [| apply IH]. -Qed. - -Theorem recursion_0 : - forall (A : Type) (a : A) (f : N -> A -> A), recursion a f N0 = a. -Proof. -intros A a f; unfold recursion; now rewrite Nrect_base. -Qed. - -Theorem recursion_succ : - forall (A : Type) (Aeq : relation A) (a : A) (f : N -> A -> A), - Aeq a a -> Proper (eq==>Aeq==>Aeq) f -> - forall n : N, Aeq (recursion a f (Nsucc n)) (f n (recursion a f n)). -Proof. -unfold recursion; intros A Aeq a f EAaa f_wd n; pattern n; apply Nrect. -rewrite Nrect_step; rewrite Nrect_base; now apply f_wd. -clear n; intro n; do 2 rewrite Nrect_step; intro IH. apply f_wd; [reflexivity|]. -now rewrite Nrect_step. -Qed. - -(** Division and modulo *) - -Program Instance div_wd : Proper (eq==>eq==>eq) Ndiv. -Program Instance mod_wd : Proper (eq==>eq==>eq) Nmod. - -Definition div_mod := fun x y (_:y<>0) => Ndiv_mod_eq x y. -Definition mod_bound_pos : forall a b, 0<=a -> 0 0<= a mod b < b. -Proof. split. now destruct (a mod b). apply Nmod_lt. now destruct b. Qed. - -(** Odd and Even *) - -Definition Even n := exists m, n = 2*m. -Definition Odd n := exists m, n = 2*m+1. -Definition even_spec := Neven_spec. -Definition odd_spec := Nodd_spec. - -(** Power *) - -Program Instance pow_wd : Proper (eq==>eq==>eq) Npow. -Definition pow_0_r := Npow_0_r. -Definition pow_succ_r n p (H:0 <= p) := Npow_succ_r n p. -Lemma pow_neg_r : forall a b, b<0 -> a^b = 0. -Proof. destruct b; discriminate. Qed. - -(** Log2 *) - -Definition log2_spec := Nlog2_spec. -Definition log2_nonpos := Nlog2_nonpos. - -(** Sqrt *) - -Definition sqrt_spec n (H:0<=n) := Nsqrt_spec n. -Lemma sqrt_neg : forall a, a<0 -> Nsqrt a = 0. -Proof. destruct a; discriminate. Qed. - -(** Gcd *) - -Definition gcd_divide_l := Ngcd_divide_l. -Definition gcd_divide_r := Ngcd_divide_r. -Definition gcd_greatest := Ngcd_greatest. -Lemma gcd_nonneg : forall a b, 0 <= Ngcd a b. -Proof. intros. now destruct (Ngcd a b). Qed. - -(** Bitwise Operations *) - -Program Instance testbit_wd : Proper (eq==>eq==>Logic.eq) Ntestbit. -Definition testbit_odd_0 := Ntestbit_odd_0. -Definition testbit_even_0 := Ntestbit_even_0. -Definition testbit_odd_succ a n (_:0<=n) := Ntestbit_odd_succ a n. -Definition testbit_even_succ a n (_:0<=n) := Ntestbit_even_succ a n. -Lemma testbit_neg_r a n (H:n<0) : Ntestbit a n = false. -Proof. now destruct n. Qed. -Definition shiftl_spec_low := Nshiftl_spec_low. -Definition shiftl_spec_high a n m (_:0<=m) := Nshiftl_spec_high a n m. -Definition shiftr_spec a n m (_:0<=m) := Nshiftr_spec a n m. -Definition lxor_spec := Nxor_spec. -Definition land_spec := Nand_spec. -Definition lor_spec := Nor_spec. -Definition ldiff_spec := Ndiff_spec. -Definition div2_spec a : Ndiv2 a = Nshiftr a 1 := eq_refl _. - -(** The instantiation of operations. - Placing them at the very end avoids having indirections in above lemmas. *) - -Definition t := N. -Definition eq := @eq N. -Definition eqb := Neqb. -Definition compare := Ncompare. -Definition eq_dec := N_eq_dec. -Definition zero := 0. -Definition one := 1. -Definition two := 2. -Definition succ := Nsucc. -Definition pred := Npred. -Definition add := Nplus. -Definition sub := Nminus. -Definition mul := Nmult. -Definition lt := Nlt. -Definition le := Nle. -Definition min := Nmin. -Definition max := Nmax. -Definition div := Ndiv. -Definition modulo := Nmod. -Definition pow := Npow. -Definition even := Neven. -Definition odd := Nodd. -Definition sqrt := Nsqrt. -Definition log2 := Nlog2. -Definition divide := Ndivide. -Definition gcd := Ngcd. -Definition testbit := Ntestbit. -Definition shiftl := Nshiftl. -Definition shiftr := Nshiftr. -Definition lxor := Nxor. -Definition land := Nand. -Definition lor := Nor. -Definition ldiff := Ndiff. -Definition div2 := Ndiv2. - -Include NProp - <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. - -End N. +Module N <: NAxiomsSig := N. (* Require Import NDefOps. -- cgit v1.2.3