diff options
Diffstat (limited to 'theories/Numbers/Integer/BigZ')
-rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 120 | ||||
-rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 643 |
2 files changed, 530 insertions, 233 deletions
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index 7df8909f..a56f90b0 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: BigZ.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export BigN. Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake. @@ -21,82 +19,64 @@ Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake. - [ZMake.Make BigN] provides the operations and basic specs w.r.t. ZArith - [ZTypeIsZAxioms] shows (mainly) that these operations implement the interface [ZAxioms] - - [ZPropSig] adds all generic properties derived from [ZAxioms] - - [ZDivPropFunct] provides generic properties of [div] and [mod] - ("Floor" variant) + - [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 - <+ !ZPropSig <+ !ZDivPropFunct <+ HasEqBool2Dec - <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties. +Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder. + Include ZMake.Make BigN [scope abstract_scope to bigZ_scope]. + Bind Scope bigZ_scope with t t_. + Include ZTypeIsZAxioms + <+ ZProp [no inline] + <+ HasEqBool2Dec [no inline] + <+ MinMaxLogicalProperties [no inline] + <+ MinMaxDecProperties [no inline]. +End BigZ. -(** Notations about [BigZ] *) +(** For precision concerning the above scope handling, see comment in BigN *) -Notation bigZ := BigZ.t. +(** Notations about [BigZ] *) -Delimit Scope bigZ_scope with bigZ. -Bind Scope bigZ_scope with bigZ. -Bind Scope bigZ_scope with BigZ.t. -Bind Scope bigZ_scope with BigZ.t_. -(* Bind Scope has no retroactive effect, let's declare scopes by hand. *) -Arguments Scope BigZ.Pos [bigN_scope]. -Arguments Scope BigZ.Neg [bigN_scope]. -Arguments Scope BigZ.to_Z [bigZ_scope]. -Arguments Scope BigZ.succ [bigZ_scope]. -Arguments Scope BigZ.pred [bigZ_scope]. -Arguments Scope BigZ.opp [bigZ_scope]. -Arguments Scope BigZ.square [bigZ_scope]. -Arguments Scope BigZ.add [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.sub [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.mul [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.div [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.eq [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.lt [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.le [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.eq [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.compare [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.min [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.max [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.eq_bool [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.power_pos [bigZ_scope positive_scope]. -Arguments Scope BigZ.power [bigZ_scope N_scope]. -Arguments Scope BigZ.sqrt [bigZ_scope]. -Arguments Scope BigZ.div_eucl [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.modulo [bigZ_scope bigZ_scope]. -Arguments Scope BigZ.gcd [bigZ_scope bigZ_scope]. +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.power : 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)%bigZ (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" := (BigZ.lt y x)(only parsing) : bigZ_scope. -Notation "x >= y" := (BigZ.le y x)(only parsing) : bigZ_scope. -Notation "x < y < z" := (x<y /\ y<z)%bigZ : bigZ_scope. -Notation "x < y <= z" := (x<y /\ y<=z)%bigZ : bigZ_scope. -Notation "x <= y < z" := (x<=y /\ y<z)%bigZ : bigZ_scope. -Notation "x <= y <= z" := (x<=y /\ y<=z)%bigZ : 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) : bigN_scope. - -Local Open Scope 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) = ((Zsgn [n]) * [n])%Z. + 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. @@ -105,7 +85,7 @@ intros p1 H1; case H1; auto. Qed. Theorem spec_to_N n: - ([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z. + ([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. @@ -135,29 +115,31 @@ symmetry. apply BigZ.add_opp_r. exact BigZ.add_opp_diag_r. Qed. -Lemma BigZeqb_correct : forall x y, BigZ.eq_bool x y = true -> x==y. +Lemma BigZeqb_correct : forall x y, (x =? y) = true -> x==y. Proof. now apply BigZ.eqb_eq. Qed. -Lemma BigZpower : power_theory 1 BigZ.mul BigZ.eq (@id N) BigZ.power. +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. red. rewrite BigZ.spec_power. unfold id. -destruct Zpower_theory as [EQ]. rewrite EQ. +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 BigZ.eq_bool b 0 then (0,a) else BigZ.div_eucl a b). + (fun a b => if b =? 0 then (0,a) else BigZ.div_eucl a b). Proof. constructor. unfold id. intros a b. BigZ.zify. -generalize (Zeq_bool_if [b] 0); destruct (Zeq_bool [b] 0). +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), Zdiv_eucl as (q',r'). +destruct BigZ.div_eucl as (q,r), Z.div_eucl as (q',r'). intros (EQ,_). injection 1. intros EQr EQq. BigZ.zify. rewrite EQr, EQq; auto. Qed. @@ -170,6 +152,7 @@ Ltac isBigZcst 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. @@ -180,16 +163,25 @@ Ltac BigZcst 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 [Ncst], + 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*x + 1*x*x. +Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + (y + 1*x)*x. Proof. intros. ring_simplify. reflexivity. Qed. diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 48db793c..180fe0a9 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: ZMake.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import ZArith. Require Import BigNumPrelude. Require Import NSig. @@ -23,113 +21,148 @@ Open Scope Z_scope. [NSig.NType] to a structure of integers [ZSig.ZType]. *) -Module Make (N:NType) <: ZType. +Module Make (NN:NType) <: ZType. Inductive t_ := - | Pos : N.t -> t_ - | Neg : N.t -> t_. + | Pos : NN.t -> t_ + | Neg : NN.t -> t_. Definition t := t_. - Definition zero := Pos N.zero. - Definition one := Pos N.one. - Definition minus_one := Neg N.one. + Bind Scope abstract_scope with 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 (N.of_N (Npos x)) + | Zpos x => Pos (NN.of_N (Npos x)) | Z0 => zero - | Zneg x => Neg (N.of_N (Npos x)) + | Zneg x => Neg (NN.of_N (Npos x)) end. Definition to_Z x := match x with - | Pos nx => N.to_Z nx - | Neg nx => Zopp (N.to_Z nx) + | 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 N.spec_0. - intros; rewrite N.spec_of_N; auto. - intros; rewrite N.spec_of_N; auto. + 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 N.spec_0. + exact NN.spec_0. Qed. Theorem spec_1: to_Z one = 1. - exact N.spec_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 N.spec_1; auto. + simpl; rewrite NN.spec_1; auto. Qed. Definition compare x y := match x, y with - | Pos nx, Pos ny => N.compare nx ny + | Pos nx, Pos ny => NN.compare nx ny | Pos nx, Neg ny => - match N.compare nx N.zero with + match NN.compare nx NN.zero with | Gt => Gt - | _ => N.compare ny N.zero + | _ => NN.compare ny NN.zero end | Neg nx, Pos ny => - match N.compare N.zero nx with + match NN.compare NN.zero nx with | Lt => Lt - | _ => N.compare N.zero ny + | _ => NN.compare NN.zero ny end - | Neg nx, Neg ny => N.compare ny nx + | Neg nx, Neg ny => NN.compare ny nx end. Theorem spec_compare : - forall x y, compare x y = Zcompare (to_Z x) (to_Z y). + 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 ?N.spec_compare, ?N.spec_0, <-?Zcompare_opp; auto; - assert (Hx:=N.spec_pos x); assert (Hy:=N.spec_pos y); - set (X:=N.to_Z x) in *; set (Y:=N.to_Z y) in *; clearbody X Y. - destruct (Zcompare_spec X 0) as [EQ|LT|GT]. - rewrite EQ. rewrite <- Zopp_0 at 2. apply Zcompare_opp. - exfalso. omega. - symmetry. change (X > -Y). omega. - destruct (Zcompare_spec 0 X) as [EQ|LT|GT]. - rewrite <- EQ. rewrite Zopp_0; auto. - symmetry. change (-X < Y). omega. - exfalso. omega. - Qed. - - Definition eq_bool x 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_eq_bool: - forall x y, eq_bool x y = Zeq_bool (to_Z x) (to_Z y). + Theorem spec_eqb x y : eqb x y = Z.eqb (to_Z x) (to_Z y). Proof. - unfold eq_bool, Zeq_bool; intros; rewrite spec_compare; reflexivity. + 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. + destruct Z.compare; split; try easy. now destruct 1. + 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) = Zmin (to_Z n) (to_Z m). + Theorem spec_min : forall n m, to_Z (min n m) = Z.min (to_Z n) (to_Z m). Proof. - unfold min, Zmin. intros. rewrite spec_compare. destruct Zcompare; auto. + unfold min, Z.min. intros. rewrite spec_compare. destruct Z.compare; auto. Qed. - Theorem spec_max : forall n m, to_Z (max n m) = Zmax (to_Z n) (to_Z m). + Theorem spec_max : forall n m, to_Z (max n m) = Z.max (to_Z n) (to_Z m). Proof. - unfold max, Zmax. intros. rewrite spec_compare. destruct Zcompare; auto. + unfold max, Z.max. intros. rewrite spec_compare. destruct Z.compare; auto. Qed. Definition to_N x := @@ -140,11 +173,11 @@ Module Make (N:NType) <: ZType. Definition abs x := Pos (to_N x). - Theorem spec_abs: forall x, to_Z (abs x) = Zabs (to_Z 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:=N.spec_pos x). - simpl; rewrite Zabs_eq; auto. - simpl; rewrite Zabs_non_eq; simpl; auto with zarith. + 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 := @@ -160,10 +193,10 @@ Module Make (N:NType) <: ZType. Definition succ x := match x with - | Pos n => Pos (N.succ n) + | Pos n => Pos (NN.succ n) | Neg n => - match N.compare N.zero n with - | Lt => Neg (N.pred n) + match NN.compare NN.zero n with + | Lt => Neg (NN.pred n) | _ => one end end. @@ -171,232 +204,260 @@ Module Make (N:NType) <: ZType. Theorem spec_succ: forall n, to_Z (succ n) = to_Z n + 1. Proof. intros x; case x; clear x; intros x. - exact (N.spec_succ x). - simpl. rewrite N.spec_compare. case Zcompare_spec; rewrite ?N.spec_0; simpl. - intros HH; rewrite <- HH; rewrite N.spec_1; ring. - intros HH; rewrite N.spec_pred, Zmax_r; auto with zarith. - generalize (N.spec_pos x); auto with zarith. + 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 (N.add nx ny) + | Pos nx, Pos ny => Pos (NN.add nx ny) | Pos nx, Neg ny => - match N.compare nx ny with - | Gt => Pos (N.sub nx ny) + match NN.compare nx ny with + | Gt => Pos (NN.sub nx ny) | Eq => zero - | Lt => Neg (N.sub ny nx) + | Lt => Neg (NN.sub ny nx) end | Neg nx, Pos ny => - match N.compare nx ny with - | Gt => Neg (N.sub nx ny) + match NN.compare nx ny with + | Gt => Neg (NN.sub nx ny) | Eq => zero - | Lt => Pos (N.sub ny nx) + | Lt => Pos (NN.sub ny nx) end - | Neg nx, Neg ny => Neg (N.add nx ny) + | 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 N.spec_add; auto with zarith); - rewrite N.spec_compare; case Zcompare_spec; - unfold zero; rewrite ?N.spec_0, ?N.spec_sub; omega with *. + 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 N.compare N.zero nx with - | Lt => Pos (N.pred nx) + match NN.compare NN.zero nx with + | Lt => Pos (NN.pred nx) | _ => minus_one end - | Neg nx => Neg (N.succ nx) + | 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 N.spec_succ; ring). - rewrite N.spec_compare; case Zcompare_spec; - rewrite ?N.spec_0, ?N.spec_1, ?N.spec_pred; - generalize (N.spec_pos x); omega with *. + 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 N.compare nx ny with - | Gt => Pos (N.sub nx ny) + match NN.compare nx ny with + | Gt => Pos (NN.sub nx ny) | Eq => zero - | Lt => Neg (N.sub ny nx) + | Lt => Neg (NN.sub ny nx) end - | Pos nx, Neg ny => Pos (N.add nx ny) - | Neg nx, Pos ny => Neg (N.add nx ny) + | Pos nx, Neg ny => Pos (NN.add nx ny) + | Neg nx, Pos ny => Neg (NN.add nx ny) | Neg nx, Neg ny => - match N.compare nx ny with - | Gt => Neg (N.sub nx ny) + match NN.compare nx ny with + | Gt => Neg (NN.sub nx ny) | Eq => zero - | Lt => Pos (N.sub ny nx) + | 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 N.spec_add; auto with zarith); - rewrite N.spec_compare; case Zcompare_spec; - unfold zero; rewrite ?N.spec_0, ?N.spec_sub; omega with *. + 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 (N.mul nx ny) - | Pos nx, Neg ny => Neg (N.mul nx ny) - | Neg nx, Pos ny => Neg (N.mul nx ny) - | Neg nx, Neg ny => Pos (N.mul nx ny) + | 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 N.spec_mul; ring. + unfold mul, to_Z; intros [x | x] [y | y]; rewrite NN.spec_mul; ring. Qed. Definition square x := match x with - | Pos nx => Pos (N.square nx) - | Neg nx => Pos (N.square nx) + | 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 N.spec_square; ring. + unfold square, to_Z; intros [x | x]; rewrite NN.spec_square; ring. Qed. - Definition power_pos x p := + Definition pow_pos x p := match x with - | Pos nx => Pos (N.power_pos nx p) + | Pos nx => Pos (NN.pow_pos nx p) | Neg nx => match p with | xH => x - | xO _ => Pos (N.power_pos nx p) - | xI _ => Neg (N.power_pos nx p) + | xO _ => Pos (NN.pow_pos nx p) + | xI _ => Neg (NN.pow_pos nx p) end end. - Theorem spec_power_pos: forall x n, to_Z (power_pos x n) = to_Z x ^ Zpos n. + 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 Zpower_2; ring. - unfold power_pos, to_Z; intros [x | x] [p | p |]; - try rewrite N.spec_power_pos; try ring. + 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 Zpos_xI; repeat rewrite Zpower_exp; auto with zarith. - repeat rewrite Zpower_mult; 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 Zpos_xO; repeat rewrite Zpower_exp; auto with zarith. - repeat rewrite Zpower_mult; 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 power x n := + Definition pow_N x n := match n with | N0 => one - | Npos p => power_pos x p + | 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_power: forall x n, to_Z (power x n) = to_Z x ^ Z_of_N n. + Theorem spec_pow: forall x y, to_Z (pow x y) = to_Z x ^ to_Z y. Proof. - destruct n; simpl. rewrite N.spec_1; reflexivity. - apply spec_power_pos. + 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 (N.sqrt nx) - | Neg nx => Neg N.zero + | Pos nx => Pos (NN.sqrt nx) + | Neg nx => Neg NN.zero end. - Theorem spec_sqrt: forall x, 0 <= to_Z x -> - to_Z (sqrt x) ^ 2 <= to_Z x < (to_Z (sqrt x) + 1) ^ 2. + Theorem spec_sqrt: forall x, to_Z (sqrt x) = Z.sqrt (to_Z x). Proof. - unfold to_Z, sqrt; intros [x | x] H. - exact (N.spec_sqrt x). - replace (N.to_Z x) with 0. - rewrite N.spec_0; simpl Zpower; unfold Zpower_pos, iter_pos; - auto with zarith. - generalize (N.spec_pos x); auto with zarith. + 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) := N.div_eucl nx ny in + let (q, r) := NN.div_eucl nx ny in (Pos q, Pos r) | Pos nx, Neg ny => - let (q, r) := N.div_eucl nx ny in - if N.eq_bool N.zero r + let (q, r) := NN.div_eucl nx ny in + if NN.eqb NN.zero r then (Neg q, zero) - else (Neg (N.succ q), Neg (N.sub ny r)) + else (Neg (NN.succ q), Neg (NN.sub ny r)) | Neg nx, Pos ny => - let (q, r) := N.div_eucl nx ny in - if N.eq_bool N.zero r + let (q, r) := NN.div_eucl nx ny in + if NN.eqb NN.zero r then (Neg q, zero) - else (Neg (N.succ q), Pos (N.sub ny r)) + else (Neg (NN.succ q), Pos (NN.sub ny r)) | Neg nx, Neg ny => - let (q, r) := N.div_eucl nx ny in + 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:=N.spec_pos x); - destruct (N.to_Z x) as [|px|px]_eqn:EQx; + 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) = Zdiv_eucl (to_Z x) (to_Z y). + (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 (N.spec_div_eucl x y); destruct (N.div_eucl x y); auto. + generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y); auto. (* Pos Neg *) - generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r). + 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; intros Hr Hq; rewrite N.spec_eq_bool, N.spec_0, Hr; - simpl; rewrite Hq, N.spec_0; auto). + try (injection 1; intros Hr Hq; 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 Zdiv_eucl. destruct (Zdiv_eucl_POS px (Zpos py)) as (q',r'). + unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r'). intros (EQ,MOD). injection 1. intros Hr' Hq'. - rewrite N.spec_eq_bool, N.spec_0, Hr'. + rewrite NN.spec_eqb, NN.spec_0, Hr'. break_nonneg r pr EQr. - subst; simpl. rewrite N.spec_0; auto. - subst. lazy iota beta delta [Zeq_bool Zcompare]. - rewrite N.spec_sub, N.spec_succ, EQy, EQr. f_equal. omega with *. + 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 (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r). + 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; intros Hr Hq; rewrite N.spec_eq_bool, N.spec_0, Hr; - simpl; rewrite Hq, N.spec_0; auto). + try (injection 1; intros Hr Hq; 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 Zdiv_eucl. destruct (Zdiv_eucl_POS px (Zpos py)) as (q',r'). + unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r'). intros (EQ,MOD). injection 1. intros Hr' Hq'. - rewrite N.spec_eq_bool, N.spec_0, Hr'. + rewrite NN.spec_eqb, NN.spec_0, Hr'. break_nonneg r pr EQr. - subst; simpl. rewrite N.spec_0; auto. - subst. lazy iota beta delta [Zeq_bool Zcompare]. - rewrite N.spec_sub, N.spec_succ, EQy, EQr. f_equal. omega with *. + 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 (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r). + 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; intros Hr Hq; rewrite Hr, Hq; auto). simpl. intros <-; auto. @@ -407,8 +468,8 @@ Module Make (N:NType) <: ZType. 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, Zdiv. - case div_eucl; case Zdiv_eucl; simpl; auto. + 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. @@ -417,25 +478,69 @@ Module Make (N:NType) <: ZType. 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, Zmod. - case div_eucl; case Zdiv_eucl; simpl; auto. + 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 (N.gcd nx ny) - | Pos nx, Neg ny => Pos (N.gcd nx ny) - | Neg nx, Pos ny => Pos (N.gcd nx ny) - | Neg nx, Neg ny => Pos (N.gcd nx ny) + | 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) = Zgcd (to_Z a) (to_Z b). + Theorem spec_gcd: forall a b, to_Z (gcd a b) = Z.gcd (to_Z a) (to_Z b). Proof. - unfold gcd, Zgcd, to_Z; intros [x | x] [y | y]; rewrite N.spec_gcd; unfold Zgcd; - auto; case N.to_Z; simpl; auto with zarith; - try rewrite Zabs_Zopp; auto; - case N.to_Z; simpl; auto with zarith. + 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 := @@ -445,12 +550,212 @@ Module Make (N:NType) <: ZType. | Gt => minus_one end. - Lemma spec_sgn : forall x, to_Z (sgn x) = Zsgn (to_Z x). + Lemma spec_sgn : forall x, to_Z (sgn x) = Z.sgn (to_Z x). Proof. - intros. unfold sgn. rewrite spec_compare. case Zcompare_spec. + intros. unfold sgn. rewrite spec_compare. case Z.compare_spec. rewrite spec_0. intros <-; auto. - rewrite spec_0, spec_1. symmetry. rewrite Zsgn_pos; auto. - rewrite spec_0, spec_m1. symmetry. rewrite Zsgn_neg; auto with zarith. + 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. |