Commit 1e30d5bf authored by Guillaume Melquiond's avatar Guillaume Melquiond

Use ZOdiv and ZOmod symmetric operators instead of biased Zdiv and Zmod operators.

parent e425e5db
......@@ -18,6 +18,7 @@ COPYING file for more details.
*)
Require Import Fcore_Raux.
Require Import ZOdiv.
Theorem Zmod_mod_mult :
forall n a b, (0 < a)%Z -> (0 <= b)%Z ->
......@@ -37,9 +38,33 @@ easy.
now elim Hb.
Qed.
Theorem ZOmod_eq :
forall a b,
ZOmod a b = (a - ZOdiv a b * b)%Z.
Proof.
intros a b.
rewrite (ZO_div_mod_eq a b) at 2.
ring.
Qed.
Theorem ZOmod_mod_mult :
forall n a b,
ZOmod (ZOmod n (a * b)) b = ZOmod n b.
Proof.
intros n a b.
assert (ZOmod n (a * b) = n + - (n / (a * b) * a) * b)%Z.
rewrite <- Zopp_mult_distr_l.
rewrite <- Zmult_assoc.
apply ZOmod_eq.
rewrite H.
apply ZO_mod_plus.
rewrite <- H.
apply ZOmod_sgn2.
Qed.
Theorem Zdiv_mod_mult :
forall n a b, (0 <= a)%Z -> (0 <= b)%Z ->
(Zmod n (a * b) / a)%Z = Zmod (n / a) b.
(Zdiv (Zmod n (a * b)) a) = Zmod (Zdiv n a) b.
Proof.
intros n a b Ha Hb.
destruct (Zle_lt_or_eq _ _ Ha) as [Ha'|Ha'].
......@@ -62,12 +87,49 @@ rewrite <- Ha'.
now rewrite 2!Zdiv_0_r, Zmod_0_l.
Qed.
Theorem ZOdiv_mod_mult :
forall n a b,
(ZOdiv (ZOmod n (a * b)) a) = ZOmod (ZOdiv n a) b.
Proof.
intros n a b.
destruct (Z_eq_dec a 0) as [Za|Za].
rewrite Za.
now rewrite 2!ZOdiv_0_r, ZOmod_0_l.
assert (ZOmod n (a * b) = n + - (n / a / b * b) * a)%Z.
rewrite (ZOmod_eq n (a * b)) at 1.
rewrite ZOdiv_ZOdiv.
ring.
rewrite H.
rewrite ZO_div_plus with (2 := Za).
apply sym_eq.
apply ZOmod_eq.
rewrite <- H.
apply ZOmod_sgn2.
Qed.
Theorem ZOmod_small_abs :
forall a b,
(Zabs a < b)%Z -> ZOmod a b = a.
Proof.
intros a b Ha.
destruct (Zle_or_lt 0 a) as [H|H].
apply ZOmod_small.
split.
exact H.
now rewrite Zabs_eq in Ha.
apply Zopp_inj.
rewrite <- ZOmod_opp_l.
apply ZOmod_small.
generalize (Zabs_non_eq a).
omega.
Qed.
Section Fcore_digits.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Definition Zdigit n k := Zmod (Zdiv n (Zpower beta k)) beta.
Definition Zdigit n k := ZOmod (ZOdiv n (Zpower beta k)) beta.
Theorem Zdigit_below :
forall n k,
......@@ -78,15 +140,25 @@ intros n [|k|k] Hk ; try easy.
now case n.
Qed.
Theorem Zdigit_ge_Zpower :
Theorem Zdigit_opp :
forall n k,
Zdigit (-n) k = Zopp (Zdigit n k).
Proof.
intros n k.
unfold Zdigit.
rewrite ZOdiv_opp_l.
apply ZOmod_opp_l.
Qed.
Theorem Zdigit_ge_Zpower_pos :
forall e n,
(0 <= n < Zpower beta e)%Z ->
forall k, (e <= k)%Z -> Zdigit n k = Z0.
Proof.
intros e n Hn k Hk.
unfold Zdigit.
rewrite Zdiv_small.
apply Zmod_0_l.
rewrite ZOdiv_small.
apply ZOmod_0_l.
split.
apply Hn.
apply Zlt_le_trans with (1 := proj2 Hn).
......@@ -106,23 +178,40 @@ apply Zle_ge.
now apply Zle_minus_le_0.
Qed.
Theorem Zdigit_not_0 :
Theorem Zdigit_ge_Zpower :
forall e n,
(Zabs n < Zpower beta e)%Z ->
forall k, (e <= k)%Z -> Zdigit n k = Z0.
Proof.
intros e [|n|n] Hn k.
easy.
apply Zdigit_ge_Zpower_pos.
now split.
intros He.
change (Zneg n) with (Zopp (Zpos n)).
rewrite Zdigit_opp.
rewrite Zdigit_ge_Zpower_pos with (2 := He).
apply Zopp_0.
now split.
Qed.
Theorem Zdigit_not_0_pos :
forall e n, (0 <= e)%Z ->
(Zpower beta e <= n < Zpower beta (e + 1))%Z ->
Zdigit n e <> Z0.
Proof.
intros e n He (Hn1,Hn2).
unfold Zdigit.
rewrite <- Zdiv_mod_mult.
rewrite Zmod_small.
rewrite <- ZOdiv_mod_mult.
rewrite ZOmod_small.
intros H.
apply Zle_not_lt with (1 := Hn1).
assert (beta ^ e > 0)%Z.
apply Zlt_gt.
now apply Zpower_gt_0.
rewrite (Z_div_mod_eq n (beta^e)) with (1 := H0).
rewrite (ZO_div_mod_eq n (beta ^ e)).
rewrite H, Zmult_0_r, Zplus_0_l.
now apply Z_mod_lt.
apply ZOmod_lt_pos_pos.
apply Zle_trans with (2 := Hn1).
apply Zpower_ge_0.
now apply Zpower_gt_0.
split.
apply Zle_trans with (2 := Hn1).
apply Zpower_ge_0.
......@@ -132,11 +221,6 @@ rewrite <- (Zmult_1_r beta) at 3.
apply Zpower_exp.
now apply Zle_ge.
easy.
apply Zpower_ge_0.
apply Zle_trans with 2%Z.
easy.
apply Zle_bool_imp_le.
apply beta.
Qed.
Theorem Zdigit_mul_pow :
......@@ -152,7 +236,7 @@ intros k' IHk' Hk' k H.
unfold Zdigit.
pattern k at 1 ; replace k with (k - k' + k')%Z by ring.
rewrite Zpower_exp by omega.
rewrite Zdiv_mult_cancel_r.
rewrite ZOdiv_mult_cancel_r.
apply refl_equal.
apply Zgt_not_eq.
now apply Zpower_gt_0.
......@@ -161,14 +245,14 @@ rewrite (Zdigit_below n) by omega.
unfold Zdigit.
replace k' with (k' - k + k)%Z by ring.
rewrite Zpower_exp by omega.
rewrite Zmult_assoc, Z_div_mult.
rewrite Zmult_assoc, ZO_div_mult.
replace (k' - k)%Z with (k' - k - 1 + 1)%Z by ring.
rewrite Zpower_exp by omega.
rewrite Zmult_assoc.
change (Zpower beta 1) with (beta * 1)%Z.
rewrite Zmult_1_r.
apply Z_mod_mult.
apply Zlt_gt.
apply ZO_mod_mult.
apply Zgt_not_eq.
now apply Zpower_gt_0.
rewrite Zdigit_below with (1 := H0).
apply sym_eq.
......@@ -182,7 +266,7 @@ Theorem Zdigit_div_pow :
Proof.
intros n k k' Hk Hk'.
unfold Zdigit.
rewrite Zdiv_Zdiv by apply Zpower_ge_0.
rewrite ZOdiv_ZOdiv.
rewrite Zplus_comm.
now rewrite Zpower_exp ; try apply Zle_ge.
Qed.
......@@ -195,25 +279,22 @@ Fixpoint Zsum_digit f k :=
Theorem Zsum_digit_digit :
forall n k,
Zsum_digit (Zdigit n) k = Zmod n (Zpower beta (Z_of_nat k)).
Zsum_digit (Zdigit n) k = ZOmod n (Zpower beta (Z_of_nat k)).
Proof.
intros n.
induction k.
apply sym_eq.
apply Zmod_1_r.
apply ZOmod_1_r.
simpl Zsum_digit.
rewrite IHk.
unfold Zdigit.
rewrite <- Zdiv_mod_mult.
rewrite <- (Zmod_mod_mult n beta).
rewrite <- ZOdiv_mod_mult.
rewrite <- (ZOmod_mod_mult n beta).
rewrite Zmult_comm.
replace (beta ^ Z_of_nat k * beta)%Z with (Zpower beta (Z_of_nat (S k))).
rewrite Zplus_comm, Zmult_comm.
apply sym_eq.
apply Z_div_mod_eq.
apply Zlt_gt.
apply Zpower_gt_0.
apply Zle_0_nat.
apply ZO_div_mod_eq.
rewrite inj_S.
unfold Zsucc.
rewrite Zpower_exp.
......@@ -222,16 +303,6 @@ apply Zmult_1_r.
apply Zle_ge.
apply Zle_0_nat.
easy.
apply Zlt_le_trans with 2%Z.
easy.
apply Zle_bool_imp_le.
apply beta.
apply Zpower_ge_0.
apply Zpower_ge_0.
apply Zle_trans with 2%Z.
easy.
apply Zle_bool_imp_le.
apply beta.
Qed.
Theorem Zpower_gt :
......@@ -286,33 +357,30 @@ destruct e1 as [|e1|e1] ; try easy.
apply Zpower_ge_0.
Qed.
Theorem Zdigit_ext_pos :
forall n1 n2, (0 <= n1)%Z -> (0 <= n2)%Z ->
Theorem Zdigit_ext :
forall n1 n2,
(forall k, Zdigit n1 k = Zdigit n2 k) ->
n1 = n2.
Proof.
intros n1 n2 Hn1 Hn2 H.
rewrite <- (Zmod_small n1 (Zpower beta (Zmax n1 n2))).
rewrite <- (Zmod_small n2 (Zpower beta (Zmax n1 n2))) at 2.
replace (Zmax n1 n2) with (Z_of_nat (Zabs_nat (Zmax n1 n2))).
intros n1 n2 H.
rewrite <- (ZOmod_small_abs n1 (Zpower beta (Zmax (Zabs n1) (Zabs n2)))).
rewrite <- (ZOmod_small_abs n2 (Zpower beta (Zmax (Zabs n1) (Zabs n2)))) at 2.
replace (Zmax (Zabs n1) (Zabs n2)) with (Z_of_nat (Zabs_nat (Zmax (Zabs n1) (Zabs n2)))).
rewrite <- 2!Zsum_digit_digit.
induction (Zabs_nat (Zmax n1 n2)).
induction (Zabs_nat (Zmax (Zabs n1) (Zabs n2))).
easy.
simpl.
now rewrite H, IHn.
rewrite inj_Zabs_nat.
apply Zabs_eq.
apply Zle_trans with (1 := Hn1).
apply Zle_trans with (Zabs n1).
apply Zabs_pos.
apply Zle_max_l.
split.
exact Hn2.
apply Zlt_le_trans with (Zpower beta n2).
apply Zlt_le_trans with (Zpower beta (Zabs n2)).
apply Zpower_gt.
apply Zpower_le.
apply Zle_max_r.
split.
exact Hn1.
apply Zlt_le_trans with (Zpower beta n1).
apply Zlt_le_trans with (Zpower beta (Zabs n1)).
apply Zpower_gt.
apply Zpower_le.
apply Zle_max_l.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment