Timings for Z.v
Require Import Classes.interfaces.canonical_names.
Require Import Algebra.AbGroups.
Require Import Algebra.Rings.CRing.
Require Import Spaces.Int Spaces.Pos.
Require Import WildCat.Core.
(** In this file we define the ring Z of integers. The underlying abelian group is already defined in Algebra.AbGroups.Z. Many of the ring axioms are proven and made opaque. Typically, everything inside IsCRing can be opaque since we will only ever rewrite along them and they are hprops. This also means we don't have to be too careful with how our proofs are structured. This allows us to freely use tactics such as rewrite. It would perhaps be possible to shorten many of the proofs here, but it would probably be unneeded due to the opacicty. *)
(** The ring of integers *)
Definition cring_Z : CRing.
exact int_mul_add_distr_l.
Local Open Scope mc_scope.
(** Multiplication of a ring element by an integer. *)
(** We call this a "catamorphism" which is the name of the map from an initial object. It seems to be a more common terminology in computer science. *)
Definition cring_catamorphism_fun (R : CRing) (z : cring_Z) : R
:= match z with
| neg z => pos_peano_rec R (-1) (fun n nr => -1 + nr) z
| 0%int => 0
| pos z => pos_peano_rec R 1 (fun n nr => 1 + nr) z
end.
(** TODO: remove these (they will be cleaned up in the future)*)
(** Left multiplication is an equivalence *)
Local Instance isequiv_group_left_op {G} `{IsGroup G}
: forall (x : G), IsEquiv (fun t => sg_op x t).
srapply isequiv_adjointify.
all: refine (associativity _ _ _ @ _ @ left_identity y).
all: refine (ap (fun x => x * y) _).
(** Right multiplication is an equivalence *)
Local Instance isequiv_group_right_op {G} `{IsGroup G}
: forall x:G, IsEquiv (fun y => sg_op y x).
srapply isequiv_adjointify.
1: exact (fun y => sg_op y (- x)).
all: refine ((associativity _ _ _)^ @ _ @ right_identity y).
all: refine (ap (y *.) _).
Global Instance issemigrouppreserving_cring_catamorphism_fun_plus (R : CRing)
: IsSemiGroupPreserving (Aop:=cring_plus) (Bop:=cring_plus)
(cring_catamorphism_fun R : cring_Z -> R).
(** Unfortunately, due to how we have defined things we need to seperate this out into 9 cases. *)
(** Some of these cases are easy however *)
2,5,8: cbn; by rewrite right_identity.
3,4: symmetry; apply left_identity.
(** This leaves us with four cases to consider *)
(** x < 0 , y < 0 *)
change (cring_catamorphism_fun R ((neg x) + (neg y))%int
= (cring_catamorphism_fun R (neg x)) + (cring_catamorphism_fun R (neg y))).
induction y as [|y IHy] using pos_peano_ind.
rewrite pos_peano_rec_beta_pos_succ.
rewrite 2 pos_peano_rec_beta_pos_succ.
rewrite simple_associativity.
rewrite (commutativity _ (-1)).
rewrite <- simple_associativity.
induction y as [|y IHy] using pos_peano_ind; intro x.
induction x as [|x] using pos_peano_ind.
1: symmetry; cbn; apply left_inverse.
rewrite pos_peano_rec_beta_pos_succ.
rewrite int_pos_sub_succ_r.
cbn; rewrite <- simple_associativity.
apply (rng_moveL_Vr (R:=R)).
induction x as [|x IHx] using pos_peano_ind.
rewrite int_pos_sub_succ_l.
cbn; apply (rng_moveL_Vr (R:=R)).
by rewrite pos_peano_rec_beta_pos_succ.
rewrite int_pos_sub_succ_succ.
rewrite 2 pos_peano_rec_beta_pos_succ.
rewrite (commutativity (-1)).
rewrite simple_associativity.
rewrite <- (simple_associativity _ _ 1).
induction y as [|y IHy] using pos_peano_ind; intro x.
induction x as [|x] using pos_peano_ind.
1: symmetry; cbn; apply right_inverse.
rewrite pos_peano_rec_beta_pos_succ.
rewrite (commutativity 1).
rewrite <- simple_associativity.
rewrite int_pos_sub_succ_l.
cbn; by rewrite right_inverse, right_identity.
induction x as [|x IHx] using pos_peano_ind.
rewrite int_pos_sub_succ_r.
rewrite pos_peano_rec_beta_pos_succ.
rewrite simple_associativity.
rewrite (right_inverse 1).
rewrite int_pos_sub_succ_succ.
rewrite 2 pos_peano_rec_beta_pos_succ.
rewrite (commutativity 1).
rewrite simple_associativity.
rewrite <- (simple_associativity _ _ (-1)).
rewrite (right_inverse 1).
induction y as [|y IHy] using pos_peano_ind.
rewrite pos_peano_rec_beta_pos_succ.
rewrite 2 pos_peano_rec_beta_pos_succ.
rewrite simple_associativity.
rewrite simple_associativity.
rewrite (commutativity 1).
Lemma cring_catamorphism_fun_negate {R} x
: cring_catamorphism_fun R (- x) = - cring_catamorphism_fun R x.
snrapply (groups.preserves_negate _).
snrapply Build_IsMonoidPreserving.
Lemma cring_catamorphism_fun_pos_mult {R} x y
: cring_catamorphism_fun R (pos x * pos y)%int
= cring_catamorphism_fun R (pos x) * cring_catamorphism_fun R (pos y).
induction x as [|x IHx] using pos_peano_ind; intro y.
change (cring_catamorphism_fun R (pos (pos_succ x * y)%pos)
= cring_catamorphism_fun R (pos (pos_succ x)) * cring_catamorphism_fun R (pos y)).
refine (issemigrouppreserving_cring_catamorphism_fun_plus
R (pos (x * y)%pos) (pos y) @ _).
transitivity ((1 + cring_catamorphism_fun R (pos x)) * cring_catamorphism_fun R (pos y)).
2: simpl; by rewrite pos_peano_rec_beta_pos_succ.
rewrite (rng_dist_r (A:=R)).
(** Preservation of * (multiplication) *)
Global Instance issemigrouppreserving_cring_catamorphism_fun_mult (R : CRing)
: IsSemiGroupPreserving (Aop:=(.*.)) (Bop:=(.*.))
(cring_catamorphism_fun R : cring_Z -> R).
2,5,8: symmetry; apply (rng_mult_zero_r (A:=R)).
3,4: cbn; symmetry; rewrite (commutativity 0); apply (rng_mult_zero_r (A:=R)).
change (cring_catamorphism_fun R (pos (x * y)%pos)
= cring_catamorphism_fun R (- (pos x : cring_Z))
* cring_catamorphism_fun R (- (pos y : cring_Z))).
by rewrite 2 cring_catamorphism_fun_negate, cring_catamorphism_fun_pos_mult,
(rng_mult_negate_negate (A:=R)).
change (cring_catamorphism_fun R (- (pos (x * y)%pos : cring_Z))
= cring_catamorphism_fun R (- (pos x : cring_Z))
* cring_catamorphism_fun R (pos y)).
by rewrite 2 cring_catamorphism_fun_negate, cring_catamorphism_fun_pos_mult,
(rng_mult_negate_l (A:=R)).
change (cring_catamorphism_fun R (- (pos (x * y)%pos : cring_Z))
= cring_catamorphism_fun R (pos x)
* cring_catamorphism_fun R (- (pos y : cring_Z))).
by rewrite 2 cring_catamorphism_fun_negate, cring_catamorphism_fun_pos_mult,
(rng_mult_negate_r (A:=R)).
apply cring_catamorphism_fun_pos_mult.
(** This is a ring homomorphism *)
Definition rng_homo_int (R : CRing) : cring_Z $-> R.
snrapply Build_RingHomomorphism.
1: exact (cring_catamorphism_fun R).
(** The integers are the initial commutative ring *)
Global Instance isinitial_cring_Z : IsInitial cring_Z.
induction n using pos_peano_ind.
symmetry; rapply (rng_homo_minus_one (B:=R)).
rewrite pos_peano_rec_beta_pos_succ.
rewrite int_neg_pos_succ.
rewrite rng_homo_minus_one.
by rewrite 2 rng_homo_zero.
induction p using pos_peano_ind.
symmetry; rapply (rng_homo_one g).
rewrite pos_peano_rec_beta_pos_succ.
rewrite int_pos_pos_succ.