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.
#[export] 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.
#[export] 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.
#[export] Instance plus_0_r: RightIdentity (+) 0 := right_identity.
#[export] Instance plus_0_l: LeftIdentity (+) 0 := left_identity.
#[export] Instance mult_1_l: LeftIdentity (.*.) 1 := left_identity.
#[export] Instance mult_1_r: RightIdentity (.*.) 1 := right_identity.
#[export] Instance plus_assoc: Associative (+) := simple_associativity.
#[export] Instance mult_assoc: Associative (.*.) := simple_associativity.
#[export] Instance plus_comm: Commutative (+) := commutativity.
#[export] Instance mult_comm: Commutative (.*.) := commutativity.
#[export] Instance mult_0_l: LeftAbsorb (.*.) 0 := left_absorb.
#[export] Instance mult_0_r: RightAbsorb (.*.) 0.
Proof.
intro. path_via (0 × x).
- apply mult_comm.
- apply left_absorb.
Qed.
#[export] 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.
exact _.
Qed.
#[export] Instance: ∀ r : R, @IsMonoidPreserving R R (+) (+) 0 0 (r *.).
Proof.
repeat (constructor; try exact _).
- 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. exact preserves_mon_unit. Qed.
Lemma preserves_1: f 1 = 1.
Proof. exact 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 (neq_isinj f).
assumption.
Qed.
Lemma injective_ne_1 x : x ≠ 1 → f x ≠ 1.
Proof.
intros. rewrite <-preserves_1.
apply (neq_isinj 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.
#[export] Instance CRing_Semi: IsSemiCRing R.
Proof.
repeat (constructor; try exact _).
Qed.
End cring_props.
Section ring_props.
Context `{IsRing R}.
#[export] Instance mult_left_absorb : LeftAbsorb (.*.) 0.
Proof.
intro y.
rapply (right_cancellation (+) (0 × y)).
lhs_V rapply simple_distribute_r.
rhs rapply left_identity.
napply (ap (.* y)).
apply left_identity.
Defined.
#[export] Instance mult_right_absorb : RightAbsorb (.*.) 0.
Proof.
intro x.
rapply (right_cancellation (+) (x × 0)).
lhs_V rapply simple_distribute_l.
rhs rapply left_identity.
napply (ap (x *.)).
apply left_identity.
Defined.
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.
#[export] 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.
#[export] 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.
#[export] Instance plus_0_r: RightIdentity (+) 0 := right_identity.
#[export] Instance plus_0_l: LeftIdentity (+) 0 := left_identity.
#[export] Instance mult_1_l: LeftIdentity (.*.) 1 := left_identity.
#[export] Instance mult_1_r: RightIdentity (.*.) 1 := right_identity.
#[export] Instance plus_assoc: Associative (+) := simple_associativity.
#[export] Instance mult_assoc: Associative (.*.) := simple_associativity.
#[export] Instance plus_comm: Commutative (+) := commutativity.
#[export] Instance mult_comm: Commutative (.*.) := commutativity.
#[export] Instance mult_0_l: LeftAbsorb (.*.) 0 := left_absorb.
#[export] Instance mult_0_r: RightAbsorb (.*.) 0.
Proof.
intro. path_via (0 × x).
- apply mult_comm.
- apply left_absorb.
Qed.
#[export] 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.
exact _.
Qed.
#[export] Instance: ∀ r : R, @IsMonoidPreserving R R (+) (+) 0 0 (r *.).
Proof.
repeat (constructor; try exact _).
- 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. exact preserves_mon_unit. Qed.
Lemma preserves_1: f 1 = 1.
Proof. exact 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 (neq_isinj f).
assumption.
Qed.
Lemma injective_ne_1 x : x ≠ 1 → f x ≠ 1.
Proof.
intros. rewrite <-preserves_1.
apply (neq_isinj 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.
#[export] Instance CRing_Semi: IsSemiCRing R.
Proof.
repeat (constructor; try exact _).
Qed.
End cring_props.
Section ring_props.
Context `{IsRing R}.
#[export] Instance mult_left_absorb : LeftAbsorb (.*.) 0.
Proof.
intro y.
rapply (right_cancellation (+) (0 × y)).
lhs_V rapply simple_distribute_r.
rhs rapply left_identity.
napply (ap (.* y)).
apply left_identity.
Defined.
#[export] Instance mult_right_absorb : RightAbsorb (.*.) 0.
Proof.
intro x.
rapply (right_cancellation (+) (x × 0)).
lhs_V rapply simple_distribute_l.
rhs rapply left_identity.
napply (ap (x *.)).
apply left_identity.
Defined.
This hint helps other results go through. We do it in two steps, since if we specify the type IsGroup R, Coq infers the wrong implicit arguments to IsGroup.
Definition isgroup_ring := abgroup_group R.
#[export] Existing Instance isgroup_ring.
#[export] Instance negate_involutive : Involutive (-) := inverse_involutive.
(* alias for convenience *)
#[export] Instance plus_negate_r : RightInverse (+) (-) 0.
Proof.
rapply inverse_r.
Defined.
#[export] Instance plus_negate_l : LeftInverse (+) (-) 0.
Proof.
rapply inverse_l.
Defined.
Lemma negate_swap_r : ∀ x y, x - y = -(y - x).
Proof.
intros; symmetry.
lhs rapply groups.inverse_sg_op.
f_ap.
apply involutive.
Defined.
Lemma negate_swap_l x y : -x + y = -(x - y).
Proof.
rhs_V rapply negate_swap_r.
apply commutativity.
Defined.
#[export] Instance isinj_ring_neg : IsInjective (-)
:= groups.isinj_group_inverse.
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.
- rapply inverse_r.
- path_via (1 × x + (- 1) × x).
+ rhs_V rapply distribute_r.
symmetry.
rhs_V exact (left_absorb x).
f_ap.
rapply inverse_r.
+ apply ap011;try reflexivity.
apply left_identity.
Defined.
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 exact (right_absorb x).
apply (ap (x *.)).
symmetry.
rapply inverse_l.
- f_ap.
apply right_identity.
Defined.
Lemma negate_mult_distr_l x y : -(x × y) = -x × y.
Proof.
lhs napply negate_mult_l.
lhs exact (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 napply 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.
rapply involutive.
Qed.
Lemma negate_0: -0 = 0.
Proof. exact groups.inverse_mon_unit. Qed.
#[export] 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 napply negate_mult_distr_l.
lhs napply negate_mult_distr_r.
exact E.
- intros E.
lhs_V napply negate_mult_distr_r.
lhs napply negate_mult_distr_l.
exact E.
Defined.
Context `{!NoZeroDivisors R} `{∀ x y:R, Stable (x = y)}.
#[export] 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.
#[export] Instance mult_right_cancel : ∀ z, PropHolds (z ≠ 0) →
RightCancellation (.*.) z.
Proof.
intros z ? x y p.
apply stable.
intro U.
napply (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.
rapply intdom_nontrivial.
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.
Proof.
rapply preserves_inverse.
Defined.
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.
- exact (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. *)
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; exact _.
Qed.
Instance invert_sr_morphism:
∀ `{!IsEquiv f}, IsSemiRingPreserving f → IsSemiRingPreserving (f^-1).
Proof.
split; exact _.
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.
#[export] Existing Instance isgroup_ring.
#[export] Instance negate_involutive : Involutive (-) := inverse_involutive.
(* alias for convenience *)
#[export] Instance plus_negate_r : RightInverse (+) (-) 0.
Proof.
rapply inverse_r.
Defined.
#[export] Instance plus_negate_l : LeftInverse (+) (-) 0.
Proof.
rapply inverse_l.
Defined.
Lemma negate_swap_r : ∀ x y, x - y = -(y - x).
Proof.
intros; symmetry.
lhs rapply groups.inverse_sg_op.
f_ap.
apply involutive.
Defined.
Lemma negate_swap_l x y : -x + y = -(x - y).
Proof.
rhs_V rapply negate_swap_r.
apply commutativity.
Defined.
#[export] Instance isinj_ring_neg : IsInjective (-)
:= groups.isinj_group_inverse.
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.
- rapply inverse_r.
- path_via (1 × x + (- 1) × x).
+ rhs_V rapply distribute_r.
symmetry.
rhs_V exact (left_absorb x).
f_ap.
rapply inverse_r.
+ apply ap011;try reflexivity.
apply left_identity.
Defined.
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 exact (right_absorb x).
apply (ap (x *.)).
symmetry.
rapply inverse_l.
- f_ap.
apply right_identity.
Defined.
Lemma negate_mult_distr_l x y : -(x × y) = -x × y.
Proof.
lhs napply negate_mult_l.
lhs exact (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 napply 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.
rapply involutive.
Qed.
Lemma negate_0: -0 = 0.
Proof. exact groups.inverse_mon_unit. Qed.
#[export] 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 napply negate_mult_distr_l.
lhs napply negate_mult_distr_r.
exact E.
- intros E.
lhs_V napply negate_mult_distr_r.
lhs napply negate_mult_distr_l.
exact E.
Defined.
Context `{!NoZeroDivisors R} `{∀ x y:R, Stable (x = y)}.
#[export] 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.
#[export] Instance mult_right_cancel : ∀ z, PropHolds (z ≠ 0) →
RightCancellation (.*.) z.
Proof.
intros z ? x y p.
apply stable.
intro U.
napply (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.
rapply intdom_nontrivial.
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.
Proof.
rapply preserves_inverse.
Defined.
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.
- exact (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. *)
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; exact _.
Qed.
Instance invert_sr_morphism:
∀ `{!IsEquiv f}, IsSemiRingPreserving f → IsSemiRingPreserving (f^-1).
Proof.
split; exact _.
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.