Library Coq.Reals.Cauchy.ConstructiveCauchyRealsMult
The multiplication and division of Cauchy reals.
WARNING: this file is experimental and likely to change in future releases.
Require
Import
QArith
Qabs
Qround
.
Require
Import
Logic.ConstructiveEpsilon
.
Require
Export
ConstructiveCauchyReals
.
Require
CMorphisms
.
Local Open
Scope
CReal_scope
.
Definition
QCauchySeq_bound
(
qn
:
positive
->
Q
) (
cvmod
:
positive
->
positive
)
:
positive
:=
match
Qnum
(
qn
(
cvmod
1%
positive
))
with
|
Z0
=> 1%
positive
|
Z.pos
p
=>
p
+
1
|
Z.neg
p
=>
p
+
1
end
.
Lemma
QCauchySeq_bounded_prop
(
qn
:
positive
->
Q
)
:
QCauchySeq
qn
->
forall
n
:
positive
,
Qlt
(
Qabs
(
qn
n
)) (
Z.pos
(
QCauchySeq_bound
qn
id
)
#
1).
Lemma
factorDenom
:
forall
(
a
:
Z
) (
b
d
:
positive
), (
(
a
#
(
d
*
b
)
)
==
(
1
#
d
)
*
(
a
#
b
)
)%
Q
.
Lemma
CReal_mult_cauchy
:
forall
(
x
y
:
CReal
) (
A
:
positive
),
(
forall
n
:
positive
, (
Qabs
(
proj1_sig
x
n
)
<
Z.pos
A
#
1)%
Q
)
->
(
forall
n
:
positive
, (
Qabs
(
proj1_sig
y
n
)
<
Z.pos
A
#
1)%
Q
)
->
QCauchySeq
(
fun
n
:
positive
=>
proj1_sig
x
(2
*
A
*
n
)%
positive
*
proj1_sig
y
(2
*
A
*
n
)%
positive
).
Definition
CReal_mult
(
x
y
:
CReal
) :
CReal
.
Infix
"
*" :=
CReal_mult
:
CReal_scope
.
Lemma
CReal_mult_comm
:
forall
x
y
:
CReal
,
x
*
y
==
y
*
x
.
Lemma
CReal_mult_proper_0_l
:
forall
x
y
:
CReal
,
y
==
0
->
x
*
y
==
0.
Lemma
CReal_mult_0_r
:
forall
r
,
r
*
0
==
0.
Lemma
CReal_mult_0_l
:
forall
r
, 0
*
r
==
0.
Lemma
CRealLt_0_aboveSig
:
forall
(
x
:
CReal
) (
n
:
positive
),
Qlt
(2
#
n
) (
proj1_sig
x
n
)
->
forall
p
:
positive
,
Pos.le
n
p
->
Qlt
(1
#
n
) (
proj1_sig
x
p
).
Lemma
CReal_mult_lt_0_compat_correct
:
forall
(
x
y
:
CReal
) (
H
: 0
<
x
) (
H0
: 0
<
y
),
(2
#
2
*
proj1_sig
H
*
proj1_sig
H0
<
proj1_sig
(
x
*
y
)%
CReal
(2
*
proj1_sig
H
*
proj1_sig
H0
)%
positive
-
proj1_sig
(
inject_Q
0) (2
*
proj1_sig
H
*
proj1_sig
H0
)%
positive
)%
Q
.
Definition
CReal_mult_lt_0_compat
:
forall
x
y
:
CReal
,
0
<
x
->
0
<
y
->
0
<
x
*
y
:=
fun
x
y
H
H0
=>
exist
_
(2
*
proj1_sig
H
*
proj1_sig
H0
)%
positive
(
CReal_mult_lt_0_compat_correct
x
y
H
H0
).
Lemma
CReal_mult_bound_indep
:
forall
(
x
y
:
CReal
) (
A
:
positive
)
(
xbound
:
forall
n
:
positive
, (
Qabs
(
proj1_sig
x
n
)
<
Z.pos
A
#
1)%
Q
)
(
ybound
:
forall
n
:
positive
, (
Qabs
(
proj1_sig
y
n
)
<
Z.pos
A
#
1)%
Q
),
x
*
y
==
exist
_
(
fun
n
:
positive
=>
proj1_sig
x
(2
*
A
*
n
)%
positive
*
proj1_sig
y
(2
*
A
*
n
)%
positive
)%
Q
(
CReal_mult_cauchy
x
y
A
xbound
ybound
).
Lemma
CReal_mult_plus_distr_l
:
forall
r1
r2
r3
:
CReal
,
r1
*
(
r2
+
r3
)
==
(
r1
*
r2
)
+
(
r1
*
r3
)
.
Lemma
CReal_mult_plus_distr_r
:
forall
r1
r2
r3
:
CReal
,
(
r2
+
r3
)
*
r1
==
(
r2
*
r1
)
+
(
r3
*
r1
)
.
Lemma
CReal_opp_mult_distr_r
:
forall
r1
r2
:
CReal
,
-
(
r1
*
r2
)
==
r1
*
(
-
r2
)
.
Lemma
CReal_mult_proper_l
:
forall
x
y
z
:
CReal
,
y
==
z
->
x
*
y
==
x
*
z
.
Lemma
CReal_mult_proper_r
:
forall
x
y
z
:
CReal
,
y
==
z
->
y
*
x
==
z
*
x
.
Lemma
CReal_mult_assoc
:
forall
x
y
z
:
CReal
,
(
x
*
y
)
*
z
==
x
*
(
y
*
z
)
.
Lemma
CReal_mult_1_l
:
forall
r
:
CReal
, 1
*
r
==
r
.
Lemma
CReal_isRingExt
:
ring_eq_ext
CReal_plus
CReal_mult
CReal_opp
CRealEq
.
Lemma
CReal_isRing
:
ring_theory
(
inject_Q
0) (
inject_Q
1)
CReal_plus
CReal_mult
CReal_minus
CReal_opp
CRealEq
.
Add
Parametric
Morphism
:
CReal_mult
with
signature
CRealEq
==>
CRealEq
==>
CRealEq
as
CReal_mult_morph
.
Instance
CReal_mult_morph_T
:
CMorphisms.Proper
(
CMorphisms.respectful
CRealEq
(
CMorphisms.respectful
CRealEq
CRealEq
))
CReal_mult
.
Add
Parametric
Morphism
:
CReal_opp
with
signature
CRealEq
==>
CRealEq
as
CReal_opp_morph
.
Instance
CReal_opp_morph_T
:
CMorphisms.Proper
(
CMorphisms.respectful
CRealEq
CRealEq
)
CReal_opp
.
Add
Parametric
Morphism
:
CReal_minus
with
signature
CRealEq
==>
CRealEq
==>
CRealEq
as
CReal_minus_morph
.
Instance
CReal_minus_morph_T
:
CMorphisms.Proper
(
CMorphisms.respectful
CRealEq
(
CMorphisms.respectful
CRealEq
CRealEq
))
CReal_minus
.
Add
Ring
CRealRing
:
CReal_isRing
.
Lemma
CReal_mult_1_r
:
forall
r
,
r
*
1
==
r
.
Lemma
CReal_opp_mult_distr_l
:
forall
r1
r2
:
CReal
,
-
(
r1
*
r2
)
==
(
-
r1
)
*
r2
.
Lemma
CReal_mult_lt_compat_l
:
forall
x
y
z
:
CReal
,
0
<
x
->
y
<
z
->
x
*
y
<
x
*
z
.
Lemma
CReal_mult_lt_compat_r
:
forall
x
y
z
:
CReal
,
0
<
x
->
y
<
z
->
y
*
x
<
z
*
x
.
Lemma
CReal_mult_eq_reg_l
:
forall
(
r
r1
r2
:
CReal
),
r
#
0
->
r
*
r1
==
r
*
r2
->
r1
==
r2
.
Lemma
CReal_abs_appart_zero
:
forall
(
x
:
CReal
) (
n
:
positive
),
Qlt
(2
#
n
) (
Qabs
(
proj1_sig
x
n
))
->
0
#
x
.
Field
Lemma
CRealArchimedean
:
forall
x
:
CReal
,
{
n
:
Z
&
x
<
inject_Q
(
n
#
1)
<
x
+
2
}
.
Definition
Rup_pos
(
x
:
CReal
)
:
{
n
:
positive
&
x
<
inject_Q
(
Z.pos
n
#
1)
}
.
Lemma
CRealLtDisjunctEpsilon
:
forall
a
b
c
d
:
CReal
,
(
CRealLtProp
a
b
\/
CRealLtProp
c
d
)
->
CRealLt
a
b
+
CRealLt
c
d
.
Lemma
CRealPosShift_correct
:
forall
(
x
:
CReal
) (
xPos
: 0
<
x
) (
n
:
positive
),
Pos.le
(
proj1_sig
xPos
)
n
->
Qlt
(1
#
proj1_sig
xPos
) (
proj1_sig
x
n
).
Lemma
CReal_inv_pos_cauchy
:
forall
(
x
:
CReal
) (
xPos
: 0
<
x
) (
k
:
positive
),
(
forall
n
:
positive
,
Pos.le
k
n
->
Qlt
(1
#
k
) (
proj1_sig
x
n
)
)
->
QCauchySeq
(
fun
n
:
positive
=>
/
proj1_sig
x
(
k
^
2
*
n
)%
positive
).
Definition
CReal_inv_pos
(
x
:
CReal
) (
xPos
: 0
<
x
) :
CReal
:=
exist
_
(
fun
n
:
positive
=>
/
proj1_sig
x
(
proj1_sig
xPos
^
2
*
n
)%
positive
)
(
CReal_inv_pos_cauchy
x
xPos
(
proj1_sig
xPos
) (
CRealPosShift_correct
x
xPos
)).
Definition
CReal_neg_lt_pos
:
forall
x
:
CReal
,
x
<
0
->
0
<
-
x
.
Definition
CReal_inv
(
x
:
CReal
) (
xnz
:
x
#
0) :
CReal
:=
match
xnz
with
|
inl
xNeg
=>
-
CReal_inv_pos
(
-
x
) (
CReal_neg_lt_pos
x
xNeg
)
|
inr
xPos
=>
CReal_inv_pos
x
xPos
end
.
Notation
"
/ x" := (
CReal_inv
x
) (
at
level
35,
right
associativity
) :
CReal_scope
.
Lemma
CReal_inv_0_lt_compat
:
forall
(
r
:
CReal
) (
rnz
:
r
#
0),
0
<
r
->
0
<
(
(/
r
)
rnz
)
.
Lemma
CReal_linear_shift
:
forall
(
x
:
CReal
) (
k
:
positive
),
QCauchySeq
(
fun
n
=>
proj1_sig
x
(
k
*
n
)%
positive
).
Lemma
CReal_linear_shift_eq
:
forall
(
x
:
CReal
) (
k
:
positive
),
x
==
(
exist
(
fun
n
:
positive
->
Q
=>
QCauchySeq
n
)
(
fun
n
:
positive
=>
proj1_sig
x
(
k
*
n
)%
positive
) (
CReal_linear_shift
x
k
)
)
.
Lemma
CReal_inv_l_pos
:
forall
(
r
:
CReal
) (
rnz
: 0
<
r
),
(
CReal_inv_pos
r
rnz
)
*
r
==
1.
Lemma
CReal_inv_l
:
forall
(
r
:
CReal
) (
rnz
:
r
#
0),
(
(/
r
)
rnz
)
*
r
==
1.
Lemma
CReal_inv_r
:
forall
(
r
:
CReal
) (
rnz
:
r
#
0),
r
*
(
(/
r
)
rnz
)
==
1.
Lemma
CReal_inv_1
:
forall
nz
: 1
#
0,
(/
1
)
nz
==
1.
Lemma
CReal_inv_mult_distr
:
forall
r1
r2
(
r1nz
:
r1
#
0) (
r2nz
:
r2
#
0) (
rmnz
:
(
r1
*
r2
)
#
0),
(/
(
r1
*
r2
))
rmnz
==
(/
r1
)
r1nz
*
(/
r2
)
r2nz
.
Lemma
Rinv_eq_compat
:
forall
x
y
(
rxnz
:
x
#
0) (
rynz
:
y
#
0),
x
==
y
->
(/
x
)
rxnz
==
(/
y
)
rynz
.
Lemma
CReal_mult_lt_reg_l
:
forall
r
r1
r2
, 0
<
r
->
r
*
r1
<
r
*
r2
->
r1
<
r2
.
Lemma
CReal_mult_lt_reg_r
:
forall
r
r1
r2
, 0
<
r
->
r1
*
r
<
r2
*
r
->
r1
<
r2
.
Lemma
CReal_mult_eq_reg_r
:
forall
r
r1
r2
,
r1
*
r
==
r2
*
r
->
r
#
0
->
r1
==
r2
.
Lemma
CReal_mult_eq_compat_l
:
forall
r
r1
r2
,
r1
==
r2
->
r
*
r1
==
r
*
r2
.
Lemma
CReal_mult_eq_compat_r
:
forall
r
r1
r2
,
r1
==
r2
->
r1
*
r
==
r2
*
r
.
Lemma
CReal_mult_pos_appart_zero
:
forall
x
y
:
CReal
, 0
<
x
*
y
->
0
#
x
.
Fixpoint
pow
(
r
:
CReal
) (
n
:
nat
) :
CReal
:=
match
n
with
|
O
=> 1
|
S
n
=>
r
*
(
pow
r
n
)
end
.
Lemma
CReal_mult_le_compat_l_half
:
forall
r
r1
r2
,
0
<
r
->
r1
<=
r2
->
r
*
r1
<=
r
*
r2
.
Lemma
CReal_invQ
:
forall
(
b
:
positive
) (
pos
:
Qlt
0 (
Z.pos
b
#
1)),
CReal_inv
(
inject_Q
(
Z.pos
b
#
1)) (
inr
(
CReal_injectQPos
(
Z.pos
b
#
1)
pos
))
==
inject_Q
(1
#
b
).
Definition
CRealQ_dense
(
a
b
:
CReal
)
:
a
<
b
->
{
q
:
Q
&
a
<
inject_Q
q
<
b
}
.
Lemma
inject_Q_mult
:
forall
q
r
:
Q
,
inject_Q
(
q
*
r
)
==
inject_Q
q
*
inject_Q
r
.
Definition
Rup_nat
(
x
:
CReal
)
:
{
n
:
nat
&
x
<
inject_Q
(
Z.of_nat
n
#
1)
}
.
Lemma
CReal_mult_le_0_compat
:
forall
(
a
b
:
CReal
),
0
<=
a
->
0
<=
b
->
0
<=
a
*
b
.
Lemma
CReal_mult_le_compat_l
:
forall
(
r
r1
r2
:
CReal
),
0
<=
r
->
r1
<=
r2
->
r
*
r1
<=
r
*
r2
.
Lemma
CReal_mult_le_compat_r
:
forall
(
r
r1
r2
:
CReal
),
0
<=
r
->
r1
<=
r2
->
r1
*
r
<=
r2
*
r
.
Lemma
CReal_mult_le_reg_l
:
forall
x
y
z
:
CReal
,
0
<
x
->
x
*
y
<=
x
*
z
->
y
<=
z
.
Lemma
CReal_mult_le_reg_r
:
forall
x
y
z
:
CReal
,
0
<
x
->
y
*
x
<=
z
*
x
->
y
<=
z
.