diff options
Diffstat (limited to 'theories/Numbers/Natural')
28 files changed, 169 insertions, 909 deletions
diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v index e2dabf0e..638cfc7e 100644 --- a/theories/Numbers/Natural/Abstract/NAdd.v +++ b/theories/Numbers/Natural/Abstract/NAdd.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Natural/Abstract/NAddOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v index 94dc9e79..144bce72 100644 --- a/theories/Numbers/Natural/Abstract/NAddOrder.v +++ b/theories/Numbers/Natural/Abstract/NAddOrder.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index c783478d..d300f857 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index a2bf4109..40453214 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v index d368cc4e..6f8a8fe5 100644 --- a/theories/Numbers/Natural/Abstract/NBits.v +++ b/theories/Numbers/Natural/Abstract/NBits.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index 882bb850..892b9266 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -133,7 +133,6 @@ Proof. intros m n; unfold ltb at 1. f_equiv. rewrite recursion_succ; f_equiv'. -reflexivity. Qed. (* Above, we rewrite applications of function. Is it possible to rewrite diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v index 90a4e9e8..fb68c139 100644 --- a/theories/Numbers/Natural/Abstract/NDiv.v +++ b/theories/Numbers/Natural/Abstract/NDiv.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Natural/Abstract/NGcd.v b/theories/Numbers/Natural/Abstract/NGcd.v index ff38b364..a1f4ddf8 100644 --- a/theories/Numbers/Natural/Abstract/NGcd.v +++ b/theories/Numbers/Natural/Abstract/NGcd.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v index 00f91311..c296315d 100644 --- a/theories/Numbers/Natural/Abstract/NIso.v +++ b/theories/Numbers/Natural/Abstract/NIso.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Natural/Abstract/NLcm.v b/theories/Numbers/Natural/Abstract/NLcm.v index 6236360b..0fe8e105 100644 --- a/theories/Numbers/Natural/Abstract/NLcm.v +++ b/theories/Numbers/Natural/Abstract/NLcm.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Natural/Abstract/NLog.v b/theories/Numbers/Natural/Abstract/NLog.v index f3418ef8..605c0aad 100644 --- a/theories/Numbers/Natural/Abstract/NLog.v +++ b/theories/Numbers/Natural/Abstract/NLog.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Natural/Abstract/NMaxMin.v b/theories/Numbers/Natural/Abstract/NMaxMin.v index 9fa4114b..e0710561 100644 --- a/theories/Numbers/Natural/Abstract/NMaxMin.v +++ b/theories/Numbers/Natural/Abstract/NMaxMin.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v index 2aaf20ef..c41275d2 100644 --- a/theories/Numbers/Natural/Abstract/NMulOrder.v +++ b/theories/Numbers/Natural/Abstract/NMulOrder.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index a46207ec..90053a73 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Natural/Abstract/NParity.v b/theories/Numbers/Natural/Abstract/NParity.v index 62d71eae..b3526c9a 100644 --- a/theories/Numbers/Natural/Abstract/NParity.v +++ b/theories/Numbers/Natural/Abstract/NParity.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Natural/Abstract/NPow.v b/theories/Numbers/Natural/Abstract/NPow.v index c35757af..9cc23004 100644 --- a/theories/Numbers/Natural/Abstract/NPow.v +++ b/theories/Numbers/Natural/Abstract/NPow.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v index 575ede4f..cb3501d4 100644 --- a/theories/Numbers/Natural/Abstract/NProperties.v +++ b/theories/Numbers/Natural/Abstract/NProperties.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,9 +9,20 @@ Require Export NAxioms. Require Import NMaxMin NParity NPow NSqrt NLog NDiv NGcd NLcm NBits. -(** This functor summarizes all known facts about N. *) +(** The two following functors summarize all known facts about N. -Module Type NProp (N:NAxiomsSig) := - NMaxMinProp N <+ NParityProp N <+ NPowProp N <+ NSqrtProp N - <+ NLog2Prop N <+ NDivProp N <+ NGcdProp N <+ NLcmProp N - <+ NBitsProp N. + - [NBasicProp] provides properties of basic functions: + + - * min max <= < + + - [NExtraProp] provides properties of advanced functions: + pow, sqrt, log2, div, gcd, and bitwise functions. + + If necessary, the earlier all-in-one functor [NProp] + could be re-obtained via [NBasicProp <+ NExtraProp] *) + +Module Type NBasicProp (N:NAxiomsMiniSig) := NMaxMinProp N. + +Module Type NExtraProp (N:NAxiomsSig)(P:NBasicProp N) := + NParityProp N P <+ NPowProp N P <+ NSqrtProp N P + <+ NLog2Prop N P <+ NDivProp N P <+ NGcdProp N P <+ NLcmProp N P + <+ NBitsProp N P. diff --git a/theories/Numbers/Natural/Abstract/NSqrt.v b/theories/Numbers/Natural/Abstract/NSqrt.v index bc989a81..8dc66884 100644 --- a/theories/Numbers/Natural/Abstract/NSqrt.v +++ b/theories/Numbers/Natural/Abstract/NSqrt.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index 7ec44dec..896ffc18 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -13,7 +13,7 @@ and proves its properties *) Require Export NSub. -Ltac f_equiv' := repeat progress (f_equiv; try intros ? ? ?; auto). +Ltac f_equiv' := repeat (repeat f_equiv; try intros ? ? ?; auto). Module NStrongRecProp (Import N : NAxiomsRecSig'). Include NSubProp N. @@ -24,7 +24,7 @@ Variable A : Type. Variable Aeq : relation A. Variable Aeq_equiv : Equivalence Aeq. -(** [strong_rec] allows to define a recursive function [phi] given by +(** [strong_rec] allows defining a recursive function [phi] given by an equation [phi(n) = F(phi)(n)] where recursive calls to [phi] in [F] are made on strictly lower numbers than [n]. @@ -82,7 +82,6 @@ Proof. intros. unfold strong_rec0. f_equiv. rewrite recursion_succ; f_equiv'. -reflexivity. Qed. Lemma strong_rec_0 : forall a, diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v index db61dd9b..18ebe77b 100644 --- a/theories/Numbers/Natural/Abstract/NSub.v +++ b/theories/Numbers/Natural/Abstract/NSub.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 89b65617..f7f4347b 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -28,23 +28,13 @@ Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake Delimit Scope bigN_scope with bigN. -Module BigN <: NType <: OrderedTypeFull <: TotalOrder. - Include NMake.Make Int31Cyclic [scope abstract_scope to bigN_scope]. - Bind Scope bigN_scope with t t'. - Include NTypeIsNAxioms - <+ NProp [no inline] +Module BigN <: NType <: OrderedTypeFull <: TotalOrder := + NMake.Make Int31Cyclic + <+ NTypeIsNAxioms + <+ NBasicProp [no inline] <+ NExtraProp [no inline] <+ HasEqBool2Dec [no inline] <+ MinMaxLogicalProperties [no inline] <+ MinMaxDecProperties [no inline]. -End BigN. - -(** Nota concerning scopes : for the first Include, we cannot bind - the scope bigN_scope to a type that doesn't exists yet. - We hence need to explicitely declare the scope substitution. - For the next Include, the abstract type t (in scope abstract_scope) - gets substituted to concrete BigN.t (in scope bigN_scope), - and the corresponding argument scope are fixed automatically. -*) (** Notations about [BigN] *) diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index d280a04b..bdcdd5ca 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -146,7 +146,7 @@ Module Make (W0:CyclicType) <: NType. Theorem spec_add: forall x y, [add x y] = [x] + [y]. Proof. intros x y. rewrite add_fold. apply spec_same_level; clear x y. - intros n x y. simpl. + intros n x y. cbv beta iota zeta. generalize (ZnZ.spec_add_c x y); case ZnZ.add_c; intros z H. rewrite spec_mk_t. assumption. rewrite spec_mk_t_S. unfold interp_carry in H. @@ -242,8 +242,8 @@ Module Make (W0:CyclicType) <: NType. Definition comparen_m n : forall m, word (dom_t n) (S m) -> dom_t n -> comparison := let op := dom_op n in - let zero := @ZnZ.zero _ op in - let compare := @ZnZ.compare _ op in + let zero := ZnZ.zero (Ops:=op) in + let compare := ZnZ.compare (Ops:=op) in let compare0 := compare zero in fun m => compare_mn_1 (dom_t n) (dom_t n) zero compare compare0 compare (S m). @@ -273,7 +273,7 @@ Module Make (W0:CyclicType) <: NType. Local Notation compare_folded := (iter_sym _ - (fun n => @ZnZ.compare _ (dom_op n)) + (fun n => ZnZ.compare (Ops:=dom_op n)) comparen_m comparenm CompOpp). @@ -358,13 +358,13 @@ Module Make (W0:CyclicType) <: NType. Definition wn_mul n : forall m, word (dom_t n) (S m) -> dom_t n -> t := let op := dom_op n in - let zero := @ZnZ.zero _ op in - let succ := @ZnZ.succ _ op in - let add_c := @ZnZ.add_c _ op in - let mul_c := @ZnZ.mul_c _ op in + let zero := ZnZ.zero in + let succ := ZnZ.succ (Ops:=op) in + let add_c := ZnZ.add_c (Ops:=op) in + let mul_c := ZnZ.mul_c (Ops:=op) in let ww := @ZnZ.WW _ op in let ow := @ZnZ.OW _ op in - let eq0 := @ZnZ.eq0 _ op in + let eq0 := ZnZ.eq0 in let mul_add := @DoubleMul.w_mul_add _ zero succ add_c mul_c in let mul_add_n1 := @DoubleMul.double_mul_add_n1 _ zero ww ow mul_add in fun m x y => @@ -464,18 +464,18 @@ Module Make (W0:CyclicType) <: NType. Definition wn_divn1 n := let op := dom_op n in let zd := ZnZ.zdigits op in - let zero := @ZnZ.zero _ op in - let ww := @ZnZ.WW _ op in - let head0 := @ZnZ.head0 _ op in - let add_mul_div := @ZnZ.add_mul_div _ op in - let div21 := @ZnZ.div21 _ op in - let compare := @ZnZ.compare _ op in - let sub := @ZnZ.sub _ op in + let zero := ZnZ.zero in + let ww := ZnZ.WW in + let head0 := ZnZ.head0 in + let add_mul_div := ZnZ.add_mul_div in + let div21 := ZnZ.div21 in + let compare := ZnZ.compare in + let sub := ZnZ.sub in let ddivn1 := DoubleDivn1.double_divn1 zd zero ww head0 add_mul_div div21 compare sub in fun m x y => let (u,v) := ddivn1 (S m) x y in (mk_t_w' n m u, mk_t n v). - Let div_gtnm n m wx wy := + Definition div_gtnm n m wx wy := let mn := Max.max n m in let d := diff n m in let op := make_op mn in @@ -522,7 +522,7 @@ Module Make (W0:CyclicType) <: NType. case (ZnZ.spec_to_Z y); auto. Qed. - Let spec_divn1 n := + Definition spec_divn1 n := DoubleDivn1.spec_double_divn1 (ZnZ.zdigits (dom_op n)) (ZnZ.zero:dom_t n) ZnZ.WW ZnZ.head0 @@ -633,17 +633,17 @@ Module Make (W0:CyclicType) <: NType. Definition wn_modn1 n := let op := dom_op n in let zd := ZnZ.zdigits op in - let zero := @ZnZ.zero _ op in - let head0 := @ZnZ.head0 _ op in - let add_mul_div := @ZnZ.add_mul_div _ op in - let div21 := @ZnZ.div21 _ op in - let compare := @ZnZ.compare _ op in - let sub := @ZnZ.sub _ op in + let zero := ZnZ.zero in + let head0 := ZnZ.head0 in + let add_mul_div := ZnZ.add_mul_div in + let div21 := ZnZ.div21 in + let compare := ZnZ.compare in + let sub := ZnZ.sub in let dmodn1 := DoubleDivn1.double_modn1 zd zero head0 add_mul_div div21 compare sub in fun m x y => reduce n (dmodn1 (S m) x y). - Let mod_gtnm n m wx wy := + Definition mod_gtnm n m wx wy := let mn := Max.max n m in let d := diff n m in let op := make_op mn in @@ -671,7 +671,7 @@ Module Make (W0:CyclicType) <: NType. reflexivity. Qed. - Let spec_modn1 n := + Definition spec_modn1 n := DoubleDivn1.spec_double_modn1 (ZnZ.zdigits (dom_op n)) (ZnZ.zero:dom_t n) ZnZ.WW ZnZ.head0 @@ -1617,40 +1617,90 @@ Module Make (W0:CyclicType) <: NType. rewrite spec_shiftr, spec_1. apply Z.div2_spec. Qed. - (** TODO : provide efficient versions instead of just converting - from/to N (see with Laurent) *) + Local Notation lorn := (fun n => + let op := dom_op n in + let lor := ZnZ.lor in + fun x y => reduce n (lor x y)). + + Definition lor : t -> t -> t := Eval red_t in same_level lorn. - Definition lor x y := of_N (N.lor (to_N x) (to_N y)). - Definition land x y := of_N (N.land (to_N x) (to_N y)). - Definition ldiff x y := of_N (N.ldiff (to_N x) (to_N y)). - Definition lxor x y := of_N (N.lxor (to_N x) (to_N y)). + Lemma lor_fold : lor = same_level lorn. + Proof. red_t; reflexivity. Qed. - Lemma spec_land: forall x y, [land x y] = Z.land [x] [y]. + Theorem spec_lor x y : [lor x y] = Z.lor [x] [y]. Proof. - intros x y. unfold land. rewrite spec_of_N. unfold to_N. - generalize (spec_pos x), (spec_pos y). - destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2). + rewrite lor_fold. apply spec_same_level; clear x y. + intros n x y. simpl. rewrite spec_reduce. apply ZnZ.spec_lor. Qed. - Lemma spec_lor: forall x y, [lor x y] = Z.lor [x] [y]. + Local Notation landn := (fun n => + let op := dom_op n in + let land := ZnZ.land in + fun x y => reduce n (land x y)). + + Definition land : t -> t -> t := Eval red_t in same_level landn. + + Lemma land_fold : land = same_level landn. + Proof. red_t; reflexivity. Qed. + + Theorem spec_land x y : [land x y] = Z.land [x] [y]. Proof. - intros x y. unfold lor. rewrite spec_of_N. unfold to_N. - generalize (spec_pos x), (spec_pos y). - destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2). + rewrite land_fold. apply spec_same_level; clear x y. + intros n x y. simpl. rewrite spec_reduce. apply ZnZ.spec_land. Qed. - Lemma spec_ldiff: forall x y, [ldiff x y] = Z.ldiff [x] [y]. + Local Notation lxorn := (fun n => + let op := dom_op n in + let lxor := ZnZ.lxor in + fun x y => reduce n (lxor x y)). + + Definition lxor : t -> t -> t := Eval red_t in same_level lxorn. + + Lemma lxor_fold : lxor = same_level lxorn. + Proof. red_t; reflexivity. Qed. + + Theorem spec_lxor x y : [lxor x y] = Z.lxor [x] [y]. Proof. - intros x y. unfold ldiff. rewrite spec_of_N. unfold to_N. - generalize (spec_pos x), (spec_pos y). - destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2). + rewrite lxor_fold. apply spec_same_level; clear x y. + intros n x y. simpl. rewrite spec_reduce. apply ZnZ.spec_lxor. Qed. - Lemma spec_lxor: forall x y, [lxor x y] = Z.lxor [x] [y]. - Proof. - intros x y. unfold lxor. rewrite spec_of_N. unfold to_N. - generalize (spec_pos x), (spec_pos y). - destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2). + Local Notation ldiffn := (fun n => + let op := dom_op n in + let lxor := ZnZ.lxor in + let land := ZnZ.land in + let m1 := ZnZ.minus_one in + fun x y => reduce n (land x (lxor y m1))). + + Definition ldiff : t -> t -> t := Eval red_t in same_level ldiffn. + + Lemma ldiff_fold : ldiff = same_level ldiffn. + Proof. red_t; reflexivity. Qed. + + Lemma ldiff_alt x y p : + 0 <= x < 2^p -> 0 <= y < 2^p -> + Z.ldiff x y = Z.land x (Z.lxor y (2^p - 1)). + Proof. + intros (Hx,Hx') (Hy,Hy'). + destruct p as [|p|p]. + - simpl in *; replace x with 0; replace y with 0; auto with zarith. + - rewrite <- Z.shiftl_1_l. change (_ - 1) with (Z.ones (Z.pos p)). + rewrite <- Z.ldiff_ones_l_low; trivial. + rewrite !Z.ldiff_land, Z.land_assoc. f_equal. + rewrite Z.land_ones; try easy. + symmetry. apply Z.mod_small; now split. + Z.le_elim Hy. + + now apply Z.log2_lt_pow2. + + now subst. + - simpl in *; omega. + Qed. + + Theorem spec_ldiff x y : [ldiff x y] = Z.ldiff [x] [y]. + Proof. + rewrite ldiff_fold. apply spec_same_level; clear x y. + intros n x y. simpl. rewrite spec_reduce. + rewrite ZnZ.spec_land, ZnZ.spec_lxor, ZnZ.spec_m1. + symmetry. apply ldiff_alt; apply ZnZ.spec_to_Z. Qed. End Make. diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 9e4e88c5..6de77e0a 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -138,8 +138,6 @@ pr pr ""; pr " Definition t := t'."; pr ""; - pr " Bind Scope abstract_scope with t t'."; - pr ""; pr " (** * A generic toolbox for building and deconstructing [t] *)"; pr ""; @@ -234,7 +232,7 @@ pr | S n1 => mk_zn2z_ops (nmake_op ww ww_op n1) end. - Let eval n m := ZnZ.to_Z (Ops:=nmake_op _ (dom_op n) m). + Definition eval n m := ZnZ.to_Z (Ops:=nmake_op _ (dom_op n) m). Theorem nmake_op_S: forall ww (w_op: ZnZ.Ops ww) x, nmake_op _ w_op (S x) = mk_zn2z_ops (nmake_op _ w_op x). @@ -326,8 +324,13 @@ pr " Lemma spec_zeron : forall n, ZnZ.to_Z (zeron n) = 0%%Z. Proof. - do_size (destruct n; [exact ZnZ.spec_0|]). - destruct n; auto. simpl. rewrite make_op_S. exact ZnZ.spec_0. + do_size (destruct n; + [match goal with + |- @eq Z (_ (zeron ?n)) _ => + apply (ZnZ.spec_0 (Specs:=dom_spec n)) + end|]). + destruct n; auto. simpl. rewrite make_op_S. fold word. + apply (ZnZ.spec_0 (Specs:=wn_spec (SizePlus 0))). Qed. (** * Digits *) @@ -533,7 +536,7 @@ pr " for i = 0 to size-1 do let pattern = (iter_str (size+1-i) "(S ") ^ "_" ^ (iter_str (size+1-i) ")") in pr -" Let mk_t_%iw m := Eval cbv beta zeta iota delta [ mk_t plus ] in +" Definition mk_t_%iw m := Eval cbv beta zeta iota delta [ mk_t plus ] in match m return word w%i (S m) -> t with | %s as p => mk_t_w %i (S p) | p => mk_t (%i+p) @@ -542,7 +545,7 @@ pr done; pr -" Let mk_t_w' n : forall m, word (dom_t n) (S m) -> t := +" Definition mk_t_w' n : forall m, word (dom_t n) (S m) -> t := match n return (forall m, word (dom_t n) (S m) -> t) with"; for i = 0 to size-1 do pr " | %i => mk_t_%iw" i i done; pr @@ -958,6 +961,11 @@ pr " end."; pr ""; pr " Ltac unfold_red := unfold reduce, %s." (iter_name 1 size "reduce_" ","); +pr ""; +for i = 0 to size do +pr " Declare Equivalent Keys reduce reduce_%i." i; +done; +pr " Declare Equivalent Keys reduce_n reduce_%i." (size + 1); pr " Ltac solve_red := diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v index e545508d..8fe9ea92 100644 --- a/theories/Numbers/Natural/BigN/Nbasic.v +++ b/theories/Numbers/Natural/BigN/Nbasic.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -320,6 +320,7 @@ Section CompareRec. Let double_to_Z_pos: forall n x, 0 <= double_to_Z n x < double_wB n := (spec_double_to_Z wm_base wm_to_Z wm_to_Z_pos). + Declare Equivalent Keys compare0_mn compare0_m. Lemma spec_compare0_mn: forall n x, compare0_mn n x = (0 ?= double_to_Z n x). @@ -371,7 +372,7 @@ Section CompareRec. intros n (H0, H); split; auto. apply Z.lt_le_trans with (1:= H). unfold double_wB, DoubleBase.double_wB; simpl. - rewrite Pshiftl_nat_S, base_xO. + rewrite base_xO. set (u := base (Pos.shiftl_nat wm_base n)). assert (0 < u). unfold u, base; auto with zarith. diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index f95167ad..d54bedd1 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index f438df40..96eb7b35 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,806 +8,8 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -Require Import - Bool Peano Peano_dec Compare_dec Plus Mult Minus Le Lt EqNat Div2 Wf_nat - NAxioms NProperties. +Require Import PeanoNat NAxioms. -(** Functions not already defined *) +(** * [PeanoNat.Nat] already implements [NAxiomSig] *) -Fixpoint leb n m := - match n, m with - | O, _ => true - | _, O => false - | S n', S m' => leb n' m' - end. - -Definition ltb n m := leb (S n) m. - -Infix "<=?" := leb (at level 70) : nat_scope. -Infix "<?" := ltb (at level 70) : nat_scope. - -Lemma leb_le n m : (n <=? m) = true <-> n <= m. -Proof. - revert m. - induction n. split; auto with arith. - destruct m; simpl. now split. - rewrite IHn. split; auto with arith. -Qed. - -Lemma ltb_lt n m : (n <? m) = true <-> n < m. -Proof. - unfold ltb, lt. apply leb_le. -Qed. - -Fixpoint pow n m := - match m with - | O => 1 - | S m => n * (pow n m) - end. - -Infix "^" := pow : nat_scope. - -Lemma pow_0_r : forall a, a^0 = 1. -Proof. reflexivity. Qed. - -Lemma pow_succ_r : forall a b, 0<=b -> a^(S b) = a * a^b. -Proof. reflexivity. Qed. - -Definition square n := n * n. - -Lemma square_spec n : square n = n * n. -Proof. reflexivity. Qed. - -Definition Even n := exists m, n = 2*m. -Definition Odd n := exists m, n = 2*m+1. - -Fixpoint even n := - match n with - | O => true - | 1 => false - | S (S n') => even n' - end. - -Definition odd n := negb (even n). - -Lemma even_spec : forall n, even n = true <-> Even n. -Proof. - fix 1. - destruct n as [|[|n]]; simpl; try rewrite even_spec; split. - now exists 0. - trivial. - discriminate. - intros (m,H). destruct m. discriminate. - simpl in H. rewrite <- plus_n_Sm in H. discriminate. - intros (m,H). exists (S m). rewrite H. simpl. now rewrite plus_n_Sm. - intros (m,H). destruct m. discriminate. exists m. - simpl in H. rewrite <- plus_n_Sm in H. inversion H. reflexivity. -Qed. - -Lemma odd_spec : forall n, odd n = true <-> Odd n. -Proof. - unfold odd. - fix 1. - destruct n as [|[|n]]; simpl; try rewrite odd_spec; split. - discriminate. - intros (m,H). rewrite <- plus_n_Sm in H; discriminate. - now exists 0. - trivial. - intros (m,H). exists (S m). rewrite H. simpl. now rewrite <- (plus_n_Sm m). - intros (m,H). destruct m. discriminate. exists m. - simpl in H. rewrite <- plus_n_Sm in H. inversion H. simpl. - now rewrite <- !plus_n_Sm, <- !plus_n_O. -Qed. - -Lemma Even_equiv : forall n, Even n <-> Even.even n. -Proof. - split. intros (p,->). apply Even.even_mult_l. do 3 constructor. - intros H. destruct (even_2n n H) as (p,->). - exists p. unfold double. simpl. now rewrite <- plus_n_O. -Qed. - -Lemma Odd_equiv : forall n, Odd n <-> Even.odd n. -Proof. - split. intros (p,->). rewrite <- plus_n_Sm, <- plus_n_O. - apply Even.odd_S. apply Even.even_mult_l. do 3 constructor. - intros H. destruct (odd_S2n n H) as (p,->). - exists p. unfold double. simpl. now rewrite <- plus_n_Sm, <- !plus_n_O. -Qed. - -(* A linear, tail-recursive, division for nat. - - In [divmod], [y] is the predecessor of the actual divisor, - and [u] is [y] minus the real remainder -*) - -Fixpoint divmod x y q u := - match x with - | 0 => (q,u) - | S x' => match u with - | 0 => divmod x' y (S q) y - | S u' => divmod x' y q u' - end - end. - -Definition div x y := - match y with - | 0 => y - | S y' => fst (divmod x y' 0 y') - end. - -Definition modulo x y := - match y with - | 0 => y - | S y' => y' - snd (divmod x y' 0 y') - end. - -Infix "/" := div : nat_scope. -Infix "mod" := modulo (at level 40, no associativity) : nat_scope. - -Lemma divmod_spec : forall x y q u, u <= y -> - let (q',u') := divmod x y q u in - x + (S y)*q + (y-u) = (S y)*q' + (y-u') /\ u' <= y. -Proof. - induction x. simpl. intuition. - intros y q u H. destruct u; simpl divmod. - generalize (IHx y (S q) y (le_n y)). destruct divmod as (q',u'). - intros (EQ,LE); split; trivial. - rewrite <- EQ, <- minus_n_O, minus_diag, <- plus_n_O. - now rewrite !plus_Sn_m, plus_n_Sm, <- plus_assoc, mult_n_Sm. - generalize (IHx y q u (le_Sn_le _ _ H)). destruct divmod as (q',u'). - intros (EQ,LE); split; trivial. - rewrite <- EQ. - rewrite !plus_Sn_m, plus_n_Sm. f_equal. now apply minus_Sn_m. -Qed. - -Lemma div_mod : forall x y, y<>0 -> x = y*(x/y) + x mod y. -Proof. - intros x y Hy. - destruct y; [ now elim Hy | clear Hy ]. - unfold div, modulo. - generalize (divmod_spec x y 0 y (le_n y)). - destruct divmod as (q,u). - intros (U,V). - simpl in *. - now rewrite <- mult_n_O, minus_diag, <- !plus_n_O in U. -Qed. - -Lemma mod_bound_pos : forall x y, 0<=x -> 0<y -> 0 <= x mod y < y. -Proof. - intros x y Hx Hy. split. auto with arith. - destruct y; [ now elim Hy | clear Hy ]. - unfold modulo. - apply le_n_S, le_minus. -Qed. - -(** Square root *) - -(** The following square root function is linear (and tail-recursive). - With Peano representation, we can't do better. For faster algorithm, - see Psqrt/Zsqrt/Nsqrt... - - We search the square root of n = k + p^2 + (q - r) - with q = 2p and 0<=r<=q. We start with p=q=r=0, hence - looking for the square root of n = k. Then we progressively - decrease k and r. When k = S k' and r=0, it means we can use (S p) - as new sqrt candidate, since (S k')+p^2+2p = k'+(S p)^2. - When k reaches 0, we have found the biggest p^2 square contained - in n, hence the square root of n is p. -*) - -Fixpoint sqrt_iter k p q r := - match k with - | O => p - | S k' => match r with - | O => sqrt_iter k' (S p) (S (S q)) (S (S q)) - | S r' => sqrt_iter k' p q r' - end - end. - -Definition sqrt n := sqrt_iter n 0 0 0. - -Lemma sqrt_iter_spec : forall k p q r, - q = p+p -> r<=q -> - let s := sqrt_iter k p q r in - s*s <= k + p*p + (q - r) < (S s)*(S s). -Proof. - induction k. - (* k = 0 *) - simpl; intros p q r Hq Hr. - split. - apply le_plus_l. - apply le_lt_n_Sm. - rewrite <- mult_n_Sm. - rewrite plus_assoc, (plus_comm p), <- plus_assoc. - apply plus_le_compat; trivial. - rewrite <- Hq. apply le_minus. - (* k = S k' *) - destruct r. - (* r = 0 *) - intros Hq _. - replace (S k + p*p + (q-0)) with (k + (S p)*(S p) + (S (S q) - S (S q))). - apply IHk. - simpl. rewrite <- plus_n_Sm. congruence. - auto with arith. - rewrite minus_diag, <- minus_n_O, <- plus_n_O. simpl. - rewrite <- plus_n_Sm; f_equal. rewrite <- plus_assoc; f_equal. - rewrite <- mult_n_Sm, (plus_comm p), <- plus_assoc. congruence. - (* r = S r' *) - intros Hq Hr. - replace (S k + p*p + (q-S r)) with (k + p*p + (q - r)). - apply IHk; auto with arith. - simpl. rewrite plus_n_Sm. f_equal. rewrite minus_Sn_m; auto. -Qed. - -Lemma sqrt_spec : forall n, - (sqrt n)*(sqrt n) <= n < S (sqrt n) * S (sqrt n). -Proof. - intros. - set (s:=sqrt n). - replace n with (n + 0*0 + (0-0)). - apply sqrt_iter_spec; auto. - simpl. now rewrite <- 2 plus_n_O. -Qed. - -(** A linear tail-recursive base-2 logarithm - - In [log2_iter], we maintain the logarithm [p] of the counter [q], - while [r] is the distance between [q] and the next power of 2, - more precisely [q + S r = 2^(S p)] and [r<2^p]. At each - recursive call, [q] goes up while [r] goes down. When [r] - is 0, we know that [q] has almost reached a power of 2, - and we increase [p] at the next call, while resetting [r] - to [q]. - - Graphically (numbers are [q], stars are [r]) : - -<< - 10 - 9 - 8 - 7 * - 6 * - 5 ... - 4 - 3 * - 2 * - 1 * * -0 * * * ->> - - We stop when [k], the global downward counter reaches 0. - At that moment, [q] is the number we're considering (since - [k+q] is invariant), and [p] its logarithm. -*) - -Fixpoint log2_iter k p q r := - match k with - | O => p - | S k' => match r with - | O => log2_iter k' (S p) (S q) q - | S r' => log2_iter k' p (S q) r' - end - end. - -Definition log2 n := log2_iter (pred n) 0 1 0. - -Lemma log2_iter_spec : forall k p q r, - 2^(S p) = q + S r -> r < 2^p -> - let s := log2_iter k p q r in - 2^s <= k + q < 2^(S s). -Proof. - induction k. - (* k = 0 *) - intros p q r EQ LT. simpl log2_iter. cbv zeta. - split. - rewrite plus_O_n. - apply plus_le_reg_l with (2^p). - simpl pow in EQ. rewrite <- plus_n_O in EQ. rewrite EQ. - rewrite plus_comm. apply plus_le_compat_r. now apply lt_le_S. - rewrite EQ, plus_comm. apply plus_lt_compat_l. apply lt_0_Sn. - (* k = S k' *) - intros p q r EQ LT. destruct r. - (* r = 0 *) - rewrite <- plus_n_Sm, <- plus_n_O in EQ. - rewrite plus_Sn_m, plus_n_Sm. apply IHk. - rewrite <- EQ. remember (S p) as p'; simpl. now rewrite <- plus_n_O. - unfold lt. now rewrite EQ. - (* r = S r' *) - rewrite plus_Sn_m, plus_n_Sm. apply IHk. - now rewrite plus_Sn_m, plus_n_Sm. - unfold lt. - now apply lt_le_weak. -Qed. - -Lemma log2_spec : forall n, 0<n -> - 2^(log2 n) <= n < 2^(S (log2 n)). -Proof. - intros. - set (s:=log2 n). - replace n with (pred n + 1). - apply log2_iter_spec; auto. - rewrite <- plus_n_Sm, <- plus_n_O. - symmetry. now apply S_pred with 0. -Qed. - -Lemma log2_nonpos : forall n, n<=0 -> log2 n = 0. -Proof. - inversion 1; now subst. -Qed. - -(** * Gcd *) - -(** We use Euclid algorithm, which is normally not structural, - but Coq is now clever enough to accept this (behind modulo - there is a subtraction, which now preserves being a subterm) -*) - -Fixpoint gcd a b := - match a with - | O => b - | S a' => gcd (b mod (S a')) (S a') - end. - -Definition divide x y := exists z, y=z*x. -Notation "( x | y )" := (divide x y) (at level 0) : nat_scope. - -Lemma gcd_divide : forall a b, (gcd a b | a) /\ (gcd a b | b). -Proof. - fix 1. - intros [|a] b; simpl. - split. - now exists 0. - exists 1. simpl. now rewrite <- plus_n_O. - fold (b mod (S a)). - destruct (gcd_divide (b mod (S a)) (S a)) as (H,H'). - set (a':=S a) in *. - split; auto. - rewrite (div_mod b a') at 2 by discriminate. - destruct H as (u,Hu), H' as (v,Hv). - rewrite mult_comm. - exists ((b/a')*v + u). - rewrite mult_plus_distr_r. - now rewrite <- mult_assoc, <- Hv, <- Hu. -Qed. - -Lemma gcd_divide_l : forall a b, (gcd a b | a). -Proof. - intros. apply gcd_divide. -Qed. - -Lemma gcd_divide_r : forall a b, (gcd a b | b). -Proof. - intros. apply gcd_divide. -Qed. - -Lemma gcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|gcd a b). -Proof. - fix 1. - intros [|a] b; simpl; auto. - fold (b mod (S a)). - intros c H H'. apply gcd_greatest; auto. - set (a':=S a) in *. - rewrite (div_mod b a') in H' by discriminate. - destruct H as (u,Hu), H' as (v,Hv). - exists (v - (b/a')*u). - rewrite mult_comm in Hv. - now rewrite mult_minus_distr_r, <- Hv, <-mult_assoc, <-Hu, minus_plus. -Qed. - -(** * Bitwise operations *) - -(** We provide here some bitwise operations for unary numbers. - Some might be really naive, they are just there for fullfiling - the same interface as other for natural representations. As - soon as binary representations such as NArith are available, - it is clearly better to convert to/from them and use their ops. -*) - -Fixpoint testbit a n := - match n with - | O => odd a - | S n => testbit (div2 a) n - end. - -Definition shiftl a n := iter_nat n _ double a. -Definition shiftr a n := iter_nat n _ div2 a. - -Fixpoint bitwise (op:bool->bool->bool) n a b := - match n with - | O => O - | S n' => - (if op (odd a) (odd b) then 1 else 0) + - 2*(bitwise op n' (div2 a) (div2 b)) - end. - -Definition land a b := bitwise andb a a b. -Definition lor a b := bitwise orb (max a b) a b. -Definition ldiff a b := bitwise (fun b b' => b && negb b') a a b. -Definition lxor a b := bitwise xorb (max a b) a b. - -Lemma double_twice : forall n, double n = 2*n. -Proof. - simpl; intros. now rewrite <- plus_n_O. -Qed. - -Lemma testbit_0_l : forall n, testbit 0 n = false. -Proof. - now induction n. -Qed. - -Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true. -Proof. - unfold testbit. rewrite odd_spec. now exists a. -Qed. - -Lemma testbit_even_0 a : testbit (2*a) 0 = false. -Proof. - unfold testbit, odd. rewrite (proj2 (even_spec _)); trivial. - now exists a. -Qed. - -Lemma testbit_odd_succ a n : testbit (2*a+1) (S n) = testbit a n. -Proof. - unfold testbit; fold testbit. - rewrite <- plus_n_Sm, <- plus_n_O. f_equal. - apply div2_double_plus_one. -Qed. - -Lemma testbit_even_succ a n : testbit (2*a) (S n) = testbit a n. -Proof. - unfold testbit; fold testbit. f_equal. apply div2_double. -Qed. - -Lemma shiftr_spec : forall a n m, - testbit (shiftr a n) m = testbit a (m+n). -Proof. - induction n; intros m. trivial. - now rewrite <- plus_n_O. - now rewrite <- plus_n_Sm, <- plus_Sn_m, <- IHn. -Qed. - -Lemma shiftl_spec_high : forall a n m, n<=m -> - testbit (shiftl a n) m = testbit a (m-n). -Proof. - induction n; intros m H. trivial. - now rewrite <- minus_n_O. - destruct m. inversion H. - simpl. apply le_S_n in H. - change (shiftl a (S n)) with (double (shiftl a n)). - rewrite double_twice, div2_double. now apply IHn. -Qed. - -Lemma shiftl_spec_low : forall a n m, m<n -> - testbit (shiftl a n) m = false. -Proof. - induction n; intros m H. inversion H. - change (shiftl a (S n)) with (double (shiftl a n)). - destruct m; simpl. - unfold odd. apply negb_false_iff. - apply even_spec. exists (shiftl a n). apply double_twice. - rewrite double_twice, div2_double. apply IHn. - now apply lt_S_n. -Qed. - -Lemma div2_bitwise : forall op n a b, - div2 (bitwise op (S n) a b) = bitwise op n (div2 a) (div2 b). -Proof. - intros. unfold bitwise; fold bitwise. - destruct (op (odd a) (odd b)). - now rewrite div2_double_plus_one. - now rewrite plus_O_n, div2_double. -Qed. - -Lemma odd_bitwise : forall op n a b, - odd (bitwise op (S n) a b) = op (odd a) (odd b). -Proof. - intros. unfold bitwise; fold bitwise. - destruct (op (odd a) (odd b)). - apply odd_spec. rewrite plus_comm. eexists; eauto. - unfold odd. apply negb_false_iff. apply even_spec. - rewrite plus_O_n; eexists; eauto. -Qed. - -Lemma div2_decr : forall a n, a <= S n -> div2 a <= n. -Proof. - destruct a; intros. apply le_0_n. - apply le_trans with a. - apply lt_n_Sm_le, lt_div2, lt_0_Sn. now apply le_S_n. -Qed. - -Lemma testbit_bitwise_1 : forall op, (forall b, op false b = false) -> - forall n m a b, a<=n -> - testbit (bitwise op n a b) m = op (testbit a m) (testbit b m). -Proof. - intros op Hop. - induction n; intros m a b Ha. - simpl. inversion Ha; subst. now rewrite testbit_0_l. - destruct m. - apply odd_bitwise. - unfold testbit; fold testbit. rewrite div2_bitwise. - apply IHn; now apply div2_decr. -Qed. - -Lemma testbit_bitwise_2 : forall op, op false false = false -> - forall n m a b, a<=n -> b<=n -> - testbit (bitwise op n a b) m = op (testbit a m) (testbit b m). -Proof. - intros op Hop. - induction n; intros m a b Ha Hb. - simpl. inversion Ha; inversion Hb; subst. now rewrite testbit_0_l. - destruct m. - apply odd_bitwise. - unfold testbit; fold testbit. rewrite div2_bitwise. - apply IHn; now apply div2_decr. -Qed. - -Lemma land_spec : forall a b n, - testbit (land a b) n = testbit a n && testbit b n. -Proof. - intros. unfold land. apply testbit_bitwise_1; trivial. -Qed. - -Lemma ldiff_spec : forall a b n, - testbit (ldiff a b) n = testbit a n && negb (testbit b n). -Proof. - intros. unfold ldiff. apply testbit_bitwise_1; trivial. -Qed. - -Lemma lor_spec : forall a b n, - testbit (lor a b) n = testbit a n || testbit b n. -Proof. - intros. unfold lor. apply testbit_bitwise_2. trivial. - destruct (le_ge_dec a b). now rewrite max_r. now rewrite max_l. - destruct (le_ge_dec a b). now rewrite max_r. now rewrite max_l. -Qed. - -Lemma lxor_spec : forall a b n, - testbit (lxor a b) n = xorb (testbit a n) (testbit b n). -Proof. - intros. unfold lxor. apply testbit_bitwise_2. trivial. - destruct (le_ge_dec a b). now rewrite max_r. now rewrite max_l. - destruct (le_ge_dec a b). now rewrite max_r. now rewrite max_l. -Qed. - -(** * Implementation of [NAxiomsSig] by [nat] *) - -Module Nat - <: NAxiomsSig <: UsualDecidableTypeFull <: OrderedTypeFull <: TotalOrder. - -(** Bi-directional induction. *) - -Theorem bi_induction : - forall A : nat -> Prop, Proper (eq==>iff) A -> - A 0 -> (forall n : nat, A n <-> A (S n)) -> forall n : nat, A n. -Proof. -intros A A_wd A0 AS. apply nat_ind. assumption. intros; now apply -> AS. -Qed. - -(** Basic operations. *) - -Definition eq_equiv : Equivalence (@eq nat) := eq_equivalence. -Local Obligation Tactic := simpl_relation. -Program Instance succ_wd : Proper (eq==>eq) S. -Program Instance pred_wd : Proper (eq==>eq) pred. -Program Instance add_wd : Proper (eq==>eq==>eq) plus. -Program Instance sub_wd : Proper (eq==>eq==>eq) minus. -Program Instance mul_wd : Proper (eq==>eq==>eq) mult. - -Theorem pred_succ : forall n : nat, pred (S n) = n. -Proof. -reflexivity. -Qed. - -Theorem one_succ : 1 = S 0. -Proof. -reflexivity. -Qed. - -Theorem two_succ : 2 = S 1. -Proof. -reflexivity. -Qed. - -Theorem add_0_l : forall n : nat, 0 + n = n. -Proof. -reflexivity. -Qed. - -Theorem add_succ_l : forall n m : nat, (S n) + m = S (n + m). -Proof. -reflexivity. -Qed. - -Theorem sub_0_r : forall n : nat, n - 0 = n. -Proof. -intro n; now destruct n. -Qed. - -Theorem sub_succ_r : forall n m : nat, n - (S m) = pred (n - m). -Proof. -induction n; destruct m; simpl; auto. apply sub_0_r. -Qed. - -Theorem mul_0_l : forall n : nat, 0 * n = 0. -Proof. -reflexivity. -Qed. - -Theorem mul_succ_l : forall n m : nat, S n * m = n * m + m. -Proof. -assert (add_S_r : forall n m, n+S m = S(n+m)) by (induction n; auto). -assert (add_comm : forall n m, n+m = m+n). - induction n; simpl; auto. intros; rewrite add_S_r; auto. -intros n m; now rewrite add_comm. -Qed. - -(** Order on natural numbers *) - -Program Instance lt_wd : Proper (eq==>eq==>iff) lt. - -Theorem lt_succ_r : forall n m : nat, n < S m <-> n <= m. -Proof. -unfold lt; split. apply le_S_n. induction 1; auto. -Qed. - - -Theorem lt_eq_cases : forall n m : nat, n <= m <-> n < m \/ n = m. -Proof. -split. -inversion 1; auto. rewrite lt_succ_r; auto. -destruct 1; [|subst; auto]. rewrite <- lt_succ_r; auto. -Qed. - -Theorem lt_irrefl : forall n : nat, ~ (n < n). -Proof. -induction n. intro H; inversion H. rewrite lt_succ_r; auto. -Qed. - -(** Facts specific to natural numbers, not integers. *) - -Theorem pred_0 : pred 0 = 0. -Proof. -reflexivity. -Qed. - -(** Recursion fonction *) - -Definition recursion {A} : A -> (nat -> A -> A) -> nat -> A := - nat_rect (fun _ => A). - -Instance recursion_wd {A} (Aeq : relation A) : - Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) recursion. -Proof. -intros a a' Ha f f' Hf n n' Hn. subst n'. -induction n; simpl; auto. apply Hf; auto. -Qed. - -Theorem recursion_0 : - forall {A} (a : A) (f : nat -> A -> A), recursion a f 0 = a. -Proof. -reflexivity. -Qed. - -Theorem recursion_succ : - forall {A} (Aeq : relation A) (a : A) (f : nat -> A -> A), - Aeq a a -> Proper (eq==>Aeq==>Aeq) f -> - forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)). -Proof. -unfold Proper, respectful in *; induction n; simpl; auto. -Qed. - -(** The instantiation of operations. - Placing them at the very end avoids having indirections in above lemmas. *) - -Definition t := nat. -Definition eq := @eq nat. -Definition eqb := beq_nat. -Definition compare := nat_compare. -Definition zero := 0. -Definition one := 1. -Definition two := 2. -Definition succ := S. -Definition pred := pred. -Definition add := plus. -Definition sub := minus. -Definition mul := mult. -Definition lt := lt. -Definition le := le. -Definition ltb := ltb. -Definition leb := leb. - -Definition min := min. -Definition max := max. -Definition max_l := max_l. -Definition max_r := max_r. -Definition min_l := min_l. -Definition min_r := min_r. - -Definition eqb_eq := beq_nat_true_iff. -Definition compare_spec := nat_compare_spec. -Definition eq_dec := eq_nat_dec. -Definition leb_le := leb_le. -Definition ltb_lt := ltb_lt. - -Definition Even := Even. -Definition Odd := Odd. -Definition even := even. -Definition odd := odd. -Definition even_spec := even_spec. -Definition odd_spec := odd_spec. - -Program Instance pow_wd : Proper (eq==>eq==>eq) pow. -Definition pow_0_r := pow_0_r. -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. - -Definition square := square. -Definition square_spec := square_spec. - -Definition log2_spec := log2_spec. -Definition log2_nonpos := log2_nonpos. -Definition log2 := log2. - -Definition sqrt_spec a (Ha:0<=a) := sqrt_spec a. -Lemma sqrt_neg : forall a, a<0 -> sqrt a = 0. inversion 1. Qed. -Definition sqrt := sqrt. - -Definition div := div. -Definition modulo := modulo. -Program Instance div_wd : Proper (eq==>eq==>eq) div. -Program Instance mod_wd : Proper (eq==>eq==>eq) modulo. -Definition div_mod := div_mod. -Definition mod_bound_pos := mod_bound_pos. - -Definition divide := divide. -Definition gcd := gcd. -Definition gcd_divide_l := gcd_divide_l. -Definition gcd_divide_r := gcd_divide_r. -Definition gcd_greatest := gcd_greatest. -Lemma gcd_nonneg : forall a b, 0<=gcd a b. -Proof. intros. apply le_O_n. Qed. - -Definition testbit := testbit. -Definition shiftl := shiftl. -Definition shiftr := shiftr. -Definition lxor := lxor. -Definition land := land. -Definition lor := lor. -Definition ldiff := ldiff. -Definition div2 := div2. - -Program Instance testbit_wd : Proper (eq==>eq==>Logic.eq) testbit. -Definition testbit_odd_0 := testbit_odd_0. -Definition testbit_even_0 := testbit_even_0. -Definition testbit_odd_succ a n (_:0<=n) := testbit_odd_succ a n. -Definition testbit_even_succ a n (_:0<=n) := testbit_even_succ a n. -Lemma testbit_neg_r a n (H:n<0) : testbit a n = false. -Proof. inversion H. Qed. -Definition shiftl_spec_low := shiftl_spec_low. -Definition shiftl_spec_high a n m (_:0<=m) := shiftl_spec_high a n m. -Definition shiftr_spec a n m (_:0<=m) := shiftr_spec a n m. -Definition lxor_spec := lxor_spec. -Definition land_spec := land_spec. -Definition lor_spec := lor_spec. -Definition ldiff_spec := ldiff_spec. -Definition div2_spec a : div2 a = shiftr a 1 := eq_refl _. - -(** Generic Properties *) - -Include NProp - <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. - -End Nat. - -(** [Nat] contains an [order] tactic for natural numbers *) - -(** Note that [Nat.order] is domain-agnostic: it will not prove - [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *) - -Section TestOrder. - Let test : forall x y, x<=y -> y<=x -> x=y. - Proof. - Nat.order. - Qed. -End TestOrder. +Module Nat <: NAxiomsSig := Nat. diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v index 2b52bffe..1049c156 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSig.v +++ b/theories/Numbers/Natural/SpecViaZ/NSig.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index e22627e8..11569b3f 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |