Library HoTT.Classes.theory.rings
Require Import
HoTT.Classes.theory.groups
HoTT.Classes.theory.apartness.
Require Import
HoTT.Classes.interfaces.abstract_algebra.
Generalizable Variables R A B C f z.
Definition is_ne_0 `(x : R) `{Zero R} `{p : PropHolds (x ≠ 0)}
: x ≠ 0 := p.
Definition is_nonneg `(x : R) `{Le R} `{Zero R} `{p : PropHolds (0 ≤ x)}
: 0 ≤ x := p.
Definition is_pos `(x : R) `{Lt R} `{Zero R} `{p : PropHolds (0 < x)}
: 0 < x := p.
(* Lemma stdlib_semiring_theory R `{SemiRing R}
: Ring_theory.semi_ring_theory 0 1 (+) (.*.) (=).
Proof.
Qed.
*)
(* We cannot apply left_cancellation (.*.) z directly in case we have
no PropHolds (0 ≠ z) instance in the context. *)
Section cancellation.
Context `(op : A → A → A) `{!Zero A}.
Lemma left_cancellation_ne_0
`{∀ z, PropHolds (z ≠ 0) → LeftCancellation op z} z
: z ≠ 0 → LeftCancellation op z.
Proof. auto. Qed.
Lemma right_cancellation_ne_0
`{∀ z, PropHolds (z ≠ 0) → RightCancellation op z} z
: z ≠ 0 → RightCancellation op z.
Proof. auto. Qed.
Lemma right_cancel_from_left `{!Commutative op} `{!LeftCancellation op z}
: RightCancellation op z.
Proof.
intros x y E.
apply (left_cancellation op z).
rewrite 2!(commutativity (f:=op) z _).
assumption.
Qed.
End cancellation.
Section strong_cancellation.
Context `{IsApart A} (op : A → A → A).
Lemma strong_right_cancel_from_left `{!Commutative op}
`{!StrongLeftCancellation op z}
: StrongRightCancellation op z.
Proof.
intros x y E.
rewrite 2!(commutativity _ z).
apply (strong_left_cancellation op z);trivial.
Qed.
Global Instance strong_left_cancellation_cancel `{!StrongLeftCancellation op z}
: LeftCancellation op z | 20.
Proof.
intros x y E1.
apply tight_apart in E1;apply tight_apart;intros E2.
apply E1. apply (strong_left_cancellation op);trivial.
Qed.
Global Instance strong_right_cancellation_cancel `{!StrongRightCancellation op z}
: RightCancellation op z | 20.
Proof.
intros x y E1.
apply tight_apart in E1;apply tight_apart;intros E2.
apply E1. apply (strong_right_cancellation op);trivial.
Qed.
End strong_cancellation.
Section semiring_props.
Context `{IsSemiCRing R}.
(* Add Ring SR : (stdlib_semiring_theory R). *)
Instance mult_ne_0 `{!NoZeroDivisors R} x y
: PropHolds (x ≠ 0) → PropHolds (y ≠ 0) → PropHolds (x × y ≠ 0).
Proof.
intros Ex Ey Exy.
unfold PropHolds in ×.
apply (no_zero_divisors x); split; eauto.
Qed.
Global Instance plus_0_r: RightIdentity (+) 0 := right_identity.
Global Instance plus_0_l: LeftIdentity (+) 0 := left_identity.
Global Instance mult_1_l: LeftIdentity (.*.) 1 := left_identity.
Global Instance mult_1_r: RightIdentity (.*.) 1 := right_identity.
Global Instance plus_assoc: Associative (+) := simple_associativity.
Global Instance mult_assoc: Associative (.*.) := simple_associativity.
Global Instance plus_comm: Commutative (+) := commutativity.
Global Instance mult_comm: Commutative (.*.) := commutativity.
Global Instance mult_0_l: LeftAbsorb (.*.) 0 := left_absorb.
Global Instance mult_0_r: RightAbsorb (.*.) 0.
Proof.
intro. path_via (0 × x).
- apply mult_comm.
- apply left_absorb.
Qed.
Global Instance plus_mult_distr_r : RightDistribute (.*.) (+).
Proof.
intros x y z.
etransitivity;[|etransitivity].
- apply mult_comm.
- apply distribute_l.
- apply ap011;apply mult_comm.
Qed.
Lemma plus_mult_distr_l : LeftDistribute (.*.) (+).
Proof.
apply _.
Qed.
Global Instance: ∀ r : R, @IsMonoidPreserving R R (+) (+) 0 0 (r *.).
Proof.
repeat (constructor; try apply _).
- red. apply distribute_l.
- apply right_absorb.
Qed.
End semiring_props.
(* Due to bug 2528 *)
#[export]
Hint Extern 3 (PropHolds (_ × _ ≠ 0)) ⇒ eapply @mult_ne_0 : typeclass_instances.
Section semiringmor_props.
Context `{IsSemiRingPreserving A B f}.
Lemma preserves_0: f 0 = 0.
Proof. apply preserves_mon_unit. Qed.
Lemma preserves_1: f 1 = 1.
Proof. apply preserves_mon_unit. Qed.
Lemma preserves_mult: ∀ x y, f (x × y) = f x × f y.
Proof.
intros. apply preserves_sg_op.
Qed.
Lemma preserves_plus: ∀ x y, f (x + y) = f x + f y.
Proof.
intros. apply preserves_sg_op.
Qed.
Lemma preserves_2: f 2 = 2.
Proof.
rewrite preserves_plus. rewrite preserves_1. reflexivity.
Qed.
Lemma preserves_3: f 3 = 3.
Proof.
rewrite ?preserves_plus, ?preserves_1.
reflexivity.
Qed.
Lemma preserves_4: f 4 = 4.
Proof.
rewrite ?preserves_plus, ?preserves_1.
reflexivity.
Qed.
Context `{!IsInjective f}.
Instance isinjective_ne_0 x : PropHolds (x ≠ 0) → PropHolds (f x ≠ 0).
Proof.
intros. rewrite <-preserves_0. apply (isinjective_ne f).
assumption.
Qed.
Lemma injective_ne_1 x : x ≠ 1 → f x ≠ 1.
Proof.
intros. rewrite <-preserves_1.
apply (isinjective_ne f).
assumption.
Qed.
End semiringmor_props.
(* Due to bug 2528 *)
#[export]
Hint Extern 12 (PropHolds (_ _ ≠ 0)) ⇒
eapply @isinjective_ne_0 : typeclass_instances.
(* Lemma stdlib_ring_theory R `{Ring R} :
Ring_theory.ring_theory 0 1 (+) (.*.) (fun x y => x - y) (-) (=).
Proof.
Qed.
*)
Section cring_props.
Context `{IsCRing R}.
Instance: LeftAbsorb (.*.) 0.
Proof.
intro.
rewrite (commutativity (f:=(.*.)) 0).
apply (left_cancellation (+) (y × 0)).
path_via (y × 0);[|apply symmetry, right_identity].
path_via (y × (0 + 0)).
- apply symmetry,distribute_l.
- apply ap. apply right_identity.
Qed.
Global Instance CRing_Semi: IsSemiCRing R.
Proof.
repeat (constructor; try apply _).
Qed.
End cring_props.
Section ring_props.
Context `{IsRing R}.
Global Instance mult_left_absorb : LeftAbsorb (.*.) 0.
Proof.
intro y.
rapply (right_cancellation (+) (0 × y)).
lhs_V rapply simple_distribute_r.
rhs rapply left_identity.
nrapply (ap (.* y)).
apply left_identity.
Defined.
Global Instance mult_right_absorb : RightAbsorb (.*.) 0.
Proof.
intro x.
rapply (right_cancellation (+) (x × 0)).
lhs_V rapply simple_distribute_l.
rhs rapply left_identity.
nrapply (ap (x *.)).
apply left_identity.
Defined.
Definition negate_involutive x : - - x = x := groups.negate_involutive x.
(* alias for convenience *)
Lemma plus_negate_r : ∀ x, x + -x = 0.
Proof. exact right_inverse. Qed.
Lemma plus_negate_l : ∀ x, -x + x = 0.
Proof. exact left_inverse. Qed.
Lemma negate_swap_r : ∀ x y, x - y = -(y - x).
Proof.
intros.
rewrite groups.negate_sg_op.
rewrite involutive.
reflexivity.
Qed.
Lemma negate_swap_l x y : -x + y = -(x - y).
Proof.
rewrite groups.negate_sg_op_distr,involutive.
reflexivity.
Qed.
Lemma negate_plus_distr : ∀ x y, -(x + y) = -x + -y.
Proof. exact groups.negate_sg_op_distr. Qed.
Lemma negate_mult_l x : -x = - 1 × x.
Proof.
apply (left_cancellation (+) x).
path_via 0.
- apply right_inverse.
- path_via (1 × x + (- 1) × x).
+ apply symmetry.
rewrite <-distribute_r. rewrite right_inverse.
apply left_absorb.
+ apply ap011;try reflexivity.
apply left_identity.
Qed.
Lemma negate_mult_r x : -x = x × -1.
Proof.
apply (right_cancellation (+) x).
transitivity (x × -1 + x × 1).
- lhs apply left_inverse.
rhs_V rapply simple_distribute_l.
lhs_V rapply (right_absorb x).
apply (ap (x *.)).
symmetry.
apply left_inverse.
- f_ap.
apply right_identity.
Defined.
Lemma negate_mult_distr_l x y : -(x × y) = -x × y.
Proof.
lhs nrapply negate_mult_l.
lhs rapply (simple_associativity (f := (.*.)) (-1) x y).
apply (ap (.* y)).
symmetry.
apply negate_mult_l.
Defined.
Lemma negate_mult_distr_r x y : -(x × y) = x × -y.
Proof.
lhs nrapply negate_mult_r.
lhs_V rapply (simple_associativity (f := (.*.)) x y).
apply (ap (x *.)).
symmetry.
apply negate_mult_r.
Defined.
Lemma negate_mult_negate x y : -x × -y = x × y.
Proof.
rewrite <-negate_mult_distr_l, <-negate_mult_distr_r.
apply involutive.
Qed.
Lemma negate_0: -0 = 0.
Proof. exact groups.negate_mon_unit. Qed.
Global Instance minus_0_r: RightIdentity (fun x y ⇒ x - y) 0.
Proof.
intro x; rewrite negate_0. apply right_identity.
Qed.
Lemma equal_by_zero_sum x y : x - y = 0 ↔ x = y.
Proof.
split; intros E.
- rewrite <- (left_identity y).
change (sg_op ?x ?y) with (0 + y).
rewrite <- E.
rewrite <-simple_associativity.
rewrite left_inverse.
apply symmetry,right_identity.
- rewrite E. apply right_inverse.
Qed.
Lemma flip_negate x y : -x = y ↔ x = -y.
Proof.
split; intros E.
- rewrite <-E, involutive. trivial.
- rewrite E, involutive. trivial.
Qed.
Lemma flip_negate_0 x : -x = 0 ↔ x = 0.
Proof.
etransitivity.
- apply flip_negate.
- rewrite negate_0.
apply reflexivity.
Qed.
Lemma flip_negate_ne_0 x : -x ≠ 0 ↔ x ≠ 0.
Proof.
split; intros E ?; apply E; apply flip_negate_0;trivial.
path_via x. apply involutive.
Qed.
Lemma negate_zero_prod_l x y : -x × y = 0 ↔ x × y = 0.
Proof.
split; intros E.
- apply (injective (-)). rewrite negate_mult_distr_l, negate_0. trivial.
- apply (injective (-)).
rewrite negate_mult_distr_l, negate_involutive, negate_0.
trivial.
Qed.
Lemma negate_zero_prod_r x y : x × -y = 0 ↔ x × y = 0.
Proof.
etransitivity.
2: apply negate_zero_prod_l.
split.
- intros E.
lhs_V nrapply negate_mult_distr_l.
lhs nrapply negate_mult_distr_r.
exact E.
- intros E.
lhs_V nrapply negate_mult_distr_r.
lhs nrapply negate_mult_distr_l.
exact E.
Defined.
Context `{!NoZeroDivisors R} `{∀ x y:R, Stable (x = y)}.
Global Instance mult_left_cancel: ∀ z, PropHolds (z ≠ 0) →
LeftCancellation (.*.) z.
Proof.
intros z z_nonzero x y E.
apply stable.
intro U.
apply (mult_ne_0 z (x - y) (is_ne_0 z)).
- intro. apply U. apply equal_by_zero_sum. trivial.
- rewrite distribute_l, E.
rewrite <-simple_distribute_l,right_inverse.
apply right_absorb.
Qed.
Instance mult_ne_0' `{!NoZeroDivisors R} x y
: PropHolds (x ≠ 0) → PropHolds (y ≠ 0) → PropHolds (x × y ≠ 0).
Proof.
intros Ex Ey Exy.
unfold PropHolds in ×.
apply (no_zero_divisors x); split; eauto.
Qed.
Global Instance mult_right_cancel : ∀ z, PropHolds (z ≠ 0) →
RightCancellation (.*.) z.
Proof.
intros z ? x y p.
apply stable.
intro U.
nrapply (mult_ne_0' (x - y) z).
- exact _.
- intros r.
apply U, equal_by_zero_sum, r.
- exact _.
- lhs rapply ring_dist_right.
rewrite <- negate_mult_distr_l.
apply equal_by_zero_sum in p.
exact p.
Defined.
Lemma plus_conjugate x y : x = y + x - y.
Proof.
rewrite (commutativity (f := (+)) y x),
<- (simple_associativity (f := (+)) x y (-y)),
right_inverse, right_identity.
reflexivity.
Qed.
Lemma plus_conjugate_alt x y : x = y + (x - y).
Proof.
rewrite (simple_associativity (f := (+))).
apply plus_conjugate.
Qed.
End ring_props.
Section integral_domain_props.
Context `{IsIntegralDomain R}.
Instance intdom_nontrivial_apart `{Apart R} `{!TrivialApart R} :
PropHolds (1 ≶ 0).
Proof.
apply apartness.ne_apart. solve_propholds.
Qed.
End integral_domain_props.
(* Due to bug 2528 *)
#[export]
Hint Extern 6 (PropHolds (1 ≶ 0)) ⇒
eapply @intdom_nontrivial_apart : typeclass_instances.
Section ringmor_props.
Context `{IsRing A} `{IsRing B} `{!IsSemiRingPreserving (f : A → B)}.
Definition preserves_negate x : f (-x) = -f x := groups.preserves_negate x.
(* alias for convenience *)
Lemma preserves_minus x y : f (x - y) = f x - f y.
Proof.
rewrite <-preserves_negate.
apply preserves_plus.
Qed.
Lemma injective_preserves_0 : (∀ x, f x = 0 → x = 0) → IsInjective f.
Proof.
intros E1 x y E.
apply equal_by_zero_sum.
apply E1.
rewrite preserves_minus, E.
apply right_inverse.
Qed.
End ringmor_props.
Section from_another_ring.
Context `{IsCRing A} `{IsHSet B}
`{Bplus : Plus B} `{Zero B} `{Bmult : Mult B} `{One B} `{Bnegate : Negate B}
(f : B → A) `{!IsInjective f}
(plus_correct : ∀ x y, f (x + y) = f x + f y) (zero_correct : f 0 = 0)
(mult_correct : ∀ x y, f (x × y) = f x × f y) (one_correct : f 1 = 1)
(negate_correct : ∀ x, f (-x) = -f x).
Lemma projected_ring: IsCRing B.
Proof.
split.
- apply (groups.projected_ab_group f);assumption.
- apply (groups.projected_com_monoid f mult_correct one_correct);assumption.
- repeat intro; apply (injective f).
rewrite plus_correct, !mult_correct, plus_correct.
apply distribute_l.
Qed.
End from_another_ring.
(* Section from_stdlib_semiring_theory.
Context
`(H: @semi_ring_theory R Rzero Rone Rplus Rmult Re)
`{!@Setoid R Re}
`{!Proper (Re ==> Re ==> Re) Rplus}
`{!Proper (Re ==> Re ==> Re) Rmult}.
Add Ring R2: H.
Definition from_stdlib_semiring_theory: @SemiRing R Re Rplus Rmult Rzero Rone.
Proof.
repeat (constructor; try assumption); repeat intro
; unfold equiv, mon_unit, sg_op, zero_is_mon_unit, plus_is_sg_op,
one_is_mon_unit, mult_is_sg_op, zero, mult, plus; ring.
Qed.
End from_stdlib_semiring_theory.
Section from_stdlib_ring_theory.
Context
`(H: @ring_theory R Rzero Rone Rplus Rmult Rminus Rnegate Re)
`{!@Setoid R Re}
`{!Proper (Re ==> Re ==> Re) Rplus}
`{!Proper (Re ==> Re ==> Re) Rmult}
`{!Proper (Re ==> Re) Rnegate}.
Add Ring R3: H.
Definition from_stdlib_ring_theory: @Ring R Re Rplus Rmult Rzero Rone Rnegate.
Proof.
repeat (constructor; try assumption); repeat intro
; unfold equiv, mon_unit, sg_op, zero_is_mon_unit, plus_is_sg_op,
one_is_mon_unit, mult_is_sg_op, mult, plus, negate; ring.
Qed.
End from_stdlib_ring_theory. *)
Global Instance id_sr_morphism `{IsSemiCRing A}: IsSemiRingPreserving (@id A) := {}.
Section morphism_composition.
Context `{Mult A} `{Plus A} `{One A} `{Zero A}
`{Mult B} `{Plus B} `{One B} `{Zero B}
`{Mult C} `{Plus C} `{One C} `{Zero C}
(f : A → B) (g : B → C).
Instance compose_sr_morphism:
IsSemiRingPreserving f → IsSemiRingPreserving g → IsSemiRingPreserving (g ∘ f).
Proof.
split; apply _.
Qed.
Instance invert_sr_morphism:
∀ `{!IsEquiv f}, IsSemiRingPreserving f → IsSemiRingPreserving (f^-1).
Proof.
split; apply _.
Qed.
End morphism_composition.
#[export]
Hint Extern 4 (IsSemiRingPreserving (_ ∘ _)) ⇒
class_apply @compose_sr_morphism : typeclass_instances.
#[export]
Hint Extern 4 (IsSemiRingPreserving (_^-1)) ⇒
class_apply @invert_sr_morphism : typeclass_instances.
HoTT.Classes.theory.groups
HoTT.Classes.theory.apartness.
Require Import
HoTT.Classes.interfaces.abstract_algebra.
Generalizable Variables R A B C f z.
Definition is_ne_0 `(x : R) `{Zero R} `{p : PropHolds (x ≠ 0)}
: x ≠ 0 := p.
Definition is_nonneg `(x : R) `{Le R} `{Zero R} `{p : PropHolds (0 ≤ x)}
: 0 ≤ x := p.
Definition is_pos `(x : R) `{Lt R} `{Zero R} `{p : PropHolds (0 < x)}
: 0 < x := p.
(* Lemma stdlib_semiring_theory R `{SemiRing R}
: Ring_theory.semi_ring_theory 0 1 (+) (.*.) (=).
Proof.
Qed.
*)
(* We cannot apply left_cancellation (.*.) z directly in case we have
no PropHolds (0 ≠ z) instance in the context. *)
Section cancellation.
Context `(op : A → A → A) `{!Zero A}.
Lemma left_cancellation_ne_0
`{∀ z, PropHolds (z ≠ 0) → LeftCancellation op z} z
: z ≠ 0 → LeftCancellation op z.
Proof. auto. Qed.
Lemma right_cancellation_ne_0
`{∀ z, PropHolds (z ≠ 0) → RightCancellation op z} z
: z ≠ 0 → RightCancellation op z.
Proof. auto. Qed.
Lemma right_cancel_from_left `{!Commutative op} `{!LeftCancellation op z}
: RightCancellation op z.
Proof.
intros x y E.
apply (left_cancellation op z).
rewrite 2!(commutativity (f:=op) z _).
assumption.
Qed.
End cancellation.
Section strong_cancellation.
Context `{IsApart A} (op : A → A → A).
Lemma strong_right_cancel_from_left `{!Commutative op}
`{!StrongLeftCancellation op z}
: StrongRightCancellation op z.
Proof.
intros x y E.
rewrite 2!(commutativity _ z).
apply (strong_left_cancellation op z);trivial.
Qed.
Global Instance strong_left_cancellation_cancel `{!StrongLeftCancellation op z}
: LeftCancellation op z | 20.
Proof.
intros x y E1.
apply tight_apart in E1;apply tight_apart;intros E2.
apply E1. apply (strong_left_cancellation op);trivial.
Qed.
Global Instance strong_right_cancellation_cancel `{!StrongRightCancellation op z}
: RightCancellation op z | 20.
Proof.
intros x y E1.
apply tight_apart in E1;apply tight_apart;intros E2.
apply E1. apply (strong_right_cancellation op);trivial.
Qed.
End strong_cancellation.
Section semiring_props.
Context `{IsSemiCRing R}.
(* Add Ring SR : (stdlib_semiring_theory R). *)
Instance mult_ne_0 `{!NoZeroDivisors R} x y
: PropHolds (x ≠ 0) → PropHolds (y ≠ 0) → PropHolds (x × y ≠ 0).
Proof.
intros Ex Ey Exy.
unfold PropHolds in ×.
apply (no_zero_divisors x); split; eauto.
Qed.
Global Instance plus_0_r: RightIdentity (+) 0 := right_identity.
Global Instance plus_0_l: LeftIdentity (+) 0 := left_identity.
Global Instance mult_1_l: LeftIdentity (.*.) 1 := left_identity.
Global Instance mult_1_r: RightIdentity (.*.) 1 := right_identity.
Global Instance plus_assoc: Associative (+) := simple_associativity.
Global Instance mult_assoc: Associative (.*.) := simple_associativity.
Global Instance plus_comm: Commutative (+) := commutativity.
Global Instance mult_comm: Commutative (.*.) := commutativity.
Global Instance mult_0_l: LeftAbsorb (.*.) 0 := left_absorb.
Global Instance mult_0_r: RightAbsorb (.*.) 0.
Proof.
intro. path_via (0 × x).
- apply mult_comm.
- apply left_absorb.
Qed.
Global Instance plus_mult_distr_r : RightDistribute (.*.) (+).
Proof.
intros x y z.
etransitivity;[|etransitivity].
- apply mult_comm.
- apply distribute_l.
- apply ap011;apply mult_comm.
Qed.
Lemma plus_mult_distr_l : LeftDistribute (.*.) (+).
Proof.
apply _.
Qed.
Global Instance: ∀ r : R, @IsMonoidPreserving R R (+) (+) 0 0 (r *.).
Proof.
repeat (constructor; try apply _).
- red. apply distribute_l.
- apply right_absorb.
Qed.
End semiring_props.
(* Due to bug 2528 *)
#[export]
Hint Extern 3 (PropHolds (_ × _ ≠ 0)) ⇒ eapply @mult_ne_0 : typeclass_instances.
Section semiringmor_props.
Context `{IsSemiRingPreserving A B f}.
Lemma preserves_0: f 0 = 0.
Proof. apply preserves_mon_unit. Qed.
Lemma preserves_1: f 1 = 1.
Proof. apply preserves_mon_unit. Qed.
Lemma preserves_mult: ∀ x y, f (x × y) = f x × f y.
Proof.
intros. apply preserves_sg_op.
Qed.
Lemma preserves_plus: ∀ x y, f (x + y) = f x + f y.
Proof.
intros. apply preserves_sg_op.
Qed.
Lemma preserves_2: f 2 = 2.
Proof.
rewrite preserves_plus. rewrite preserves_1. reflexivity.
Qed.
Lemma preserves_3: f 3 = 3.
Proof.
rewrite ?preserves_plus, ?preserves_1.
reflexivity.
Qed.
Lemma preserves_4: f 4 = 4.
Proof.
rewrite ?preserves_plus, ?preserves_1.
reflexivity.
Qed.
Context `{!IsInjective f}.
Instance isinjective_ne_0 x : PropHolds (x ≠ 0) → PropHolds (f x ≠ 0).
Proof.
intros. rewrite <-preserves_0. apply (isinjective_ne f).
assumption.
Qed.
Lemma injective_ne_1 x : x ≠ 1 → f x ≠ 1.
Proof.
intros. rewrite <-preserves_1.
apply (isinjective_ne f).
assumption.
Qed.
End semiringmor_props.
(* Due to bug 2528 *)
#[export]
Hint Extern 12 (PropHolds (_ _ ≠ 0)) ⇒
eapply @isinjective_ne_0 : typeclass_instances.
(* Lemma stdlib_ring_theory R `{Ring R} :
Ring_theory.ring_theory 0 1 (+) (.*.) (fun x y => x - y) (-) (=).
Proof.
Qed.
*)
Section cring_props.
Context `{IsCRing R}.
Instance: LeftAbsorb (.*.) 0.
Proof.
intro.
rewrite (commutativity (f:=(.*.)) 0).
apply (left_cancellation (+) (y × 0)).
path_via (y × 0);[|apply symmetry, right_identity].
path_via (y × (0 + 0)).
- apply symmetry,distribute_l.
- apply ap. apply right_identity.
Qed.
Global Instance CRing_Semi: IsSemiCRing R.
Proof.
repeat (constructor; try apply _).
Qed.
End cring_props.
Section ring_props.
Context `{IsRing R}.
Global Instance mult_left_absorb : LeftAbsorb (.*.) 0.
Proof.
intro y.
rapply (right_cancellation (+) (0 × y)).
lhs_V rapply simple_distribute_r.
rhs rapply left_identity.
nrapply (ap (.* y)).
apply left_identity.
Defined.
Global Instance mult_right_absorb : RightAbsorb (.*.) 0.
Proof.
intro x.
rapply (right_cancellation (+) (x × 0)).
lhs_V rapply simple_distribute_l.
rhs rapply left_identity.
nrapply (ap (x *.)).
apply left_identity.
Defined.
Definition negate_involutive x : - - x = x := groups.negate_involutive x.
(* alias for convenience *)
Lemma plus_negate_r : ∀ x, x + -x = 0.
Proof. exact right_inverse. Qed.
Lemma plus_negate_l : ∀ x, -x + x = 0.
Proof. exact left_inverse. Qed.
Lemma negate_swap_r : ∀ x y, x - y = -(y - x).
Proof.
intros.
rewrite groups.negate_sg_op.
rewrite involutive.
reflexivity.
Qed.
Lemma negate_swap_l x y : -x + y = -(x - y).
Proof.
rewrite groups.negate_sg_op_distr,involutive.
reflexivity.
Qed.
Lemma negate_plus_distr : ∀ x y, -(x + y) = -x + -y.
Proof. exact groups.negate_sg_op_distr. Qed.
Lemma negate_mult_l x : -x = - 1 × x.
Proof.
apply (left_cancellation (+) x).
path_via 0.
- apply right_inverse.
- path_via (1 × x + (- 1) × x).
+ apply symmetry.
rewrite <-distribute_r. rewrite right_inverse.
apply left_absorb.
+ apply ap011;try reflexivity.
apply left_identity.
Qed.
Lemma negate_mult_r x : -x = x × -1.
Proof.
apply (right_cancellation (+) x).
transitivity (x × -1 + x × 1).
- lhs apply left_inverse.
rhs_V rapply simple_distribute_l.
lhs_V rapply (right_absorb x).
apply (ap (x *.)).
symmetry.
apply left_inverse.
- f_ap.
apply right_identity.
Defined.
Lemma negate_mult_distr_l x y : -(x × y) = -x × y.
Proof.
lhs nrapply negate_mult_l.
lhs rapply (simple_associativity (f := (.*.)) (-1) x y).
apply (ap (.* y)).
symmetry.
apply negate_mult_l.
Defined.
Lemma negate_mult_distr_r x y : -(x × y) = x × -y.
Proof.
lhs nrapply negate_mult_r.
lhs_V rapply (simple_associativity (f := (.*.)) x y).
apply (ap (x *.)).
symmetry.
apply negate_mult_r.
Defined.
Lemma negate_mult_negate x y : -x × -y = x × y.
Proof.
rewrite <-negate_mult_distr_l, <-negate_mult_distr_r.
apply involutive.
Qed.
Lemma negate_0: -0 = 0.
Proof. exact groups.negate_mon_unit. Qed.
Global Instance minus_0_r: RightIdentity (fun x y ⇒ x - y) 0.
Proof.
intro x; rewrite negate_0. apply right_identity.
Qed.
Lemma equal_by_zero_sum x y : x - y = 0 ↔ x = y.
Proof.
split; intros E.
- rewrite <- (left_identity y).
change (sg_op ?x ?y) with (0 + y).
rewrite <- E.
rewrite <-simple_associativity.
rewrite left_inverse.
apply symmetry,right_identity.
- rewrite E. apply right_inverse.
Qed.
Lemma flip_negate x y : -x = y ↔ x = -y.
Proof.
split; intros E.
- rewrite <-E, involutive. trivial.
- rewrite E, involutive. trivial.
Qed.
Lemma flip_negate_0 x : -x = 0 ↔ x = 0.
Proof.
etransitivity.
- apply flip_negate.
- rewrite negate_0.
apply reflexivity.
Qed.
Lemma flip_negate_ne_0 x : -x ≠ 0 ↔ x ≠ 0.
Proof.
split; intros E ?; apply E; apply flip_negate_0;trivial.
path_via x. apply involutive.
Qed.
Lemma negate_zero_prod_l x y : -x × y = 0 ↔ x × y = 0.
Proof.
split; intros E.
- apply (injective (-)). rewrite negate_mult_distr_l, negate_0. trivial.
- apply (injective (-)).
rewrite negate_mult_distr_l, negate_involutive, negate_0.
trivial.
Qed.
Lemma negate_zero_prod_r x y : x × -y = 0 ↔ x × y = 0.
Proof.
etransitivity.
2: apply negate_zero_prod_l.
split.
- intros E.
lhs_V nrapply negate_mult_distr_l.
lhs nrapply negate_mult_distr_r.
exact E.
- intros E.
lhs_V nrapply negate_mult_distr_r.
lhs nrapply negate_mult_distr_l.
exact E.
Defined.
Context `{!NoZeroDivisors R} `{∀ x y:R, Stable (x = y)}.
Global Instance mult_left_cancel: ∀ z, PropHolds (z ≠ 0) →
LeftCancellation (.*.) z.
Proof.
intros z z_nonzero x y E.
apply stable.
intro U.
apply (mult_ne_0 z (x - y) (is_ne_0 z)).
- intro. apply U. apply equal_by_zero_sum. trivial.
- rewrite distribute_l, E.
rewrite <-simple_distribute_l,right_inverse.
apply right_absorb.
Qed.
Instance mult_ne_0' `{!NoZeroDivisors R} x y
: PropHolds (x ≠ 0) → PropHolds (y ≠ 0) → PropHolds (x × y ≠ 0).
Proof.
intros Ex Ey Exy.
unfold PropHolds in ×.
apply (no_zero_divisors x); split; eauto.
Qed.
Global Instance mult_right_cancel : ∀ z, PropHolds (z ≠ 0) →
RightCancellation (.*.) z.
Proof.
intros z ? x y p.
apply stable.
intro U.
nrapply (mult_ne_0' (x - y) z).
- exact _.
- intros r.
apply U, equal_by_zero_sum, r.
- exact _.
- lhs rapply ring_dist_right.
rewrite <- negate_mult_distr_l.
apply equal_by_zero_sum in p.
exact p.
Defined.
Lemma plus_conjugate x y : x = y + x - y.
Proof.
rewrite (commutativity (f := (+)) y x),
<- (simple_associativity (f := (+)) x y (-y)),
right_inverse, right_identity.
reflexivity.
Qed.
Lemma plus_conjugate_alt x y : x = y + (x - y).
Proof.
rewrite (simple_associativity (f := (+))).
apply plus_conjugate.
Qed.
End ring_props.
Section integral_domain_props.
Context `{IsIntegralDomain R}.
Instance intdom_nontrivial_apart `{Apart R} `{!TrivialApart R} :
PropHolds (1 ≶ 0).
Proof.
apply apartness.ne_apart. solve_propholds.
Qed.
End integral_domain_props.
(* Due to bug 2528 *)
#[export]
Hint Extern 6 (PropHolds (1 ≶ 0)) ⇒
eapply @intdom_nontrivial_apart : typeclass_instances.
Section ringmor_props.
Context `{IsRing A} `{IsRing B} `{!IsSemiRingPreserving (f : A → B)}.
Definition preserves_negate x : f (-x) = -f x := groups.preserves_negate x.
(* alias for convenience *)
Lemma preserves_minus x y : f (x - y) = f x - f y.
Proof.
rewrite <-preserves_negate.
apply preserves_plus.
Qed.
Lemma injective_preserves_0 : (∀ x, f x = 0 → x = 0) → IsInjective f.
Proof.
intros E1 x y E.
apply equal_by_zero_sum.
apply E1.
rewrite preserves_minus, E.
apply right_inverse.
Qed.
End ringmor_props.
Section from_another_ring.
Context `{IsCRing A} `{IsHSet B}
`{Bplus : Plus B} `{Zero B} `{Bmult : Mult B} `{One B} `{Bnegate : Negate B}
(f : B → A) `{!IsInjective f}
(plus_correct : ∀ x y, f (x + y) = f x + f y) (zero_correct : f 0 = 0)
(mult_correct : ∀ x y, f (x × y) = f x × f y) (one_correct : f 1 = 1)
(negate_correct : ∀ x, f (-x) = -f x).
Lemma projected_ring: IsCRing B.
Proof.
split.
- apply (groups.projected_ab_group f);assumption.
- apply (groups.projected_com_monoid f mult_correct one_correct);assumption.
- repeat intro; apply (injective f).
rewrite plus_correct, !mult_correct, plus_correct.
apply distribute_l.
Qed.
End from_another_ring.
(* Section from_stdlib_semiring_theory.
Context
`(H: @semi_ring_theory R Rzero Rone Rplus Rmult Re)
`{!@Setoid R Re}
`{!Proper (Re ==> Re ==> Re) Rplus}
`{!Proper (Re ==> Re ==> Re) Rmult}.
Add Ring R2: H.
Definition from_stdlib_semiring_theory: @SemiRing R Re Rplus Rmult Rzero Rone.
Proof.
repeat (constructor; try assumption); repeat intro
; unfold equiv, mon_unit, sg_op, zero_is_mon_unit, plus_is_sg_op,
one_is_mon_unit, mult_is_sg_op, zero, mult, plus; ring.
Qed.
End from_stdlib_semiring_theory.
Section from_stdlib_ring_theory.
Context
`(H: @ring_theory R Rzero Rone Rplus Rmult Rminus Rnegate Re)
`{!@Setoid R Re}
`{!Proper (Re ==> Re ==> Re) Rplus}
`{!Proper (Re ==> Re ==> Re) Rmult}
`{!Proper (Re ==> Re) Rnegate}.
Add Ring R3: H.
Definition from_stdlib_ring_theory: @Ring R Re Rplus Rmult Rzero Rone Rnegate.
Proof.
repeat (constructor; try assumption); repeat intro
; unfold equiv, mon_unit, sg_op, zero_is_mon_unit, plus_is_sg_op,
one_is_mon_unit, mult_is_sg_op, mult, plus, negate; ring.
Qed.
End from_stdlib_ring_theory. *)
Global Instance id_sr_morphism `{IsSemiCRing A}: IsSemiRingPreserving (@id A) := {}.
Section morphism_composition.
Context `{Mult A} `{Plus A} `{One A} `{Zero A}
`{Mult B} `{Plus B} `{One B} `{Zero B}
`{Mult C} `{Plus C} `{One C} `{Zero C}
(f : A → B) (g : B → C).
Instance compose_sr_morphism:
IsSemiRingPreserving f → IsSemiRingPreserving g → IsSemiRingPreserving (g ∘ f).
Proof.
split; apply _.
Qed.
Instance invert_sr_morphism:
∀ `{!IsEquiv f}, IsSemiRingPreserving f → IsSemiRingPreserving (f^-1).
Proof.
split; apply _.
Qed.
End morphism_composition.
#[export]
Hint Extern 4 (IsSemiRingPreserving (_ ∘ _)) ⇒
class_apply @compose_sr_morphism : typeclass_instances.
#[export]
Hint Extern 4 (IsSemiRingPreserving (_^-1)) ⇒
class_apply @invert_sr_morphism : typeclass_instances.