diff options
Diffstat (limited to 'theories/ZArith')
35 files changed, 290 insertions, 434 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index f238ef6e..cb0c6880 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1,14 +1,14 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* 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 *) (************************************************************************) Require Export BinNums BinPos Pnat. -Require Import BinNat Bool Plus Mult Equalities GenericMinMax +Require Import BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties. Require BinIntDef. @@ -73,6 +73,23 @@ Proof. decide equality; apply Pos.eq_dec. Defined. +(** * Proofs of morphisms, obvious since eq is Leibniz *) + +Local Obligation Tactic := simpl_relation. +Program Definition succ_wd : Proper (eq==>eq) succ := _. +Program Definition pred_wd : Proper (eq==>eq) pred := _. +Program Definition opp_wd : Proper (eq==>eq) opp := _. +Program Definition add_wd : Proper (eq==>eq==>eq) add := _. +Program Definition sub_wd : Proper (eq==>eq==>eq) sub := _. +Program Definition mul_wd : Proper (eq==>eq==>eq) mul := _. +Program Definition lt_wd : Proper (eq==>eq==>iff) lt := _. +Program Definition div_wd : Proper (eq==>eq==>eq) div := _. +Program Definition mod_wd : Proper (eq==>eq==>eq) modulo := _. +Program Definition quot_wd : Proper (eq==>eq==>eq) quot := _. +Program Definition rem_wd : Proper (eq==>eq==>eq) rem := _. +Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _. +Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _. + (** * Properties of [pos_sub] *) (** [pos_sub] can be written in term of positive comparison @@ -138,15 +155,23 @@ Qed. Module Import Private_BootStrap. -(** * Properties of addition *) - -(** ** Zero is neutral for addition *) +(** ** Operations and constants *) Lemma add_0_r n : n + 0 = n. Proof. now destruct n. Qed. +Lemma mul_0_r n : n * 0 = 0. +Proof. + now destruct n. +Qed. + +Lemma mul_1_l n : 1 * n = n. +Proof. + now destruct n. +Qed. + (** ** Addition is commutative *) Lemma add_comm n m : n + m = m + n. @@ -196,28 +221,25 @@ Proof. symmetry. now apply Pos.add_sub_assoc. Qed. -Lemma add_assoc n m p : n + (m + p) = n + m + p. +Local Arguments add !x !y. + +Lemma add_assoc_pos p n m : pos p + (n + m) = pos p + n + m. Proof. - assert (AUX : forall x y z, pos x + (y + z) = pos x + y + z). - { intros x [|y|y] [|z|z]; rewrite ?add_0_r; trivial. - - simpl. now rewrite Pos.add_assoc. - - simpl (_ + neg _). symmetry. apply pos_sub_add. - - simpl (neg _ + _); simpl (_ + neg _). - now rewrite (add_comm _ (pos _)), <- 2 pos_sub_add, Pos.add_comm. - - apply opp_inj. rewrite !opp_add_distr. simpl opp. - simpl (neg _ + _); simpl (_ + neg _). - rewrite add_comm, Pos.add_comm. apply pos_sub_add. } - destruct n. - - trivial. - - apply AUX. - - apply opp_inj. rewrite !opp_add_distr. simpl opp. apply AUX. + destruct n as [|n|n], m as [|m|m]; simpl; trivial. + - now rewrite Pos.add_assoc. + - symmetry. apply pos_sub_add. + - symmetry. apply add_0_r. + - now rewrite <- pos_sub_add, add_comm, <- pos_sub_add, Pos.add_comm. + - apply opp_inj. rewrite !opp_add_distr, !pos_sub_opp. + rewrite add_comm, Pos.add_comm. apply pos_sub_add. Qed. -(** ** Subtraction and successor *) - -Lemma sub_succ_l n m : succ n - m = succ (n - m). +Lemma add_assoc n m p : n + (m + p) = n + m + p. Proof. - unfold sub, succ. now rewrite <- 2 add_assoc, (add_comm 1). + destruct n. + - trivial. + - apply add_assoc_pos. + - apply opp_inj. rewrite !opp_add_distr. simpl. apply add_assoc_pos. Qed. (** ** Opposite is inverse for addition *) @@ -227,132 +249,34 @@ Proof. destruct n; simpl; trivial; now rewrite pos_sub_diag. Qed. -Lemma add_opp_diag_l n : - n + n = 0. -Proof. - rewrite add_comm. apply add_opp_diag_r. -Qed. - -(** ** Commutativity of multiplication *) - -Lemma mul_comm n m : n * m = m * n. -Proof. - destruct n, m; simpl; trivial; f_equal; apply Pos.mul_comm. -Qed. - -(** ** Associativity of multiplication *) - -Lemma mul_assoc n m p : n * (m * p) = n * m * p. -Proof. - destruct n, m, p; simpl; trivial; f_equal; apply Pos.mul_assoc. -Qed. - -(** Multiplication and constants *) - -Lemma mul_1_l n : 1 * n = n. -Proof. - now destruct n. -Qed. - -Lemma mul_1_r n : n * 1 = n. -Proof. - destruct n; simpl; now rewrite ?Pos.mul_1_r. -Qed. - (** ** Multiplication and Opposite *) -Lemma mul_opp_l n m : - n * m = - (n * m). -Proof. - now destruct n, m. -Qed. - Lemma mul_opp_r n m : n * - m = - (n * m). Proof. now destruct n, m. Qed. -Lemma mul_opp_opp n m : - n * - m = n * m. -Proof. - now destruct n, m. -Qed. - -Lemma mul_opp_comm n m : - n * m = n * - m. -Proof. - now destruct n, m. -Qed. - (** ** Distributivity of multiplication over addition *) Lemma mul_add_distr_pos (p:positive) n m : - pos p * (n + m) = pos p * n + pos p * m. -Proof. - destruct n as [|n|n], m as [|m|m]; simpl; trivial; - rewrite ?pos_sub_spec, ?Pos.mul_compare_mono_l; try case Pos.compare_spec; - intros; now rewrite ?Pos.mul_add_distr_l, ?Pos.mul_sub_distr_l. -Qed. - -Lemma mul_add_distr_l n m p : n * (m + p) = n * m + n * p. + (n + m) * pos p = n * pos p + m * pos p. Proof. - destruct n as [|n|n]. trivial. - apply mul_add_distr_pos. - change (neg n) with (- pos n). - rewrite !mul_opp_l, <- opp_add_distr. f_equal. - apply mul_add_distr_pos. + destruct n as [|n|n], m as [|m|m]; simpl; trivial. + - now rewrite Pos.mul_add_distr_r. + - rewrite ?pos_sub_spec, ?Pos.mul_compare_mono_r; case Pos.compare_spec; + simpl; trivial; intros; now rewrite Pos.mul_sub_distr_r. + - rewrite ?pos_sub_spec, ?Pos.mul_compare_mono_r; case Pos.compare_spec; + simpl; trivial; intros; now rewrite Pos.mul_sub_distr_r. + - now rewrite Pos.mul_add_distr_r. Qed. Lemma mul_add_distr_r n m p : (n + m) * p = n * p + m * p. Proof. - rewrite !(mul_comm _ p). apply mul_add_distr_l. -Qed. - -(** ** Basic properties of divisibility *) - -Lemma divide_Zpos p q : (pos p|pos q) <-> (p|q)%positive. -Proof. - split. - intros ([ |r|r],H); simpl in *; destr_eq H. exists r; auto. - intros (r,H). exists (pos r); simpl; now f_equal. -Qed. - -Lemma divide_Zpos_Zneg_r n p : (n|pos p) <-> (n|neg p). -Proof. - split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- H. -Qed. - -Lemma divide_Zpos_Zneg_l n p : (pos p|n) <-> (neg p|n). -Proof. - split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- mul_opp_r. -Qed. - -(** ** Conversions between [Z.testbit] and [N.testbit] *) - -Lemma testbit_of_N a n : - testbit (of_N a) (of_N n) = N.testbit a n. -Proof. - destruct a as [|a], n; simpl; trivial. now destruct a. -Qed. - -Lemma testbit_of_N' a n : 0<=n -> - testbit (of_N a) n = N.testbit a (to_N n). -Proof. - intro Hn. rewrite <- testbit_of_N. f_equal. - destruct n; trivial; now destruct Hn. -Qed. - -Lemma testbit_Zpos a n : 0<=n -> - testbit (pos a) n = N.testbit (N.pos a) (to_N n). -Proof. - intro Hn. now rewrite <- testbit_of_N'. -Qed. - -Lemma testbit_Zneg a n : 0<=n -> - testbit (neg a) n = negb (N.testbit (Pos.pred_N a) (to_N n)). -Proof. - intro Hn. - rewrite <- testbit_of_N' by trivial. - destruct n as [ |n|n]; - [ | simpl; now destruct (Pos.pred_N a) | now destruct Hn]. - unfold testbit. - now destruct a as [|[ | | ]| ]. + destruct p as [|p|p]. + - now rewrite !mul_0_r. + - apply mul_add_distr_pos. + - apply opp_inj. rewrite opp_add_distr, <- !mul_opp_r. + apply mul_add_distr_pos. Qed. End Private_BootStrap. @@ -397,6 +321,8 @@ Qed. (** ** Specification of successor and predecessor *) +Local Arguments pos_sub : simpl nomatch. + Lemma succ_pred n : succ (pred n) = n. Proof. unfold succ, pred. now rewrite <- add_assoc, add_opp_diag_r, add_0_r. @@ -511,6 +437,45 @@ Proof. rewrite (compare_antisym n m). case compare_spec; intuition. Qed. +(** ** Induction principles based on successor / predecessor *) + +Lemma peano_ind (P : Z -> Prop) : + P 0 -> + (forall x, P x -> P (succ x)) -> + (forall x, P x -> P (pred x)) -> + forall z, P z. +Proof. + intros H0 Hs Hp z; destruct z. + assumption. + induction p using Pos.peano_ind. + now apply (Hs 0). + rewrite <- Pos.add_1_r. + now apply (Hs (pos p)). + induction p using Pos.peano_ind. + now apply (Hp 0). + rewrite <- Pos.add_1_r. + now apply (Hp (neg p)). +Qed. + +Lemma bi_induction (P : Z -> Prop) : + Proper (eq ==> iff) P -> + P 0 -> + (forall x, P x <-> P (succ x)) -> + forall z, P z. +Proof. + intros _ H0 Hs. induction z using peano_ind. + assumption. + now apply -> Hs. + apply Hs. now rewrite succ_pred. +Qed. + +(** We can now derive all properties of basic functions and orders, + and use these properties for proving the specs of more advanced + functions. *) + +Include ZBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. + + (** ** Specification of absolute value *) Lemma abs_eq n : 0 <= n -> abs n = n. @@ -693,7 +658,7 @@ Lemma div_eucl_eq a b : b<>0 -> Proof. destruct a as [ |a|a], b as [ |b|b]; unfold div_eucl; trivial; (now destruct 1) || intros _; - generalize (pos_div_eucl_eq a (pos b) (eq_refl _)); + generalize (pos_div_eucl_eq a (pos b) Logic.eq_refl); destruct pos_div_eucl as (q,r); rewrite mul_comm. - (* pos pos *) trivial. @@ -756,7 +721,7 @@ Proof. destruct a as [|a|a]; unfold modulo, div_eucl. now split. now apply pos_div_eucl_bound. - generalize (pos_div_eucl_bound a (pos b) (eq_refl _)). + generalize (pos_div_eucl_bound a (pos b) Logic.eq_refl). destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr'). destruct r as [|r|r]; (now destruct Hr) || clear Hr. now split. @@ -773,7 +738,7 @@ Proof. destruct b as [|b|b]; try easy; intros _. destruct a as [|a|a]; unfold modulo, div_eucl. now split. - generalize (pos_div_eucl_bound a (pos b) (eq_refl _)). + generalize (pos_div_eucl_bound a (pos b) Logic.eq_refl). destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr'). destruct r as [|r|r]; (now destruct Hr) || clear Hr. now split. @@ -783,7 +748,7 @@ Proof. change (neg b - neg r <= 0). unfold le, lt in *. rewrite <- compare_sub. simpl in *. now rewrite <- Pos.compare_antisym, Hr'. - generalize (pos_div_eucl_bound a (pos b) (eq_refl _)). + generalize (pos_div_eucl_bound a (pos b) Logic.eq_refl). destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr'). split; destruct r; try easy. red; simpl; now rewrite <- Pos.compare_antisym. @@ -839,6 +804,25 @@ Proof. intros _. apply rem_opp_l'. Qed. Lemma rem_opp_r a b : b<>0 -> rem a (-b) = rem a b. Proof. intros _. apply rem_opp_r'. Qed. +(** ** Extra properties about [divide] *) + +Lemma divide_Zpos p q : (pos p|pos q) <-> (p|q)%positive. +Proof. + split. + intros ([ |r|r],H); simpl in *; destr_eq H. exists r; auto. + intros (r,H). exists (pos r); simpl; now f_equal. +Qed. + +Lemma divide_Zpos_Zneg_r n p : (n|pos p) <-> (n|neg p). +Proof. + split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- H. +Qed. + +Lemma divide_Zpos_Zneg_l n p : (pos p|n) <-> (neg p|n). +Proof. + split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- mul_opp_r. +Qed. + (** ** Correctness proofs for gcd *) Lemma ggcd_gcd a b : fst (ggcd a b) = gcd a b. @@ -898,6 +882,38 @@ Proof. destruct (Pos.ggcd a b) as (g,(aa,bb)); auto. Qed. +(** ** Extra properties about [testbit] *) + +Lemma testbit_of_N a n : + testbit (of_N a) (of_N n) = N.testbit a n. +Proof. + destruct a as [|a], n; simpl; trivial. now destruct a. +Qed. + +Lemma testbit_of_N' a n : 0<=n -> + testbit (of_N a) n = N.testbit a (to_N n). +Proof. + intro Hn. rewrite <- testbit_of_N. f_equal. + destruct n; trivial; now destruct Hn. +Qed. + +Lemma testbit_Zpos a n : 0<=n -> + testbit (pos a) n = N.testbit (N.pos a) (to_N n). +Proof. + intro Hn. now rewrite <- testbit_of_N'. +Qed. + +Lemma testbit_Zneg a n : 0<=n -> + testbit (neg a) n = negb (N.testbit (Pos.pred_N a) (to_N n)). +Proof. + intro Hn. + rewrite <- testbit_of_N' by trivial. + destruct n as [ |n|n]; + [ | simpl; now destruct (Pos.pred_N a) | now destruct Hn]. + unfold testbit. + now destruct a as [|[ | | ]| ]. +Qed. + (** ** Proofs of specifications for bitwise operations *) Lemma div2_spec a : div2 a = shiftr a 1. @@ -959,7 +975,7 @@ Proof. destruct m; easy || now destruct Hm. destruct a as [ |a|a]. (* a = 0 *) - replace (Pos.iter n div2 0) with 0 + replace (Pos.iter div2 0 n) with 0 by (apply Pos.iter_invariant; intros; subst; trivial). now rewrite 2 testbit_0_l. (* a > 0 *) @@ -982,7 +998,7 @@ Proof. rewrite ?Pos.iter_succ; apply testbit_even_0. destruct a as [ |a|a]. (* a = 0 *) - replace (Pos.iter n (mul 2) 0) with 0 + replace (Pos.iter (mul 2) 0 n) with 0 by (apply Pos.iter_invariant; intros; subst; trivial). apply testbit_0_l. (* a > 0 *) @@ -1013,7 +1029,7 @@ Proof. f_equal. now rewrite Pos.add_comm, Pos.add_sub. destruct a; unfold shiftl. (* ... a = 0 *) - replace (Pos.iter n (mul 2) 0) with 0 + replace (Pos.iter (mul 2) 0 n) with 0 by (apply Pos.iter_invariant; intros; subst; trivial). now rewrite 2 testbit_0_l. (* ... a > 0 *) @@ -1103,61 +1119,10 @@ Proof. now rewrite N.lxor_spec, xorb_negb_negb. Qed. -(** ** Induction principles based on successor / predecessor *) -Lemma peano_ind (P : Z -> Prop) : - P 0 -> - (forall x, P x -> P (succ x)) -> - (forall x, P x -> P (pred x)) -> - forall z, P z. -Proof. - intros H0 Hs Hp z; destruct z. - assumption. - induction p using Pos.peano_ind. - now apply (Hs 0). - rewrite <- Pos.add_1_r. - now apply (Hs (pos p)). - induction p using Pos.peano_ind. - now apply (Hp 0). - rewrite <- Pos.add_1_r. - now apply (Hp (neg p)). -Qed. +(** Generic properties of advanced functions. *) -Lemma bi_induction (P : Z -> Prop) : - Proper (eq ==> iff) P -> - P 0 -> - (forall x, P x <-> P (succ x)) -> - forall z, P z. -Proof. - intros _ H0 Hs. induction z using peano_ind. - assumption. - now apply -> Hs. - apply Hs. now rewrite succ_pred. -Qed. - - -(** * Proofs of morphisms, obvious since eq is Leibniz *) - -Local Obligation Tactic := simpl_relation. -Program Definition succ_wd : Proper (eq==>eq) succ := _. -Program Definition pred_wd : Proper (eq==>eq) pred := _. -Program Definition opp_wd : Proper (eq==>eq) opp := _. -Program Definition add_wd : Proper (eq==>eq==>eq) add := _. -Program Definition sub_wd : Proper (eq==>eq==>eq) sub := _. -Program Definition mul_wd : Proper (eq==>eq==>eq) mul := _. -Program Definition lt_wd : Proper (eq==>eq==>iff) lt := _. -Program Definition div_wd : Proper (eq==>eq==>eq) div := _. -Program Definition mod_wd : Proper (eq==>eq==>eq) modulo := _. -Program Definition quot_wd : Proper (eq==>eq==>eq) quot := _. -Program Definition rem_wd : Proper (eq==>eq==>eq) rem := _. -Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _. -Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _. - -(** The Bind Scope prevents Z to stay associated with abstract_scope. - (TODO FIX) *) - -Include ZProp. Bind Scope Z_scope with Z. -Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. +Include ZExtraProp. (** In generic statements, the predicates [lt] and [le] have been favored, whereas [gt] and [ge] don't even exist in the abstract @@ -1277,6 +1242,8 @@ Qed. End Z. +Bind Scope Z_scope with Z.t Z. + (** Re-export Notations *) Infix "+" := Z.add : Z_scope. @@ -1394,11 +1361,11 @@ Lemma inj_gcd p q : Z.pos (Pos.gcd p q) = Z.gcd (Z.pos p) (Z.pos q). Proof. reflexivity. Qed. Definition inj_divide p q : (Z.pos p|Z.pos q) <-> (p|q)%positive. -Proof. apply Z.Private_BootStrap.divide_Zpos. Qed. +Proof. apply Z.divide_Zpos. Qed. Lemma inj_testbit a n : 0<=n -> Z.testbit (Z.pos a) n = N.testbit (N.pos a) (Z.to_N n). -Proof. apply Z.Private_BootStrap.testbit_Zpos. Qed. +Proof. apply Z.testbit_Zpos. Qed. (** Some results concerning Z.neg *) @@ -1436,14 +1403,14 @@ Lemma add_neg_pos p q : Z.neg p + Z.pos q = Z.pos_sub q p. Proof. reflexivity. Qed. Lemma divide_pos_neg_r n p : (n|Z.pos p) <-> (n|Z.neg p). -Proof. apply Z.Private_BootStrap.divide_Zpos_Zneg_r. Qed. +Proof. apply Z.divide_Zpos_Zneg_r. Qed. Lemma divide_pos_neg_l n p : (Z.pos p|n) <-> (Z.neg p|n). -Proof. apply Z.Private_BootStrap.divide_Zpos_Zneg_l. Qed. +Proof. apply Z.divide_Zpos_Zneg_l. Qed. Lemma testbit_neg a n : 0<=n -> Z.testbit (Z.neg a) n = negb (N.testbit (Pos.pred_N a) (Z.to_N n)). -Proof. apply Z.Private_BootStrap.testbit_Zneg. Qed. +Proof. apply Z.testbit_Zneg. Qed. End Pos2Z. diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index 00387eec..9bb86fd5 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* 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 *) @@ -126,7 +126,7 @@ Infix "*" := mul : Z_scope. (** ** Power function *) -Definition pow_pos (z:Z) (n:positive) := Pos.iter n (mul z) 1. +Definition pow_pos (z:Z) := Pos.iter (mul z) 1. Definition pow x y := match y with @@ -306,7 +306,7 @@ Definition to_pos (z:Z) : positive := Definition iter (n:Z) {A} (f:A -> A) (x:A) := match n with - | pos p => Pos.iter p f x + | pos p => Pos.iter f x p | _ => x end. @@ -568,8 +568,8 @@ Definition testbit a n := Definition shiftl a n := match n with | 0 => a - | pos p => Pos.iter p (mul 2) a - | neg p => Pos.iter p div2 a + | pos p => Pos.iter (mul 2) a p + | neg p => Pos.iter div2 a p end. Definition shiftr a n := shiftl a (-n). diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index 5350f86d..09909bdb 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.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 *) @@ -151,9 +151,7 @@ Section Efficient_Rec. forall P:Z -> Prop, (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> 0 <= x -> P x) -> forall x:Z, 0 <= x -> P x. - Proof. - exact Zlt_0_rec. - Qed. + Proof. intros; now apply Zlt_0_rec. Qed. (** Obsolete version of [Z.lt] induction principle on non-negative numbers *) @@ -170,7 +168,7 @@ Section Efficient_Rec. (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> P x) -> forall x:Z, 0 <= x -> P x. Proof. - exact Z_lt_rec. + intros; now apply Z_lt_rec. Qed. (** An even more general induction principle using [Z.lt]. *) @@ -196,7 +194,7 @@ Section Efficient_Rec. (forall x:Z, (forall y:Z, z <= y < x -> P y) -> z <= x -> P x) -> forall x:Z, z <= x -> P x. Proof. - exact Zlt_lower_bound_rec. + intros; now apply Zlt_lower_bound_rec with z. Qed. End Efficient_Rec. diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v index e9cac8e1..04cccd04 100644 --- a/theories/ZArith/ZArith.v +++ b/theories/ZArith/ZArith.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/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v index 0891c60a..4c93173b 100644 --- a/theories/ZArith/ZArith_base.v +++ b/theories/ZArith/ZArith_base.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/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v index e392c8b3..ac69cebd 100644 --- a/theories/ZArith/ZArith_dec.v +++ b/theories/ZArith/ZArith_dec.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/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v deleted file mode 100644 index 9fe3a365..00000000 --- a/theories/ZArith/ZOdiv.v +++ /dev/null @@ -1,88 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Export ZOdiv_def. -Require Import BinInt Zquot. - -Notation ZO_div_mod_eq := Z.quot_rem' (only parsing). -Notation ZOmod_lt := Zrem_lt (only parsing). -Notation ZOmod_sgn := Zrem_sgn (only parsing). -Notation ZOmod_sgn2 := Zrem_sgn2 (only parsing). -Notation ZOmod_lt_pos := Zrem_lt_pos (only parsing). -Notation ZOmod_lt_neg := Zrem_lt_neg (only parsing). -Notation ZOmod_lt_pos_pos := Zrem_lt_pos_pos (only parsing). -Notation ZOmod_lt_pos_neg := Zrem_lt_pos_neg (only parsing). -Notation ZOmod_lt_neg_pos := Zrem_lt_neg_pos (only parsing). -Notation ZOmod_lt_neg_neg := Zrem_lt_neg_neg (only parsing). - -Notation ZOdiv_opp_l := Zquot_opp_l (only parsing). -Notation ZOdiv_opp_r := Zquot_opp_r (only parsing). -Notation ZOmod_opp_l := Zrem_opp_l (only parsing). -Notation ZOmod_opp_r := Zrem_opp_r (only parsing). -Notation ZOdiv_opp_opp := Zquot_opp_opp (only parsing). -Notation ZOmod_opp_opp := Zrem_opp_opp (only parsing). - -Notation Remainder := Remainder (only parsing). -Notation Remainder_alt := Remainder_alt (only parsing). -Notation Remainder_equiv := Remainder_equiv (only parsing). -Notation ZOdiv_mod_unique_full := Zquot_mod_unique_full (only parsing). -Notation ZOdiv_unique_full := Zquot_unique_full (only parsing). -Notation ZOdiv_unique := Zquot_unique (only parsing). -Notation ZOmod_unique_full := Zrem_unique_full (only parsing). -Notation ZOmod_unique := Zrem_unique (only parsing). - -Notation ZOmod_0_l := Zrem_0_l (only parsing). -Notation ZOmod_0_r := Zrem_0_r (only parsing). -Notation ZOdiv_0_l := Zquot_0_l (only parsing). -Notation ZOdiv_0_r := Zquot_0_r (only parsing). -Notation ZOmod_1_r := Zrem_1_r (only parsing). -Notation ZOdiv_1_r := Zquot_1_r (only parsing). -Notation ZOdiv_1_l := Zquot_1_l (only parsing). -Notation ZOmod_1_l := Zrem_1_l (only parsing). -Notation ZO_div_same := Z_quot_same (only parsing). -Notation ZO_mod_same := Z_rem_same (only parsing). -Notation ZO_mod_mult := Z_rem_mult (only parsing). -Notation ZO_div_mult := Z_quot_mult (only parsing). - -Notation ZO_div_pos := Z_quot_pos (only parsing). -Notation ZO_div_lt := Z_quot_lt (only parsing). -Notation ZOdiv_small := Zquot_small (only parsing). -Notation ZOmod_small := Zrem_small (only parsing). -Notation ZO_div_monotone := Z_quot_monotone (only parsing). -Notation ZO_mult_div_le := Z_mult_quot_le (only parsing). -Notation ZO_mult_div_ge := Z_mult_quot_ge (only parsing). -Definition ZO_div_exact_full_1 a b := proj1 (Z_quot_exact_full a b). -Definition ZO_div_exact_full_2 a b := proj2 (Z_quot_exact_full a b). -Notation ZOmod_le := Zrem_le (only parsing). -Notation ZOdiv_le_upper_bound := Zquot_le_upper_bound (only parsing). -Notation ZOdiv_lt_upper_bound := Zquot_lt_upper_bound (only parsing). -Notation ZOdiv_le_lower_bound := Zquot_le_lower_bound (only parsing). -Notation ZOdiv_sgn := Zquot_sgn (only parsing). - -Notation ZO_mod_plus := Z_rem_plus (only parsing). -Notation ZO_div_plus := Z_quot_plus (only parsing). -Notation ZO_div_plus_l := Z_quot_plus_l (only parsing). -Notation ZOdiv_mult_cancel_r := Zquot_mult_cancel_r (only parsing). -Notation ZOdiv_mult_cancel_l := Zquot_mult_cancel_l (only parsing). -Notation ZOmult_mod_distr_l := Zmult_rem_distr_l (only parsing). -Notation ZOmult_mod_distr_r := Zmult_rem_distr_r (only parsing). -Notation ZOmod_mod := Zrem_rem (only parsing). -Notation ZOmult_mod := Zmult_rem (only parsing). -Notation ZOplus_mod := Zplus_rem (only parsing). -Notation ZOplus_mod_idemp_l := Zplus_rem_idemp_l (only parsing). -Notation ZOplus_mod_idemp_r := Zplus_rem_idemp_r (only parsing). -Notation ZOmult_mod_idemp_l := Zmult_rem_idemp_l (only parsing). -Notation ZOmult_mod_idemp_r := Zmult_rem_idemp_r (only parsing). -Notation ZOdiv_ZOdiv := Zquot_Zquot (only parsing). -Notation ZOdiv_mult_le := Zquot_mult_le (only parsing). -Notation ZOmod_divides := Zrem_divides (only parsing). - -Notation ZOdiv_eucl_Zdiv_eucl_pos := Zquotrem_Zdiv_eucl_pos (only parsing). -Notation ZOdiv_Zdiv_pos := Zquot_Zdiv_pos (only parsing). -Notation ZOmod_Zmod_pos := Zrem_Zmod_pos (only parsing). -Notation ZOmod_Zmod_zero := Zrem_Zmod_zero (only parsing). diff --git a/theories/ZArith/ZOdiv_def.v b/theories/ZArith/ZOdiv_def.v deleted file mode 100644 index 8b823d9f..00000000 --- a/theories/ZArith/ZOdiv_def.v +++ /dev/null @@ -1,15 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Import BinInt. - -Notation ZOdiv_eucl := Z.quotrem (only parsing). -Notation ZOdiv := Z.quot (only parsing). -Notation ZOmod := Z.rem (only parsing). - -Notation ZOdiv_eucl_correct := Z.quotrem_eq. diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v index aa3d1188..146009bc 100644 --- a/theories/ZArith/Zabs.v +++ b/theories/ZArith/Zabs.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* 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/ZArith/Zbool.v b/theories/ZArith/Zbool.v index 81e52728..61eb2a34 100644 --- a/theories/ZArith/Zbool.v +++ b/theories/ZArith/Zbool.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/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v index 6aa26d19..d4ac72e9 100644 --- a/theories/ZArith/Zcompare.v +++ b/theories/ZArith/Zcompare.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* 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/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index dceac4f2..9604a06e 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.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 *) @@ -53,17 +53,18 @@ Theorem Z_lt_abs_rec : forall n:Z, P n. Proof. intros P HP p. - set (Q := fun z => 0 <= z -> P z * P (- z)) in *. - cut (Q (Z.abs p)); [ intros | apply (Z_lt_rec Q); auto with zarith ]. - elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith. - unfold Q; clear Q; intros. + set (Q := fun z => 0 <= z -> P z * P (- z)). + enough (H:Q (Z.abs p)) by + (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith). + apply (Z_lt_rec Q); auto with zarith. + subst Q; intros x H. split; apply HP. - rewrite Z.abs_eq; auto; intros. - elim (H (Z.abs m)); intros; auto with zarith. - elim (Zabs_dec m); intro eq; rewrite eq; trivial. - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. - elim (H (Z.abs m)); intros; auto with zarith. - elim (Zabs_dec m); intro eq; rewrite eq; trivial. + - rewrite Z.abs_eq; auto; intros. + destruct (H (Z.abs m)); auto with zarith. + destruct (Zabs_dec m) as [-> | ->]; trivial. + - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. + destruct (H (Z.abs m)); auto with zarith. + destruct (Zabs_dec m) as [-> | ->]; trivial. Qed. Theorem Z_lt_abs_induction : @@ -73,16 +74,17 @@ Theorem Z_lt_abs_induction : Proof. intros P HP p. set (Q := fun z => 0 <= z -> P z /\ P (- z)) in *. - cut (Q (Z.abs p)); [ intros | apply (Z_lt_induction Q); auto with zarith ]. - elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith. - unfold Q; clear Q; intros. + enough (Q (Z.abs p)) by + (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith). + apply (Z_lt_induction Q); auto with zarith. + subst Q; intros. split; apply HP. - rewrite Z.abs_eq; auto; intros. - elim (H (Z.abs m)); intros; auto with zarith. - elim (Zabs_dec m); intro eq; rewrite eq; trivial. - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. - elim (H (Z.abs m)); intros; auto with zarith. - elim (Zabs_dec m); intro eq; rewrite eq; trivial. + - rewrite Z.abs_eq; auto; intros. + elim (H (Z.abs m)); intros; auto with zarith. + elim (Zabs_dec m); intro eq; rewrite eq; trivial. + - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. + destruct (H (Z.abs m)); auto with zarith. + destruct (Zabs_dec m) as [-> | ->]; trivial. Qed. (** To do case analysis over the sign of [z] *) diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v index bf19c8ec..b5d04719 100644 --- a/theories/ZArith/Zdigits.v +++ b/theories/ZArith/Zdigits.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* 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 *) @@ -41,7 +41,7 @@ Section VALUE_OF_BOOLEAN_VECTORS. Lemma binary_value : forall n:nat, Bvector n -> Z. Proof. - simple induction n; intros. + refine (nat_rect _ _ _); intros. exact 0%Z. inversion H0. @@ -152,7 +152,7 @@ Section Z_BRIC_A_BRAC. Lemma binary_value_pos : forall (n:nat) (bv:Bvector n), (binary_value n bv >= 0)%Z. Proof. - induction bv as [| a n v IHbv]; simpl. + induction bv as [| a n v IHbv]; cbn. omega. destruct a; destruct (binary_value n v); simpl; auto. @@ -212,14 +212,11 @@ Section Z_BRIC_A_BRAC. (z < two_power_nat (S n))%Z -> (Z.div2 z < two_power_nat n)%Z. Proof. intros. - cut (2 * Z.div2 z < 2 * two_power_nat n)%Z; intros. - omega. - + enough (2 * Z.div2 z < 2 * two_power_nat n)%Z by omega. rewrite <- two_power_nat_S. - destruct (Zeven.Zeven_odd_dec z); intros. + destruct (Zeven.Zeven_odd_dec z) as [Heven|Hodd]; intros. rewrite <- Zeven.Zeven_div2; auto. - - generalize (Zeven.Zodd_div2 z z0); omega. + generalize (Zeven.Zodd_div2 z Hodd); omega. Qed. Lemma Z_to_two_compl_Sn_z : diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 2e3a2280..d0d10891 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* 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 *) @@ -666,24 +666,22 @@ Theorem Zdiv_eucl_extended : {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < Z.abs b}. Proof. intros b Hb a. - elim (Z_le_gt_dec 0 b); intro Hb'. - cut (b > 0); [ intro Hb'' | omega ]. - rewrite Z.abs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ]. - cut (- b > 0); [ intro Hb'' | omega ]. - elim (Zdiv_eucl_exist Hb'' a); intros qr. - elim qr; intros q r Hqr. - exists (- q, r). - elim Hqr; intros. - split. - rewrite <- Z.mul_opp_comm; assumption. - rewrite Z.abs_neq; [ assumption | omega ]. + destruct (Z_le_gt_dec 0 b) as [Hb'|Hb']. + - assert (Hb'' : b > 0) by omega. + rewrite Z.abs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ]. + - assert (Hb'' : - b > 0) by omega. + destruct (Zdiv_eucl_exist Hb'' a) as ((q,r),[]). + exists (- q, r). + split. + + rewrite <- Z.mul_opp_comm; assumption. + + rewrite Z.abs_neq; [ assumption | omega ]. Qed. Arguments Zdiv_eucl_extended : default implicits. (** * Division and modulo in Z agree with same in nat: *) -Require Import NPeano. +Require Import PeanoNat. Lemma div_Zdiv (n m: nat): m <> O -> Z.of_nat (n / m) = Z.of_nat n / Z.of_nat m. diff --git a/theories/ZArith/Zeuclid.v b/theories/ZArith/Zeuclid.v index 39e846a0..f5cacc7e 100644 --- a/theories/ZArith/Zeuclid.v +++ b/theories/ZArith/Zeuclid.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/ZArith/Zeven.v b/theories/ZArith/Zeven.v index c83a863f..d88bf7a9 100644 --- a/theories/ZArith/Zeven.v +++ b/theories/ZArith/Zeven.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 *) @@ -197,12 +197,14 @@ Qed. Lemma Zquot2_quot n : Z.quot2 n = n ÷ 2. Proof. assert (AUX : forall m, 0 < m -> Z.quot2 m = m ÷ 2). - { intros m Hm. + { + intros m Hm. apply Z.quot_unique with (if Z.odd m then Z.sgn m else 0). now apply Z.lt_le_incl. rewrite Z.sgn_pos by trivial. destruct (Z.odd m); now split. - apply Zquot2_odd_eqn. } + apply Zquot2_odd_eqn. + } destruct (Z.lt_trichotomy 0 n) as [POS|[NUL|NEG]]. - now apply AUX. - now subst. diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v index 1e19479e..14286bde 100644 --- a/theories/ZArith/Zgcd_alt.v +++ b/theories/ZArith/Zgcd_alt.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 *) @@ -23,6 +23,7 @@ Require Import ZArith_base. Require Import ZArithRing. Require Import Zdiv. Require Import Znumtheory. +Require Import Omega. Open Scope Z_scope. @@ -104,8 +105,7 @@ Open Scope Z_scope. Lemma fibonacci_pos : forall n, 0 <= fibonacci n. Proof. - cut (forall N n, (n<N)%nat -> 0<=fibonacci n). - eauto. + enough (forall N n, (n<N)%nat -> 0<=fibonacci n) by eauto. induction N. inversion 1. intros. diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v index 411fec67..1942c2ab 100644 --- a/theories/ZArith/Zhints.v +++ b/theories/ZArith/Zhints.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/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index 59c16469..6e349569 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.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 *) @@ -59,7 +59,7 @@ Section Log_pos. (* Log of positive integers *) Lemma Zlog2_up_log_sup : forall p, Z.log2_up (Zpos p) = log_sup p. Proof. - induction p; simpl. + induction p; simpl log_sup. - change (Zpos p~1) with (2*(Zpos p)+1). rewrite Z.log2_up_succ_double, Zlog2_log_inf; try easy. unfold Z.succ. now rewrite !(Z.add_comm _ 1), Z.add_assoc. diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v index 78091794..c436b3ad 100644 --- a/theories/ZArith/Zmax.v +++ b/theories/ZArith/Zmax.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/ZArith/Zmin.v b/theories/ZArith/Zmin.v index 98282b38..1cfa2e03 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.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/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v index d3376a0e..05a94a8e 100644 --- a/theories/ZArith/Zminmax.v +++ b/theories/ZArith/Zminmax.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/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index 203f9766..b401e6b6 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.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/ZArith/Znat.v b/theories/ZArith/Znat.v index 8031b357..20e7c2e8 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* 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 *) @@ -271,7 +271,7 @@ Qed. Lemma inj_testbit a n : Z.testbit (Z.of_N a) (Z.of_N n) = N.testbit a n. -Proof. apply Z.Private_BootStrap.testbit_of_N. Qed. +Proof. apply Z.testbit_of_N. Qed. End N2Z. @@ -426,7 +426,7 @@ Qed. Lemma inj_testbit a n : 0<=n -> Z.testbit (Z.of_N a) n = N.testbit a (Z.to_N n). -Proof. apply Z.Private_BootStrap.testbit_of_N'. Qed. +Proof. apply Z.testbit_of_N'. Qed. End Z2N. @@ -637,7 +637,7 @@ Qed. (** [Z.of_nat] and usual operations *) -Lemma inj_compare n m : (Z.of_nat n ?= Z.of_nat m) = nat_compare n m. +Lemma inj_compare n m : (Z.of_nat n ?= Z.of_nat m) = (n ?= m)%nat. Proof. now rewrite <-!nat_N_Z, N2Z.inj_compare, <- Nat2N.inj_compare. Qed. @@ -690,23 +690,23 @@ Proof. now rewrite <- !nat_N_Z, Nat2N.inj_sub, N2Z.inj_sub. Qed. -Lemma inj_pred_max n : Z.of_nat (pred n) = Z.max 0 (Z.pred (Z.of_nat n)). +Lemma inj_pred_max n : Z.of_nat (Nat.pred n) = Z.max 0 (Z.pred (Z.of_nat n)). Proof. now rewrite <- !nat_N_Z, Nat2N.inj_pred, N2Z.inj_pred_max. Qed. -Lemma inj_pred n : (0<n)%nat -> Z.of_nat (pred n) = Z.pred (Z.of_nat n). +Lemma inj_pred n : (0<n)%nat -> Z.of_nat (Nat.pred n) = Z.pred (Z.of_nat n). Proof. rewrite nat_compare_lt, Nat2N.inj_compare. intros. now rewrite <- !nat_N_Z, Nat2N.inj_pred, N2Z.inj_pred. Qed. -Lemma inj_min n m : Z.of_nat (min n m) = Z.min (Z.of_nat n) (Z.of_nat m). +Lemma inj_min n m : Z.of_nat (Nat.min n m) = Z.min (Z.of_nat n) (Z.of_nat m). Proof. now rewrite <- !nat_N_Z, Nat2N.inj_min, N2Z.inj_min. Qed. -Lemma inj_max n m : Z.of_nat (max n m) = Z.max (Z.of_nat n) (Z.of_nat m). +Lemma inj_max n m : Z.of_nat (Nat.max n m) = Z.max (Z.of_nat n) (Z.of_nat m). Proof. now rewrite <- !nat_N_Z, Nat2N.inj_max, N2Z.inj_max. Qed. @@ -777,13 +777,13 @@ Proof. intros. now rewrite <- !Z_N_nat, Z2N.inj_sub, N2Nat.inj_sub. Qed. -Lemma inj_pred n : Z.to_nat (Z.pred n) = pred (Z.to_nat n). +Lemma inj_pred n : Z.to_nat (Z.pred n) = Nat.pred (Z.to_nat n). Proof. now rewrite <- !Z_N_nat, Z2N.inj_pred, N2Nat.inj_pred. Qed. Lemma inj_compare n m : 0<=n -> 0<=m -> - nat_compare (Z.to_nat n) (Z.to_nat m) = (n ?= m). + (Z.to_nat n ?= Z.to_nat m)%nat = (n ?= m). Proof. intros Hn Hm. now rewrite <- Nat2Z.inj_compare, !id. Qed. @@ -798,12 +798,12 @@ Proof. intros Hn Hm. unfold Z.lt. now rewrite nat_compare_lt, inj_compare. Qed. -Lemma inj_min n m : Z.to_nat (Z.min n m) = min (Z.to_nat n) (Z.to_nat m). +Lemma inj_min n m : Z.to_nat (Z.min n m) = Nat.min (Z.to_nat n) (Z.to_nat m). Proof. now rewrite <- !Z_N_nat, Z2N.inj_min, N2Nat.inj_min. Qed. -Lemma inj_max n m : Z.to_nat (Z.max n m) = max (Z.to_nat n) (Z.to_nat m). +Lemma inj_max n m : Z.to_nat (Z.max n m) = Nat.max (Z.to_nat n) (Z.to_nat m). Proof. now rewrite <- !Z_N_nat, Z2N.inj_max, N2Nat.inj_max. Qed. @@ -876,13 +876,13 @@ Proof. intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_sub, N2Nat.inj_sub. Qed. -Lemma inj_pred n : 0<n -> Z.abs_nat (Z.pred n) = pred (Z.abs_nat n). +Lemma inj_pred n : 0<n -> Z.abs_nat (Z.pred n) = Nat.pred (Z.abs_nat n). Proof. intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_pred, N2Nat.inj_pred. Qed. Lemma inj_compare n m : 0<=n -> 0<=m -> - nat_compare (Z.abs_nat n) (Z.abs_nat m) = (n ?= m). + (Z.abs_nat n ?= Z.abs_nat m)%nat = (n ?= m). Proof. intros. now rewrite <- !Zabs_N_nat, <- N2Nat.inj_compare, Zabs2N.inj_compare. Qed. @@ -898,13 +898,13 @@ Proof. Qed. Lemma inj_min n m : 0<=n -> 0<=m -> - Z.abs_nat (Z.min n m) = min (Z.abs_nat n) (Z.abs_nat m). + Z.abs_nat (Z.min n m) = Nat.min (Z.abs_nat n) (Z.abs_nat m). Proof. intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_min, N2Nat.inj_min. Qed. Lemma inj_max n m : 0<=n -> 0<=m -> - Z.abs_nat (Z.max n m) = max (Z.abs_nat n) (Z.abs_nat m). + Z.abs_nat (Z.max n m) = Nat.max (Z.abs_nat n) (Z.abs_nat m). Proof. intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_max, N2Nat.inj_max. Qed. diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index 0f58f524..f69cf315 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.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 *) @@ -308,11 +308,11 @@ Section extended_euclid_algorithm. intros v3 Hv3; generalize Hv3; pattern v3. apply Zlt_0_rec. clear v3 Hv3; intros. - elim (Z_zerop x); intro. + destruct (Z_zerop x) as [Heq|Hneq]. apply Euclid_intro with (u := u1) (v := u2) (d := u3). assumption. apply H3. - rewrite a0; auto with zarith. + rewrite Heq; auto with zarith. set (q := u3 / x) in *. assert (Hq : 0 <= u3 - q * x < x). replace (u3 - q * x) with (u3 mod x). @@ -605,11 +605,10 @@ Qed. Lemma prime_rel_prime : forall p:Z, prime p -> forall a:Z, ~ (p | a) -> rel_prime p a. Proof. - simple induction 1; intros. - constructor; intuition. - elim (prime_divisors p H x H3); intuition; subst; auto with zarith. - absurd (p | a); auto with zarith. - absurd (p | a); intuition. + intros; constructor; intros; auto with zarith. + apply prime_divisors in H1; intuition; subst; auto with zarith. + - absurd (p | a); auto with zarith. + - absurd (p | a); intuition. Qed. Hint Resolve prime_rel_prime: zarith. diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 39cf87fa..e090302e 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* 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/ZArith/Zpow_alt.v b/theories/ZArith/Zpow_alt.v index a35dcb68..8f661a9c 100644 --- a/theories/ZArith/Zpow_alt.v +++ b/theories/ZArith/Zpow_alt.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 *) @@ -30,12 +30,12 @@ Infix "^^" := Zpower_alt (at level 30, right associativity) : Z_scope. Lemma Piter_mul_acc : forall f, (forall x y:Z, (f x)*y = f (x*y)) -> - forall p k, Pos.iter p f k = (Pos.iter p f 1)*k. + forall p k, Pos.iter f k p = (Pos.iter f 1 p)*k. Proof. intros f Hf. induction p; simpl; intros. - - set (g := Pos.iter p f 1) in *. now rewrite !IHp, Hf, Z.mul_assoc. - - set (g := Pos.iter p f 1) in *. now rewrite !IHp, Z.mul_assoc. + - set (g := Pos.iter f 1 p) in *. now rewrite !IHp, Hf, Z.mul_assoc. + - set (g := Pos.iter f 1 p) in *. now rewrite !IHp, Z.mul_assoc. - now rewrite Hf, Z.mul_1_l. Qed. diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v index 2fbb70ba..740c45fd 100644 --- a/theories/ZArith/Zpow_def.v +++ b/theories/ZArith/Zpow_def.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/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index 86dfce16..ac41a98f 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.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 *) @@ -152,10 +152,8 @@ Qed. Theorem Zpow_mod_correct a m n : n <> 0 -> Zpow_mod a m n = (a ^ m) mod n. Proof. - intros Hn. destruct m; simpl. - - trivial. + intros Hn. destruct m; simpl; trivial. - apply Zpow_mod_pos_correct; auto with zarith. - - rewrite Z.mod_0_l; auto with zarith. Qed. (* Complements about power and number theory. *) diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index 27f0cfd2..747bd4fd 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.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 *) @@ -25,7 +25,7 @@ Local Open Scope Z_scope. (** [Zpower_nat z n] is the n-th power of [z] when [n] is an unary integer (type [nat]) and [z] a signed integer (type [Z]) *) -Definition Zpower_nat (z:Z) (n:nat) := nat_iter n (Z.mul z) 1. +Definition Zpower_nat (z:Z) := nat_rect _ 1 (fun _ => Z.mul z). Lemma Zpower_nat_0_r z : Zpower_nat z 0 = 1. Proof. reflexivity. Qed. @@ -42,7 +42,7 @@ Lemma Zpower_nat_is_exp : Proof. induction n. - intros. now rewrite Zpower_nat_0_r, Z.mul_1_l. - - intros. simpl. now rewrite 2 Zpower_nat_succ_r, IHn, Z.mul_assoc. + - intros. simpl. now rewrite IHn, Z.mul_assoc. Qed. (** Conversions between powers of unary and binary integers *) @@ -94,12 +94,12 @@ Section Powers_of_2. calculus is possible. [shift n m] computes [2^n * m], i.e. [m] shifted by [n] positions *) - Definition shift_nat (n:nat) (z:positive) := nat_iter n xO z. - Definition shift_pos (n z:positive) := Pos.iter n xO z. + Definition shift_nat (n:nat) (z:positive) := nat_rect _ z (fun _ => xO) n. + Definition shift_pos (n z:positive) := Pos.iter xO z n. Definition shift (n:Z) (z:positive) := match n with | Z0 => z - | Zpos p => Pos.iter p xO z + | Zpos p => Pos.iter xO z p | Zneg p => z end. @@ -154,7 +154,7 @@ Section Powers_of_2. Lemma shift_nat_plus n m x : shift_nat (n + m) x = shift_nat n (shift_nat m x). Proof. - apply iter_nat_plus. + induction n; simpl; now f_equal. Qed. Theorem shift_nat_correct n x : @@ -247,20 +247,20 @@ Section power_div_with_rest. end, 2 * d). Definition Zdiv_rest (x:Z) (p:positive) := - let (qr, d) := Pos.iter p Zdiv_rest_aux (x, 0, 1) in qr. + let (qr, d) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in qr. Lemma Zdiv_rest_correct1 (x:Z) (p:positive) : - let (_, d) := Pos.iter p Zdiv_rest_aux (x, 0, 1) in + let (_, d) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in d = two_power_pos p. Proof. rewrite Pos2Nat.inj_iter, two_power_pos_nat. induction (Pos.to_nat p); simpl; trivial. - destruct (nat_iter n Zdiv_rest_aux (x,0,1)) as ((q,r),d). + destruct (nat_rect _ _ _ _) as ((q,r),d). unfold Zdiv_rest_aux. rewrite two_power_nat_S; now f_equal. Qed. Lemma Zdiv_rest_correct2 (x:Z) (p:positive) : - let '(q,r,d) := Pos.iter p Zdiv_rest_aux (x, 0, 1) in + let '(q,r,d) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in x = q * d + r /\ 0 <= r < d. Proof. apply Pos.iter_invariant; [|omega]. @@ -287,7 +287,7 @@ Section power_div_with_rest. Lemma Zdiv_rest_correct (x:Z) (p:positive) : Zdiv_rest_proofs x p. Proof. generalize (Zdiv_rest_correct1 x p); generalize (Zdiv_rest_correct2 x p). - destruct (Pos.iter p Zdiv_rest_aux (x, 0, 1)) as ((q,r),d). + destruct (Pos.iter Zdiv_rest_aux (x, 0, 1) p) as ((q,r),d). intros (H1,(H2,H3)) ->. now exists q r. Qed. @@ -299,7 +299,7 @@ Section power_div_with_rest. Proof. unfold Zdiv_rest. generalize (Zdiv_rest_correct1 x p); generalize (Zdiv_rest_correct2 x p). - destruct (Pos.iter p Zdiv_rest_aux (x, 0, 1)) as ((q,r),d). + destruct (Pos.iter Zdiv_rest_aux (x, 0, 1) p) as ((q,r),d). intros H ->. now rewrite two_power_pos_equiv in H. Qed. diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index 7f064c2b..3ef11189 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.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/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v index 24f3715e..65959a69 100644 --- a/theories/ZArith/Zsqrt_compat.v +++ b/theories/ZArith/Zsqrt_compat.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 *) @@ -53,7 +53,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p). | xI xH => c_sqrt 3 1 2 _ _ | xO (xO p') => match sqrtrempos p' with - | c_sqrt s' r' Heq Hint => + | c_sqrt _ s' r' Heq Hint => match Z_le_gt_dec (4 * s' + 1) (4 * r') with | left Hle => c_sqrt (Zpos (xO (xO p'))) (2 * s' + 1) @@ -63,7 +63,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p). end | xO (xI p') => match sqrtrempos p' with - | c_sqrt s' r' Heq Hint => + | c_sqrt _ s' r' Heq Hint => match Z_le_gt_dec (4 * s' + 1) (4 * r' + 2) with | left Hle => c_sqrt (Zpos (xO (xI p'))) (2 * s' + 1) @@ -74,7 +74,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p). end | xI (xO p') => match sqrtrempos p' with - | c_sqrt s' r' Heq Hint => + | c_sqrt _ s' r' Heq Hint => match Z_le_gt_dec (4 * s' + 1) (4 * r' + 1) with | left Hle => c_sqrt (Zpos (xI (xO p'))) (2 * s' + 1) @@ -85,7 +85,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p). end | xI (xI p') => match sqrtrempos p' with - | c_sqrt s' r' Heq Hint => + | c_sqrt _ s' r' Heq Hint => match Z_le_gt_dec (4 * s' + 1) (4 * r' + 3) with | left Hle => c_sqrt (Zpos (xI (xI p'))) (2 * s' + 1) @@ -114,7 +114,7 @@ Definition Zsqrt : | Zpos p => fun h => match sqrtrempos p with - | c_sqrt s r Heq Hint => + | c_sqrt _ s r Heq Hint => existT (fun s:Z => {r : Z | @@ -150,7 +150,7 @@ Definition Zsqrt_plain (x:Z) : Z := match x with | Zpos p => match Zsqrt (Zpos p) (Pos2Z.is_nonneg p) with - | existT s _ => s + | existT _ s _ => s end | Zneg p => 0 | Z0 => 0 diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v index 9d2e9cab..cba709e8 100644 --- a/theories/ZArith/Zwf.v +++ b/theories/ZArith/Zwf.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/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v index 929aedc9..25ef852a 100644 --- a/theories/ZArith/auxiliary.v +++ b/theories/ZArith/auxiliary.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* 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/ZArith/vo.itarget b/theories/ZArith/vo.itarget index 88751cc0..178111cd 100644 --- a/theories/ZArith/vo.itarget +++ b/theories/ZArith/vo.itarget @@ -23,8 +23,6 @@ Zmin.vo Zmisc.vo Znat.vo Znumtheory.vo -ZOdiv_def.vo -ZOdiv.vo Zquot.vo Zorder.vo Zpow_def.vo |