Timings for rings.v

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
    `{forall z, PropHolds (z <> 0) -> LeftCancellation op z} z
    : z <> 0 -> LeftCancellation op z.

  Proof.

 auto.

 Qed.

  Lemma right_cancellation_ne_0
    `{forall 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: forall 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: forall x y, f (x * y) = f x * f y.

  Proof.

  intros.

 apply preserves_sg_op.

  Qed.

  Lemma preserves_plus: forall 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 : forall 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 : forall 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} `{forall x y:R, Stable (x = y)}.

  #[export] Instance mult_left_cancel:  forall 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 : forall 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 : (forall 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 : forall x y, f (x + y) = f x + f y) (zero_correct : f 0 = 0)
    (mult_correct : forall x y, f (x * y) = f x * f y) (one_correct : f 1 = 1)
    (negate_correct : forall 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:
    forall `{!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.