diff options
Diffstat (limited to 'theories/Numbers/Integer/BigZ/ZMake.v')
-rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 379 |
1 files changed, 172 insertions, 207 deletions
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 98ad4c64..3196f11e 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: ZMake.v 11576 2008-11-10 19:13:15Z msozeau $ i*) +(*i $Id$ i*) Require Import ZArith. Require Import BigNumPrelude. @@ -17,31 +17,31 @@ Require Import ZSig. Open Scope Z_scope. -(** * ZMake - - A generic transformation from a structure of natural numbers +(** * ZMake + + A generic transformation from a structure of natural numbers [NSig.NType] to a structure of integers [ZSig.ZType]. *) Module Make (N:NType) <: ZType. - - Inductive t_ := + + Inductive t_ := | Pos : N.t -> t_ | Neg : N.t -> t_. - + Definition t := t_. Definition zero := Pos N.zero. Definition one := Pos N.one. Definition minus_one := Neg N.one. - Definition of_Z x := + Definition of_Z x := match x with | Zpos x => Pos (N.of_N (Npos x)) | Z0 => zero | Zneg x => Neg (N.of_N (Npos x)) end. - + Definition to_Z x := match x with | Pos nx => N.to_Z nx @@ -49,6 +49,7 @@ Module Make (N:NType) <: ZType. 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. @@ -85,72 +86,52 @@ Module Make (N:NType) <: ZType. | Neg nx, Neg ny => N.compare ny nx end. - Definition lt n m := compare n m = Lt. - Definition le n m := compare n m <> Gt. - 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_compare : + forall x y, compare x y = Zcompare (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. - Theorem spec_compare: forall x y, - match compare x y with - Eq => to_Z x = to_Z y - | Lt => to_Z x < to_Z y - | Gt => to_Z x > to_Z y - end. - unfold compare, to_Z; intros x y; case x; case y; clear x y; - intros x y; auto; generalize (N.spec_pos x) (N.spec_pos y). - generalize (N.spec_compare y x); case N.compare; auto with zarith. - generalize (N.spec_compare y N.zero); case N.compare; - try rewrite N.spec_0; auto with zarith. - generalize (N.spec_compare x N.zero); case N.compare; - rewrite N.spec_0; auto with zarith. - generalize (N.spec_compare x N.zero); case N.compare; - rewrite N.spec_0; auto with zarith. - generalize (N.spec_compare N.zero y); case N.compare; - try rewrite N.spec_0; auto with zarith. - generalize (N.spec_compare N.zero x); case N.compare; - rewrite N.spec_0; auto with zarith. - generalize (N.spec_compare N.zero x); case N.compare; - rewrite N.spec_0; auto with zarith. - generalize (N.spec_compare x y); case N.compare; auto with zarith. - Qed. - - Definition eq_bool x y := + Definition eq_bool x y := match compare x y with | Eq => true | _ => false end. - Theorem spec_eq_bool: forall x y, - if eq_bool x y then to_Z x = to_Z y else to_Z x <> to_Z y. - intros x y; unfold eq_bool; - generalize (spec_compare x y); case compare; auto with zarith. + Theorem spec_eq_bool: + forall x y, eq_bool x y = Zeq_bool (to_Z x) (to_Z y). + Proof. + unfold eq_bool, Zeq_bool; intros; rewrite spec_compare; reflexivity. Qed. - Definition cmp_sign x y := - match x, y with - | Pos nx, Neg ny => - if N.eq_bool ny N.zero then Eq else Gt - | Neg nx, Pos ny => - if N.eq_bool nx N.zero then Eq else Lt - | _, _ => Eq - end. + Definition lt n m := to_Z n < to_Z m. + Definition le n m := to_Z n <= to_Z m. + + 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). + Proof. + unfold min, Zmin. intros. rewrite spec_compare. destruct Zcompare; auto. + Qed. + + Theorem spec_max : forall n m, to_Z (max n m) = Zmax (to_Z n) (to_Z m). + Proof. + unfold max, Zmax. intros. rewrite spec_compare. destruct Zcompare; auto. + Qed. - Theorem spec_cmp_sign: forall x y, - match cmp_sign x y with - | Gt => 0 <= to_Z x /\ to_Z y < 0 - | Lt => to_Z x < 0 /\ 0 <= to_Z y - | Eq => True - end. - Proof. - intros [x | x] [y | y]; unfold cmp_sign; auto. - generalize (N.spec_eq_bool y N.zero); case N.eq_bool; auto. - rewrite N.spec_0; unfold to_Z. - generalize (N.spec_pos x) (N.spec_pos y); auto with zarith. - generalize (N.spec_eq_bool x N.zero); case N.eq_bool; auto. - rewrite N.spec_0; unfold to_Z. - generalize (N.spec_pos x) (N.spec_pos y); auto with zarith. - Qed. - Definition to_N x := match x with | Pos nx => nx @@ -160,21 +141,23 @@ 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). + 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. Qed. - - Definition opp x := - match x with + + 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 (N.succ n) @@ -186,12 +169,12 @@ Module Make (N:NType) <: ZType. end. 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; generalize (N.spec_compare N.zero x); case N.compare; - rewrite N.spec_0; simpl. + 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; auto with zarith. + intros HH; rewrite N.spec_pred, Zmax_r; auto with zarith. generalize (N.spec_pos x); auto with zarith. Qed. @@ -212,19 +195,13 @@ Module Make (N:NType) <: ZType. end | Neg nx, Neg ny => Neg (N.add nx ny) end. - + Theorem spec_add: forall x y, to_Z (add x y) = to_Z x + to_Z y. - unfold add, to_Z; intros [x | x] [y | y]. - exact (N.spec_add x y). - unfold zero; generalize (N.spec_compare x y); case N.compare. - rewrite N.spec_0; auto with zarith. - intros; rewrite N.spec_sub; try ring; auto with zarith. - intros; rewrite N.spec_sub; try ring; auto with zarith. - unfold zero; generalize (N.spec_compare x y); case N.compare. - rewrite N.spec_0; auto with zarith. - intros; rewrite N.spec_sub; try ring; auto with zarith. - intros; rewrite N.spec_sub; try ring; auto with zarith. - intros; rewrite N.spec_add; try ring; auto with zarith. + 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 *. Qed. Definition pred x := @@ -238,17 +215,17 @@ Module Make (N:NType) <: ZType. end. Theorem spec_pred: forall x, to_Z (pred x) = to_Z x - 1. - unfold pred, to_Z, minus_one; intros [x | x]. - generalize (N.spec_compare N.zero x); case N.compare; - rewrite N.spec_0; try rewrite N.spec_1; auto with zarith. - intros H; exact (N.spec_pred _ H). - generalize (N.spec_pos x); auto with zarith. - rewrite N.spec_succ; ring. + 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 *. Qed. Definition sub x y := match x, y with - | Pos nx, Pos ny => + | Pos nx, Pos ny => match N.compare nx ny with | Gt => Pos (N.sub nx ny) | Eq => zero @@ -256,7 +233,7 @@ Module Make (N:NType) <: ZType. end | Pos nx, Neg ny => Pos (N.add nx ny) | Neg nx, Pos ny => Neg (N.add nx ny) - | Neg nx, Neg ny => + | Neg nx, Neg ny => match N.compare nx ny with | Gt => Neg (N.sub nx ny) | Eq => zero @@ -265,20 +242,14 @@ Module Make (N:NType) <: ZType. end. Theorem spec_sub: forall x y, to_Z (sub x y) = to_Z x - to_Z y. - unfold sub, to_Z; intros [x | x] [y | y]. - unfold zero; generalize (N.spec_compare x y); case N.compare. - rewrite N.spec_0; auto with zarith. - intros; rewrite N.spec_sub; try ring; auto with zarith. - intros; rewrite N.spec_sub; try ring; auto with zarith. - rewrite N.spec_add; ring. - rewrite N.spec_add; ring. - unfold zero; generalize (N.spec_compare x y); case N.compare. - rewrite N.spec_0; auto with zarith. - intros; rewrite N.spec_sub; try ring; auto with zarith. - intros; rewrite N.spec_sub; try ring; auto with zarith. + 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 *. Qed. - Definition mul x y := + 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) @@ -286,25 +257,26 @@ Module Make (N:NType) <: ZType. | Neg nx, Neg ny => Pos (N.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. Qed. - Definition square x := + Definition square x := match x with | Pos nx => Pos (N.square nx) | Neg nx => Pos (N.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. Qed. Definition power_pos x p := match x with | Pos nx => Pos (N.power_pos nx p) - | Neg nx => + | Neg nx => match p with | xH => x | xO _ => Pos (N.power_pos nx p) @@ -313,9 +285,10 @@ Module Make (N:NType) <: ZType. end. Theorem spec_power_pos: forall x n, to_Z (power_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 |]; + unfold power_pos, to_Z; intros [x | x] [p | p |]; try rewrite N.spec_power_pos; try ring. assert (F: 0 <= 2 * Zpos p). assert (0 <= Zpos p); auto with zarith. @@ -329,15 +302,28 @@ Module Make (N:NType) <: ZType. rewrite F0; ring. Qed. + Definition power x n := + match n with + | N0 => one + | Npos p => power_pos x p + end. + + Theorem spec_power: forall x n, to_Z (power x n) = to_Z x ^ Z_of_N n. + Proof. + destruct n; simpl. rewrite N.spec_1; reflexivity. + apply spec_power_pos. + Qed. + + Definition sqrt x := match x with | Pos nx => Pos (N.sqrt nx) | Neg nx => Neg N.zero end. - - Theorem spec_sqrt: forall x, 0 <= to_Z x -> + Theorem spec_sqrt: forall x, 0 <= to_Z x -> to_Z (sqrt x) ^ 2 <= to_Z x < (to_Z (sqrt x) + 1) ^ 2. + Proof. unfold to_Z, sqrt; intros [x | x] H. exact (N.spec_sqrt x). replace (N.to_Z x) with 0. @@ -353,113 +339,75 @@ Module Make (N:NType) <: ZType. (Pos q, Pos r) | Pos nx, Neg ny => let (q, r) := N.div_eucl nx ny in - match N.compare N.zero r with - | Eq => (Neg q, zero) - | _ => (Neg (N.succ q), Neg (N.sub ny r)) - end + if N.eq_bool N.zero r + then (Neg q, zero) + else (Neg (N.succ q), Neg (N.sub ny r)) | Neg nx, Pos ny => let (q, r) := N.div_eucl nx ny in - match N.compare N.zero r with - | Eq => (Neg q, zero) - | _ => (Neg (N.succ q), Pos (N.sub ny r)) - end + if N.eq_bool N.zero r + then (Neg q, zero) + else (Neg (N.succ q), Pos (N.sub ny r)) | Neg nx, Neg ny => let (q, r) := N.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; + [clear H|clear H|elim H; reflexivity]. Theorem spec_div_eucl: forall x y, - to_Z y <> 0 -> - let (q,r) := div_eucl x y in - (to_Z q, to_Z r) = Zdiv_eucl (to_Z x) (to_Z y). - unfold div_eucl, to_Z; intros [x | x] [y | y] H. - assert (H1: 0 < N.to_Z y). - generalize (N.spec_pos y); auto with zarith. - generalize (N.spec_div_eucl x y H1); case N.div_eucl; auto. - assert (HH: 0 < N.to_Z y). - generalize (N.spec_pos y); auto with zarith. - generalize (N.spec_div_eucl x y HH); case N.div_eucl; auto. - intros q r; generalize (N.spec_pos x) HH; unfold Zdiv_eucl; - case_eq (N.to_Z x); case_eq (N.to_Z y); - try (intros; apply False_ind; auto with zarith; fail). - intros p He1 He2 _ _ H1; injection H1; intros H2 H3. - generalize (N.spec_compare N.zero r); case N.compare; - unfold zero; rewrite N.spec_0; try rewrite H3; auto. - rewrite H2; intros; apply False_ind; auto with zarith. - rewrite H2; intros; apply False_ind; auto with zarith. - intros p _ _ _ H1; discriminate H1. - intros p He p1 He1 H1 _. - generalize (N.spec_compare N.zero r); case N.compare. - change (- Zpos p) with (Zneg p). - unfold zero; lazy zeta. - rewrite N.spec_0; intros H2; rewrite <- H2. - intros H3; rewrite <- H3; auto. - rewrite N.spec_0; intros H2. - change (- Zpos p) with (Zneg p); lazy iota beta. - intros H3; rewrite <- H3; auto. - rewrite N.spec_succ; rewrite N.spec_sub. - generalize H2; case (N.to_Z r). - intros; apply False_ind; auto with zarith. - intros p2 _; rewrite He; auto with zarith. - change (Zneg p) with (- (Zpos p)); apply f_equal2 with (f := @pair Z Z); ring. - intros p2 H4; discriminate H4. - assert (N.to_Z r = (Zpos p1 mod (Zpos p))). - unfold Zmod, Zdiv_eucl; rewrite <- H3; auto. - case (Z_mod_lt (Zpos p1) (Zpos p)); auto with zarith. - rewrite N.spec_0; intros H2; generalize (N.spec_pos r); - intros; apply False_ind; auto with zarith. - assert (HH: 0 < N.to_Z y). - generalize (N.spec_pos y); auto with zarith. - generalize (N.spec_div_eucl x y HH); case N.div_eucl; auto. - intros q r; generalize (N.spec_pos x) HH; unfold Zdiv_eucl; - case_eq (N.to_Z x); case_eq (N.to_Z y); - try (intros; apply False_ind; auto with zarith; fail). - intros p He1 He2 _ _ H1; injection H1; intros H2 H3. - generalize (N.spec_compare N.zero r); case N.compare; - unfold zero; rewrite N.spec_0; try rewrite H3; auto. - rewrite H2; intros; apply False_ind; auto with zarith. - rewrite H2; intros; apply False_ind; auto with zarith. - intros p _ _ _ H1; discriminate H1. - intros p He p1 He1 H1 _. - generalize (N.spec_compare N.zero r); case N.compare. - change (- Zpos p1) with (Zneg p1). - unfold zero; lazy zeta. - rewrite N.spec_0; intros H2; rewrite <- H2. - intros H3; rewrite <- H3; auto. - rewrite N.spec_0; intros H2. - change (- Zpos p1) with (Zneg p1); lazy iota beta. - intros H3; rewrite <- H3; auto. - rewrite N.spec_succ; rewrite N.spec_sub. - generalize H2; case (N.to_Z r). - intros; apply False_ind; auto with zarith. - intros p2 _; rewrite He; auto with zarith. - intros p2 H4; discriminate H4. - assert (N.to_Z r = (Zpos p1 mod (Zpos p))). - unfold Zmod, Zdiv_eucl; rewrite <- H3; auto. - case (Z_mod_lt (Zpos p1) (Zpos p)); auto with zarith. - rewrite N.spec_0; generalize (N.spec_pos r); intros; apply False_ind; auto with zarith. - assert (H1: 0 < N.to_Z y). - generalize (N.spec_pos y); auto with zarith. - generalize (N.spec_div_eucl x y H1); case N.div_eucl; auto. - intros q r; generalize (N.spec_pos x) H1; unfold Zdiv_eucl; - case_eq (N.to_Z x); case_eq (N.to_Z y); - try (intros; apply False_ind; auto with zarith; fail). - change (-0) with 0; lazy iota beta; auto. - intros p _ _ _ _ H2; injection H2. - intros H3 H4; rewrite H3; rewrite H4; auto. - intros p _ _ _ H2; discriminate H2. - intros p He p1 He1 _ _ H2. - change (- Zpos p1) with (Zneg p1); lazy iota beta. - change (- Zpos p) with (Zneg p); lazy iota beta. - rewrite <- H2; auto. + let (q,r) := div_eucl x y in + (to_Z q, to_Z r) = Zdiv_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. + (* Pos Neg *) + generalize (N.spec_div_eucl x y); destruct (N.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). + 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'). + intros (EQ,MOD). injection 1. intros Hr' Hq'. + rewrite N.spec_eq_bool, N.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 *. + (* Neg Pos *) + generalize (N.spec_div_eucl x y); destruct (N.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). + 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'). + intros (EQ,MOD). injection 1. intros Hr' Hq'. + rewrite N.spec_eq_bool, N.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 *. + (* Neg Neg *) + generalize (N.spec_div_eucl x y); destruct (N.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. Qed. Definition div x y := fst (div_eucl x y). Definition spec_div: forall x y, - to_Z y <> 0 -> to_Z (div x y) = to_Z x / to_Z y. - intros x y H1; generalize (spec_div_eucl x y H1); unfold div, Zdiv. + 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 q r q11 r1 H; injection H; auto. Qed. @@ -467,8 +415,9 @@ Module Make (N:NType) <: ZType. Definition modulo x y := snd (div_eucl x y). Theorem spec_modulo: - forall x y, to_Z y <> 0 -> to_Z (modulo x y) = to_Z x mod to_Z y. - intros x y H1; generalize (spec_div_eucl x y H1); unfold modulo, Zmod. + 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 q r q11 r1 H; injection H; auto. Qed. @@ -478,14 +427,30 @@ Module Make (N:NType) <: ZType. | 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) + | Neg nx, Neg ny => Pos (N.gcd nx ny) end. Theorem spec_gcd: forall a b, to_Z (gcd a b) = Zgcd (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. 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) = Zsgn (to_Z x). + Proof. + intros. unfold sgn. rewrite spec_compare. case Zcompare_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. + Qed. + End Make. |