diff options
Diffstat (limited to 'theories/Numbers/Integer/BigZ')
-rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 208 | ||||
-rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 759 |
2 files changed, 0 insertions, 967 deletions
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v deleted file mode 100644 index 7c76011f..00000000 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ /dev/null @@ -1,208 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) -(************************************************************************) - -Require Export BigN. -Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake. - -(** * [BigZ] : arbitrary large efficient integers. - - The following [BigZ] module regroups both the operations and - all the abstract properties: - - - [ZMake.Make BigN] provides the operations and basic specs w.r.t. ZArith - - [ZTypeIsZAxioms] shows (mainly) that these operations implement - the interface [ZAxioms] - - [ZProp] adds all generic properties derived from [ZAxioms] - - [MinMax*Properties] provides properties of [min] and [max] - -*) - -Delimit Scope bigZ_scope with bigZ. - -Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder := - ZMake.Make BigN - <+ ZTypeIsZAxioms - <+ ZBasicProp [no inline] <+ ZExtraProp [no inline] - <+ HasEqBool2Dec [no inline] - <+ MinMaxLogicalProperties [no inline] - <+ MinMaxDecProperties [no inline]. - -(** For precision concerning the above scope handling, see comment in BigN *) - -(** Notations about [BigZ] *) - -Local Open Scope bigZ_scope. - -Notation bigZ := BigZ.t. -Bind Scope bigZ_scope with bigZ BigZ.t BigZ.t_. -Arguments BigZ.Pos _%bigN. -Arguments BigZ.Neg _%bigN. -Local Notation "0" := BigZ.zero : bigZ_scope. -Local Notation "1" := BigZ.one : bigZ_scope. -Local Notation "2" := BigZ.two : bigZ_scope. -Infix "+" := BigZ.add : bigZ_scope. -Infix "-" := BigZ.sub : bigZ_scope. -Notation "- x" := (BigZ.opp x) : bigZ_scope. -Infix "*" := BigZ.mul : bigZ_scope. -Infix "/" := BigZ.div : bigZ_scope. -Infix "^" := BigZ.pow : bigZ_scope. -Infix "?=" := BigZ.compare : bigZ_scope. -Infix "=?" := BigZ.eqb (at level 70, no associativity) : bigZ_scope. -Infix "<=?" := BigZ.leb (at level 70, no associativity) : bigZ_scope. -Infix "<?" := BigZ.ltb (at level 70, no associativity) : bigZ_scope. -Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope. -Notation "x != y" := (~x==y) (at level 70, no associativity) : bigZ_scope. -Infix "<" := BigZ.lt : bigZ_scope. -Infix "<=" := BigZ.le : bigZ_scope. -Notation "x > y" := (y < x) (only parsing) : bigZ_scope. -Notation "x >= y" := (y <= x) (only parsing) : bigZ_scope. -Notation "x < y < z" := (x<y /\ y<z) : bigZ_scope. -Notation "x < y <= z" := (x<y /\ y<=z) : bigZ_scope. -Notation "x <= y < z" := (x<=y /\ y<z) : bigZ_scope. -Notation "x <= y <= z" := (x<=y /\ y<=z) : bigZ_scope. -Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope. -Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigZ_scope. -Infix "÷" := BigZ.quot (at level 40, left associativity) : bigZ_scope. - -(** Some additional results about [BigZ] *) - -Theorem spec_to_Z: forall n : bigZ, - BigN.to_Z (BigZ.to_N n) = ((Z.sgn [n]) * [n])%Z. -Proof. -intros n; case n; simpl; intros p; - generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. -intros p1 H1; case H1; auto. -intros p1 H1; case H1; auto. -Qed. - -Theorem spec_to_N n: - ([n] = Z.sgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z. -Proof. -case n; simpl; intros p; - generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. -intros p1 H1; case H1; auto. -intros p1 H1; case H1; auto. -Qed. - -Theorem spec_to_Z_pos: forall n, (0 <= [n])%Z -> - BigN.to_Z (BigZ.to_N n) = [n]. -Proof. -intros n; case n; simpl; intros p; - generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. -intros p1 _ H1; case H1; auto. -intros p1 H1; case H1; auto. -Qed. - -(** [BigZ] is a ring *) - -Lemma BigZring : - ring_theory 0 1 BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq. -Proof. -constructor. -exact BigZ.add_0_l. exact BigZ.add_comm. exact BigZ.add_assoc. -exact BigZ.mul_1_l. exact BigZ.mul_comm. exact BigZ.mul_assoc. -exact BigZ.mul_add_distr_r. -symmetry. apply BigZ.add_opp_r. -exact BigZ.add_opp_diag_r. -Qed. - -Lemma BigZeqb_correct : forall x y, (x =? y) = true -> x==y. -Proof. now apply BigZ.eqb_eq. Qed. - -Definition BigZ_of_N n := BigZ.of_Z (Z.of_N n). - -Lemma BigZpower : power_theory 1 BigZ.mul BigZ.eq BigZ_of_N BigZ.pow. -Proof. -constructor. -intros. unfold BigZ.eq, BigZ_of_N. rewrite BigZ.spec_pow, BigZ.spec_of_Z. -rewrite Zpower_theory.(rpow_pow_N). -destruct n; simpl. reflexivity. -induction p; simpl; intros; BigZ.zify; rewrite ?IHp; auto. -Qed. - -Lemma BigZdiv : div_theory BigZ.eq BigZ.add BigZ.mul (@id _) - (fun a b => if b =? 0 then (0,a) else BigZ.div_eucl a b). -Proof. -constructor. unfold id. intros a b. -BigZ.zify. -case Z.eqb_spec. -BigZ.zify. auto with zarith. -intros NEQ. -generalize (BigZ.spec_div_eucl a b). -generalize (Z_div_mod_full [a] [b] NEQ). -destruct BigZ.div_eucl as (q,r), Z.div_eucl as (q',r'). -intros (EQ,_). injection 1 as EQr EQq. -BigZ.zify. rewrite EQr, EQq; auto. -Qed. - -(** Detection of constants *) - -Ltac isBigZcst t := - match t with - | BigZ.Pos ?t => isBigNcst t - | BigZ.Neg ?t => isBigNcst t - | BigZ.zero => constr:(true) - | BigZ.one => constr:(true) - | BigZ.two => constr:(true) - | BigZ.minus_one => constr:(true) - | _ => constr:(false) - end. - -Ltac BigZcst t := - match isBigZcst t with - | true => constr:(t) - | false => constr:(NotConstant) - end. - -Ltac BigZ_to_N t := - match t with - | BigZ.Pos ?t => BigN_to_N t - | BigZ.zero => constr:(0%N) - | BigZ.one => constr:(1%N) - | BigZ.two => constr:(2%N) - | _ => constr:(NotConstant) - end. - -(** Registration for the "ring" tactic *) - -Add Ring BigZr : BigZring - (decidable BigZeqb_correct, - constants [BigZcst], - power_tac BigZpower [BigZ_to_N], - div BigZdiv). - -Section TestRing. -Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + (y + 1*x)*x. -Proof. -intros. ring_simplify. reflexivity. -Qed. -Let test' : forall x y, 1 + x*y + x^2 - 1*1 - y*x + 1*(-x)*x == 0. -Proof. -intros. ring_simplify. reflexivity. -Qed. -End TestRing. - -(** [BigZ] also benefits from an "order" tactic *) - -Ltac bigZ_order := BigZ.order. - -Section TestOrder. -Let test : forall x y : bigZ, x<=y -> y<=x -> x==y. -Proof. bigZ_order. Qed. -End TestOrder. - -(** We can use at least a bit of (r)omega by translating to [Z]. *) - -Section TestOmega. -Let test : forall x y : bigZ, x<=y -> y<=x -> x==y. -Proof. intros x y. BigZ.zify. omega. Qed. -End TestOmega. - -(** Todo: micromega *) diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v deleted file mode 100644 index fec6e068..00000000 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ /dev/null @@ -1,759 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) -(************************************************************************) - -Require Import ZArith. -Require Import BigNumPrelude. -Require Import NSig. -Require Import ZSig. - -Open Scope Z_scope. - -(** * ZMake - - A generic transformation from a structure of natural numbers - [NSig.NType] to a structure of integers [ZSig.ZType]. -*) - -Module Make (NN:NType) <: ZType. - - Inductive t_ := - | Pos : NN.t -> t_ - | Neg : NN.t -> t_. - - Definition t := t_. - - Definition zero := Pos NN.zero. - Definition one := Pos NN.one. - Definition two := Pos NN.two. - Definition minus_one := Neg NN.one. - - Definition of_Z x := - match x with - | Zpos x => Pos (NN.of_N (Npos x)) - | Z0 => zero - | Zneg x => Neg (NN.of_N (Npos x)) - end. - - Definition to_Z x := - match x with - | Pos nx => NN.to_Z nx - | Neg nx => Z.opp (NN.to_Z nx) - end. - - Theorem spec_of_Z: forall x, to_Z (of_Z x) = x. - Proof. - intros x; case x; unfold to_Z, of_Z, zero. - exact NN.spec_0. - intros; rewrite NN.spec_of_N; auto. - intros; rewrite NN.spec_of_N; auto. - Qed. - - Definition eq x y := (to_Z x = to_Z y). - - Theorem spec_0: to_Z zero = 0. - exact NN.spec_0. - Qed. - - Theorem spec_1: to_Z one = 1. - exact NN.spec_1. - Qed. - - Theorem spec_2: to_Z two = 2. - exact NN.spec_2. - Qed. - - Theorem spec_m1: to_Z minus_one = -1. - simpl; rewrite NN.spec_1; auto. - Qed. - - Definition compare x y := - match x, y with - | Pos nx, Pos ny => NN.compare nx ny - | Pos nx, Neg ny => - match NN.compare nx NN.zero with - | Gt => Gt - | _ => NN.compare ny NN.zero - end - | Neg nx, Pos ny => - match NN.compare NN.zero nx with - | Lt => Lt - | _ => NN.compare NN.zero ny - end - | Neg nx, Neg ny => NN.compare ny nx - end. - - Theorem spec_compare : - forall x y, compare x y = Z.compare (to_Z x) (to_Z y). - Proof. - unfold compare, to_Z. - destruct x as [x|x], y as [y|y]; - rewrite ?NN.spec_compare, ?NN.spec_0, ?Z.compare_opp; auto; - assert (Hx:=NN.spec_pos x); assert (Hy:=NN.spec_pos y); - set (X:=NN.to_Z x) in *; set (Y:=NN.to_Z y) in *; clearbody X Y. - - destruct (Z.compare_spec X 0) as [EQ|LT|GT]. - + rewrite <- Z.opp_0 in EQ. now rewrite EQ, Z.compare_opp. - + exfalso. omega. - + symmetry. change (X > -Y). omega. - - destruct (Z.compare_spec 0 X) as [EQ|LT|GT]. - + rewrite <- EQ, Z.opp_0; auto. - + symmetry. change (-X < Y). omega. - + exfalso. omega. - Qed. - - Definition eqb x y := - match compare x y with - | Eq => true - | _ => false - end. - - Theorem spec_eqb x y : eqb x y = Z.eqb (to_Z x) (to_Z y). - Proof. - apply Bool.eq_iff_eq_true. - unfold eqb. rewrite Z.eqb_eq, <- Z.compare_eq_iff, spec_compare. - split; [now destruct Z.compare | now intros ->]. - Qed. - - Definition lt n m := to_Z n < to_Z m. - Definition le n m := to_Z n <= to_Z m. - - - Definition ltb (x y : t) : bool := - match compare x y with - | Lt => true - | _ => false - end. - - Theorem spec_ltb x y : ltb x y = Z.ltb (to_Z x) (to_Z y). - Proof. - apply Bool.eq_iff_eq_true. - rewrite Z.ltb_lt. unfold Z.lt, ltb. rewrite spec_compare. - split; [now destruct Z.compare | now intros ->]. - Qed. - - Definition leb (x y : t) : bool := - match compare x y with - | Gt => false - | _ => true - end. - - Theorem spec_leb x y : leb x y = Z.leb (to_Z x) (to_Z y). - Proof. - apply Bool.eq_iff_eq_true. - rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare. - now destruct Z.compare; split. - Qed. - - Definition min n m := match compare n m with Gt => m | _ => n end. - Definition max n m := match compare n m with Lt => m | _ => n end. - - Theorem spec_min : forall n m, to_Z (min n m) = Z.min (to_Z n) (to_Z m). - Proof. - unfold min, Z.min. intros. rewrite spec_compare. destruct Z.compare; auto. - Qed. - - Theorem spec_max : forall n m, to_Z (max n m) = Z.max (to_Z n) (to_Z m). - Proof. - unfold max, Z.max. intros. rewrite spec_compare. destruct Z.compare; auto. - Qed. - - Definition to_N x := - match x with - | Pos nx => nx - | Neg nx => nx - end. - - Definition abs x := Pos (to_N x). - - Theorem spec_abs: forall x, to_Z (abs x) = Z.abs (to_Z x). - Proof. - intros x; case x; clear x; intros x; assert (F:=NN.spec_pos x). - simpl; rewrite Z.abs_eq; auto. - simpl; rewrite Z.abs_neq; simpl; auto with zarith. - Qed. - - Definition opp x := - match x with - | Pos nx => Neg nx - | Neg nx => Pos nx - end. - - Theorem spec_opp: forall x, to_Z (opp x) = - to_Z x. - Proof. - intros x; case x; simpl; auto with zarith. - Qed. - - Definition succ x := - match x with - | Pos n => Pos (NN.succ n) - | Neg n => - match NN.compare NN.zero n with - | Lt => Neg (NN.pred n) - | _ => one - end - end. - - Theorem spec_succ: forall n, to_Z (succ n) = to_Z n + 1. - Proof. - intros x; case x; clear x; intros x. - exact (NN.spec_succ x). - simpl. rewrite NN.spec_compare. case Z.compare_spec; rewrite ?NN.spec_0; simpl. - intros HH; rewrite <- HH; rewrite NN.spec_1; ring. - intros HH; rewrite NN.spec_pred, Z.max_r; auto with zarith. - generalize (NN.spec_pos x); auto with zarith. - Qed. - - Definition add x y := - match x, y with - | Pos nx, Pos ny => Pos (NN.add nx ny) - | Pos nx, Neg ny => - match NN.compare nx ny with - | Gt => Pos (NN.sub nx ny) - | Eq => zero - | Lt => Neg (NN.sub ny nx) - end - | Neg nx, Pos ny => - match NN.compare nx ny with - | Gt => Neg (NN.sub nx ny) - | Eq => zero - | Lt => Pos (NN.sub ny nx) - end - | Neg nx, Neg ny => Neg (NN.add nx ny) - end. - - Theorem spec_add: forall x y, to_Z (add x y) = to_Z x + to_Z y. - Proof. - unfold add, to_Z; intros [x | x] [y | y]; - try (rewrite NN.spec_add; auto with zarith); - rewrite NN.spec_compare; case Z.compare_spec; - unfold zero; rewrite ?NN.spec_0, ?NN.spec_sub; omega with *. - Qed. - - Definition pred x := - match x with - | Pos nx => - match NN.compare NN.zero nx with - | Lt => Pos (NN.pred nx) - | _ => minus_one - end - | Neg nx => Neg (NN.succ nx) - end. - - Theorem spec_pred: forall x, to_Z (pred x) = to_Z x - 1. - Proof. - unfold pred, to_Z, minus_one; intros [x | x]; - try (rewrite NN.spec_succ; ring). - rewrite NN.spec_compare; case Z.compare_spec; - rewrite ?NN.spec_0, ?NN.spec_1, ?NN.spec_pred; - generalize (NN.spec_pos x); omega with *. - Qed. - - Definition sub x y := - match x, y with - | Pos nx, Pos ny => - match NN.compare nx ny with - | Gt => Pos (NN.sub nx ny) - | Eq => zero - | Lt => Neg (NN.sub ny nx) - end - | Pos nx, Neg ny => Pos (NN.add nx ny) - | Neg nx, Pos ny => Neg (NN.add nx ny) - | Neg nx, Neg ny => - match NN.compare nx ny with - | Gt => Neg (NN.sub nx ny) - | Eq => zero - | Lt => Pos (NN.sub ny nx) - end - end. - - Theorem spec_sub: forall x y, to_Z (sub x y) = to_Z x - to_Z y. - Proof. - unfold sub, to_Z; intros [x | x] [y | y]; - try (rewrite NN.spec_add; auto with zarith); - rewrite NN.spec_compare; case Z.compare_spec; - unfold zero; rewrite ?NN.spec_0, ?NN.spec_sub; omega with *. - Qed. - - Definition mul x y := - match x, y with - | Pos nx, Pos ny => Pos (NN.mul nx ny) - | Pos nx, Neg ny => Neg (NN.mul nx ny) - | Neg nx, Pos ny => Neg (NN.mul nx ny) - | Neg nx, Neg ny => Pos (NN.mul nx ny) - end. - - Theorem spec_mul: forall x y, to_Z (mul x y) = to_Z x * to_Z y. - Proof. - unfold mul, to_Z; intros [x | x] [y | y]; rewrite NN.spec_mul; ring. - Qed. - - Definition square x := - match x with - | Pos nx => Pos (NN.square nx) - | Neg nx => Pos (NN.square nx) - end. - - Theorem spec_square: forall x, to_Z (square x) = to_Z x * to_Z x. - Proof. - unfold square, to_Z; intros [x | x]; rewrite NN.spec_square; ring. - Qed. - - Definition pow_pos x p := - match x with - | Pos nx => Pos (NN.pow_pos nx p) - | Neg nx => - match p with - | xH => x - | xO _ => Pos (NN.pow_pos nx p) - | xI _ => Neg (NN.pow_pos nx p) - end - end. - - Theorem spec_pow_pos: forall x n, to_Z (pow_pos x n) = to_Z x ^ Zpos n. - Proof. - assert (F0: forall x, (-x)^2 = x^2). - intros x; rewrite Z.pow_2_r; ring. - unfold pow_pos, to_Z; intros [x | x] [p | p |]; - try rewrite NN.spec_pow_pos; try ring. - assert (F: 0 <= 2 * Zpos p). - assert (0 <= Zpos p); auto with zarith. - rewrite Pos2Z.inj_xI; repeat rewrite Zpower_exp; auto with zarith. - repeat rewrite Z.pow_mul_r; auto with zarith. - rewrite F0; ring. - assert (F: 0 <= 2 * Zpos p). - assert (0 <= Zpos p); auto with zarith. - rewrite Pos2Z.inj_xO; repeat rewrite Zpower_exp; auto with zarith. - repeat rewrite Z.pow_mul_r; auto with zarith. - rewrite F0; ring. - Qed. - - Definition pow_N x n := - match n with - | N0 => one - | Npos p => pow_pos x p - end. - - Theorem spec_pow_N: forall x n, to_Z (pow_N x n) = to_Z x ^ Z.of_N n. - Proof. - destruct n; simpl. apply NN.spec_1. - apply spec_pow_pos. - Qed. - - Definition pow x y := - match to_Z y with - | Z0 => one - | Zpos p => pow_pos x p - | Zneg p => zero - end. - - Theorem spec_pow: forall x y, to_Z (pow x y) = to_Z x ^ to_Z y. - Proof. - intros. unfold pow. destruct (to_Z y); simpl. - apply NN.spec_1. - apply spec_pow_pos. - apply NN.spec_0. - Qed. - - Definition log2 x := - match x with - | Pos nx => Pos (NN.log2 nx) - | Neg nx => zero - end. - - Theorem spec_log2: forall x, to_Z (log2 x) = Z.log2 (to_Z x). - Proof. - intros. destruct x as [p|p]; simpl. apply NN.spec_log2. - rewrite NN.spec_0. - destruct (Z_le_lt_eq_dec _ _ (NN.spec_pos p)) as [LT|EQ]. - rewrite Z.log2_nonpos; auto with zarith. - now rewrite <- EQ. - Qed. - - Definition sqrt x := - match x with - | Pos nx => Pos (NN.sqrt nx) - | Neg nx => Neg NN.zero - end. - - Theorem spec_sqrt: forall x, to_Z (sqrt x) = Z.sqrt (to_Z x). - Proof. - destruct x as [p|p]; simpl. - apply NN.spec_sqrt. - rewrite NN.spec_0. - destruct (Z_le_lt_eq_dec _ _ (NN.spec_pos p)) as [LT|EQ]. - rewrite Z.sqrt_neg; auto with zarith. - now rewrite <- EQ. - Qed. - - Definition div_eucl x y := - match x, y with - | Pos nx, Pos ny => - let (q, r) := NN.div_eucl nx ny in - (Pos q, Pos r) - | Pos nx, Neg ny => - let (q, r) := NN.div_eucl nx ny in - if NN.eqb NN.zero r - then (Neg q, zero) - else (Neg (NN.succ q), Neg (NN.sub ny r)) - | Neg nx, Pos ny => - let (q, r) := NN.div_eucl nx ny in - if NN.eqb NN.zero r - then (Neg q, zero) - else (Neg (NN.succ q), Pos (NN.sub ny r)) - | Neg nx, Neg ny => - let (q, r) := NN.div_eucl nx ny in - (Pos q, Neg r) - end. - - Ltac break_nonneg x px EQx := - let H := fresh "H" in - assert (H:=NN.spec_pos x); - destruct (NN.to_Z x) as [|px|px] eqn:EQx; - [clear H|clear H|elim H; reflexivity]. - - Theorem spec_div_eucl: forall x y, - let (q,r) := div_eucl x y in - (to_Z q, to_Z r) = Z.div_eucl (to_Z x) (to_Z y). - Proof. - unfold div_eucl, to_Z. intros [x | x] [y | y]. - (* Pos Pos *) - generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y); auto. - (* Pos Neg *) - generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). - break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1 as Hq Hr; rewrite NN.spec_eqb, NN.spec_0, Hr; - simpl; rewrite Hq, NN.spec_0; auto). - change (- Zpos py) with (Zneg py). - assert (GT : Zpos py > 0) by (compute; auto). - generalize (Z_div_mod (Zpos px) (Zpos py) GT). - unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r'). - intros (EQ,MOD). injection 1 as Hq' Hr'. - rewrite NN.spec_eqb, NN.spec_0, Hr'. - break_nonneg r pr EQr. - subst; simpl. rewrite NN.spec_0; auto. - subst. lazy iota beta delta [Z.eqb]. - rewrite NN.spec_sub, NN.spec_succ, EQy, EQr. f_equal. omega with *. - (* Neg Pos *) - generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). - break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1 as Hq Hr; rewrite NN.spec_eqb, NN.spec_0, Hr; - simpl; rewrite Hq, NN.spec_0; auto). - change (- Zpos px) with (Zneg px). - assert (GT : Zpos py > 0) by (compute; auto). - generalize (Z_div_mod (Zpos px) (Zpos py) GT). - unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r'). - intros (EQ,MOD). injection 1 as Hq' Hr'. - rewrite NN.spec_eqb, NN.spec_0, Hr'. - break_nonneg r pr EQr. - subst; simpl. rewrite NN.spec_0; auto. - subst. lazy iota beta delta [Z.eqb]. - rewrite NN.spec_sub, NN.spec_succ, EQy, EQr. f_equal. omega with *. - (* Neg Neg *) - generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). - break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1 as -> ->; auto). - simpl. intros <-; auto. - Qed. - - Definition div x y := fst (div_eucl x y). - - Definition spec_div: forall x y, - to_Z (div x y) = to_Z x / to_Z y. - Proof. - intros x y; generalize (spec_div_eucl x y); unfold div, Z.div. - case div_eucl; case Z.div_eucl; simpl; auto. - intros q r q11 r1 H; injection H; auto. - Qed. - - Definition modulo x y := snd (div_eucl x y). - - Theorem spec_modulo: - forall x y, to_Z (modulo x y) = to_Z x mod to_Z y. - Proof. - intros x y; generalize (spec_div_eucl x y); unfold modulo, Z.modulo. - case div_eucl; case Z.div_eucl; simpl; auto. - intros q r q11 r1 H; injection H; auto. - Qed. - - Definition quot x y := - match x, y with - | Pos nx, Pos ny => Pos (NN.div nx ny) - | Pos nx, Neg ny => Neg (NN.div nx ny) - | Neg nx, Pos ny => Neg (NN.div nx ny) - | Neg nx, Neg ny => Pos (NN.div nx ny) - end. - - Definition rem x y := - if eqb y zero then x - else - match x, y with - | Pos nx, Pos ny => Pos (NN.modulo nx ny) - | Pos nx, Neg ny => Pos (NN.modulo nx ny) - | Neg nx, Pos ny => Neg (NN.modulo nx ny) - | Neg nx, Neg ny => Neg (NN.modulo nx ny) - end. - - Lemma spec_quot : forall x y, to_Z (quot x y) = (to_Z x) ÷ (to_Z y). - Proof. - intros [x|x] [y|y]; simpl; symmetry; rewrite NN.spec_div; - (* Nota: we rely here on [forall a b, a ÷ 0 = b / 0] *) - destruct (Z.eq_dec (NN.to_Z y) 0) as [EQ|NEQ]; - try (rewrite EQ; now destruct (NN.to_Z x)); - rewrite ?Z.quot_opp_r, ?Z.quot_opp_l, ?Z.opp_involutive, ?Z.opp_inj_wd; - trivial; apply Z.quot_div_nonneg; - generalize (NN.spec_pos x) (NN.spec_pos y); Z.order. - Qed. - - Lemma spec_rem : forall x y, - to_Z (rem x y) = Z.rem (to_Z x) (to_Z y). - Proof. - intros x y. unfold rem. rewrite spec_eqb, spec_0. - case Z.eqb_spec; intros Hy. - (* Nota: we rely here on [Z.rem a 0 = a] *) - rewrite Hy. now destruct (to_Z x). - destruct x as [x|x], y as [y|y]; simpl in *; symmetry; - rewrite ?Z.eq_opp_l, ?Z.opp_0 in Hy; - rewrite NN.spec_modulo, ?Z.rem_opp_r, ?Z.rem_opp_l, ?Z.opp_involutive, - ?Z.opp_inj_wd; - trivial; apply Z.rem_mod_nonneg; - generalize (NN.spec_pos x) (NN.spec_pos y); Z.order. - Qed. - - Definition gcd x y := - match x, y with - | Pos nx, Pos ny => Pos (NN.gcd nx ny) - | Pos nx, Neg ny => Pos (NN.gcd nx ny) - | Neg nx, Pos ny => Pos (NN.gcd nx ny) - | Neg nx, Neg ny => Pos (NN.gcd nx ny) - end. - - Theorem spec_gcd: forall a b, to_Z (gcd a b) = Z.gcd (to_Z a) (to_Z b). - Proof. - unfold gcd, Z.gcd, to_Z; intros [x | x] [y | y]; rewrite NN.spec_gcd; unfold Z.gcd; - auto; case NN.to_Z; simpl; auto with zarith; - try rewrite Z.abs_opp; auto; - case NN.to_Z; simpl; auto with zarith. - Qed. - - Definition sgn x := - match compare zero x with - | Lt => one - | Eq => zero - | Gt => minus_one - end. - - Lemma spec_sgn : forall x, to_Z (sgn x) = Z.sgn (to_Z x). - Proof. - intros. unfold sgn. rewrite spec_compare. case Z.compare_spec. - rewrite spec_0. intros <-; auto. - rewrite spec_0, spec_1. symmetry. rewrite Z.sgn_pos_iff; auto. - rewrite spec_0, spec_m1. symmetry. rewrite Z.sgn_neg_iff; auto with zarith. - Qed. - - Definition even z := - match z with - | Pos n => NN.even n - | Neg n => NN.even n - end. - - Definition odd z := - match z with - | Pos n => NN.odd n - | Neg n => NN.odd n - end. - - Lemma spec_even : forall z, even z = Z.even (to_Z z). - Proof. - intros [n|n]; simpl; rewrite NN.spec_even; trivial. - destruct (NN.to_Z n) as [|p|p]; now try destruct p. - Qed. - - Lemma spec_odd : forall z, odd z = Z.odd (to_Z z). - Proof. - intros [n|n]; simpl; rewrite NN.spec_odd; trivial. - destruct (NN.to_Z n) as [|p|p]; now try destruct p. - Qed. - - Definition norm_pos z := - match z with - | Pos _ => z - | Neg n => if NN.eqb n NN.zero then Pos n else z - end. - - Definition testbit a n := - match norm_pos n, norm_pos a with - | Pos p, Pos a => NN.testbit a p - | Pos p, Neg a => negb (NN.testbit (NN.pred a) p) - | Neg p, _ => false - end. - - Definition shiftl a n := - match norm_pos a, n with - | Pos a, Pos n => Pos (NN.shiftl a n) - | Pos a, Neg n => Pos (NN.shiftr a n) - | Neg a, Pos n => Neg (NN.shiftl a n) - | Neg a, Neg n => Neg (NN.succ (NN.shiftr (NN.pred a) n)) - end. - - Definition shiftr a n := shiftl a (opp n). - - Definition lor a b := - match norm_pos a, norm_pos b with - | Pos a, Pos b => Pos (NN.lor a b) - | Neg a, Pos b => Neg (NN.succ (NN.ldiff (NN.pred a) b)) - | Pos a, Neg b => Neg (NN.succ (NN.ldiff (NN.pred b) a)) - | Neg a, Neg b => Neg (NN.succ (NN.land (NN.pred a) (NN.pred b))) - end. - - Definition land a b := - match norm_pos a, norm_pos b with - | Pos a, Pos b => Pos (NN.land a b) - | Neg a, Pos b => Pos (NN.ldiff b (NN.pred a)) - | Pos a, Neg b => Pos (NN.ldiff a (NN.pred b)) - | Neg a, Neg b => Neg (NN.succ (NN.lor (NN.pred a) (NN.pred b))) - end. - - Definition ldiff a b := - match norm_pos a, norm_pos b with - | Pos a, Pos b => Pos (NN.ldiff a b) - | Neg a, Pos b => Neg (NN.succ (NN.lor (NN.pred a) b)) - | Pos a, Neg b => Pos (NN.land a (NN.pred b)) - | Neg a, Neg b => Pos (NN.ldiff (NN.pred b) (NN.pred a)) - end. - - Definition lxor a b := - match norm_pos a, norm_pos b with - | Pos a, Pos b => Pos (NN.lxor a b) - | Neg a, Pos b => Neg (NN.succ (NN.lxor (NN.pred a) b)) - | Pos a, Neg b => Neg (NN.succ (NN.lxor a (NN.pred b))) - | Neg a, Neg b => Pos (NN.lxor (NN.pred a) (NN.pred b)) - end. - - Definition div2 x := shiftr x one. - - Lemma Zlnot_alt1 : forall x, -(x+1) = Z.lnot x. - Proof. - unfold Z.lnot, Z.pred; auto with zarith. - Qed. - - Lemma Zlnot_alt2 : forall x, Z.lnot (x-1) = -x. - Proof. - unfold Z.lnot, Z.pred; auto with zarith. - Qed. - - Lemma Zlnot_alt3 : forall x, Z.lnot (-x) = x-1. - Proof. - unfold Z.lnot, Z.pred; auto with zarith. - Qed. - - Lemma spec_norm_pos : forall x, to_Z (norm_pos x) = to_Z x. - Proof. - intros [x|x]; simpl; trivial. - rewrite NN.spec_eqb, NN.spec_0. - case Z.eqb_spec; simpl; auto with zarith. - Qed. - - Lemma spec_norm_pos_pos : forall x y, norm_pos x = Neg y -> - 0 < NN.to_Z y. - Proof. - intros [x|x] y; simpl; try easy. - rewrite NN.spec_eqb, NN.spec_0. - case Z.eqb_spec; simpl; try easy. - inversion 2. subst. generalize (NN.spec_pos y); auto with zarith. - Qed. - - Ltac destr_norm_pos x := - rewrite <- (spec_norm_pos x); - let H := fresh in - let x' := fresh x in - assert (H := spec_norm_pos_pos x); - destruct (norm_pos x) as [x'|x']; - specialize (H x' (eq_refl _)) || clear H. - - Lemma spec_testbit: forall x p, testbit x p = Z.testbit (to_Z x) (to_Z p). - Proof. - intros x p. unfold testbit. - destr_norm_pos p; simpl. destr_norm_pos x; simpl. - apply NN.spec_testbit. - rewrite NN.spec_testbit, NN.spec_pred, Z.max_r by auto with zarith. - symmetry. apply Z.bits_opp. apply NN.spec_pos. - symmetry. apply Z.testbit_neg_r; auto with zarith. - Qed. - - Lemma spec_shiftl: forall x p, to_Z (shiftl x p) = Z.shiftl (to_Z x) (to_Z p). - Proof. - intros x p. unfold shiftl. - destr_norm_pos x; destruct p as [p|p]; simpl; - assert (Hp := NN.spec_pos p). - apply NN.spec_shiftl. - rewrite Z.shiftl_opp_r. apply NN.spec_shiftr. - rewrite !NN.spec_shiftl. - rewrite !Z.shiftl_mul_pow2 by apply NN.spec_pos. - symmetry. apply Z.mul_opp_l. - rewrite Z.shiftl_opp_r, NN.spec_succ, NN.spec_shiftr, NN.spec_pred, Z.max_r - by auto with zarith. - now rewrite Zlnot_alt1, Z.lnot_shiftr, Zlnot_alt2. - Qed. - - Lemma spec_shiftr: forall x p, to_Z (shiftr x p) = Z.shiftr (to_Z x) (to_Z p). - Proof. - intros. unfold shiftr. rewrite spec_shiftl, spec_opp. - apply Z.shiftl_opp_r. - Qed. - - Lemma spec_land: forall x y, to_Z (land x y) = Z.land (to_Z x) (to_Z y). - Proof. - intros x y. unfold land. - destr_norm_pos x; destr_norm_pos y; simpl; - rewrite ?NN.spec_succ, ?NN.spec_land, ?NN.spec_ldiff, ?NN.spec_lor, - ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1; auto with zarith. - now rewrite Z.ldiff_land, Zlnot_alt2. - now rewrite Z.ldiff_land, Z.land_comm, Zlnot_alt2. - now rewrite Z.lnot_lor, !Zlnot_alt2. - Qed. - - Lemma spec_lor: forall x y, to_Z (lor x y) = Z.lor (to_Z x) (to_Z y). - Proof. - intros x y. unfold lor. - destr_norm_pos x; destr_norm_pos y; simpl; - rewrite ?NN.spec_succ, ?NN.spec_land, ?NN.spec_ldiff, ?NN.spec_lor, - ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1; auto with zarith. - now rewrite Z.lnot_ldiff, Z.lor_comm, Zlnot_alt2. - now rewrite Z.lnot_ldiff, Zlnot_alt2. - now rewrite Z.lnot_land, !Zlnot_alt2. - Qed. - - Lemma spec_ldiff: forall x y, to_Z (ldiff x y) = Z.ldiff (to_Z x) (to_Z y). - Proof. - intros x y. unfold ldiff. - destr_norm_pos x; destr_norm_pos y; simpl; - rewrite ?NN.spec_succ, ?NN.spec_land, ?NN.spec_ldiff, ?NN.spec_lor, - ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1; auto with zarith. - now rewrite Z.ldiff_land, Zlnot_alt3. - now rewrite Z.lnot_lor, Z.ldiff_land, <- Zlnot_alt2. - now rewrite 2 Z.ldiff_land, Zlnot_alt2, Z.land_comm, Zlnot_alt3. - Qed. - - Lemma spec_lxor: forall x y, to_Z (lxor x y) = Z.lxor (to_Z x) (to_Z y). - Proof. - intros x y. unfold lxor. - destr_norm_pos x; destr_norm_pos y; simpl; - rewrite ?NN.spec_succ, ?NN.spec_lxor, ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1; - auto with zarith. - now rewrite !Z.lnot_lxor_r, Zlnot_alt2. - now rewrite !Z.lnot_lxor_l, Zlnot_alt2. - now rewrite <- Z.lxor_lnot_lnot, !Zlnot_alt2. - Qed. - - Lemma spec_div2: forall x, to_Z (div2 x) = Z.div2 (to_Z x). - Proof. - intros x. unfold div2. now rewrite spec_shiftr, Z.div2_spec, spec_1. - Qed. - -End Make. |