@@ -71,206 +70,206 @@
-
Canonical rat_subType :=
Eval hnf in [subType for valq].
-
Definition rat_eqMixin :=
[eqMixin of rat by <:].
+
Canonical rat_subType :=
Eval hnf in [subType for valq].
+
Definition rat_eqMixin :=
[eqMixin of rat by <:].
Canonical rat_eqType :=
EqType rat rat_eqMixin.
-
Definition rat_choiceMixin :=
[choiceMixin of rat by <:].
+
Definition rat_choiceMixin :=
[choiceMixin of rat by <:].
Canonical rat_choiceType :=
ChoiceType rat rat_choiceMixin.
-
Definition rat_countMixin :=
[countMixin of rat by <:].
+
Definition rat_countMixin :=
[countMixin of rat by <:].
Canonical rat_countType :=
CountType rat rat_countMixin.
-
Canonical rat_subCountType :=
[subCountType of rat].
+
Canonical rat_subCountType :=
[subCountType of rat].
-
Definition numq x :=
nosimpl (
(valq x).1).
-
Definition denq x :=
nosimpl (
(valq x).2).
+
Definition numq x :=
nosimpl (
(valq x).1).
+
Definition denq x :=
nosimpl (
(valq x).2).
-
Lemma denq_gt0 x : 0
< denq x.
-
Hint Resolve denq_gt0.
+
Lemma denq_gt0 x : 0
< denq x.
+
Hint Resolve denq_gt0 :
core.
Definition denq_ge0 x :=
ltrW (
denq_gt0 x).
-
Lemma denq_lt0 x :
(denq x < 0
) = false.
+
Lemma denq_lt0 x :
(denq x < 0
) = false.
-
Lemma denq_neq0 x :
denq x != 0.
-
Hint Resolve denq_neq0.
+
Lemma denq_neq0 x :
denq x != 0.
+
Hint Resolve denq_neq0 :
core.
-
Lemma denq_eq0 x :
(denq x == 0
) = false.
+
Lemma denq_eq0 x :
(denq x == 0
) = false.
-
Lemma coprime_num_den x :
coprime `|numq x| `|denq x|.
+
Lemma coprime_num_den x :
coprime `|numq x| `|denq x|.
-
Fact RatK x P : @
Rat (numq x, denq x) P = x.
+
Fact RatK x P : @
Rat (numq x, denq x) P = x.
-
Fact fracq_subproof :
∀ x :
int × int,
+
Fact fracq_subproof :
∀ x :
int × int,
let n :=
-
if x.2 == 0
then 0
else
-
(-1
) ^ ((x.2 < 0
) (+) (x.1 < 0
)) × (`|x.1| %/ gcdn `|x.1| `|x.2|)%:Z in
-
let d :=
if x.2 == 0
then 1
else (`|x.2| %/ gcdn `|x.1| `|x.2|)%:Z in
-
(0
< d) && (coprime `|n| `|d|).
+
if x.2 == 0
then 0
else
+
(-1
) ^ ((x.2 < 0
) (+) (x.1 < 0
)) × (`|x.1| %/ gcdn `|x.1| `|x.2|)%:Z in
+
let d :=
if x.2 == 0
then 1
else (`|x.2| %/ gcdn `|x.1| `|x.2|)%:Z in
+
(0
< d) && (coprime `|n| `|d|).
-
Definition fracq (
x :
int × int) :=
nosimpl (@
Rat (_, _) (
fracq_subproof x)).
+
Definition fracq (
x :
int × int) :=
nosimpl (@
Rat (_, _) (
fracq_subproof x)).
-
Fact ratz_frac n :
ratz n = fracq (n, 1
).
+
Fact ratz_frac n :
ratz n = fracq (n, 1
).
-
Fact valqK x :
fracq (
valq x)
= x.
+
Fact valqK x :
fracq (
valq x)
= x.
-
Fact scalq_key :
unit.
-
Definition scalq_def x :=
sgr x.2 × (gcdn `|x.1| `|x.2|)%:Z.
-
Definition scalq :=
locked_with scalq_key scalq_def.
-
Canonical scalq_unlockable :=
[unlockable fun scalq].
+
Fact scalq_key :
unit.
+
Definition scalq_def x :=
sgr x.2 × (gcdn `|x.1| `|x.2|)%:Z.
+
Definition scalq :=
locked_with scalq_key scalq_def.
+
Canonical scalq_unlockable :=
[unlockable fun scalq].
-
Fact scalq_eq0 x :
(scalq x == 0
) = (x.2 == 0
).
+
Fact scalq_eq0 x :
(scalq x == 0
) = (x.2 == 0
).
-
Lemma sgr_scalq x :
sgr (
scalq x)
= sgr x.2.
+
Lemma sgr_scalq x :
sgr (
scalq x)
= sgr x.2.
-
Lemma signr_scalq x :
(scalq x < 0
) = (x.2 < 0
).
+
Lemma signr_scalq x :
(scalq x < 0
) = (x.2 < 0
).
Lemma scalqE x :
-
x.2 != 0
→ scalq x = (-1
) ^+ (
x.2 < 0)%
R × (gcdn `|x.1| `|x.2|)%:Z.
+
x.2 != 0
→ scalq x = (-1
) ^+ (
x.2 < 0)%
R × (gcdn `|x.1| `|x.2|)%:Z.
Fact valq_frac x :
-
x.2 != 0
→ x = (scalq x × numq (
fracq x)
, scalq x × denq (
fracq x)
).
+
x.2 != 0
→ x = (scalq x × numq (
fracq x)
, scalq x × denq (
fracq x)
).
-
Definition zeroq :=
fracq (0
, 1
).
-
Definition oneq :=
fracq (1
, 1
).
+
Definition zeroq :=
fracq (0
, 1
).
+
Definition oneq :=
fracq (1
, 1
).
-
Fact frac0q x :
fracq (0
, x) = zeroq.
+
Fact frac0q x :
fracq (0
, x) = zeroq.
-
Fact fracq0 x :
fracq (x, 0
) = zeroq.
+
Fact fracq0 x :
fracq (x, 0
) = zeroq.
-
CoInductive fracq_spec (
x :
int × int) :
int × int → rat → Type :=
- |
FracqSpecN of x.2 = 0 :
fracq_spec x (x.1, 0
) zeroq
- |
FracqSpecP k fx of k != 0 :
fracq_spec x (k × numq fx, k × denq fx) fx.
+
Variant fracq_spec (
x :
int × int) :
int × int → rat → Type :=
+ |
FracqSpecN of x.2 = 0 :
fracq_spec x (x.1, 0
) zeroq
+ |
FracqSpecP k fx of k != 0 :
fracq_spec x (k × numq fx, k × denq fx) fx.
Fact fracqP x :
fracq_spec x x (
fracq x).
-
Lemma rat_eqE x y :
(x == y) = (numq x == numq y) && (denq x == denq y).
+
Lemma rat_eqE x y :
(x == y) = (numq x == numq y) && (denq x == denq y).
-
Lemma sgr_denq x :
sgr (
denq x)
= 1.
+
Lemma sgr_denq x :
sgr (
denq x)
= 1.
-
Lemma normr_denq x :
`|denq x| = denq x.
+
Lemma normr_denq x :
`|denq x| = denq x.
-
Lemma absz_denq x :
`|denq x|%
N = denq x :> int.
+
Lemma absz_denq x :
`|denq x|%
N = denq x :> int.
-
Lemma rat_eq x y :
(x == y) = (numq x × denq y == numq y × denq x).
+
Lemma rat_eq x y :
(x == y) = (numq x × denq y == numq y × denq x).
-
Fact fracq_eq x y :
x.2 != 0
→ y.2 != 0
→
-
(fracq x == fracq y) = (x.1 × y.2 == y.1 × x.2).
+
Fact fracq_eq x y :
x.2 != 0
→ y.2 != 0
→
+
(fracq x == fracq y) = (x.1 × y.2 == y.1 × x.2).
-
Fact fracq_eq0 x :
(fracq x == zeroq) = (x.1 == 0
) || (x.2 == 0
).
+
Fact fracq_eq0 x :
(fracq x == zeroq) = (x.1 == 0
) || (x.2 == 0
).
-
Fact fracqMM x n d :
x != 0
→ fracq (x × n, x × d) = fracq (n, d).
+
Fact fracqMM x n d :
x != 0
→ fracq (x × n, x × d) = fracq (n, d).
-
Definition addq_subdef (
x y :
int × int) :=
(x.1 × y.2 + y.1 × x.2, x.2 × y.2).
-
Definition addq (
x y :
rat) :=
nosimpl fracq (
addq_subdef (
valq x) (
valq y)).
+
Definition addq_subdef (
x y :
int × int) :=
(x.1 × y.2 + y.1 × x.2, x.2 × y.2).
+
Definition addq (
x y :
rat) :=
nosimpl fracq (
addq_subdef (
valq x) (
valq y)).
-
Definition oppq_subdef (
x :
int × int) :=
(- x.1, x.2).
-
Definition oppq (
x :
rat) :=
nosimpl fracq (
oppq_subdef (
valq x)).
+
Definition oppq_subdef (
x :
int × int) :=
(- x.1, x.2).
+
Definition oppq (
x :
rat) :=
nosimpl fracq (
oppq_subdef (
valq x)).
-
Fact addq_subdefC :
commutative addq_subdef.
+
Fact addq_subdefC :
commutative addq_subdef.
-
Fact addq_subdefA :
associative addq_subdef.
+
Fact addq_subdefA :
associative addq_subdef.
-
Fact addq_frac x y :
x.2 != 0
→ y.2 != 0
→
-
(addq (
fracq x) (
fracq y)
) = fracq (
addq_subdef x y).
+
Fact addq_frac x y :
x.2 != 0
→ y.2 != 0
→
+
(addq (
fracq x) (
fracq y)
) = fracq (
addq_subdef x y).
-
Fact ratzD :
{morph ratz : x y / x + y >-> addq x y}.
+
Fact ratzD :
{morph ratz : x y / x + y >-> addq x y}.
-
Fact oppq_frac x :
oppq (
fracq x)
= fracq (
oppq_subdef x).
+
Fact oppq_frac x :
oppq (
fracq x)
= fracq (
oppq_subdef x).
-
Fact ratzN :
{morph ratz : x / - x >-> oppq x}.
+
Fact ratzN :
{morph ratz : x / - x >-> oppq x}.
-
Fact addqC :
commutative addq.
+
Fact addqC :
commutative addq.
-
Fact addqA :
associative addq.
+
Fact addqA :
associative addq.
-
Fact add0q :
left_id zeroq addq.
+
Fact add0q :
left_id zeroq addq.
-
Fact addNq :
left_inverse (
fracq (0
, 1
))
oppq addq.
+
Fact addNq :
left_inverse (
fracq (0
, 1
))
oppq addq.
Definition rat_ZmodMixin :=
ZmodMixin addqA addqC add0q addNq.
Canonical rat_ZmodType :=
ZmodType rat rat_ZmodMixin.
-
Definition mulq_subdef (
x y :
int × int) :=
nosimpl (x.1 × y.1, x.2 × y.2).
-
Definition mulq (
x y :
rat) :=
nosimpl fracq (
mulq_subdef (
valq x) (
valq y)).
+
Definition mulq_subdef (
x y :
int × int) :=
nosimpl (x.1 × y.1, x.2 × y.2).
+
Definition mulq (
x y :
rat) :=
nosimpl fracq (
mulq_subdef (
valq x) (
valq y)).
-
Fact mulq_subdefC :
commutative mulq_subdef.
+
Fact mulq_subdefC :
commutative mulq_subdef.
-
Fact mul_subdefA :
associative mulq_subdef.
+
Fact mul_subdefA :
associative mulq_subdef.
-
Definition invq_subdef (
x :
int × int) :=
nosimpl (x.2, x.1).
-
Definition invq (
x :
rat) :=
nosimpl fracq (
invq_subdef (
valq x)).
+
Definition invq_subdef (
x :
int × int) :=
nosimpl (x.2, x.1).
+
Definition invq (
x :
rat) :=
nosimpl fracq (
invq_subdef (
valq x)).
-
Fact mulq_frac x y :
(mulq (
fracq x) (
fracq y)
) = fracq (
mulq_subdef x y).
+
Fact mulq_frac x y :
(mulq (
fracq x) (
fracq y)
) = fracq (
mulq_subdef x y).
-
Fact ratzM :
{morph ratz : x y / x × y >-> mulq x y}.
+
Fact ratzM :
{morph ratz : x y / x × y >-> mulq x y}.
Fact invq_frac x :
-
x.1 != 0
→ x.2 != 0
→ invq (
fracq x)
= fracq (
invq_subdef x).
+
x.1 != 0
→ x.2 != 0
→ invq (
fracq x)
= fracq (
invq_subdef x).
-
Fact mulqC :
commutative mulq.
+
Fact mulqC :
commutative mulq.
-
Fact mulqA :
associative mulq.
+
Fact mulqA :
associative mulq.
-
Fact mul1q :
left_id oneq mulq.
+
Fact mul1q :
left_id oneq mulq.
-
Fact mulq_addl :
left_distributive mulq addq.
+
Fact mulq_addl :
left_distributive mulq addq.
-
Fact nonzero1q :
oneq != zeroq.
+
Fact nonzero1q :
oneq != zeroq.
Definition rat_comRingMixin :=
@@ -279,16 +278,16 @@
Canonical rat_comRing :=
Eval hnf in ComRingType rat mulqC.
-
Fact mulVq x :
x != 0
→ mulq (
invq x)
x = 1.
+
Fact mulVq x :
x != 0
→ mulq (
invq x)
x = 1.
-
Fact invq0 :
invq 0
= 0.
+
Fact invq0 :
invq 0
= 0.
Definition RatFieldUnitMixin :=
FieldUnitMixin mulVq invq0.
Canonical rat_unitRing :=
Eval hnf in UnitRingType rat RatFieldUnitMixin.
-
Canonical rat_comUnitRing :=
Eval hnf in [comUnitRingType of rat].
+
Canonical rat_comUnitRing :=
Eval hnf in [comUnitRingType of rat].
Fact rat_field_axiom :
GRing.Field.mixin_of rat_unitRing.
@@ -300,28 +299,37 @@
Canonical rat_fieldType :=
FieldType rat rat_field_axiom.
-
Lemma numq_eq0 x :
(numq x == 0
) = (x == 0
).
+
Canonical rat_countZmodType :=
[countZmodType of rat].
+
Canonical rat_countRingType :=
[countRingType of rat].
+
Canonical rat_countComRingType :=
[countComRingType of rat].
+
Canonical rat_countUnitRingType :=
[countUnitRingType of rat].
+
Canonical rat_countComUnitRingType :=
[countComUnitRingType of rat].
+
Canonical rat_countIdomainType :=
[countIdomainType of rat].
+
Canonical rat_countFieldType :=
[countFieldType of rat].
-
Notation "n %:Q" := (
(n : int)%:~R : rat)
+
Lemma numq_eq0 x :
(numq x == 0
) = (x == 0
).
+
+
+
Notation "n %:Q" := (
(n : int)%:~R : rat)
(
at level 2,
left associativity,
format "n %:Q") :
ring_scope.
-
Hint Resolve denq_neq0 denq_gt0 denq_ge0.
+
Hint Resolve denq_neq0 denq_gt0 denq_ge0 :
core.
Definition subq (
x y :
rat) :
rat := (
addq x (
oppq y)).
Definition divq (
x y :
rat) :
rat := (
mulq x (
invq y)).
-
Notation "0" :=
zeroq :
rat_scope.
-
Notation "1" :=
oneq :
rat_scope.
-
Infix "+" :=
addq :
rat_scope.
-
Notation "- x" := (
oppq x) :
rat_scope.
-
Infix "×" :=
mulq :
rat_scope.
-
Notation "x ^-1" := (
invq x) :
rat_scope.
-
Infix "-" :=
subq :
rat_scope.
-
Infix "/" :=
divq :
rat_scope.
+
Notation "0" :=
zeroq :
rat_scope.
+
Notation "1" :=
oneq :
rat_scope.
+
Infix "+" :=
addq :
rat_scope.
+
Notation "- x" := (
oppq x) :
rat_scope.
+
Infix "×" :=
mulq :
rat_scope.
+
Notation "x ^-1" := (
invq x) :
rat_scope.
+
Infix "-" :=
subq :
rat_scope.
+
Infix "/" :=
divq :
rat_scope.
@@ -330,21 +338,21 @@
ratz should not be used, %:Q should be used instead