Record strictorder (A : Type)(R : A -> A -> CProp) : CProp :=
{so_trans : Ctransitive R;
so_asym : antisymmetric R}.
Record is_COrdField (F : CField)
(less : CCSetoid_relation F) (leEq : Relation F)
(greater : CCSetoid_relation F) (grEq : Relation F) : CProp :=
{ax_less_strorder : strictorder less;
ax_plus_resp_less : forall x y, less x y -> forall z, less (x[+]z) (y[+]z);
ax_mult_resp_pos : forall x y, less 0 x -> less 0 y -> less 0 (x[*]y);
ax_less_conf_ap : forall x y, ⇔ (x [#] y) (less x y or less y x);
def_leEq : forall x y, (leEq x y) <-> (~ (less y x));
def_greater : forall x y, ⇔ (greater x y) (less y x);
def_grEq : forall x y, (grEq x y) <-> (leEq y x)}.
Record COrdField : Type :=
{cof_crr :> CField;
cof_less : CCSetoid_relation cof_crr;
cof_leEq : cof_crr -> cof_crr -> Prop;
cof_greater : CCSetoid_relation cof_crr;
cof_grEq : cof_crr -> cof_crr -> Prop;
cof_proof : is_COrdField cof_crr cof_less cof_leEq cof_greater cof_grEq}.
In the names of lemmas, < is written as less and "0 < "
is written as pos.
Infix "<" := cof_less (at level 70, no associativity).
Infix ">" := cof_greater (at level 70, no associativity).
Infix "≤" := cof_leEq (at level 70, no associativity).
Infix "[>=]" := cof_grEq (at level 70, no associativity).
Definition default_greater (X:CField) (lt:CCSetoid_relation X) : CCSetoid_relation X.
Defined.
Definition default_leEq (X:CField) (lt:CCSetoid_relation X) : Relation X :=
(fun x y => (~ (lt y x))).
Definition default_grEq (X:CField) (le:Relation X) : Relation X :=
(fun x y => (le y x)).
In the names of lemmas, ≤ is written as leEq and
0 ≤ is written as nonneg.
Variable F : COrdField.
Lemma COrdField_is_COrdField : is_COrdField F cof_less (@cof_leEq F) cof_greater (@cof_grEq F).
Lemma less_strorder : strictorder (cof_less (c:=F)).
Lemma less_transitive_unfolded : forall x y z : F, x [<] y -> y [<] z -> x [<] z.
Lemma less_antisymmetric_unfolded : forall x y : F, x [<] y -> ~ (y [<] x).
Lemma less_irreflexive : irreflexive (cof_less (c:=F)).
Lemma less_irreflexive_unfolded : forall x : F, ~ (x [<] x).
Lemma plus_resp_less_rht : forall x y z : F, x [<] y -> x[+]z [<] y[+]z.
Lemma mult_resp_pos : forall x y : F, 0 [<] x -> 0 [<] y -> 0 [<] x[*]y.
Lemma less_conf_ap : forall x y : F, ⇔ (x [#] y) (x [<] y or y [<] x).
Lemma leEq_def : forall x y : F, (x [<=] y) <-> (~ (y [<] x)).
Lemma greater_def : forall x y : F, ⇔ (x [>] y) (y [<] x).
Lemma grEq_def : forall x y : F, (x [>=] y) <-> (y [<=] x).
Lemma less_wdr : forall x y z : F, x [<] y -> y [=] z -> x [<] z.
Lemma less_wdl : forall x y z : F, x [<] y -> x [=] z -> z [<] y.
End COrdField_axioms.
Section OrdField_basics.
Let in the rest of this section (and all subsections)
R be an ordered field
Variable R : COrdField.
Lemma less_imp_ap : forall x y : R, x [<] y -> x [#] y.
Lemma Greater_imp_ap : forall x y : R, y [<] x -> x [#] y.
Lemma ap_imp_less : forall x y : R, x [#] y -> x [<] y or y [<] x.
Lemma less_imp_ap : forall x y : R, x [<] y -> x [#] y.
Lemma Greater_imp_ap : forall x y : R, y [<] x -> x [#] y.
Lemma ap_imp_less : forall x y : R, x [#] y -> x [<] y or y [<] x.
Now properties which can be derived.
Lemma less_cotransitive : cotransitive (cof_less (c:=R)).
Lemma less_cotransitive_unfolded : forall x y : R, x [<] y -> forall z, x [<] z or z [<] y.
Lemma pos_ap_zero : forall x : R, 0 [<] x -> x [#] 0.
Lemma leEq_not_eq : forall x y : R, x [<=] y -> x [#] y -> x [<] y.
End OrdField_basics.
Section Basic_Properties_of_leEq.
Variable R : COrdField.
Lemma leEq_wdr : forall x y z : R, x [<=] y -> y [=] z -> x [<=] z.
Lemma leEq_wdl : forall x y z : R, x [<=] y -> x [=] z -> z [<=] y.
Lemma leEq_reflexive : forall x : R, x [<=] x.
Lemma eq_imp_leEq : forall x y : R, x [=] y -> x [<=] y.
Lemma leEq_imp_eq : forall x y : R, x [<=] y -> y [<=] x -> x [=] y.
Lemma lt_equiv_imp_eq : forall x x' : R,
(forall y, x [<] y -> x' [<] y) -> (forall y, x' [<] y -> x [<] y) -> x [=] x'.
Lemma less_leEq_trans : forall x y z : R, x [<] y -> y [<=] z -> x [<] z.
Lemma leEq_less_trans : forall x y z : R, x [<=] y -> y [<] z -> x [<] z.
Lemma leEq_transitive : forall x y z : R, x [<=] y -> y [<=] z -> x [<=] z.
Lemma less_leEq : forall x y : R, x [<] y -> x [<=] y.
Lemma leEq_or_leEq : forall x y:R, ~ (~ (x[<=]y or y[<=]x)).
Lemma leEq_less_or_equal : forall x y:R, x[<=]y -> ~ (~ (x[<]y or x[=]y)).
End Basic_Properties_of_leEq.
Section infinity_of_cordfields.
Infinity of ordered fields
In an ordered field we have that 1+1 and 1+1+1 and so on are all apart from zero. We first show this, so that we can define 2, 3 and so on. These are elements of NonZeros, so that we can write e.g. x/2.
Variable R : COrdField.
Lemma pos_one : (0:R) [<] 1.
Lemma nring_less_succ : forall m : N, (nring m:R) [<] nring (S m).
Lemma nring_less : forall m n : N, m < n -> (nring m:R) [<] nring n.
Lemma nring_leEq : forall m n : N, m <= n -> (nring m:R) [<=] nring n.
Lemma nring_apart : forall m n : N, m <> n -> (nring m:R) [#] nring n.
Lemma nring_ap_zero : forall n : N, n <> 0 -> nring (R:=R) n [#] 0.
Lemma nring_ap_zero' : forall n : N, 0 <> n -> nring (R:=R) n [#] 0.
Lemma nring_ap_zero_imp : forall n : N, nring (R:=R) n [#] 0 -> 0 <> n.
Definition Snring (n : N) := nring (R:=R) (S n).
Lemma pos_Snring : forall n : N, (0:R) [<] Snring n.
Lemma nringS_ap_zero : forall m : N, nring (R:=R) (S m) [#] 0.
Lemma nring_fac_ap_zero : forall n : N, nring (R:=R) (fac n) [#] 0.
Section up_to_four.
Properties of one up to four
In the names of lemmas, we denote the numbers 0,1,2,3,4 and so on, by zero, one, two etc.Lemma less_plusOne : forall x : R, x [<] x[+]1.
Lemma zero_lt_posplus1 : forall x : R, 0 [<=] x -> 0 [<] x[+]1.
Lemma plus_one_ext_less : forall x y : R, x [<] y -> x [<] y[+]1.
Lemma one_less_two : (1:R) [<] 2.
Lemma two_less_three : (2:R) [<] 3.
Lemma three_less_four : (3:R) [<] 4.
Lemma pos_two : (0:R) [<] 2.
Lemma one_less_three : (1:R) [<] 3.
Lemma two_less_four : (2:R) [<] 4.
Lemma pos_three : (0:R) [<] 3.
Lemma one_less_four : (1:R) [<] 4.
Lemma pos_four : (0:R) [<] 4.
Lemma two_ap_zero : 2 [#] (0:R).
Lemma three_ap_zero : 3 [#] (0:R).
Lemma four_ap_zero : 4 [#] (0:R).
End up_to_four.
Section More_than_four.
Lemma pos_six : (0:R) [<] 6.
Lemma pos_eight : (0:R) [<] 8.
Lemma pos_nine : (0:R) [<] 9.
Lemma pos_twelve : (0:R) [<] 12.
Lemma pos_sixteen : (0:R) [<] 16.
Lemma pos_eighteen : (0:R) [<] 18.
Lemma pos_twentyfour : (0:R) [<] 24.
Lemma pos_fortyeight : (0:R) [<] 48.
Lemma six_ap_zero : 6 [#] (0:R).
Lemma eight_ap_zero : 8 [#] (0:R).
Lemma nine_ap_zero : 9 [#] (0:R).
Lemma twelve_ap_zero : 12 [#] (0:R).
Lemma sixteen_ap_zero : 16 [#] (0:R).
Lemma eighteen_ap_zero : 18 [#] (0:R).
Lemma twentyfour_ap_zero : 24 [#] (0:R).
Lemma fortyeight_ap_zero : 48 [#] (0:R).
End More_than_four.
End infinity_of_cordfields.
Notation " x /OneNZ" := (x[/] 1[//]ring_non_triv _) (at level 20).
Notation " x /TwoNZ" := (x[/] 2[//]two_ap_zero _) (at level 20).
Notation " x /ThreeNZ" := (x[/] 3[//]three_ap_zero _) (at level 20).
Notation " x /FourNZ" := (x[/] 4[//]four_ap_zero _) (at level 20).
Notation " x /SixNZ" := (x[/] 6[//]six_ap_zero _) (at level 20).
Notation " x /EightNZ" := (x[/] 8[//]eight_ap_zero _) (at level 20).
Notation " x /NineNZ" := (x[/] 9[//]nine_ap_zero _) (at level 20).
Notation " x /TwelveNZ" := (x[/] 12[//]twelve_ap_zero _) (at level 20).
Notation " x /SixteenNZ" := (x[/] 16[//]sixteen_ap_zero _) (at level 20).
Notation " x /EighteenNZ" := (x[/] 18[//]eighteen_ap_zero _) (at level 20).
Notation " x /TwentyFourNZ" := (x[/] 24[//]twentyfour_ap_zero _) (at level 20).
Notation " x /FortyEightNZ" := (x[/] 48[//]fortyeight_ap_zero _) (at level 20).
Section consequences_of_infinity.
Variable F : COrdField.
Lemma square_eq : forall x a : F, a [#] 0 -> x[^]2 [=] a[^]2 -> {x [=] a} + {x [=] [--]a}.
Ordered fields have characteristic zero.
We do not use a special predicate for positivity,
(e.g. PosP), but just write 0 < x.
Reasons: it is more natural; in ordinary mathematics we also write 0 < x
(or x > 0).
Lemma plus_resp_less_lft : forall x y z : R, x [<] y -> z[+]x [<] z[+]y.
Lemma inv_resp_less : forall x y : R, x [<] y -> [--]y [<] [--]x.
Lemma minus_resp_less : forall x y z : R, x [<] y -> x[-]z [<] y[-]z.
Lemma minus_resp_less_rht : forall x y z : R, y [<] x -> z[-]x [<] z[-]y.
Lemma plus_resp_less_both : forall a b c d : R, a [<] b -> c [<] d -> a[+]c [<] b[+]d.
For versions of plus_resp_less_both where one < in the
assumption is replaced by ≤ .
Cancellation laws
Cancellation laws
Lemma plus_cancel_less : forall x y z : R, x[+]z [<] y[+]z -> x [<] y.
Lemma inv_cancel_less : forall x y : R, [--]x [<] [--]y -> y [<] x.
Lemmas where an operation is transformed into the inverse operation on the other side of an inequality are called laws for shifting. The names of laws for shifting start with shift_, and then come the operation and the inequality, in the order in which they occur in the conclusion. If the shifted operand changes sides w.r.t. the operation and its inverse, the name gets a prime.
It would be nicer to write the laws for shifting as bi-implications, However, it is impractical to use these in Coq.
Lemma shift_less_plus : forall x y z : R, x[-]z [<] y -> x [<] y[+]z.
Lemma shift_less_plus' : forall x y z : R, x[-]y [<] z -> x [<] y[+]z.
Lemma shift_less_minus : forall x y z : R, x[+]z [<] y -> x [<] y[-]z.
Lemma shift_less_minus' : forall x y z : R, z[+]x [<] y -> x [<] y[-]z.
Lemma shift_plus_less : forall x y z : R, x [<] z[-]y -> x[+]y [<] z.
Lemma shift_plus_less' : forall x y z : R, y [<] z[-]x -> x[+]y [<] z.
Lemma shift_minus_less : forall x y z : R, x [<] z[+]y -> x[-]y [<] z.
Lemma shift_minus_less' : forall x y z : R, x [<] y[+]z -> x[-]y [<] z.
Some special cases of laws for shifting.
Lemma shift_zero_less_minus : forall x y : R, x [<] y -> 0 [<] y[-]x.
Lemma shift_zero_less_minus' : forall x y : R, 0 [<] y[-]x -> x [<] y.
Lemma qltone : forall q : R, q [<] 1 -> q[-]1 [#] 0.
End addition.
Section multiplication.
Multiplication and division
By Convention in CFields, we often have redundant premises in lemmas. E.g. the informal statement ``for all x,y : R with 0 < x and 0 < y we have 0 < y/x'' is formalized as follows.forall (x y : R) x_, (0 [<] x) -> (0 [<] y) -> (0 [<] y[/]x[//]H)
We do this to keep it easy to use such lemmas.
Lemma mult_resp_less : forall x y z : R, x [<] y -> 0 [<] z -> x[*]z [<] y[*]z.
Lemma recip_resp_pos : forall (y : R) y_, 0 [<] y -> 0 [<] (1[/] y[//]y_).
Lemma div_resp_less_rht : forall (x y z : R) z_, x [<] y -> 0 [<] z -> (x[/] z[//]z_) [<] (y[/] z[//]z_).
Lemma div_resp_pos : forall (x y : R) x_, 0 [<] x -> 0 [<] y -> 0 [<] (y[/] x[//]x_).
Lemma mult_resp_less_lft : forall x y z : R, x [<] y -> 0 [<] z -> z[*]x [<] z[*]y.
Lemma mult_resp_less_both : forall x y u v : R,
0 [<=] x -> x [<] y -> 0 [<=] u -> u [<] v -> x[*]u [<] y[*]v.
Lemma recip_resp_less : forall (x y : R) x_ y_, 0 [<] x -> x [<] y -> (1[/] y[//]y_) [<] (1[/] x[//]x_).
Lemma div_resp_less : forall (x y z : R) z_, 0 [<] z -> x [<] y -> (x[/] z[//]z_) [<] (y[/] z[//]z_).
Cancellation laws
Laws for shifting
Lemma shift_div_less : forall (x y z : R) y_, 0 [<] y -> x [<] z[*]y -> (x[/] y[//]y_) [<] z.
Lemma shift_div_less' : forall (x y z : R) y_, 0 [<] y -> x [<] y[*]z -> (x[/] y[//]y_) [<] z.
Lemma shift_less_div : forall (x y z : R) y_, 0 [<] y -> x[*]y [<] z -> x [<] (z[/] y[//]y_).
Lemma shift_less_mult : forall (x y z : R) z_, 0 [<] z -> (x[/] z[//]z_) [<] y -> x [<] y[*]z.
Lemma shift_less_mult' : forall (x y z : R) y_, 0 [<] y -> (x[/] y[//]y_) [<] z -> x [<] y[*]z.
Lemma shift_mult_less : forall (x y z : R) y_, 0 [<] y -> x [<] (z[/] y[//]y_) -> x[*]y [<] z.
Other properties of multiplication and division
Lemma minusOne_less : forall x : R, x[-]1 [<] x.
Lemma swap_div : forall (x y z : R) y_ z_, 0 [<] y -> 0 [<] z -> (x[/] z[//]z_) [<] y -> (x[/] y[//]y_) [<] z.
Lemma eps_div_less_eps : forall (ε d : R) d_, 0 [<] ε -> 1 [<] d -> (ε[/] d[//]d_) [<] ε.
Lemma pos_div_two : forall ε : R, 0 [<] ε -> 0 [<] ε [/]2.
Lemma pos_div_two' : forall ε : R, 0 [<] ε -> ε [/]2 [<] ε.
Lemma pos_div_three : forall ε : R, 0 [<] ε -> 0 [<] ε [/]3.
Lemma pos_div_three' : forall ε : R, 0 [<] ε -> ε [/]3 [<] ε.
Lemma pos_div_four : forall ε : R, 0 [<] ε -> 0 [<] ε [/]4.
Lemma pos_div_four' : forall ε : R, 0 [<] ε -> ε [/]4 [<] ε.
Lemma pos_div_six : forall ε : R, 0 [<] ε -> 0 [<] ε [/]6.
Lemma pos_div_eight : forall ε : R, 0 [<] ε -> 0 [<] ε [/]8.
Lemma pos_div_nine : forall ε : R, 0 [<] ε -> 0 [<] ε [/]9.
Lemma pos_div_twelve : forall ε : R, 0 [<] ε -> 0 [<] ε [/]12.
Lemma pos_div_sixteen : forall ε : R, 0 [<] ε -> 0 [<] ε [/]16.
Lemma pos_div_eighteen : forall ε : R, 0 [<] ε -> 0 [<] ε [/]18.
Lemma pos_div_twentyfour : forall ε : R, 0 [<] ε -> 0 [<] ε [/]24.
Lemma pos_div_fortyeight : forall ε : R, 0 [<] ε -> 0 [<] ε [/]48.
End multiplication.
Section misc.
Lemma nring_pos : forall m : N, 0 < m -> 0 [<] nring (R:=R) m.
Lemma less_nring : forall n m : N, nring (R:=R) n [<] nring m -> n < m.
Lemma pos_nring_fac : forall n : N, 0 [<] nring (R:=R) (fac n).
Lemma Smallest_less_Average : forall a b : R, a [<] b -> a [<] (a[+]b) [/]2.
Lemma Average_less_Greatest : forall a b : R, a [<] b -> (a[+]b) [/]2 [<] b.
Lemma Sum_resp_less : forall (f g : N -> R) a b, a <= b ->
(forall i, a <= i -> i <= b -> f i [<] g i) -> ∑ a b f [<] ∑ a b g.
Lemma Sumx_resp_less : forall n, 0 < n -> forall f g : forall i, i < n -> R,
(forall i H, f i H [<] g i H) -> Sumx f [<] Sumx g.
Lemma positive_Sum_two : forall x y : R, 0 [<] x[+]y -> 0 [<] x or 0 [<] y.
Lemma positive_Sumx : forall n (f : forall i, i < n -> R),
nat_less_n_fun f -> 0 [<] Sumx f -> {i : N | {H : i < n | 0 [<] f i H}}.
Lemma negative_Sumx : forall n (f : forall i, i < n -> R),
nat_less_n_fun f -> Sumx f [<] 0 -> {i : N | {H : i < n | f i H [<] 0}}.
End misc.
End Properties_of_Ordering.
Add Parametric Morphism c : (@cof_leEq c) with signature (@cs_eq (cof_crr c)) ==> (@cs_eq c) ==> iff as cof_leEq_wd.
Qed.