diff options
Diffstat (limited to 'theories/Numbers/Integer/SpecViaZ')
-rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSig.v | 74 | ||||
-rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 334 |
2 files changed, 355 insertions, 53 deletions
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v index ff797e32..98ac5dfc 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSig.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,9 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: ZSig.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - -Require Import ZArith Znumtheory. +Require Import BinInt. Open Scope Z_scope. @@ -35,11 +33,14 @@ Module Type ZType. Parameter spec_of_Z: forall x, to_Z (of_Z x) = x. Parameter compare : t -> t -> comparison. - Parameter eq_bool : t -> t -> bool. + Parameter eqb : t -> t -> bool. + Parameter ltb : t -> t -> bool. + Parameter leb : t -> t -> bool. Parameter min : t -> t -> t. Parameter max : t -> t -> t. Parameter zero : t. Parameter one : t. + Parameter two : t. Parameter minus_one : t. Parameter succ : t -> t. Parameter add : t -> t -> t. @@ -48,22 +49,39 @@ Module Type ZType. Parameter opp : t -> t. Parameter mul : t -> t -> t. Parameter square : t -> t. - Parameter power_pos : t -> positive -> t. - Parameter power : t -> N -> t. + Parameter pow_pos : t -> positive -> t. + Parameter pow_N : t -> N -> t. + Parameter pow : t -> t -> t. Parameter sqrt : t -> t. + Parameter log2 : t -> t. Parameter div_eucl : t -> t -> t * t. Parameter div : t -> t -> t. Parameter modulo : t -> t -> t. + Parameter quot : t -> t -> t. + Parameter rem : t -> t -> t. Parameter gcd : t -> t -> t. Parameter sgn : t -> t. Parameter abs : t -> t. + Parameter even : t -> bool. + Parameter odd : t -> bool. + Parameter testbit : t -> t -> bool. + Parameter shiftr : t -> t -> t. + Parameter shiftl : t -> t -> t. + Parameter land : t -> t -> t. + Parameter lor : t -> t -> t. + Parameter ldiff : t -> t -> t. + Parameter lxor : t -> t -> t. + Parameter div2 : t -> t. - Parameter spec_compare: forall x y, compare x y = Zcompare [x] [y]. - Parameter spec_eq_bool: forall x y, eq_bool x y = Zeq_bool [x] [y]. - Parameter spec_min : forall x y, [min x y] = Zmin [x] [y]. - Parameter spec_max : forall x y, [max x y] = Zmax [x] [y]. + Parameter spec_compare: forall x y, compare x y = ([x] ?= [y]). + Parameter spec_eqb : forall x y, eqb x y = ([x] =? [y]). + Parameter spec_ltb : forall x y, ltb x y = ([x] <? [y]). + Parameter spec_leb : forall x y, leb x y = ([x] <=? [y]). + Parameter spec_min : forall x y, [min x y] = Z.min [x] [y]. + Parameter spec_max : forall x y, [max x y] = Z.max [x] [y]. Parameter spec_0: [zero] = 0. Parameter spec_1: [one] = 1. + Parameter spec_2: [two] = 2. Parameter spec_m1: [minus_one] = -1. Parameter spec_succ: forall n, [succ n] = [n] + 1. Parameter spec_add: forall x y, [add x y] = [x] + [y]. @@ -72,17 +90,30 @@ Module Type ZType. Parameter spec_opp: forall x, [opp x] = - [x]. Parameter spec_mul: forall x y, [mul x y] = [x] * [y]. Parameter spec_square: forall x, [square x] = [x] * [x]. - Parameter spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n. - Parameter spec_power: forall x n, [power x n] = [x] ^ Z_of_N n. - Parameter spec_sqrt: forall x, 0 <= [x] -> - [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2. + Parameter spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n. + Parameter spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z.of_N n. + Parameter spec_pow: forall x n, [pow x n] = [x] ^ [n]. + Parameter spec_sqrt: forall x, [sqrt x] = Z.sqrt [x]. + Parameter spec_log2: forall x, [log2 x] = Z.log2 [x]. Parameter spec_div_eucl: forall x y, - let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y]. + let (q,r) := div_eucl x y in ([q], [r]) = Z.div_eucl [x] [y]. Parameter spec_div: forall x y, [div x y] = [x] / [y]. Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y]. - Parameter spec_gcd: forall a b, [gcd a b] = Zgcd (to_Z a) (to_Z b). - Parameter spec_sgn : forall x, [sgn x] = Zsgn [x]. - Parameter spec_abs : forall x, [abs x] = Zabs [x]. + Parameter spec_quot: forall x y, [quot x y] = [x] รท [y]. + Parameter spec_rem: forall x y, [rem x y] = Z.rem [x] [y]. + Parameter spec_gcd: forall a b, [gcd a b] = Z.gcd [a] [b]. + Parameter spec_sgn : forall x, [sgn x] = Z.sgn [x]. + Parameter spec_abs : forall x, [abs x] = Z.abs [x]. + Parameter spec_even : forall x, even x = Z.even [x]. + Parameter spec_odd : forall x, odd x = Z.odd [x]. + Parameter spec_testbit: forall x p, testbit x p = Z.testbit [x] [p]. + Parameter spec_shiftr: forall x p, [shiftr x p] = Z.shiftr [x] [p]. + Parameter spec_shiftl: forall x p, [shiftl x p] = Z.shiftl [x] [p]. + Parameter spec_land: forall x y, [land x y] = Z.land [x] [y]. + Parameter spec_lor: forall x y, [lor x y] = Z.lor [x] [y]. + Parameter spec_ldiff: forall x y, [ldiff x y] = Z.ldiff [x] [y]. + Parameter spec_lxor: forall x y, [lxor x y] = Z.lxor [x] [y]. + Parameter spec_div2: forall x, [div2 x] = Z.div2 [x]. End ZType. @@ -90,12 +121,15 @@ Module Type ZType_Notation (Import Z:ZType). Notation "[ x ]" := (to_Z x). Infix "==" := eq (at level 70). Notation "0" := zero. + Notation "1" := one. + Notation "2" := two. Infix "+" := add. Infix "-" := sub. Infix "*" := mul. + Infix "^" := pow. Notation "- x" := (opp x). Infix "<=" := le. Infix "<" := lt. End ZType_Notation. -Module Type ZType' := ZType <+ ZType_Notation.
\ No newline at end of file +Module Type ZType' := ZType <+ ZType_Notation. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index 879a17dd..bfbc063c 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -1,27 +1,24 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ZSigZAxioms.v 14641 2011-11-06 11:59:10Z herbelin $ i*) +Require Import Bool ZArith OrdersFacts Nnat ZAxioms ZSig. -Require Import ZArith ZAxioms ZDivFloor ZSig. +(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *) -(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] - - It also provides [sgn], [abs], [div], [mod] -*) - - -Module ZTypeIsZAxioms (Import Z : ZType'). +Module ZTypeIsZAxioms (Import ZZ : ZType'). Hint Rewrite - spec_0 spec_1 spec_add spec_sub spec_pred spec_succ - spec_mul spec_opp spec_of_Z spec_div spec_modulo - spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn + spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ + spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_square spec_sqrt + spec_compare spec_eqb spec_ltb spec_leb spec_max spec_min + spec_abs spec_sgn spec_pow spec_log2 spec_even spec_odd spec_gcd + spec_quot spec_rem spec_testbit spec_shiftl spec_shiftr + spec_land spec_lor spec_ldiff spec_lxor spec_div2 : zsimpl. Ltac zsimpl := autorewrite with zsimpl. @@ -44,9 +41,19 @@ Proof. intros. zify. auto with zarith. Qed. +Theorem one_succ : 1 == succ 0. +Proof. +now zify. +Qed. + +Theorem two_succ : 2 == succ 1. +Proof. +now zify. +Qed. + Section Induction. -Variable A : Z.t -> Prop. +Variable A : ZZ.t -> Prop. Hypothesis A_wd : Proper (eq==>iff) A. Hypothesis A0 : A 0. Hypothesis AS : forall n, A n <-> A (succ n). @@ -131,36 +138,66 @@ Qed. (** Order *) -Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). +Lemma eqb_eq x y : eqb x y = true <-> x == y. +Proof. + zify. apply Z.eqb_eq. +Qed. + +Lemma leb_le x y : leb x y = true <-> x <= y. +Proof. + zify. apply Z.leb_le. +Qed. + +Lemma ltb_lt x y : ltb x y = true <-> x < y. Proof. - intros. zify. destruct (Zcompare_spec [x] [y]); auto. + zify. apply Z.ltb_lt. Qed. -Definition eqb := eq_bool. +Lemma compare_eq_iff n m : compare n m = Eq <-> n == m. +Proof. + intros. zify. apply Z.compare_eq_iff. +Qed. + +Lemma compare_lt_iff n m : compare n m = Lt <-> n < m. +Proof. + intros. zify. reflexivity. +Qed. -Lemma eqb_eq : forall x y, eq_bool x y = true <-> x == y. +Lemma compare_le_iff n m : compare n m <> Gt <-> n <= m. Proof. - intros. zify. symmetry. apply Zeq_is_eq_bool. + intros. zify. reflexivity. Qed. +Lemma compare_antisym n m : compare m n = CompOpp (compare n m). +Proof. + intros. zify. apply Z.compare_antisym. +Qed. + +Include BoolOrderFacts ZZ ZZ ZZ [no inline]. + Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare. Proof. -intros x x' Hx y y' Hy. rewrite 2 spec_compare, Hx, Hy; intuition. +intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy. Qed. -Instance lt_wd : Proper (eq ==> eq ==> iff) lt. +Instance eqb_wd : Proper (eq ==> eq ==> Logic.eq) eqb. Proof. -intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition. +intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy. Qed. -Theorem lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m. +Instance ltb_wd : Proper (eq ==> eq ==> Logic.eq) ltb. Proof. -intros. zify. omega. +intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy. Qed. -Theorem lt_irrefl : forall n, ~ n < n. +Instance leb_wd : Proper (eq ==> eq ==> Logic.eq) leb. Proof. -intros. zify. omega. +intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy. +Qed. + +Instance lt_wd : Proper (eq ==> eq ==> iff) lt. +Proof. +intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition. Qed. Theorem lt_succ_r : forall n m, n < (succ m) <-> n <= m. @@ -190,13 +227,15 @@ Qed. (** Part specific to integers, not natural numbers *) -Program Instance opp_wd : Proper (eq ==> eq) opp. - Theorem succ_pred : forall n, succ (pred n) == n. Proof. intros. zify. auto with zarith. Qed. +(** Opp *) + +Program Instance opp_wd : Proper (eq ==> eq) opp. + Theorem opp_0 : - 0 == 0. Proof. intros. zify. auto with zarith. @@ -207,6 +246,8 @@ Proof. intros. zify. auto with zarith. Qed. +(** Abs / Sgn *) + Theorem abs_eq : forall n, 0 <= n -> abs n == n. Proof. intros n. zify. omega with *. @@ -222,16 +263,102 @@ Proof. intros n. zify. omega with *. Qed. -Theorem sgn_pos : forall n, 0<n -> sgn n == succ 0. +Theorem sgn_pos : forall n, 0<n -> sgn n == 1. Proof. intros n. zify. omega with *. Qed. -Theorem sgn_neg : forall n, n<0 -> sgn n == opp (succ 0). +Theorem sgn_neg : forall n, n<0 -> sgn n == opp 1. Proof. intros n. zify. omega with *. Qed. +(** Power *) + +Program Instance pow_wd : Proper (eq==>eq==>eq) pow. + +Lemma pow_0_r : forall a, a^0 == 1. +Proof. + intros. now zify. +Qed. + +Lemma pow_succ_r : forall a b, 0<=b -> a^(succ b) == a * a^b. +Proof. + intros a b. zify. intros. now rewrite Z.add_1_r, Z.pow_succ_r. +Qed. + +Lemma pow_neg_r : forall a b, b<0 -> a^b == 0. +Proof. + intros a b. zify. intros Hb. + destruct [b]; reflexivity || discriminate. +Qed. + +Lemma pow_pow_N : forall a b, 0<=b -> a^b == pow_N a (Z.to_N (to_Z b)). +Proof. + intros a b. zify. intros Hb. now rewrite spec_pow_N, Z2N.id. +Qed. + +Lemma pow_pos_N : forall a p, pow_pos a p == pow_N a (Npos p). +Proof. + intros a b. red. now rewrite spec_pow_N, spec_pow_pos. +Qed. + +(** Square *) + +Lemma square_spec n : square n == n * n. +Proof. + now zify. +Qed. + +(** Sqrt *) + +Lemma sqrt_spec : forall n, 0<=n -> + (sqrt n)*(sqrt n) <= n /\ n < (succ (sqrt n))*(succ (sqrt n)). +Proof. + intros n. zify. apply Z.sqrt_spec. +Qed. + +Lemma sqrt_neg : forall n, n<0 -> sqrt n == 0. +Proof. + intros n. zify. apply Z.sqrt_neg. +Qed. + +(** Log2 *) + +Lemma log2_spec : forall n, 0<n -> + 2^(log2 n) <= n /\ n < 2^(succ (log2 n)). +Proof. + intros n. zify. apply Z.log2_spec. +Qed. + +Lemma log2_nonpos : forall n, n<=0 -> log2 n == 0. +Proof. + intros n. zify. apply Z.log2_nonpos. +Qed. + +(** Even / Odd *) + +Definition Even n := exists m, n == 2*m. +Definition Odd n := exists m, n == 2*m+1. + +Lemma even_spec n : even n = true <-> Even n. +Proof. + unfold Even. zify. rewrite Z.even_spec. + split; intros (m,Hm). + - exists (of_Z m). now zify. + - exists [m]. revert Hm. now zify. +Qed. + +Lemma odd_spec n : odd n = true <-> Odd n. +Proof. + unfold Odd. zify. rewrite Z.odd_spec. + split; intros (m,Hm). + - exists (of_Z m). now zify. + - exists [m]. revert Hm. now zify. +Qed. + +(** Div / Mod *) + Program Instance div_wd : Proper (eq==>eq==>eq) div. Program Instance mod_wd : Proper (eq==>eq==>eq) modulo. @@ -252,8 +379,149 @@ Proof. intros a b. zify. intros. apply Z_mod_neg; auto with zarith. Qed. +Definition mod_bound_pos : + forall a b, 0<=a -> 0<b -> 0 <= modulo a b /\ modulo a b < b := + fun a b _ H => mod_pos_bound a b H. + +(** Quot / Rem *) + +Program Instance quot_wd : Proper (eq==>eq==>eq) quot. +Program Instance rem_wd : Proper (eq==>eq==>eq) rem. + +Theorem quot_rem : forall a b, ~b==0 -> a == b*(quot a b) + rem a b. +Proof. +intros a b. zify. apply Z.quot_rem. +Qed. + +Theorem rem_bound_pos : + forall a b, 0<=a -> 0<b -> 0 <= rem a b /\ rem a b < b. +Proof. +intros a b. zify. apply Z.rem_bound_pos. +Qed. + +Theorem rem_opp_l : forall a b, ~b==0 -> rem (-a) b == -(rem a b). +Proof. +intros a b. zify. apply Z.rem_opp_l. +Qed. + +Theorem rem_opp_r : forall a b, ~b==0 -> rem a (-b) == rem a b. +Proof. +intros a b. zify. apply Z.rem_opp_r. +Qed. + +(** Gcd *) + +Definition divide n m := exists p, m == p*n. +Local Notation "( x | y )" := (divide x y) (at level 0). + +Lemma spec_divide : forall n m, (n|m) <-> Z.divide [n] [m]. +Proof. + intros n m. split. + - intros (p,H). exists [p]. revert H; now zify. + - intros (z,H). exists (of_Z z). now zify. +Qed. + +Lemma gcd_divide_l : forall n m, (gcd n m | n). +Proof. + intros n m. apply spec_divide. zify. apply Z.gcd_divide_l. +Qed. + +Lemma gcd_divide_r : forall n m, (gcd n m | m). +Proof. + intros n m. apply spec_divide. zify. apply Z.gcd_divide_r. +Qed. + +Lemma gcd_greatest : forall n m p, (p|n) -> (p|m) -> (p|gcd n m). +Proof. + intros n m p. rewrite !spec_divide. zify. apply Z.gcd_greatest. +Qed. + +Lemma gcd_nonneg : forall n m, 0 <= gcd n m. +Proof. + intros. zify. apply Z.gcd_nonneg. +Qed. + +(** Bitwise operations *) + +Program Instance testbit_wd : Proper (eq==>eq==>Logic.eq) testbit. + +Lemma testbit_odd_0 : forall a, testbit (2*a+1) 0 = true. +Proof. + intros. zify. apply Z.testbit_odd_0. +Qed. + +Lemma testbit_even_0 : forall a, testbit (2*a) 0 = false. +Proof. + intros. zify. apply Z.testbit_even_0. +Qed. + +Lemma testbit_odd_succ : forall a n, 0<=n -> + testbit (2*a+1) (succ n) = testbit a n. +Proof. + intros a n. zify. apply Z.testbit_odd_succ. +Qed. + +Lemma testbit_even_succ : forall a n, 0<=n -> + testbit (2*a) (succ n) = testbit a n. +Proof. + intros a n. zify. apply Z.testbit_even_succ. +Qed. + +Lemma testbit_neg_r : forall a n, n<0 -> testbit a n = false. +Proof. + intros a n. zify. apply Z.testbit_neg_r. +Qed. + +Lemma shiftr_spec : forall a n m, 0<=m -> + testbit (shiftr a n) m = testbit a (m+n). +Proof. + intros a n m. zify. apply Z.shiftr_spec. +Qed. + +Lemma shiftl_spec_high : forall a n m, 0<=m -> n<=m -> + testbit (shiftl a n) m = testbit a (m-n). +Proof. + intros a n m. zify. intros Hn H. + now apply Z.shiftl_spec_high. +Qed. + +Lemma shiftl_spec_low : forall a n m, m<n -> + testbit (shiftl a n) m = false. +Proof. + intros a n m. zify. intros H. now apply Z.shiftl_spec_low. +Qed. + +Lemma land_spec : forall a b n, + testbit (land a b) n = testbit a n && testbit b n. +Proof. + intros a n m. zify. now apply Z.land_spec. +Qed. + +Lemma lor_spec : forall a b n, + testbit (lor a b) n = testbit a n || testbit b n. +Proof. + intros a n m. zify. now apply Z.lor_spec. +Qed. + +Lemma ldiff_spec : forall a b n, + testbit (ldiff a b) n = testbit a n && negb (testbit b n). +Proof. + intros a n m. zify. now apply Z.ldiff_spec. +Qed. + +Lemma lxor_spec : forall a b n, + testbit (lxor a b) n = xorb (testbit a n) (testbit b n). +Proof. + intros a n m. zify. now apply Z.lxor_spec. +Qed. + +Lemma div2_spec : forall a, div2 a == shiftr a 1. +Proof. + intros a. zify. now apply Z.div2_spec. +Qed. + End ZTypeIsZAxioms. -Module ZType_ZAxioms (Z : ZType) - <: ZAxiomsSig <: ZDivSig <: HasCompare Z <: HasEqBool Z <: HasMinMax Z - := Z <+ ZTypeIsZAxioms. +Module ZType_ZAxioms (ZZ : ZType) + <: ZAxiomsSig <: OrderFunctions ZZ <: HasMinMax ZZ + := ZZ <+ ZTypeIsZAxioms. |