Timings for dec_fields.v

Require Import
  HoTT.Classes.interfaces.abstract_algebra
  HoTT.Classes.interfaces.orders
  HoTT.Classes.theory.dec_fields.

Require Export
  HoTT.Classes.orders.rings.

Generalizable Variables F f R Fle Flt.

Section contents.

Context `{IsDecField F} `{Apart F} `{!TrivialApart F}
  `{!FullPseudoSemiRingOrder Fle Flt} `{DecidablePaths F}.

(* Add Ring F : (stdlib_ring_theory F). *)

Instance pos_dec_recip_compat x : PropHolds (0 < x) -> PropHolds (0 < /x).

Proof.

intros E.

apply (strictly_order_reflecting (x *.)).

rewrite dec_recip_inverse by (apply orders.lt_ne_flip;trivial).

rewrite mult_0_r.

 solve_propholds.

Qed.

Instance nonneg_dec_recip_compat x : PropHolds (0 ≤ x) -> PropHolds (0 ≤ /x).

Proof.

intros E.

 red.

destruct (dec (x = 0)) as [E2 | E2].

-

 rewrite E2, dec_recip_0.

 rewrite E2 in E;trivial.

-

 apply lt_le.

 apply pos_dec_recip_compat.

  apply lt_iff_le_ne.

 split;trivial.

  apply symmetric_neq;trivial.

Qed.

Lemma neg_dec_recip_compat x : x < 0 -> /x < 0.

Proof.

intros.

 apply flip_neg_negate.

rewrite dec_recip_negate.

apply pos_dec_recip_compat.

apply flip_neg_negate.

 trivial.

Qed.

Lemma nonpos_dec_recip_compat x : x ≤ 0 -> /x ≤ 0.

Proof.

intros.

 apply flip_nonpos_negate.

rewrite dec_recip_negate.

apply nonneg_dec_recip_compat.

apply flip_nonpos_negate;trivial.

Qed.

Lemma flip_le_dec_recip x y : 0 < y -> y ≤ x  -> /x ≤ /y.

Proof.

intros E1 E2.

apply (order_reflecting_pos (.*.) x).

-

 apply lt_le_trans with y;trivial.

-

 rewrite dec_recip_inverse.

  +

 apply (order_reflecting_pos (.*.) y);trivial.

    rewrite (commutativity x), simple_associativity, dec_recip_inverse.

    *

 rewrite mult_1_l,mult_1_r.

 trivial.

    *

 apply lt_ne_flip;trivial.

  +

 apply lt_ne_flip.

    apply lt_le_trans with y;trivial.

Qed.

Lemma flip_le_dec_recip_l x y : 0 < y -> /y ≤ x  -> /x ≤ y.

Proof.

intros E1 E2.

rewrite <-(dec_recip_involutive y).

apply flip_le_dec_recip;trivial.

apply pos_dec_recip_compat;trivial.

Qed.

Lemma flip_le_dec_recip_r x y : 0 < y -> y ≤ /x  -> x ≤ /y.

Proof.

intros E1 E2.

rewrite <-(dec_recip_involutive x).

apply flip_le_dec_recip;trivial.

Qed.

Lemma flip_lt_dec_recip x y : 0 < y -> y < x  -> /x < /y.

Proof.

intros E1 E2.

assert (0 < x) by (transitivity y;trivial).

apply (strictly_order_reflecting (x *.)).

rewrite dec_recip_inverse.

-

 apply (strictly_order_reflecting (y *.)).

  rewrite (commutativity x), simple_associativity, dec_recip_inverse.

  +

 rewrite mult_1_l,mult_1_r.

 trivial.

  +

 apply lt_ne_flip.

 trivial.

-

 apply lt_ne_flip;trivial.

Qed.

Lemma flip_lt_dec_recip_l x y : 0 < y -> /y < x  -> /x < y.

Proof.

intros E1 E2.

rewrite <-(dec_recip_involutive y).

apply flip_lt_dec_recip; trivial.

apply pos_dec_recip_compat.

 trivial.

Qed.

Lemma flip_lt_dec_recip_r x y : 0 < y -> y < /x  -> x < /y.

Proof.

intros E1 E2.

rewrite <-(dec_recip_involutive x).

apply flip_lt_dec_recip;trivial.

Qed.

End contents.

(* Due to bug #2528 *)

#[export]
Hint Extern 12 (PropHolds (0 ≤ _)) =>
  eapply @nonneg_dec_recip_compat : typeclass_instances.

#[export]
Hint Extern 12 (PropHolds (0 < _)) =>
  eapply @pos_dec_recip_compat : typeclass_instances.