Definition distributive S (mult plus : CSetoid_bin_op S) :=
forall x y z, mult x (plus y z) [=] plus (mult x y) (mult x z).
Record is_CRing (G : CAbGroup) (1 : G) (mult : CSetoid_bin_op G) : CProp :=
{ax_mult_assoc : associative mult;
ax_mult_mon : is_CMonoid (Build_CSemiGroup G mult ax_mult_assoc) 1;
ax_mult_com : commutes mult;
ax_dist : distributive mult csg_op;
ax_non_triv : 1 [#] 0}.
Record CRing : Type :=
{cr_crr :> CAbGroup;
cr_one : cr_crr;
cr_mult : CSetoid_bin_op cr_crr;
cr_proof : is_CRing cr_crr cr_one cr_mult}.
Definition cr_plus := @csg_op.
Definition cr_inv := @cg_inv.
Definition cr_minus := cg_minus.
Notation 1 := (cr_one _).
forall x y z, mult x (plus y z) [=] plus (mult x y) (mult x z).
Record is_CRing (G : CAbGroup) (1 : G) (mult : CSetoid_bin_op G) : CProp :=
{ax_mult_assoc : associative mult;
ax_mult_mon : is_CMonoid (Build_CSemiGroup G mult ax_mult_assoc) 1;
ax_mult_com : commutes mult;
ax_dist : distributive mult csg_op;
ax_non_triv : 1 [#] 0}.
Record CRing : Type :=
{cr_crr :> CAbGroup;
cr_one : cr_crr;
cr_mult : CSetoid_bin_op cr_crr;
cr_proof : is_CRing cr_crr cr_one cr_mult}.
Definition cr_plus := @csg_op.
Definition cr_inv := @cg_inv.
Definition cr_minus := cg_minus.
Notation 1 := (cr_one _).
In the names of lemmas, we will denote 1 with one,
and × with mult.
Variable R : CRing.
Lemma CRing_is_CRing : is_CRing R 1 cr_mult.
Lemma mult_assoc : associative (cr_mult (c:=R)).
Lemma mult_commutes : commutes (cr_mult (c:=R)).
Lemma mult_mon : is_CMonoid (Build_CSemiGroup R cr_mult mult_assoc) 1.
Lemma dist : distributive (S:=R) cr_mult (cr_plus R).
Lemma ring_non_triv : (1:R) [#] 0.
Lemma mult_wd : forall x1 x2 y1 y2 : R, x1 [=] x2 -> y1 [=] y2 -> x1[*]y1 [=] x2[*]y2.
Lemma mult_wdl : forall x1 x2 y : R, x1 [=] x2 -> x1[*]y [=] x2[*]y.
Lemma mult_wdr : forall x y1 y2 : R, y1 [=] y2 -> x[*]y1 [=] x[*]y2.
End CRing_axioms.
Section Ring_constructions.
Lemma CRing_is_CRing : is_CRing R 1 cr_mult.
Lemma mult_assoc : associative (cr_mult (c:=R)).
Lemma mult_commutes : commutes (cr_mult (c:=R)).
Lemma mult_mon : is_CMonoid (Build_CSemiGroup R cr_mult mult_assoc) 1.
Lemma dist : distributive (S:=R) cr_mult (cr_plus R).
Lemma ring_non_triv : (1:R) [#] 0.
Lemma mult_wd : forall x1 x2 y1 y2 : R, x1 [=] x2 -> y1 [=] y2 -> x1[*]y1 [=] x2[*]y2.
Lemma mult_wdl : forall x1 x2 y : R, x1 [=] x2 -> x1[*]y [=] x2[*]y.
Lemma mult_wdr : forall x y1 y2 : R, y1 [=] y2 -> x[*]y1 [=] x[*]y2.
End CRing_axioms.
Section Ring_constructions.
The multiplicative monoid of a ring is defined as follows.
Definition Build_multCMonoid : CMonoid := Build_CMonoid _ _ (mult_mon R).
End Ring_constructions.
Section Ring_unfolded.
End Ring_constructions.
Section Ring_unfolded.
Variable R : CRing.
Lemma mult_assoc_unfolded : forall x y z : R, x[*] (y[*]z) [=] x[*]y[*]z.
Lemma mult_commut_unfolded : forall x y : R, x[*]y [=] y[*]x.
Lemma mult_one : forall x : R, x[*]1 [=] x.
Lemma one_mult : forall x : R, 1[*]x [=] x.
Lemma ring_dist_unfolded : forall x y z : R, x[*] (y[+]z) [=] x[*]y[+]x[*]z.
Lemma ring_distl_unfolded : forall x y z : R, (y[+]z) [*]x [=] y[*]x[+]z[*]x.
End Ring_unfolded.
Section Ring_basics.
Lemma mult_assoc_unfolded : forall x y z : R, x[*] (y[*]z) [=] x[*]y[*]z.
Lemma mult_commut_unfolded : forall x y : R, x[*]y [=] y[*]x.
Lemma mult_one : forall x : R, x[*]1 [=] x.
Lemma one_mult : forall x : R, 1[*]x [=] x.
Lemma ring_dist_unfolded : forall x y z : R, x[*] (y[+]z) [=] x[*]y[+]x[*]z.
Lemma ring_distl_unfolded : forall x y z : R, (y[+]z) [*]x [=] y[*]x[+]z[*]x.
End Ring_unfolded.
Section Ring_basics.
Variable R : CRing.
Lemma one_ap_zero : (1:R) [#] 0.
Definition is_zero_rht S (op : CSetoid_bin_op S) 0 : Prop := forall x, op x 0 [=] 0.
Definition is_zero_lft S (op : CSetoid_bin_op S) 0 : Prop := forall x, op 0 x [=] 0.
Lemma cring_mult_zero : forall x : R, x[*]0 [=] 0.
Lemma x_mult_zero : forall x y : R, y [=] 0 -> x[*]y [=] 0.
Lemma cring_mult_zero_op : forall x : R, 0[*]x [=] 0.
Lemma cring_inv_mult_lft : forall x y : R, x[*] [--]y [=] [--] (x[*]y).
Lemma cring_inv_mult_rht : forall x y : R, [--]x[*]y [=] [--] (x[*]y).
Lemma cring_mult_ap_zero :(forall x y : R, x[*]y [#] 0 -> x [#] 0):CProp.
Lemma cring_mult_ap_zero_op : (forall x y : R, x[*]y [#] 0 -> y [#] 0)
:CProp.
Lemma inv_mult_invol : forall x y : R, [--]x[*] [--]y [=] x[*]y.
Lemma ring_dist_minus : forall x y z : R, x[*] (y[-]z) [=] x[*]y[-]x[*]z.
Lemma ring_distl_minus : forall x y z : R, (y[-]z) [*]x [=] y[*]x[-]z[*]x.
Lemma mult_minus1 : forall x:R, [--]1 [*] x [=] [--]x.
Lemma ring_distr1 : forall a b1 b2:R,
a [*] (b1[-]b2) [=] a[*]b1 [-] a[*]b2.
Lemma ring_distr2 : forall a1 a2 b:R,
(a1[-]a2) [*] b [=] a1[*]b [-] a2[*]b.
End Ring_basics.
Lemma one_ap_zero : (1:R) [#] 0.
Definition is_zero_rht S (op : CSetoid_bin_op S) 0 : Prop := forall x, op x 0 [=] 0.
Definition is_zero_lft S (op : CSetoid_bin_op S) 0 : Prop := forall x, op 0 x [=] 0.
Lemma cring_mult_zero : forall x : R, x[*]0 [=] 0.
Lemma x_mult_zero : forall x y : R, y [=] 0 -> x[*]y [=] 0.
Lemma cring_mult_zero_op : forall x : R, 0[*]x [=] 0.
Lemma cring_inv_mult_lft : forall x y : R, x[*] [--]y [=] [--] (x[*]y).
Lemma cring_inv_mult_rht : forall x y : R, [--]x[*]y [=] [--] (x[*]y).
Lemma cring_mult_ap_zero :(forall x y : R, x[*]y [#] 0 -> x [#] 0):CProp.
Lemma cring_mult_ap_zero_op : (forall x y : R, x[*]y [#] 0 -> y [#] 0)
:CProp.
Lemma inv_mult_invol : forall x y : R, [--]x[*] [--]y [=] x[*]y.
Lemma ring_dist_minus : forall x y z : R, x[*] (y[-]z) [=] x[*]y[-]x[*]z.
Lemma ring_distl_minus : forall x y z : R, (y[-]z) [*]x [=] y[*]x[-]z[*]x.
Lemma mult_minus1 : forall x:R, [--]1 [*] x [=] [--]x.
Lemma ring_distr1 : forall a b1 b2:R,
a [*] (b1[-]b2) [=] a[*]b1 [-] a[*]b2.
Lemma ring_distr2 : forall a1 a2 b:R,
(a1[-]a2) [*] b [=] a1[*]b [-] a2[*]b.
End Ring_basics.
Ring Definitions
Some auxiliary functions and operations over a ring; especially geared towards CReals.
Variable R : CRing.
Fixpoint nexp (m : N) : R -> R :=
match m with
| O => fun _ : R => 1
| S n => fun x : R => nexp n x[*]x
end.
Lemma nexp_well_def : forall n, fun_wd (nexp n).
Lemma nexp_strong_ext : forall n, fun_strext (nexp n).
Definition nexp_op n := Build_CSetoid_un_op R (nexp n) (nexp_strong_ext n).
End exponentiation.
Notation "x ^ n" := (nexp_op _ n x) (at level 20).
Section nat_injection.
Fixpoint nexp (m : N) : R -> R :=
match m with
| O => fun _ : R => 1
| S n => fun x : R => nexp n x[*]x
end.
Lemma nexp_well_def : forall n, fun_wd (nexp n).
Lemma nexp_strong_ext : forall n, fun_strext (nexp n).
Definition nexp_op n := Build_CSetoid_un_op R (nexp n) (nexp_strong_ext n).
End exponentiation.
Notation "x ^ n" := (nexp_op _ n x) (at level 20).
Section nat_injection.
The injection of Coq natural numbers into a ring is called nring.
Note that this need not really be an injection; when it is, the ring is said
to have characteristic 0.
Fixpoint nring (m : N) : R :=
match m with
| O => 0
| S n => nring n[+]1
end.
Definition Char0 := forall n : N, 0 < n -> nring n [#] 0.
Lemma nring_comm_plus : forall n m, nring (n + m) [=] nring n[+]nring m.
Lemma nring_comm_mult : forall n m, nring (n * m) [=] nring n[*]nring m.
End nat_injection.
Notation 2 := (nring 2).
Notation 3 := (nring 3).
Notation 4 := (nring 4).
Notation 6 := (nring 6).
Notation 8 := (nring 8).
Notation 12 := (nring 12).
Notation 16 := (nring 16).
Notation 9 := (nring 9).
Notation 18 := (nring 18).
Notation 24 := (nring 24).
Notation 48 := (nring 48).
Lemma one_plus_one : forall R : CRing, 1[+]1 [=] (2:R).
Lemma x_plus_x : forall (R : CRing) (x : R), x[+]x [=] 2[*]x.
In a ring of characteristic zero, nring is really an injection.
Lemma nring_different : forall R, Char0 R -> forall i j, i <> j -> nring i [#] (nring j:R).
Section int_injection.
The injection of Coq integers into a ring is called zring. Again,
this need not really be an injection.
The first definition is now obsolete, having been replaced by a more efficient one. It is kept to avoid having to redo all the proofs.
The first definition is now obsolete, having been replaced by a more efficient one. It is kept to avoid having to redo all the proofs.
Definition zring_old k : R := caseZ_diff k (fun m n => nring m[-]nring n).
Lemma zring_old_zero : zring_old 0 [=] 0.
Lemma zring_old_diff : forall m n : N, zring_old (m - n) [=] nring m[-]nring n.
Lemma zring_old_plus_nat : forall n : N, zring_old n [=] nring n.
Lemma zring_old_inv_nat : forall n : N, zring_old (- n) [=] [--] (nring n).
Lemma zring_old_plus : forall i j, zring_old (i + j) [=] zring_old i[+]zring_old j.
Lemma zring_old_inv : forall i, zring_old (- i) [=] [--] (zring_old i).
Lemma zring_old_minus : forall i j, zring_old (i - j) [=] zring_old i[-]zring_old j.
Lemma zring_old_mult : forall i j, zring_old (i * j) [=] zring_old i[*]zring_old j.
Lemma zring_old_one : zring_old 1 [=] 1.
Lemma zring_old_inv_one : forall x, zring_old (-1) [*]x [=] [--]x.
The zring function can be defined directly. This is done here.
Fixpoint pring_aux (p : positive) (pow2 : R) {struct p} : R :=
match p with
| xH => pow2
| xO p => pring_aux p (2[*]pow2)
| xI p => pow2[+]pring_aux p (2[*]pow2)
end.
Definition pring (p : positive) : R := pring_aux p 1.
Definition zring (z : Z) : R :=
match z with
| Z0 => 0
| Zpos p => pring p
| Zneg p => [--] (pring p)
end.
Lemma pring_aux_lemma : forall p r r', r [=] r' -> pring_aux p r [=] pring_aux p r'.
Lemma double_nring : forall n, 2[*]nring (R:=R) n [=] nring (R:=R) (n + n).
Lemma pring_aux_nring : forall p n, pring_aux p (nring n) [=] nring (Pmult_nat p n).
Lemma pring_convert : forall p, pring p [=] nring (nat_of_P p).
Lemma zring_zring_old : forall z : Z, zring z [=] zring_old z.
Lemma zring_zero : zring 0 [=] 0.
Lemma zring_diff : forall m n : N, zring (m - n) [=] nring m[-]nring n.
Lemma zring_plus_nat : forall n : N, zring n [=] nring n.
Lemma zring_inv_nat : forall n : N, zring (- n) [=] [--] (nring n).
Lemma zring_plus : forall i j, zring (i + j) [=] zring i[+]zring j.
Lemma zring_inv : forall i, zring (- i) [=] [--] (zring i).
Lemma zring_minus : forall i j, zring (i - j) [=] zring i[-]zring j.
Lemma zring_mult : forall i j, zring (i * j) [=] zring i[*]zring j.
Lemma zring_one : zring 1 [=] 1.
Lemma zring_inv_one : forall x, zring (-1) [*]x [=] [--]x.
End int_injection.
Section Ring_sums.
Section infinite_ring_sums.
Fixpoint Sum_upto (f : N -> R) (n : N) {struct n} : R :=
match n with
| O => 0
| S x => f x[+]Sum_upto f x
end.
Lemma sum_upto_O : forall f : N -> R, Sum_upto f 0 [=] 0.
Definition Sum_from_upto f m n : R := Sum_upto f n[-]Sum_upto f m.
Fixpoint Sum_upto (f : N -> R) (n : N) {struct n} : R :=
match n with
| O => 0
| S x => f x[+]Sum_upto f x
end.
Lemma sum_upto_O : forall f : N -> R, Sum_upto f 0 [=] 0.
Definition Sum_from_upto f m n : R := Sum_upto f n[-]Sum_upto f m.
Here's an alternative def of Sum_from_upto, with a lemma that
it's equivalent to the original.
Definition seq_from (f : N -> R) (n i : N) : R := f (n + i).
Definition Sum_from_upto_alt f m n : R := Sum_upto (seq_from f m) (n - m).
End infinite_ring_sums.
Section ring_sums_over_lists.
Fixpoint RList_Mem (l : list R) (n : N) {struct n} : R :=
match l, n with
| nil, _ => 0
| cons a _, O => a
| cons _ k, S y => RList_Mem k y
end.
Fixpoint List_Sum_upto (l : list R) (n : N) {struct n} : R :=
match n with
| O => 0
| S x => RList_Mem l x[+]List_Sum_upto l x
end.
Lemma list_sum_upto_O : forall l : list R, List_Sum_upto l 0 [=] 0.
Definition List_Sum_from_upto l m n := List_Sum_upto l n[-]List_Sum_upto l m.
End ring_sums_over_lists.
End Ring_sums.
Section Dist_properties.
Variable R : CRing.
Lemma dist_1b : forall x y z : R, (x[+]y) [*]z [=] x[*]z[+]y[*]z.
Lemma dist_2a : forall x y z : R, z[*] (x[-]y) [=] z[*]x[-]z[*]y.
Lemma dist_2b : forall x y z : R, (x[-]y) [*]z [=] x[*]z[-]y[*]z.
Lemma mult_distr_sum0_lft : forall (f : N -> R) x n,
∑0 n (fun i => x[*]f i) [=] x[*]∑0 n f.
Lemma mult_distr_sum_lft : forall (f : N -> R) x m n,
∑ m n (fun i => x[*]f i) [=] x[*]∑ m n f.
Lemma mult_distr_sum_rht : forall (f : N -> R) x m n,
∑ m n (fun i => f i[*]x) [=] ∑ m n f[*]x.
Lemma sumx_const : forall n (x : R), Sumx (fun i (_ : i < n) => x) [=] nring n[*]x.
End Dist_properties.
Variable R : CRing.
Lemma dist_1b : forall x y z : R, (x[+]y) [*]z [=] x[*]z[+]y[*]z.
Lemma dist_2a : forall x y z : R, z[*] (x[-]y) [=] z[*]x[-]z[*]y.
Lemma dist_2b : forall x y z : R, (x[-]y) [*]z [=] x[*]z[-]y[*]z.
Lemma mult_distr_sum0_lft : forall (f : N -> R) x n,
∑0 n (fun i => x[*]f i) [=] x[*]∑0 n f.
Lemma mult_distr_sum_lft : forall (f : N -> R) x m n,
∑ m n (fun i => x[*]f i) [=] x[*]∑ m n f.
Lemma mult_distr_sum_rht : forall (f : N -> R) x m n,
∑ m n (fun i => f i[*]x) [=] ∑ m n f[*]x.
Lemma sumx_const : forall n (x : R), Sumx (fun i (_ : i < n) => x) [=] nring n[*]x.
End Dist_properties.
Section NExp_properties.
Variable R : CRing.
Lemma nexp_wd : forall (x y : R) n, x [=] y -> x[^]n [=] y[^]n.
Lemma nexp_strext : forall (x y : R) n, x[^]n [#] y[^]n -> x [#] y.
Lemma nexp_Sn : forall (x : R) n, x[*]x[^]n [=] x[^]S n.
Lemma nexp_plus : forall (x : R) m n, x[^]m[*]x[^]n [=] x[^] (m + n).
Lemma one_nexp : forall n : N, (1:R) [^]n [=] 1.
Lemma mult_nexp : forall (x y : R) n, (x[*]y) [^]n [=] x[^]n[*]y[^]n.
Lemma nexp_mult : forall (x : R) m n, (x[^]m) [^]n [=] x[^] (m * n).
Lemma zero_nexp : forall n, 0 < n -> (0:R) [^]n [=] 0.
Lemma inv_nexp_even : forall (x : R) n, even n -> [--]x[^]n [=] x[^]n.
Lemma inv_nexp_two : forall x : R, [--]x[^]2 [=] x[^]2.
Lemma inv_nexp_odd : forall (x : R) n, odd n -> [--]x[^]n [=] [--] (x[^]n).
Lemma nexp_one : forall x : R, x[^]1 [=] x.
Lemma nexp_two : forall x : R, x[^]2 [=] x[*]x.
Lemma inv_one_even_nexp : forall n : N, even n -> [--]1[^]n [=] (1:R).
Lemma inv_one_odd_nexp : forall n : N, odd n -> [--]1[^]n [=] [--] (1:R).
Lemma square_plus : forall x y : R, (x[+]y) [^]2 [=] x[^]2[+]y[^]2[+]2[*]x[*]y.
Lemma square_minus : forall x y : R, (x[-]y) [^]2 [=] x[^]2[+]y[^]2[-]2[*]x[*]y.
Lemma nexp_funny : forall x y : R, (x[+]y) [*] (x[-]y) [=] x[^]2[-]y[^]2.
Lemma nexp_funny' : forall x y : R, (x[-]y) [*] (x[+]y) [=] x[^]2[-]y[^]2.
End NExp_properties.
Add Parametric Morphism c n : (nexp c n) with signature (@cs_eq (cr_crr c)) ==> (@cs_eq c) as nexp_morph_wd.
Qed.
Section CRing_Ops.
Variable R : CRing.
Lemma nexp_wd : forall (x y : R) n, x [=] y -> x[^]n [=] y[^]n.
Lemma nexp_strext : forall (x y : R) n, x[^]n [#] y[^]n -> x [#] y.
Lemma nexp_Sn : forall (x : R) n, x[*]x[^]n [=] x[^]S n.
Lemma nexp_plus : forall (x : R) m n, x[^]m[*]x[^]n [=] x[^] (m + n).
Lemma one_nexp : forall n : N, (1:R) [^]n [=] 1.
Lemma mult_nexp : forall (x y : R) n, (x[*]y) [^]n [=] x[^]n[*]y[^]n.
Lemma nexp_mult : forall (x : R) m n, (x[^]m) [^]n [=] x[^] (m * n).
Lemma zero_nexp : forall n, 0 < n -> (0:R) [^]n [=] 0.
Lemma inv_nexp_even : forall (x : R) n, even n -> [--]x[^]n [=] x[^]n.
Lemma inv_nexp_two : forall x : R, [--]x[^]2 [=] x[^]2.
Lemma inv_nexp_odd : forall (x : R) n, odd n -> [--]x[^]n [=] [--] (x[^]n).
Lemma nexp_one : forall x : R, x[^]1 [=] x.
Lemma nexp_two : forall x : R, x[^]2 [=] x[*]x.
Lemma inv_one_even_nexp : forall n : N, even n -> [--]1[^]n [=] (1:R).
Lemma inv_one_odd_nexp : forall n : N, odd n -> [--]1[^]n [=] [--] (1:R).
Lemma square_plus : forall x y : R, (x[+]y) [^]2 [=] x[^]2[+]y[^]2[+]2[*]x[*]y.
Lemma square_minus : forall x y : R, (x[-]y) [^]2 [=] x[^]2[+]y[^]2[-]2[*]x[*]y.
Lemma nexp_funny : forall x y : R, (x[+]y) [*] (x[-]y) [=] x[^]2[-]y[^]2.
Lemma nexp_funny' : forall x y : R, (x[-]y) [*] (x[+]y) [=] x[^]2[-]y[^]2.
End NExp_properties.
Add Parametric Morphism c n : (nexp c n) with signature (@cs_eq (cr_crr c)) ==> (@cs_eq c) as nexp_morph_wd.
Qed.
Section CRing_Ops.
Functional Operations
Now for partial functions.
Let R be a ring and let F,G:(PartFunct R) with predicates respectively P and Q.
Variable R : CRing.
Variables F G : PartFunct R.
Section Part_Function_Mult.
Lemma part_function_mult_strext : forall x y (Hx : Conj P Q x) (Hy : Conj P Q y),
F x (Prj1 Hx) [*]G x (Prj2 Hx) [#] F y (Prj1 Hy) [*]G y (Prj2 Hy) -> x [#] y.
Definition Fmult := Build_PartFunct R _ (conj_wd (dom_wd _ F) (dom_wd _ G))
(fun x Hx => F x (Prj1 Hx) [*]G x (Prj2 Hx)) part_function_mult_strext.
End Part_Function_Mult.
Section Part_Function_Nth_Power.
Variable n : N.
Lemma part_function_nth_strext : forall x y Hx Hy, F x Hx[^]n [#] F y Hy[^]n -> x [#] y.
Definition Fnth := Build_PartFunct R _ (dom_wd R F)
(fun x Hx => F x Hx[^]n) part_function_nth_strext.
End Part_Function_Nth_Power.
Let R':R->CProp.
Variable R':R -> CProp.
Lemma included_FMult : ⊆ R' P -> ⊆ R' Q -> ⊆ R' (Dom Fmult).
Lemma included_FMult' : ⊆ R' (Dom Fmult) -> ⊆ R' P.
Lemma included_FMult'' : ⊆ R' (Dom Fmult) -> ⊆ R' Q.
Variable n:nat.
Lemma included_FNth : ⊆ R' P -> forall n, ⊆ R' (Dom (Fnth n)).
Lemma included_FNth' : forall n, ⊆ R' (Dom (Fnth n)) -> ⊆ R' (Dom F).
End CRing_Ops.
Definition Fscalmult (R:CRing) α F := Fmult R [-C-]α F.
Infix "{*}" := Fmult (at level 40, left associativity).
Infix "{**}" := Fscalmult (at level 40, left associativity).
Infix "{^}" := Fnth (at level 30, right associativity).
Section ScalarMultiplication.
Variable R : CRing.
Variable F : PartFunct R.
Variable R':R -> CProp.
Lemma included_FScalMult : ⊆ R' P -> forall c, ⊆ R' (Dom (c{**}F)).
Lemma included_FScalMult' : forall c, ⊆ R' (Dom (c{**}F)) -> ⊆ R' P.
End ScalarMultiplication.