FinMatrix.CoqExt.RExt.RExtAbs

Require Export RExtBase RExtBool.

Notation "| r |" := (Rabs r) : R_scope.

#[export] Hint Rewrite
  Rabs_R0
  Rabs_Ropp
  Rabs_Rabsolu
  : R.

#[export] Hint Resolve
  Rabs_pos
  sqrt_pos
  Rabs_right
  Rabs_pos_eq
  Rabs_left
  Rabs_left1
  Rabs_no_R0
  : R.

Lemma Rabs_right_sym : forall r : R, 0 <= r -> r = |r|.
Proof. intros; symmetry; ra. Qed.
#[export] Hint Resolve Rabs_right_sym : R.

Lemma Rabs_left_sym : forall r : R, r < 0 -> - r = |r|.
Proof. intros; symmetry; ra. Qed.
#[export] Hint Resolve Rabs_left_sym : R.

Lemma Rabs_left1_sym : forall r : R, r <= 0 -> - r = |r|.
Proof. intros; symmetry; ra. Qed.
#[export] Hint Resolve Rabs_left1_sym : R.

Lemma Rabs_neg_l : forall r, 0 <= r -> | -r | = r.
Proof. ra. Qed.
#[export] Hint Resolve Rabs_neg_l : R.

Lemma Rabs_neg_r : forall r, r < 0 -> | -r| = -r.
Proof. ra. Qed.
#[export] Hint Resolve Rabs_neg_r : R.

Lemma Rabs_pos_imply : forall r, 0 <= r -> | r | = r.
Proof. ra. Qed.

Lemma Rabs_pos_if : forall r, | r | = r -> 0 <= r.
Proof.
  intros.
  bdestruct (r <=? 0); auto; ra.
  apply Rabs_left1 in H0.
  assert (r = 0); lra.
Qed.
#[export] Hint Resolve Rabs_pos_if : R.

Lemma Rabs_neg_imply : forall r, r <= 0 -> | r | = - r.
Proof. ra. Qed.
#[export] Hint Resolve Rabs_neg_imply : R.

Lemma Rabs_neg_if : forall r, | r | = - r -> r <= 0.
Proof.
  intros. bdestruct (r <=? 0); ra.
  bdestruct (r =? 0); ra.
  assert (r > 0); ra.
  rewrite Rabs_right in H; ra.
Qed.
#[export] Hint Resolve Rabs_neg_if : R.

Lemma Rabs_le_rev : forall a b : R, |a| <= b -> - b <= a <= b.
Proof.
  intros. bdestruct (a <? 0).
  - assert (|a| = -a); ra.
  - assert (|a| = a); ra.
    apply Rabs_pos_imply; ra.
Qed.

Lemma Rdiv_abs_gt0 : forall r, r > 0 -> r / | r | = 1.
Proof. intros. rewrite Rabs_right; ra. Qed.
#[export] Hint Resolve Rdiv_abs_gt0 : R.

Lemma Rdiv_abs_lt0 : forall r, r < 0 -> r / | r | = -1.
Proof. intros. rewrite Rabs_left; ra. Qed.
#[export] Hint Resolve Rdiv_abs_lt0 : R.