Require Import ZArith.
Require Import Zquot.
Section Zmissing.
About Z
Theorem Zopp_le_cancel :
forall x y :
Z,
(-
y <= -
x)%
Z ->
Zle x y.
Proof.
intros x y Hxy.
apply Zplus_le_reg_r with (-
x -
y)%
Z.
now ring_simplify.
Qed.
Theorem Zgt_not_eq :
forall x y :
Z,
(
y <
x)%
Z -> (
x <>
y)%
Z.
Proof.
intros x y H Hn.
apply Zlt_irrefl with x.
now rewrite Hn at 1.
Qed.
End Zmissing.
Section Proof_Irrelevance.
Scheme eq_dep_elim :=
Induction for eq Sort Type.
Definition eqbool_dep P (
h1 :
P true)
b :=
match b return P b ->
Prop with
|
true =>
fun (
h2 :
P true) =>
h1 =
h2
|
false =>
fun (
h2 :
P false) =>
False
end.
Lemma eqbool_irrelevance :
forall (
b :
bool) (
h1 h2 :
b =
true),
h1 =
h2.
Proof.
End Proof_Irrelevance.
Section Even_Odd.
Zeven, used for rounding to nearest, ties to even
Definition Zeven (
n :
Z) :=
match n with
|
Zpos (
xO _) =>
true
|
Zneg (
xO _) =>
true
|
Z0 =>
true
|
_ =>
false
end.
Theorem Zeven_mult :
forall x y,
Zeven (
x *
y) =
orb (
Zeven x) (
Zeven y).
Proof.
now intros [|[xp|xp|]|[xp|xp|]] [|[yp|yp|]|[yp|yp|]].
Qed.
Theorem Zeven_opp :
forall x,
Zeven (-
x) =
Zeven x.
Proof.
now intros [|[n|n|]|[n|n|]].
Qed.
Theorem Zeven_ex :
forall x,
exists p,
x = (2 *
p +
if Zeven x then 0
else 1)%
Z.
Proof.
intros [|[
n|
n|]|[
n|
n|]].
now exists Z0.
now exists (
Zpos n).
now exists (
Zpos n).
now exists Z0.
exists (
Zneg n - 1)%
Z.
change (2 *
Zneg n - 1 = 2 * (
Zneg n - 1) + 1)%
Z.
ring.
now exists (
Zneg n).
now exists (-1)%
Z.
Qed.
Theorem Zeven_2xp1 :
forall n,
Zeven (2 *
n + 1) =
false.
Proof.
intros n.
destruct (
Zeven_ex (2 *
n + 1))
as (
p,
Hp).
revert Hp.
case (
Zeven (2 *
n + 1)) ;
try easy.
intros H.
apply False_ind.
omega.
Qed.
Theorem Zeven_plus :
forall x y,
Zeven (
x +
y) =
Bool.eqb (
Zeven x) (
Zeven y).
Proof.
intros x y.
destruct (
Zeven_ex x)
as (
px,
Hx).
rewrite Hx at 1.
destruct (
Zeven_ex y)
as (
py,
Hy).
rewrite Hy at 1.
replace (2 *
px + (
if Zeven x then 0
else 1) + (2 *
py + (
if Zeven y then 0
else 1)))%
Z
with (2 * (
px +
py) + ((
if Zeven x then 0
else 1) + (
if Zeven y then 0
else 1)))%
Z by ring.
case (
Zeven x) ;
case (
Zeven y).
rewrite Zplus_0_r.
now rewrite Zeven_mult.
apply Zeven_2xp1.
apply Zeven_2xp1.
replace (2 * (
px +
py) + (1 + 1))%
Z with (2 * (
px +
py + 1))%
Z by ring.
now rewrite Zeven_mult.
Qed.
End Even_Odd.
Section Zpower.
Theorem Zpower_plus :
forall n k1 k2, (0 <=
k1)%
Z -> (0 <=
k2)%
Z ->
Zpower n (
k1 +
k2) = (
Zpower n k1 *
Zpower n k2)%
Z.
Proof.
Theorem Zpower_Zpower_nat :
forall b e, (0 <=
e)%
Z ->
Zpower b e =
Zpower_nat b (
Zabs_nat e).
Proof.
Theorem Zpower_nat_S :
forall b e,
Zpower_nat b (
S e) = (
b *
Zpower_nat b e)%
Z.
Proof.
Theorem Zpower_pos_gt_0 :
forall b p, (0 <
b)%
Z ->
(0 <
Zpower_pos b p)%
Z.
Proof.
Theorem Zeven_Zpower :
forall b e, (0 <
e)%
Z ->
Zeven (
Zpower b e) =
Zeven b.
Proof.
Theorem Zeven_Zpower_odd :
forall b e, (0 <=
e)%
Z ->
Zeven b =
false ->
Zeven (
Zpower b e) =
false.
Proof.
The radix must be greater than 1
Record radix := {
radix_val :>
Z ;
radix_prop :
Zle_bool 2
radix_val =
true }.
Theorem radix_val_inj :
forall r1 r2,
radix_val r1 =
radix_val r2 ->
r1 =
r2.
Proof.
intros (
r1,
H1) (
r2,
H2)
H.
simpl in H.
revert H1.
rewrite H.
intros H1.
apply f_equal.
apply eqbool_irrelevance.
Qed.
Definition radix2 :=
Build_radix 2 (
refl_equal _).
Variable r :
radix.
Theorem radix_gt_0 : (0 <
r)%
Z.
Proof.
Theorem radix_gt_1 : (1 <
r)%
Z.
Proof.
Theorem Zpower_gt_1 :
forall p,
(0 <
p)%
Z ->
(1 <
Zpower r p)%
Z.
Proof.
Theorem Zpower_gt_0 :
forall p,
(0 <=
p)%
Z ->
(0 <
Zpower r p)%
Z.
Proof.
Theorem Zpower_ge_0 :
forall e,
(0 <=
Zpower r e)%
Z.
Proof.
Theorem Zpower_le :
forall e1 e2, (
e1 <=
e2)%
Z ->
(
Zpower r e1 <=
Zpower r e2)%
Z.
Proof.
Theorem Zpower_lt :
forall e1 e2, (0 <=
e2)%
Z -> (
e1 <
e2)%
Z ->
(
Zpower r e1 <
Zpower r e2)%
Z.
Proof.
Theorem Zpower_lt_Zpower :
forall e1 e2,
(
Zpower r (
e1 - 1) <
Zpower r e2)%
Z ->
(
e1 <=
e2)%
Z.
Proof.
End Zpower.
Section Div_Mod.
Theorem Zmod_mod_mult :
forall n a b, (0 <
a)%
Z -> (0 <=
b)%
Z ->
Zmod (
Zmod n (
a *
b))
b =
Zmod n b.
Proof.
Theorem ZOmod_eq :
forall a b,
Z.rem a b = (
a -
Z.quot a b *
b)%
Z.
Proof.
intros a b.
rewrite (Z.quot_rem' a b) at 2.
ring.
Qed.
Theorem ZOmod_mod_mult :
forall n a b,
Z.rem (
Z.rem n (
a *
b))
b =
Z.rem n b.
Proof.
Theorem Zdiv_mod_mult :
forall n a b, (0 <=
a)%
Z -> (0 <=
b)%
Z ->
(
Zdiv (
Zmod n (
a *
b))
a) =
Zmod (
Zdiv n a)
b.
Proof.
Theorem ZOdiv_mod_mult :
forall n a b,
(
Z.quot (
Z.rem n (
a *
b))
a) =
Z.rem (
Z.quot n a)
b.
Proof.
Theorem ZOdiv_small_abs :
forall a b,
(
Zabs a <
b)%
Z ->
Z.quot a b =
Z0.
Proof.
Theorem ZOmod_small_abs :
forall a b,
(
Zabs a <
b)%
Z ->
Z.rem a b =
a.
Proof.
Theorem ZOdiv_plus :
forall a b c, (0 <=
a *
b)%
Z ->
(
Z.quot (
a +
b)
c =
Z.quot a c +
Z.quot b c +
Z.quot (
Z.rem a c +
Z.rem b c)
c)%
Z.
Proof.
End Div_Mod.
Section Same_sign.
Theorem Zsame_sign_trans :
forall v u w,
v <>
Z0 ->
(0 <=
u *
v)%
Z -> (0 <=
v *
w)%
Z -> (0 <=
u *
w)%
Z.
Proof.
intros [|v|v] [|u|u] [|w|w] Zv Huv Hvw ; try easy ; now elim Zv.
Qed.
Theorem Zsame_sign_trans_weak :
forall v u w, (
v =
Z0 ->
w =
Z0) ->
(0 <=
u *
v)%
Z -> (0 <=
v *
w)%
Z -> (0 <=
u *
w)%
Z.
Proof.
intros [|v|v] [|u|u] [|w|w] Zv Huv Hvw ; try easy ; now discriminate Zv.
Qed.
Theorem Zsame_sign_imp :
forall u v,
(0 <
u -> 0 <=
v)%
Z ->
(0 < -
u -> 0 <= -
v)%
Z ->
(0 <=
u *
v)%
Z.
Proof.
Theorem Zsame_sign_odiv :
forall u v, (0 <=
v)%
Z ->
(0 <=
u *
Z.quot u v)%
Z.
Proof.
End Same_sign.
Boolean comparisons
Section Zeq_bool.
Inductive Zeq_bool_prop (
x y :
Z) :
bool ->
Prop :=
|
Zeq_bool_true_ :
x =
y ->
Zeq_bool_prop x y true
|
Zeq_bool_false_ :
x <>
y ->
Zeq_bool_prop x y false.
Theorem Zeq_bool_spec :
forall x y,
Zeq_bool_prop x y (
Zeq_bool x y).
Proof.
intros x y.
generalize (
Zeq_is_eq_bool x y).
case (
Zeq_bool x y) ;
intros (
H1,
H2) ;
constructor.
now apply H2.
intros H.
specialize (
H1 H).
discriminate H1.
Qed.
Theorem Zeq_bool_true :
forall x y,
x =
y ->
Zeq_bool x y =
true.
Proof.
Theorem Zeq_bool_false :
forall x y,
x <>
y ->
Zeq_bool x y =
false.
Proof.
End Zeq_bool.
Section Zle_bool.
Inductive Zle_bool_prop (
x y :
Z) :
bool ->
Prop :=
|
Zle_bool_true_ : (
x <=
y)%
Z ->
Zle_bool_prop x y true
|
Zle_bool_false_ : (
y <
x)%
Z ->
Zle_bool_prop x y false.
Theorem Zle_bool_spec :
forall x y,
Zle_bool_prop x y (
Zle_bool x y).
Proof.
intros x y.
generalize (
Zle_is_le_bool x y).
case Zle_bool ;
intros (
H1,
H2) ;
constructor.
now apply H2.
destruct (
Zle_or_lt x y)
as [
H|
H].
now specialize (
H1 H).
exact H.
Qed.
Theorem Zle_bool_true :
forall x y :
Z,
(
x <=
y)%
Z ->
Zle_bool x y =
true.
Proof.
Theorem Zle_bool_false :
forall x y :
Z,
(
y <
x)%
Z ->
Zle_bool x y =
false.
Proof.
End Zle_bool.
Section Zlt_bool.
Inductive Zlt_bool_prop (
x y :
Z) :
bool ->
Prop :=
|
Zlt_bool_true_ : (
x <
y)%
Z ->
Zlt_bool_prop x y true
|
Zlt_bool_false_ : (
y <=
x)%
Z ->
Zlt_bool_prop x y false.
Theorem Zlt_bool_spec :
forall x y,
Zlt_bool_prop x y (
Zlt_bool x y).
Proof.
intros x y.
generalize (
Zlt_is_lt_bool x y).
case Zlt_bool ;
intros (
H1,
H2) ;
constructor.
now apply H2.
destruct (
Zle_or_lt y x)
as [
H|
H].
exact H.
now specialize (
H1 H).
Qed.
Theorem Zlt_bool_true :
forall x y :
Z,
(
x <
y)%
Z ->
Zlt_bool x y =
true.
Proof.
Theorem Zlt_bool_false :
forall x y :
Z,
(
y <=
x)%
Z ->
Zlt_bool x y =
false.
Proof.
Theorem negb_Zle_bool :
forall x y :
Z,
negb (
Zle_bool x y) =
Zlt_bool y x.
Proof.
Theorem negb_Zlt_bool :
forall x y :
Z,
negb (
Zlt_bool x y) =
Zle_bool y x.
Proof.
End Zlt_bool.
Section Zcompare.
Inductive Zcompare_prop (
x y :
Z) :
comparison ->
Prop :=
|
Zcompare_Lt_ : (
x <
y)%
Z ->
Zcompare_prop x y Lt
|
Zcompare_Eq_ :
x =
y ->
Zcompare_prop x y Eq
|
Zcompare_Gt_ : (
y <
x)%
Z ->
Zcompare_prop x y Gt.
Theorem Zcompare_spec :
forall x y,
Zcompare_prop x y (
Zcompare x y).
Proof.
Theorem Zcompare_Lt :
forall x y,
(
x <
y)%
Z ->
Zcompare x y =
Lt.
Proof.
easy.
Qed.
Theorem Zcompare_Eq :
forall x y,
(
x =
y)%
Z ->
Zcompare x y =
Eq.
Proof.
Theorem Zcompare_Gt :
forall x y,
(
y <
x)%
Z ->
Zcompare x y =
Gt.
Proof.
intros x y.
apply Zlt_gt.
Qed.
End Zcompare.
Section cond_Zopp.
Definition cond_Zopp (
b :
bool)
m :=
if b then Zopp m else m.
Theorem abs_cond_Zopp :
forall b m,
Zabs (
cond_Zopp b m) =
Zabs m.
Proof.
Theorem cond_Zopp_Zlt_bool :
forall m,
cond_Zopp (
Zlt_bool m 0)
m =
Zabs m.
Proof.
End cond_Zopp.
Section fast_pow_pos.
Fixpoint Zfast_pow_pos (
v :
Z) (
e :
positive) :
Z :=
match e with
|
xH =>
v
|
xO e' =>
Z.square (
Zfast_pow_pos v e')
|
xI e' =>
Zmult v (
Z.square (
Zfast_pow_pos v e'))
end.
Theorem Zfast_pow_pos_correct :
forall v e,
Zfast_pow_pos v e =
Zpower_pos v e.
Proof.
End fast_pow_pos.
Section faster_div.
Lemma Zdiv_eucl_unique :
forall a b,
Zdiv_eucl a b = (
Zdiv a b,
Zmod a b).
Proof.
Fixpoint Zpos_div_eucl_aux1 (
a b :
positive) {
struct b} :=
match b with
|
xO b' =>
match a with
|
xO a' =>
let (
q,
r) :=
Zpos_div_eucl_aux1 a'
b'
in (
q, 2 *
r)%
Z
|
xI a' =>
let (
q,
r) :=
Zpos_div_eucl_aux1 a'
b'
in (
q, 2 *
r + 1)%
Z
|
xH => (
Z0,
Zpos a)
end
|
xH => (
Zpos a,
Z0)
|
xI _ =>
Z.pos_div_eucl a (
Zpos b)
end.
Lemma Zpos_div_eucl_aux1_correct :
forall a b,
Zpos_div_eucl_aux1 a b =
Z.pos_div_eucl a (
Zpos b).
Proof.
Definition Zpos_div_eucl_aux (
a b :
positive) :=
match Pos.compare a b with
|
Lt => (
Z0,
Zpos a)
|
Eq => (1%
Z,
Z0)
|
Gt =>
Zpos_div_eucl_aux1 a b
end.
Lemma Zpos_div_eucl_aux_correct :
forall a b,
Zpos_div_eucl_aux a b =
Z.pos_div_eucl a (
Zpos b).
Proof.
Definition Zfast_div_eucl (
a b :
Z) :=
match a with
|
Z0 => (0, 0)%
Z
|
Zpos a' =>
match b with
|
Z0 => (0, 0)%
Z
|
Zpos b' =>
Zpos_div_eucl_aux a'
b'
|
Zneg b' =>
let (
q,
r) :=
Zpos_div_eucl_aux a'
b'
in
match r with
|
Z0 => (-
q, 0)%
Z
|
Zpos _ => (-(
q + 1), (
b +
r))%
Z
|
Zneg _ => (-(
q + 1), (
b +
r))%
Z
end
end
|
Zneg a' =>
match b with
|
Z0 => (0, 0)%
Z
|
Zpos b' =>
let (
q,
r) :=
Zpos_div_eucl_aux a'
b'
in
match r with
|
Z0 => (-
q, 0)%
Z
|
Zpos _ => (-(
q + 1), (
b -
r))%
Z
|
Zneg _ => (-(
q + 1), (
b -
r))%
Z
end
|
Zneg b' =>
let (
q,
r) :=
Zpos_div_eucl_aux a'
b'
in (
q, (-
r)%
Z)
end
end.
Theorem Zfast_div_eucl_correct :
forall a b :
Z,
Zfast_div_eucl a b =
Zdiv_eucl a b.
Proof.
End faster_div.
Section Iter.
Context {
A :
Type}.
Variable (
f :
A ->
A).
Fixpoint iter_nat (
n :
nat) (
x :
A) {
struct n} :
A :=
match n with
|
S n' =>
iter_nat n' (
f x)
|
O =>
x
end.
Lemma iter_nat_plus :
forall (
p q :
nat) (
x :
A),
iter_nat (
p +
q)
x =
iter_nat p (
iter_nat q x).
Proof.
Lemma iter_nat_S :
forall (
p :
nat) (
x :
A),
iter_nat (
S p)
x =
f (
iter_nat p x).
Proof.
induction p.
easy.
simpl.
intros x.
apply IHp.
Qed.
Fixpoint iter_pos (
n :
positive) (
x :
A) {
struct n} :
A :=
match n with
|
xI n' =>
iter_pos n' (
iter_pos n' (
f x))
|
xO n' =>
iter_pos n' (
iter_pos n'
x)
|
xH =>
f x
end.
Lemma iter_pos_nat :
forall (
p :
positive) (
x :
A),
iter_pos p x =
iter_nat (
Pos.to_nat p)
x.
Proof.
End Iter.