diff options
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/Int.v | 128 | ||||
| -rw-r--r-- | theories/ZArith/ZOdiv.v | 88 | ||||
| -rw-r--r-- | theories/ZArith/ZOdiv_def.v | 15 | ||||
| -rw-r--r-- | theories/ZArith/Zeven.v | 6 | ||||
| -rw-r--r-- | theories/ZArith/vo.itarget | 2 |
5 files changed, 171 insertions, 68 deletions
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index bac50fc4..7c840c56 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -16,28 +16,29 @@ Require Import ZArith. Delimit Scope Int_scope with I. - +Local Open Scope Int_scope. (** * a specification of integers *) Module Type Int. - Open Scope Int_scope. + Parameter t : Set. + Bind Scope Int_scope with t. - Parameter int : Set. + (** For compatibility *) + Definition int := t. - Parameter i2z : int -> Z. - Arguments i2z _%I. + Parameter i2z : t -> Z. - Parameter _0 : int. - Parameter _1 : int. - Parameter _2 : int. - Parameter _3 : int. - Parameter plus : int -> int -> int. - Parameter opp : int -> int. - Parameter minus : int -> int -> int. - Parameter mult : int -> int -> int. - Parameter max : int -> int -> int. + Parameter _0 : t. + Parameter _1 : t. + Parameter _2 : t. + Parameter _3 : t. + Parameter plus : t -> t -> t. + Parameter opp : t -> t. + Parameter minus : t -> t -> t. + Parameter mult : t -> t -> t. + Parameter max : t -> t -> t. Notation "0" := _0 : Int_scope. Notation "1" := _1 : Int_scope. @@ -54,10 +55,10 @@ Module Type Int. Notation "x == y" := (i2z x = i2z y) (at level 70, y at next level, no associativity) : Int_scope. - Notation "x <= y" := (Zle (i2z x) (i2z y)): Int_scope. - Notation "x < y" := (Zlt (i2z x) (i2z y)) : Int_scope. - Notation "x >= y" := (Zge (i2z x) (i2z y)) : Int_scope. - Notation "x > y" := (Zgt (i2z x) (i2z y)): Int_scope. + Notation "x <= y" := (i2z x <= i2z y)%Z : Int_scope. + Notation "x < y" := (i2z x < i2z y)%Z : Int_scope. + Notation "x >= y" := (i2z x >= i2z y)%Z : Int_scope. + Notation "x > y" := (i2z x > i2z y)%Z : Int_scope. Notation "x <= y <= z" := (x <= y /\ y <= z) : Int_scope. Notation "x <= y < z" := (x <= y /\ y < z) : Int_scope. Notation "x < y < z" := (x < y /\ y < z) : Int_scope. @@ -65,41 +66,39 @@ Module Type Int. (** Some decidability fonctions (informative). *) - Axiom gt_le_dec : forall x y: int, {x > y} + {x <= y}. - Axiom ge_lt_dec : forall x y : int, {x >= y} + {x < y}. - Axiom eq_dec : forall x y : int, { x == y } + {~ x==y }. + Axiom gt_le_dec : forall x y : t, {x > y} + {x <= y}. + Axiom ge_lt_dec : forall x y : t, {x >= y} + {x < y}. + Axiom eq_dec : forall x y : t, { x == y } + {~ x==y }. (** Specifications *) (** First, we ask [i2z] to be injective. Said otherwise, our ad-hoc equality [==] and the generic [=] are in fact equivalent. We define [==] - nonetheless since the translation to [Z] for using automatic tactic is easier. *) + nonetheless since the translation to [Z] for using automatic tactic + is easier. *) - Axiom i2z_eq : forall n p : int, n == p -> n = p. + Axiom i2z_eq : forall n p : t, n == p -> n = p. (** Then, we express the specifications of the above parameters using their Z counterparts. *) - Open Scope Z_scope. - Axiom i2z_0 : i2z _0 = 0. - Axiom i2z_1 : i2z _1 = 1. - Axiom i2z_2 : i2z _2 = 2. - Axiom i2z_3 : i2z _3 = 3. - Axiom i2z_plus : forall n p, i2z (n + p) = i2z n + i2z p. - Axiom i2z_opp : forall n, i2z (-n) = -i2z n. - Axiom i2z_minus : forall n p, i2z (n - p) = i2z n - i2z p. - Axiom i2z_mult : forall n p, i2z (n * p) = i2z n * i2z p. - Axiom i2z_max : forall n p, i2z (max n p) = Zmax (i2z n) (i2z p). + Axiom i2z_0 : i2z _0 = 0%Z. + Axiom i2z_1 : i2z _1 = 1%Z. + Axiom i2z_2 : i2z _2 = 2%Z. + Axiom i2z_3 : i2z _3 = 3%Z. + Axiom i2z_plus : forall n p, i2z (n + p) = (i2z n + i2z p)%Z. + Axiom i2z_opp : forall n, i2z (-n) = (-i2z n)%Z. + Axiom i2z_minus : forall n p, i2z (n - p) = (i2z n - i2z p)%Z. + Axiom i2z_mult : forall n p, i2z (n * p) = (i2z n * i2z p)%Z. + Axiom i2z_max : forall n p, i2z (max n p) = Z.max (i2z n) (i2z p). End Int. (** * Facts and tactics using [Int] *) -Module MoreInt (I:Int). - Import I. - - Open Scope Int_scope. +Module MoreInt (Import I:Int). + Local Notation int := I.t. (** A magic (but costly) tactic that goes from [int] back to the [Z] friendly world ... *) @@ -108,13 +107,14 @@ Module MoreInt (I:Int). i2z_0 i2z_1 i2z_2 i2z_3 i2z_plus i2z_opp i2z_minus i2z_mult i2z_max : i2z. Ltac i2z := match goal with - | H : (eq (A:=int) ?a ?b) |- _ => - generalize (f_equal i2z H); - try autorewrite with i2z; clear H; intro H; i2z - | |- (eq (A:=int) ?a ?b) => apply (i2z_eq a b); try autorewrite with i2z; i2z - | H : _ |- _ => progress autorewrite with i2z in H; i2z - | _ => try autorewrite with i2z - end. + | H : ?a = ?b |- _ => + generalize (f_equal i2z H); + try autorewrite with i2z; clear H; intro H; i2z + | |- ?a = ?b => + apply (i2z_eq a b); try autorewrite with i2z; i2z + | H : _ |- _ => progress autorewrite with i2z in H; i2z + | _ => try autorewrite with i2z + end. (** A reflexive version of the [i2z] tactic *) @@ -124,14 +124,14 @@ Module MoreInt (I:Int). Anyhow, [i2z_refl] is enough for applying [romega]. *) Ltac i2z_gen := match goal with - | |- (eq (A:=int) ?a ?b) => apply (i2z_eq a b); i2z_gen - | H : (eq (A:=int) ?a ?b) |- _ => + | |- ?a = ?b => apply (i2z_eq a b); i2z_gen + | H : ?a = ?b |- _ => generalize (f_equal i2z H); clear H; i2z_gen - | H : (eq (A:=Z) ?a ?b) |- _ => revert H; i2z_gen - | H : (Zlt ?a ?b) |- _ => revert H; i2z_gen - | H : (Zle ?a ?b) |- _ => revert H; i2z_gen - | H : (Zgt ?a ?b) |- _ => revert H; i2z_gen - | H : (Zge ?a ?b) |- _ => revert H; i2z_gen + | H : eq (A:=Z) ?a ?b |- _ => revert H; i2z_gen + | H : Z.lt ?a ?b |- _ => revert H; i2z_gen + | H : Z.le ?a ?b |- _ => revert H; i2z_gen + | H : Z.gt ?a ?b |- _ => revert H; i2z_gen + | H : Z.ge ?a ?b |- _ => revert H; i2z_gen | H : _ -> ?X |- _ => (* A [Set] or [Type] part cannot be dealt with easily using the [ExprP] datatype. So we forget it, leaving @@ -201,11 +201,11 @@ Module MoreInt (I:Int). with z2ez trm := match constr:trm with - | (?x+?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZplus ex ey) - | (?x-?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZminus ex ey) - | (?x*?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmult ex ey) - | (Zmax ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EZmax ex ey) - | (-?x)%Z => let ex := z2ez x in constr:(EZopp ex) + | (?x + ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZplus ex ey) + | (?x - ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZminus ex ey) + | (?x * ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmult ex ey) + | (Z.max ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EZmax ex ey) + | (- ?x)%Z => let ex := z2ez x in constr:(EZopp ex) | i2z ?x => let ex := i2ei x in constr:(EZofI ex) | ?x => constr:(EZraw x) end. @@ -360,8 +360,9 @@ End MoreInt. (** It's always nice to know that our [Int] interface is realizable :-) *) Module Z_as_Int <: Int. - Open Scope Z_scope. - Definition int := Z. + Local Open Scope Z_scope. + Definition t := Z. + Definition int := t. Definition _0 := 0. Definition _1 := 1. Definition _2 := 2. @@ -380,10 +381,9 @@ Module Z_as_Int <: Int. Lemma i2z_1 : i2z _1 = 1. Proof. auto. Qed. Lemma i2z_2 : i2z _2 = 2. Proof. auto. Qed. Lemma i2z_3 : i2z _3 = 3. Proof. auto. Qed. - Lemma i2z_plus : forall n p, i2z (n + p) = i2z n + i2z p. Proof. auto. Qed. - Lemma i2z_opp : forall n, i2z (- n) = - i2z n. Proof. auto. Qed. - Lemma i2z_minus : forall n p, i2z (n - p) = i2z n - i2z p. Proof. auto. Qed. - Lemma i2z_mult : forall n p, i2z (n * p) = i2z n * i2z p. Proof. auto. Qed. - Lemma i2z_max : forall n p, i2z (max n p) = Zmax (i2z n) (i2z p). Proof. auto. Qed. + Lemma i2z_plus n p : i2z (n + p) = i2z n + i2z p. Proof. auto. Qed. + Lemma i2z_opp n : i2z (- n) = - i2z n. Proof. auto. Qed. + Lemma i2z_minus n p : i2z (n - p) = i2z n - i2z p. Proof. auto. Qed. + Lemma i2z_mult n p : i2z (n * p) = i2z n * i2z p. Proof. auto. Qed. + Lemma i2z_max n p : i2z (max n p) = Zmax (i2z n) (i2z p). Proof. auto. Qed. End Z_as_Int. - diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v new file mode 100644 index 00000000..17c5bae3 --- /dev/null +++ b/theories/ZArith/ZOdiv.v @@ -0,0 +1,88 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \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 new file mode 100644 index 00000000..38d25797 --- /dev/null +++ b/theories/ZArith/ZOdiv_def.v @@ -0,0 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \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/Zeven.v b/theories/ZArith/Zeven.v index 550b66f7..f4d702b2 100644 --- a/theories/ZArith/Zeven.v +++ b/theories/ZArith/Zeven.v @@ -197,14 +197,12 @@ Qed. Lemma Zquot2_quot n : Z.quot2 n = n ÷ 2. Proof. assert (AUX : forall m, 0 < m -> Z.quot2 m = m ÷ 2). - BeginSubproof. - 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. - EndSubproof. + apply Zquot2_odd_eqn. } destruct (Z.lt_trichotomy 0 n) as [POS|[NUL|NEG]]. - now apply AUX. - now subst. diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget index 178111cd..88751cc0 100644 --- a/theories/ZArith/vo.itarget +++ b/theories/ZArith/vo.itarget @@ -23,6 +23,8 @@ Zmin.vo Zmisc.vo Znat.vo Znumtheory.vo +ZOdiv_def.vo +ZOdiv.vo Zquot.vo Zorder.vo Zpow_def.vo |