FinMatrix.CoqExt.RExt


Require Export Lia Lra Reals.
Require Import ZExt QExt QcExt.
Require Export Basic.
Require Export Hierarchy.

Open Scope R_scope.

Config the usage of Coq-Standard-Library Reals: Hints, Opaque, auto

Config hint db for autounfold
Global Hint Unfold
  Rminus
  Rdiv
  Rsqr
  : R.

Config hint db for autorewrite, for rewriting of equations
#[export] Hint Rewrite
  
  Rabs_R0
  Rabs_Ropp
  Rabs_Rabsolu

  
  Rplus_0_l
  Rplus_0_r

  
  Ropp_0
  Rminus_0_r
  Ropp_involutive
  Rplus_opp_r
  Rplus_opp_l
  Rminus_diag

  
  Rsqr_0
  Rsqr_1
  Rmult_0_l
  Rmult_0_r
  Rmult_1_l
  Rmult_1_r



  
  pow1
  pow_O
  pow_1

  
  Rpower_O
  Rpower_1
  
  
  Rsqr_mult

  
  sqrt_Rsqr_abs
  
  sqrt_0
  : R.

Note that, these leamms should be used careful, they may generate an undesired burden of proof. Thus, we use a new database name "sqrt"
#[export] Hint Rewrite
  
  Rsqr_sqrt
  sqrt_Rsqr
  : sqrt.

Config hint db for auto，for solving equalities or inequalities
Global Hint Resolve
  
  eq_sym
  sqrt_0
  Rsqr_eq_0

  Rsqr_sqrt
  sqrt_Rsqr
  sin2_cos2
  acos_0
  acos_1

  
  Rlt_0_1
  PI_RGT_0
  Rabs_pos
  Rabs_no_R0
  sqrt_pos
  
  
  Rplus_le_le_0_compat
  Rplus_lt_le_0_compat
  Rplus_le_lt_0_compat
  Rplus_lt_0_compat

  
  Rle_0_sqr

  Rsqr_pos_lt
  Rmult_lt_0_compat
  Rinv_0_lt_compat
  Rinv_lt_0_compat
  Rdiv_lt_0_compat


  
  Rlt_gt
  Rgt_lt
  Rge_le
  Rle_ge
  Rlt_le
  Rsqr_pos_lt

  
  Rgt_not_eq
  Rlt_not_eq

  
  sqrt_lt_R0
  sqrt_inj
  : R.

Control Opaque / Transparent of the definitions
Global Opaque
  PI
  sqrt
  Rpower
  sin
  cos
  tan
  asin
  atan
  acos
  ln
.

Section TEST_psatz.
  Goal forall x y, x ^ 2 + y * y >= x * y.
    intros.
    nra.
  Qed.

End TEST_psatz.

Automation for proof

arithmetric on reals : lra + nra
Ltac ra :=
  intros; unfold Rsqr in *; try lra; try nra; auto with R.

Try to prove equality of two R values, using `R` db, especially for triangle
Ltac req :=
  autorewrite with R; ra.

Convert `a ^ (n + 2)` to `(a ^ 2) * (a ^ n)`
Ltac simp_pow :=
  match goal with
  | |- context[?a ^ 4] => replace (a ^ 4) with ((a ^ 2) ^ 2); [|ring]
  | |- context[?a ^ 3] => replace (a ^ 3) with ((a ^ 2) * a)%R; [|ring]
  end.

Decidable procedure for comparison of R

Notations for comparison with decidable procedure

Infix "??=" := (Req_EM_T) : R_scope.


Notation "x ??>= y" := (Rle_lt_dec y x) : R_scope.
Notation "x ??> y" := (Rlt_le_dec y x) : R_scope.

Infix "??<=" := (Rle_lt_dec) : R_scope.
Infix "??<" := (Rlt_le_dec) : R_scope.

Verify above notations are reasonable


Lemma ReqDec_spec : forall a b : R, a = b <-> if a ??= b then true else false.
Proof. intros. destruct (_??=_); split; intros; try congruence. Qed.

Lemma RgeDec_spec : forall a b : R,
    (if a ??>= b then true else false) = (if b ??<= a then true else false).
Proof. intros. auto. Qed.

Lemma RgtDec_spec : forall a b : R,
    (if a ??> b then true else false) = (if b ??< a then true else false).
Proof. intros. auto. Qed.

Lemma RleDec_spec : forall a b : R, a <= b <-> if a ??<= b then true else false.
Proof. intros. destruct (_??<=_); split; intros; try congruence. lra. Qed.

Lemma RltDec_spec : forall a b : R, a < b <-> if a ??< b then true else false.
Proof. intros. destruct (_??<_); split; intros; try congruence. lra. Qed.

Aditional properties about RxxDec


Lemma RleDec_refl : forall {B} (x : R) (b1 b2 : B),
    (if x ??<= x then b1 else b2) = b1.
Proof. intros. destruct (_??<= _); ra. Qed.

Reqb,Rleb,Rltb: Boolean comparison of R


#[export] Instance R_eq_Dec : Dec (@eq R).
Proof. constructor. apply Req_EM_T. Defined.

#[export] Instance R_le_Dec : Dec Rle.
Proof. constructor. intros. destruct (Rle_lt_dec a b); auto. right; lra. Qed.

#[export] Instance R_lt_Dec : Dec Rlt.
Proof. constructor. intros. destruct (Rlt_le_dec a b); auto. right; lra. Qed.

Definition Reqb (r1 r2 : R) : bool := Acmpb R_eq_Dec r1 r2.
Definition Rleb (r1 r2 : R) : bool := Acmpb R_le_Dec r1 r2.
Definition Rltb (r1 r2 : R) : bool := Acmpb R_lt_Dec r1 r2.
Infix "=?" := Reqb : R_scope.
Infix "<=?" := Rleb : R_scope.
Infix "<?" := Rltb : R_scope.
Infix ">?" := (fun x y => y <? x) : R_scope.
Infix ">=?" := (fun x y => y <=? x) : R_scope.

Lemma Reqb_true : forall x y, x =? y = true <-> x = y.
Proof. apply Acmpb_true. Qed.

Lemma Reqb_false : forall x y, x =? y = false <-> x <> y.
Proof. apply Acmpb_false. Qed.

Lemma Reqb_reflect : forall x y, reflect (x = y) (x =? y).
Proof.
  intros. unfold Reqb,Acmpb. destruct dec; constructor; auto.
Qed.
#[export] Hint Resolve Reqb_reflect : bdestruct.

Lemma Reqb_refl : forall r, r =? r = true.
Proof. intros. unfold Reqb,Acmpb. destruct dec; auto. Qed.

Lemma Reqb_comm : forall r1 r2, (r1 =? r2) = (r2 =? r1).
Proof. intros. unfold Reqb,Acmpb. destruct dec,dec; auto. lra. Qed.

Lemma Reqb_trans : forall r1 r2 r3, r1 =? r2 = true ->
  r2 =? r3 = true -> r1 =? r3 = true.
Proof. intros. unfold Reqb,Acmpb in *. destruct dec,dec,dec; auto. lra. Qed.

Lemma Rltb_reflect : forall x y, reflect (x < y) (x <? y).
Proof. intros. unfold Rltb,Acmpb in *. destruct dec; auto; constructor; lra. Qed.
#[export] Hint Resolve Rltb_reflect : bdestruct.

Lemma Rleb_reflect : forall x y, reflect (x <= y) (x <=? y).
Proof. intros. unfold Rleb,Acmpb in *. destruct dec; auto; constructor; lra. Qed.
#[export] Hint Resolve Rleb_reflect : bdestruct.

Lemma Rleb_refl : forall x : R, x <=? x = true.
Proof. intros. bdestruct (x <=? x); ra. Qed.

Lemma Rleb_opp_r : forall x y : R, (x <=? - y) = (- x >=? y).
Proof. intros. bdestruct (x <=? -y); bdestruct (-x >=? y); ra. Qed.

Lemma Rleb_opp_l : forall x y : R, (- x <=? y) = (x >=? - y).
Proof. intros. bdestruct (- x <=? y); bdestruct (x >=? -y); ra. Qed.

(a - b <? 0) = (0 <? b - a)
Lemma Rminus_ltb0_comm : forall a b : R, (a - b <? 0) = (0 <? b - a).
Proof. intros. unfold Rltb,Acmpb. destruct dec,dec; auto; lra. Qed.

(a - b >? 0) = (0 >? b - a)
Lemma Rminus_gtb0_comm : forall a b : R, (a - b >? 0) = (0 >? b - a).
Proof. intros. unfold Rltb,Acmpb. destruct dec,dec; auto; lra. Qed.

Suplymentary properties about "real number R"


Rsqr, Rpow2, x*x

There are several ways to represent square:
For example, write sqrt of x has multiple ways: x * x x² Rsqr x Rmult x x x ^ 2 pow x 2
x * x，it is a notation for "Rmult x x" x ^ 2, it is a notation for "pow x 2" x² , it is a notation for "Rsqr x", which defined as x * x. In Coq-std-lib, I should use which one to representing square? What's the famous way? After the search, I find that: x * x，9 x ^ 2, 14 x², 100 So, we should mainly use x², and other ways should be converted to this way, and the lost lemmas should be given manually.
Another question, the lra tactic is working well on "x * x" and "pow x 2", but not working on "x²". So, we use "try (unfold Rsqr in *; lra)" insead of "try lra". In addition, using the tactics ring and field also need to unfold Rsqr.
In conclusion, there are two cases: 1. when use "ring,field,lra", write: unfold Rsqr in *; ring. 2. other cases, write: autorewrite with R; auto with R.
We always prefer x², an exception is when using ring or field tactic.
Lemma xx_Rsqr x : x * x = x².
Proof. auto. Qed.
#[export] Hint Rewrite xx_Rsqr : R.

r ^ 2 = r²
Lemma Rpow2_Rsqr r : r ^ 2 = r².
Proof. ra. Qed.
#[export] Hint Rewrite Rpow2_Rsqr : R.

r ^ 4 = (r²)²
Lemma Rpow4_Rsqr_Rsqr r : r ^ 4 = r²².
Proof. ra. Qed.
#[export] Hint Rewrite Rpow4_Rsqr_Rsqr : R.

r ^ 4 = (r ^ 2) ^ 2
Lemma Rpow4_Rsqr_Rsqr' : forall r : R, r ^ 4 = (r ^ 2) ^ 2.
Proof. intros. lra. Qed.

r² = 1 -> r = 1 \/ r = -1
Lemma Rsqr_eq1 : forall r : R, r² = 1 -> r = 1 \/ r = -1.
Proof.
  intros. replace 1 with 1² in H; [|cbv;ring].
  apply Rsqr_eq_abs_0 in H. rewrite Rabs_R1 in H.
  bdestruct (r <? 0).
  - apply Rabs_left in H0. lra.
  - rewrite Rabs_right in H; auto. lra.
Qed.

x <= 0 -> y <= 0 -> x² = y² -> x = y
Lemma Rsqr_inj_neg : forall x y : R, x <= 0 -> y <= 0 -> x² = y² -> x = y.
Proof. intros. replace x with (- -x)%R; ra. Qed.

About R0 and 0



Lemma Rsqr_R0 : R0² = R0.
Proof.
  ra.
Qed.
#[export] Hint Rewrite Rsqr_R0 : R.
Global Hint Resolve Rsqr_R0 : R.

Lemma Rplus_eq0_if_both0 : forall a b : R, a = 0 -> b = 0 -> a + b = 0.
Proof. intros. subst. lra. Qed.

About R1 and 1



(R1)² = 1
Lemma Rsqr_R1 : (R1)² = 1.
Proof. ra. Qed.

0 <= 1
Lemma zero_le_1 : 0 <= 1.
Proof. auto with R. Qed.

0 <> 1
Lemma zero_neq_1 : 0 <> 1.
Proof. auto with R. Qed.

/ R1 = 1
Lemma Rinv_R1 : / R1 = 1.
Proof. ra. Qed.

a / 1 = a
Lemma Rdiv_1 : forall a, a / 1 = a.
Proof. ra. Qed.

0 / a = 0
Lemma Rdiv_0_eq0 : forall a : R, a <> 0 -> 0 / a = 0.
Proof. intros. field; auto. Qed.

#[export] Hint Rewrite
  Rsqr_R1
  Rinv_1
  Rinv_R1
  Rdiv_1
  Rdiv_0_eq0
  : R.

#[export] Hint Resolve
  Rsqr_R1
  Rinv_1
  zero_le_1
  zero_neq_1
  : R.

Module TEST_R1_and_1.
  Goal 1 = R1. auto with R. Qed.
  Goal R1² = 1. auto with R. Qed.
  Goal 1² = R1. auto with R. Qed.
  Goal /R1 = R1. auto with R. Qed.
  Goal /R1 = 1. auto with R. Qed.
  Goal /1 = R1. auto with R. Qed.
  Goal 0 <= R1. auto with R. Qed.
End TEST_R1_and_1.

About "-a" and "a-b"


Lemma Rsub_opp r1 r2 : r1 - (- r2) = r1 + r2.
Proof.
  ring.
Qed.
#[export] Hint Rewrite Rsub_opp : R.
Lemma Rsqr_opp : forall r : R, (- r)² = r ².
Proof. intros. rewrite <- Rsqr_neg. auto. Qed.

Lemma Ropp_Rmul_Ropp_l : forall (r : R), - ((- r) * r) = r².
Proof. intros. cbv. ring. Qed.

Lemma Ropp_Rmul_Ropp_r : forall (r : R), - (r * (- r)) = r².
Proof. intros. cbv. ring. Qed.

Lemma Rmult_neg1_l : forall r : R, (- 1) * r = - r.
Proof. intros. lra. Qed.

Lemma Rmult_neg1_r : forall r : R, r * (- 1) = - r.
Proof. intros. lra. Qed.

#[export] Hint Rewrite
  
  
  Rsqr_opp
  Ropp_mult_distr_l_reverse
  Ropp_mult_distr_r_reverse
  Rdiv_opp_l
  Rdiv_opp_r
  Rmult_neg1_l
  Rmult_neg1_r
  : R.

About "/a" and "a/b"


Lemma Rinv_ab_simpl_a : forall r1 r2 r3,
    r1 <> 0 -> r3 <> 0 -> (r1 * r2) * / (r1 * r3) = r2 * / r3.
Proof. intros. field; auto. Qed.

Lemma Rinv_ab_simpl_b : forall r1 r2 r3,
    r2 <> 0 -> r3 <> 0 -> (r1 * r2) * / (r3 * r2) = r1 * / r3.
Proof. intros. field; auto. Qed.

Lemma Rdiv_1_neq_0_compat : forall r : R, r <> 0 -> 1 / r <> 0.
Proof. intros. pose proof (Rinv_neq_0_compat r H). ra. Qed.

#[export] Hint Rewrite
  Rinv_ab_simpl_a
  Rinv_ab_simpl_b
  : R.

About "square"


r * r

Lemma Rsqr_ge0 : forall r, 0 <= r * r.
Proof. ra. Qed.

r1² + r2²

r1² + r2² = 0 <-> r1 = 0 /\ r2 = 0
Lemma Rplus2_sqr_eq0 : forall r1 r2, r1² + r2² = 0 <-> r1 = 0 /\ r2 = 0.
Proof. ra. Qed.


r1² + r2² = 0 -> r1 = 0
Lemma Rplus2_sqr_eq0_l : forall r1 r2, r1² + r2² = 0 -> r1 = 0.
Proof. ra. Qed.

r1² + r2² = 0 -> r2 = 0
Lemma Rplus2_sqr_eq0_r : forall r1 r2, r1² + r2² = 0 -> r2 = 0.
Proof. ra. Qed.

r1² + r2² <> 0 <-> r1 <> 0 \/ r2 <> 0
Lemma Rplus2_sqr_neq0 : forall r1 r2, r1² + r2² <> 0 <-> r1 <> 0 \/ r2 <> 0.
Proof. ra. Qed.

r1*r1 + r2*r2 <> 0 -> 0 < r1*r1 + r2*r2
Lemma Rplus2_sqr_neq0_iff_gt0 : forall r1 r2 : R,
  r1² + r2² <> 0 <-> 0 < r1² + r2².
Proof. ra. Qed.

2 * a * b <= a² + b²
Lemma R_neq1 : forall r1 r2 : R, 2 * r1 * r2 <= r1² + r2².
Proof. intros. apply Rge_le. apply Rminus_ge. rewrite <- Rsqr_minus. auto with R. Qed.

0 <= r1² + r2²
Lemma Rplus2_sqr_ge0 : forall r1 r2 : R, 0 <= r1² + r2².
Proof. ra. Qed.


0 < r1² + r2² <-> (r1 <> 0 \/ r2 <> 0)
Lemma Rplus2_sqr_gt0 : forall r1 r2 : R, 0 < r1² + r2² <-> (r1 <> 0 \/ r2 <> 0).
Proof. ra. Qed.

r1 <> 0 -> 0 < r1² + r2²
Lemma Rplus2_sqr_gt0_l : forall r1 r2, r1 <> 0 -> 0 < r1² + r2².
Proof. ra. Qed.

r2 <> 0 -> 0 < r1² + r2²
Lemma Rplus2_sqr_gt0_r : forall r1 r2, r2 <> 0 -> 0 < r1² + r2².
Proof. ra. Qed.

r1² + r2² + r3²

r1² + r2² + r3² = 0 <-> r1 = 0 /\ r2 = 0 /\ r3 = 0
Lemma Rplus3_sqr_eq0 : forall r1 r2 r3 : R,
  r1² + r2² + r3² = 0 <-> r1 = 0 /\ r2 = 0 /\ r3 = 0.
Proof. ra. Qed.

r1² + r2² + r3² <> 0 <-> r1 <> 0 \/ r2 <> 0 \/ r3 <> 0
Lemma Rplus3_sqr_neq0 : forall r1 r2 r3 : R,
  r1² + r2² + r3² <> 0 <-> r1 <> 0 \/ r2 <> 0 \/ r3 <> 0.
Proof. ra. Qed.

r1² + r2² + r3² + r4²

r1² + r2² + r3² + r4² = 0 <-> r1 = 0 /\ r2 = 0 /\ r3 = 0 /\ r4 = 0
Lemma Rplus4_sqr_eq0 : forall r1 r2 r3 r4 : R,
  r1² + r2² + r3² + r4² = 0 <-> r1 = 0 /\ r2 = 0 /\ r3 = 0 /\ r4 = 0.
Proof. ra. Qed.

r1² + r2² + r3² + r4² <> 0 <-> r1 <> 0 \/ r2 <> 0 \/ r3 <> 0 \/ r4 <> 0
Lemma Rplus4_sqr_neq0 : forall r1 r2 r3 r4 : R,
  r1² + r2² + r3² + r4² <> 0 <-> r1 <> 0 \/ r2 <> 0 \/ r3 <> 0 \/ r4 <> 0.
Proof. ra. Qed.

Global Hint Resolve
  Rsqr_ge0
  Rplus2_sqr_eq0
  Rplus2_sqr_eq0_l
  Rplus2_sqr_eq0_r
  Rplus2_sqr_neq0
  Rplus2_sqr_neq0_iff_gt0
  Rplus2_sqr_ge0
  Rplus2_sqr_gt0
  Rplus3_sqr_eq0
  Rplus3_sqr_neq0
  Rplus4_sqr_eq0
  Rplus4_sqr_neq0
  R_neq1
  : R.

Section test.
r * r = 0 <-> r = 0
  Goal forall r, r * r = 0 <-> r = 0. ra. Qed.
  Goal forall r, r * r <> 0 <-> r <> 0. ra. Qed.
  Goal forall r1 r2 : R, 0 <= r1 * r1 + r2 * r2. ra. Qed.
  Goal forall r1 r2 : R, r1 <> 0 \/ r2 <> 0 <-> r1 * r1 + r2 * r2 <> 0. ra. Qed.
  Goal forall r1 r2 : R, r1 * r1 + r2 * r2 <> 0 <-> 0 < r1 * r1 + r2 * r2. ra. Qed.
  Goal forall r1 r2 r3 : R,
      r1 <> 0 \/ r2 <> 0 \/ r3 <> 0 <-> r1 * r1 + r2 * r2 + r3 * r3 <> 0. ra. Qed.
  Goal forall r1 r2 r3 r4 : R,
      r1 <> 0 \/ r2 <> 0 \/ r3 <> 0 \/ r4 <> 0 <->
        r1 * r1 + r2 * r2 + r3 * r3 + r4 * r4 <> 0. ra. Qed.
End test.

About "absolute value"


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

Lemma Rabs_neg_left : forall r, 0 <= r -> | -r | = r.
Proof.
  intros. rewrite Rabs_Ropp. apply Rabs_right; nra.
Qed.

Lemma Rabs_neg_right : forall r, r < 0 -> | -r| = -r.
Proof.
  intros. rewrite Rabs_Ropp. apply Rabs_left; nra.
Qed.

Global Hint Resolve
  Rabs_right
  Rabs_pos_eq
  Rabs_left
  Rabs_left1
  Rabs_neg_left
  Rabs_neg_right
  : R.

About "sqrt"

sqrt (r * r) = |r|
Lemma sqrt_square_abs : forall r, sqrt (r * r) = |r|.
Proof.
  intros. destruct (Rcase_abs r).
  - replace (r * r) with ((-r) * (-r)) by nra.
    rewrite sqrt_square; try nra. auto with R.
  - rewrite sqrt_square; auto with R.
Qed.

Lemma sqrt_1 : sqrt 1 = 1.
Proof.
  apply Rsqr_inj; autorewrite with R; auto with R.
Qed.

Lemma sqrt_0_eq0 : forall r, r = 0 -> sqrt r = 0.
Proof. intros. rewrite H. ra. Qed.

Lemma sqrt_le0_eq_0 : forall r, r <= 0 -> sqrt r = 0.
Proof.
  intros. Transparent sqrt. unfold sqrt. destruct (Rcase_abs r); auto.
  assert (r = 0); try lra. subst. compute.
  destruct (Rsqrt_exists). destruct a.
  symmetry in H1. auto with R.
Qed.

Lemma sqrt_lt0_eq_0 : forall r, r < 0 -> sqrt r = 0.
Proof.
  intros. apply sqrt_le0_eq_0. auto with R.
Qed.

Lemma sqrt_gt0_imply_gt0 : forall (x : R), 0 < sqrt x -> 0 < x.
Proof.
  intros. replace 0 with (sqrt 0) in H; auto with R.
  apply sqrt_lt_0_alt in H; auto.
Qed.

Lemma sqrt_gt0_imply_ge0 : forall (x : R), 0 < sqrt x -> 0 <= x.
Proof.
  intros. apply Rlt_le. apply sqrt_gt0_imply_gt0; auto.
Qed.

Lemma sqrt_eq1_imply_eq1 : forall (x : R), sqrt x = 1 -> x = 1.
Proof.
  intros.
  assert ((sqrt x)² = 1). rewrite H. autounfold with R in *; ring.
  rewrite <- H0.
  apply eq_sym. apply Rsqr_sqrt.
  assert (0 < sqrt x). rewrite H; auto with R.
  apply sqrt_gt0_imply_gt0 in H1. auto with R.
Qed.

Lemma sqrt_eq1_iff : forall (x : R), sqrt x = 1 <-> x = 1.
Proof.
  intros. split; intros.
  - apply sqrt_eq1_imply_eq1; auto.
  - subst. rewrite sqrt_1; auto.
Qed.

sqrt x = 0 <-> x <= 0
Lemma sqrt_eq0_iff : forall r, sqrt r = 0 <-> r <= 0.
Proof.
  intros. split; intros.
  - bdestruct (r <=? 0); ra.
    apply Rnot_le_lt in H0. apply sqrt_lt_R0 in H0. ra.
  - apply sqrt_neg_0; auto.
Qed.

sqrt x <> 0 <-> x > 0
Lemma sqrt_neq0_iff : forall r, sqrt r <> 0 <-> r > 0.
Proof.
  intros. split; intros; ra.
  bdestruct (r =? 0). subst. autorewrite with R in H. ra.
  bdestruct (r <? 0); ra. apply sqrt_lt0_eq_0 in H1. ra.
Qed.

( √ r1 * √ r2)^2 = r1 * r2
Lemma Rsqr_sqrt_sqrt r1 r2 : 0 <= r1 -> 0 <= r2 ->
  ((sqrt r1) * (sqrt r2))² = r1 * r2.
Proof.
  destruct (Rcase_abs r1), (Rcase_abs r2); try lra.
  autorewrite with R; auto with R.
  autorewrite with sqrt; ra.
Qed.

If the sqrt of the sum of squares of two real numbers equal to 0, iff both of them are 0.
Lemma Rsqrt_plus_sqr_eq0_iff : forall r1 r2 : R,
  sqrt (r1² + r2²) = 0 <-> r1 = 0 /\ r2 = 0.
Proof.
  intros. autorewrite with R. split; intros H.
  - apply sqrt_eq_0 in H; ra.
  - destruct H; subst. autorewrite with R; auto with R.
Qed.

The multiplication of the square roots of two real numbers is >= 0
Lemma Rmult_sqrt_sqrt_ge0 : forall r1 r2 : R, 0 <= (sqrt r1) * (sqrt r2).
Proof.
  intros. apply Rmult_le_pos; auto with R.
Qed.

The addition of the square roots of two real numbers is >= 0
Lemma Rplus_sqrt_sqrt_ge0 : forall r1 r2 : R, 0 <= (sqrt r1) + (sqrt r2).
Proof.
  intros. apply Rplus_le_le_0_compat; auto with R.
Qed.

Lemma Rsqr_plus_sqr_neq0_l : forall r1 r2, r1 <> 0 -> sqrt (r1² + r2²) <> 0.
Proof.
  intros. auto 6 with R.
Qed.

Lemma Rsqr_plus_sqr_neq0_r : forall r1 r2, r2 <> 0 -> sqrt (r1² + r2²) <> 0.
Proof.
  intros. auto 6 with R.
Qed.

/(sqrt (1+(b/a)²)) = abs(a) / sqrt(a*a + b*b)
Lemma Rinv_sqrt_plus_1_sqr_div_a_b (a b : R) : a <> 0 ->
  (/ (sqrt (1+(b/a)²)) = |a| / sqrt(a*a + b*b)).
Proof.
  intros.
  replace (1 + (b/a)²) with ((a*a + b*b) / (|a|*|a|)).
  - rewrite sqrt_div_alt.
    + rewrite sqrt_square.
      * field. split; autorewrite with R; auto 6 with R.
      * auto with R.
    + autorewrite with R; auto with R.
  - unfold Rsqr.
    destruct (Rcase_abs a).
    + replace (|a|) with (-a). field; auto. rewrite Rabs_left; auto.
    + replace (|a|) with a. field; auto. rewrite Rabs_right; auto.
Qed.

(√ r1 * √ r2) * (√ r1 * √ r2) = r1 * r2
Lemma sqrt_mult_sqrt : forall (r1 r2 : R),
  0 <= r1 -> 0 <= r2 ->
  ((sqrt r1) * (sqrt r2)) * ((sqrt r1) * (sqrt r2)) = r1 * r2.
Proof.
  intros. ring_simplify. repeat rewrite pow2_sqrt; auto.
Qed.

#[export] Hint Rewrite
  sqrt_square_abs
  
  sqrt_1
  Rsqr_sqrt_sqrt
  sqrt_mult_sqrt
  : R.

Global Hint Resolve
  sqrt_1
  sqrt_le0_eq_0
  sqrt_lt0_eq_0
  sqrt_gt0_imply_gt0
  sqrt_gt0_imply_ge0
  sqrt_eq1_imply_eq1
  Rsqr_sqrt_sqrt
  sqrt_mult_sqrt
  Rmult_sqrt_sqrt_ge0
  Rplus_sqrt_sqrt_ge0
  sqrt_square
  Rsqr_plus_sqr_neq0_l
  Rsqr_plus_sqr_neq0_r
  : R.

simplify expression has sqrt and pow2
Ltac simpl_sqrt_pow2 :=
  repeat (
  
  unfold Rsqr;
  
  try rewrite sqrt_mult_sqrt;
  
  try rewrite pow2_sqrt;
  
  try rewrite sqrt_pow2;
  
  try rewrite sqrt_sqrt
  ).

Section TEST_Rsqrt.
  Goal sqrt R1 = R1. autorewrite with R; auto with R. Qed.

End TEST_Rsqrt.

Automatically prove the goal such as "sqrt x = y"
Ltac solve_sqrt_eq :=
  match goal with
  | |- sqrt ?x = ?y => apply Rsqr_inj; [ra|ra|rewrite Rsqr_sqrt;ra]
  end.

About "trigonometric functions"

sin R0 = 0
Lemma sin_R0 : sin R0 = 0.
Proof. pose proof sin_0. ra. Qed.

cos R0 = 1
Lemma cos_R0 : cos R0 = 1.
Proof. pose proof cos_0. ra. Qed.

Lemma sin_PI2_neg : sin (- (PI/2)) = -1.
Proof.
  rewrite sin_neg. rewrite sin_PI2. auto.
Qed.

Lemma cos_PI2_neg : cos (- (PI/2)) = 0.
Proof.
  rewrite cos_neg. apply cos_PI2.
Qed.

Lemma sin_plus_PI : forall r, sin (r + PI) = (- (sin r))%R.
Proof.
  apply neg_sin.
Qed.

Lemma sin_sub_PI : forall r, sin (r - PI) = (- (sin r))%R.
Proof.
  intros. replace (r - PI)%R with (- (PI - r))%R; try ring.
  rewrite sin_neg. rewrite Rtrigo_facts.sin_pi_minus. auto.
Qed.

Lemma cos_plus_PI : forall r, cos (r + PI) = (- (cos r))%R.
Proof.
  apply neg_cos.
Qed.

Lemma cos_sub_PI : forall r, cos (r - PI) = (- (cos r))%R.
Proof.
  intros. replace (r - PI)%R with (- (PI - r))%R; try ring.
  rewrite cos_neg. apply Rtrigo_facts.cos_pi_minus.
Qed.

Lemma cos2_sin2: forall x : R, (cos x)² + (sin x)² = 1.
Proof.
  intros. rewrite Rplus_comm. apply sin2_cos2.
Qed.

Lemma cos2' : forall x : R, (cos x) ^ 2 = (1 - (sin x) ^ 2)%R.
Proof. intros. autorewrite with R. rewrite cos2. auto. Qed.

Lemma sin2' : forall x : R, (sin x) ^ 2 = (1 - (cos x) ^ 2)%R.
Proof. intros. autorewrite with R. rewrite sin2. auto. Qed.

Lemma Rtan_rw : forall r : R, sin r * / cos r = tan r.
Proof. auto. Qed.

Lemma cos_neg0 : forall r : R, - PI / 2 < r < PI / 2 -> cos r <> 0.
Proof. intros. assert (0 < cos r). { apply cos_gt_0; ra. } ra. Qed.

#[export] Hint Rewrite
  sin_0
  sin_R0
  cos_0
  cos_R0
  sin_PI
  cos_PI
  sin_PI2
  cos_PI2
  sin_PI2_neg
  cos_PI2_neg
  sin_plus_PI
  sin_sub_PI
  cos_plus_PI
  cos_sub_PI
  sin2_cos2
  cos2_sin2
  cos_plus
  cos_minus
  sin_plus
  sin_minus
  cos_neg
  sin_neg
  Rtan_rw
  atan_tan
  asin_sin
  acos_cos
  asin_opp
  acos_opp
  atan_opp
  : R.

#[export] Hint Resolve
  sin_0
  sin_R0
  cos_0
  cos_R0
  sin_PI
  cos_PI
  sin_PI2
  cos_PI2
  sin_PI2_neg
  cos_PI2_neg
  sin_plus_PI
  sin_sub_PI
  cos_plus_PI
  cos_sub_PI
  sin2_cos2
  cos2_sin2
  cos_neg
  sin_neg
  cos_neg0
  : R.

Section TEST_sin_cos_tan.
  Goal forall x, cos x * cos x + sin x * sin x = R1.
  intros; autorewrite with R; auto with R. Qed.

  Goal forall x, sin x * sin x + cos x * cos x = R1.
  intros; autorewrite with R; auto with R. Qed.

End TEST_sin_cos_tan.

About "Rpower"

Rpower rules: 
  1. Definition of Rpower
  a^n       = a * a * ... * a    (* there are n numbers *)
  a^0       = 1 (a ≠ 0)
  a^(-n)    = 1 / a^n (a ≠ 0)
  a^(m/n)   = n√ a^m  (a > 0)
  a^(-m/n)  = 1 / n√ a^m  (a > 0)
Lemma Rpower_neq0 x y : x <> 0 -> Rpower x y <> 0.
Proof.
  Abort.

Automatic solving equalites or inequalities on real numbers


r = 0


Lemma Rmult_eq_self_imply_0_or_k1 : forall k x,
    k * x = x -> x = 0 \/ (x <> 0 /\ k = R1).
Proof. ra. Qed.

Lemma Rsqr_eq0_if0 : forall r, r = 0 -> r² = 0. ra. Qed.

Lemma Rmult_eq_reg_l_rev : forall r r1 r2 : R, r * r1 = r * r2 -> r1 <> r2 -> r = 0.
Proof. ra. Qed.

Lemma Rmult_eq_reg_r_rev : forall r r1 r2 : R, r1 * r = r2 * r -> r1 <> r2 -> r = 0.
Proof. ra. Qed.

0 <= x

deprecated

Section TEST_zero_le.
  Goal forall r, 0 <= r * r. ra. Qed.
  Goal forall r, 0 <= r². ra. Qed.
  Goal forall r1 r2, 0 <= r1 * r1 + r2 * r2. ra. Qed.
  Goal forall r1 r2, 0 <= r1² + r2². ra. Qed.
  Goal forall r1 r2, 0 <= r1 * r1 + r2². ra. Qed.
  Goal forall r1 r2, 0 <= r1² + r2 * r2. ra. Qed.
  Goal forall r, 0 <= r -> 0 <= r * 5. ra. Qed.
  Goal forall r, 0 <= r -> 0 <= r * 5 * 10. ra. Qed.
  Goal forall r, 0 <= r -> 0 <= r * (/5) * 10. ra. Qed.
End TEST_zero_le.

a >= 0 -> b < 0 -> a / b <= 0
Lemma Rdiv_ge0_lt0_le0 : forall a b : R, a >= 0 -> b < 0 -> a / b <= 0.
Proof. intros. unfold Rdiv. assert (/b<0); ra. Qed.

Lemma Rdiv_gt_0_compat_neg: forall a b : R, a < 0 -> b < 0 -> 0 < a / b.
Proof. intros. unfold Rdiv. assert (/b < 0); ra. Qed.

Lemma Rdiv_ge_0_compat: forall a b : R, 0 <= a -> 0 < b -> 0 <= a / b.
Proof. intros. unfold Rdiv. assert (0 < /b); ra. Qed.

Lemma Rsqr_gt0 : forall a : R, 0 <= a * a.
Proof. intros. nra. Qed.

0 <= a -> 0 <= b -> a + b = 0 -> b = 0
Lemma Rplus_eq_0_r : forall a b : R, 0 <= a -> 0 <= b -> a + b = 0 -> b = 0.
Proof. intros. lra. Qed.

Hint Resolve
  Rdiv_ge0_lt0_le0
  Rdiv_gt_0_compat_neg
  Rdiv_ge_0_compat
  : R.

0 < x

deprecated

Section TEST_zero_lt.
  Goal forall r, 0 <> r -> 0 < r * r. ra. Qed.
  Goal forall r, 0 <> r -> 0 < r². ra. Qed.
  Goal forall r, 0 < r -> 0 < r * r. ra. Qed.
  Goal forall r, 0 < r -> 0 < r². ra. Qed.
  Goal forall r1 r2, r1 <> 0 -> 0 < r1 * r1 + r2 * r2. ra. Qed.
  Goal forall r1 r2, r1 <> 0 -> 0 < r1² + r2 * r2. ra. Qed.
  Goal forall r1 r2, r1 <> 0 -> 0 < r1 * r1 + r2². ra. Qed.

  Goal forall r1 r2, r2 <> 0 -> 0 < r1 * r1 + r2 * r2. ra. Qed.
  Goal forall r1 r2, r2 <> 0 -> 0 < r1² + r2 * r2. ra. Qed.
  Goal forall r1 r2, r2 <> 0 -> 0 < r1 * r1 + r2². ra. Qed.

  Goal forall r1 r2, 0 < r1 -> 0 < r1 * r1 + r2 * r2. ra. Qed.
  Goal forall r1 r2, 0 < r2 -> 0 < r1 * r1 + r2 * r2. ra. Qed.

  Goal forall r, 0 < r -> 0 < r * 10. ra. Qed.
  Goal forall r, 0 < r -> 0 < r + 10. ra. Qed.
  Goal forall r, 0 < r -> 0 < r * 100 + 23732. ra. Qed.

End TEST_zero_lt.

This property is used in in Complex. Although lra can solve it, but using a special lemma name combined with the match machanism could speed up the proof.
a <> b -> a <= b -> a < b
Lemma Rneq_le_lt : forall a b, a <> b -> a <= b -> a < b.
Proof. ra. Qed.

0 < r -> 0 < 1 / r
Lemma Rinv1_gt0 : forall r : R, 0 < r -> 0 < 1 / r.
Proof. cbv. ra. Qed.

0 < a -> b < 0 -> a / b < 0
Lemma Rdiv_lt_0_compat_l: forall a b : R, 0 < a -> b < 0 -> a / b < 0.
Proof. intros. unfold Rdiv. assert (/b < 0); ra. Qed.

a < 0 -> 0 < b -> a / b < 0
Lemma Rdiv_lt_0_compat_r: forall a b : R, a < 0 -> 0 < b -> a / b < 0.
Proof. intros. unfold Rdiv. assert (/b > 0); ra. Qed.

#[export] Hint Resolve
  Rdiv_lt_0_compat_l
  Rdiv_lt_0_compat_r
  Rneq_le_lt
  Rinv1_gt0
  : R.

x <> 0



Section TEST_neq_zero.
  Goal forall r, r² <> 0 <-> r <> 0. ra. Qed.
  Goal forall r, r² <> 0 -> r <> 0. ra. Qed.
  Goal forall r, r <> 0 -> r * r <> 0. ra. Qed.
  Goal forall r, r <> 0 -> r² <> 0. ra. Qed.

  Goal forall r, 0 <> r * r -> r <> 0. ra. Qed.
  Goal forall r, r * r <> 0 -> 0 <> r. ra. Qed.
  Goal forall r, 0 <> r * r -> 0 <> r. ra. Qed.

  Goal forall r1 r2 r3 r4 : R,
    r1 <> 0 \/ r2 <> 0 \/ r3 <> 0 \/ r4 <> 0 <->
    r1 * r1 + r2 * r2 + r3 * r3 + r4 * r4 <> 0.
  Proof. ra. Qed.

End TEST_neq_zero.

a < b


Lemma Rdiv_le_imply_Rmul_gt a b c : b > 0 -> a * /b < c -> a < b * c.
Proof.
  intros.
  apply (Rmult_lt_compat_l b) in H0; auto.
  replace (b * (a * /b)) with a in H0; auto.
  field. auto with R.
Qed.
Global Hint Resolve Rdiv_le_imply_Rmul_gt : R.

Lemma Rmul_gt_imply_Rdiv_le a b c : b > 0 -> a < b * c -> a * /b < c.
Proof.
  intros.
  apply (Rmult_lt_compat_l (/b)) in H0; auto with R.
  autorewrite with R in *.
  replace (/b * a) with (a / b) in *; try field; auto with R.
  replace (/b * (b * c)) with c in *; try field; auto with R.
Qed.
Global Hint Resolve Rmul_gt_imply_Rdiv_le : R.

Lemma Rlt_Rminus : forall a b : R, a < b -> 0 < b - a.
Proof. intros. apply (proj2 (Rlt_0_minus a b)); auto. Qed.


Ltac tac_le :=
  autounfold with R;
  match goal with
  | |- 0 < ?a + - ?b => apply Rlt_Rminus
  | |- ?a * (?b * /?c) < ?e => replace (a * (b * /c)) with ((a * b) * /c)
  | |- ?a * /?b < ?c => assert (a < b * c); assert (0 < b)
  | |- _ => idtac
  end; try lra; auto with R.

Section TEST_tac_le.

This proof cannot be finished in one step
  Goal forall h T, 0 < h -> h < 9200 -> -60 < T -> T < 60 -> h / (273.15 + T) < 153.
    ra. Abort.

Naming the hypothesises
  Variable h T : R.
  Hypothesis Hh1 : 0 < h.
  Hypothesis Hh2 : h < 9200.
  Hypothesis HT1 : -60 < T.
  Hypothesis HT2 : T < 60.

a simpler proposition can be proved in one step
  Goal h * 0.0065 < 273.15 + T. ra. Qed.

We can finish the original proof with manually help
  Goal h / (273.15 + T) < 153.
    autounfold with R.
    assert (273.15 + T > 0). ra.
    assert (h < (273.15 + T) * 153). ra. auto with R.
  Qed.

Another example, also need to manually
  Goal h / (273.15 + T) < 1 / 0.0065.
  Proof.
    ra.     autounfold with R.
    assert (273.15 + T > 0). ra.
    assert (h < (273.15 + T) * (1/0.0065)). ra. auto with R.
  Qed.

  Goal h / (273.15 + T) < 1 / 0.0065.
  Proof.
    tac_le.
  Qed.

This example shows the usage of tac_le and ra together.
  Goal 0 < 1 - (0.0065 * (h * / (273.15 + T))).
  Proof.
    assert (h / (273.15 + T) < 1/0.0065).
    tac_le. ra.
  Qed.

  Goal 0 < 1 - (0.0065 * (h * / (273.15 + T))).
  Proof.
    do 3 tac_le.
  Qed.

End TEST_tac_le.

Examples which cannot automatically solved now

This example comes from a proof about Carg in Complex.
Goal forall a b r, a > 0 -> b <= r / a -> 0 <= r - b *a.
Proof.
  intros.
  ra.   apply Rmult_le_compat_r with (r:=a) in H0; ra.
  unfold Rdiv in H0. rewrite Rmult_assoc in H0.
  rewrite Rinv_l in H0; ra.
Qed.

Compare with PI

Section compare_with_PI.

How to prove the inequalities about PI
  Goal 2 < PI.
  Proof.
  Abort.

One method: give the upper and lower bound of PI with concrete value by axiom, then use transitivity to solve it by lra.
  Notation PI_ub := 3.14159266.
  Notation PI_lb := 3.14159265.

  Axiom PI_upper_bound : PI < PI_ub.
  Axiom PI_lower_bound : PI_lb < PI.

  Lemma PI_bound : PI_lb < PI < PI_ub.
  Proof. split. apply PI_lower_bound. apply PI_upper_bound. Qed.

  Goal 2 < PI.
  Proof.
    apply Rlt_trans with PI_lb. lra. apply PI_bound.
  Abort.

  Goal 2 < PI.
  Proof.
    pose proof PI_bound. lra.
  Abort.

End compare_with_PI.

OLD CODE EARLY, they should be carefuly CHECKED and then DISCARDED







Simplification for trigonometric functions



















Split a large range to small pieces

Split the range of (-π,π] to several small ranges
Section a_strange_problem.

Tips: A strange problem about "lra": If I declare a condition here, the next proof will be finished by lra, otherwise, the next proof will not be done.
  Variable b: R.
  Hypotheses Hb : - PI < b < PI.

  Lemma Rsplit_neg_pi_to_pi' : forall a : R,
      -PI < a <= PI <->
        a = -PI/2 \/ a = 0 \/ a = PI/2 \/
          (-PI < a < -PI/2) \/ (-PI/2 < a < 0) \/
          (0 < a < PI/2) \/ (PI/2 < a <= PI).
  Proof.
    intros.
    lra.
  Qed.
End a_strange_problem.

Lemma Rsplit_neg_pi_to_pi : forall a : R,
    -PI < a <= PI <->
      a = -PI/2 \/ a = 0 \/ a = PI/2 \/
        (-PI < a < -PI/2) \/ (-PI/2 < a < 0) \/
        (0 < a < PI/2) \/ (PI/2 < a <= PI).
Proof.
  intros.
  pose proof PI_bound. lra.
Qed.

atan

背景： 在 atan2 的证明中，经常需要化简形如 atan ((a * b) / (a * c)) 的式子
atan (k * a) (k * b) = atan a b
Lemma atan_ka_kb : forall a b k : R,
    b <> 0 -> k <> 0 -> atan ((k * a) / (k * b)) = atan (a/b).
Proof. intros. f_equal. field. ra. Qed.

atan (a * k) (b * k) = atan a b
Lemma atan_ak_bk : forall a b k : R,
    b <> 0 -> k <> 0 -> atan ((a * k) /(b * k)) = atan (a/b).
Proof. intros. f_equal. field. ra. Qed.

0 < atan x < π/2
Lemma atan_bound_gt0 : forall x, x > 0 -> 0 < atan x < PI/2.
Proof.
  intros. split.
  - rewrite <- atan_0. apply atan_increasing; ra.
  - pose proof (atan_bound x); ra.
Qed.

  • π/2 < atan x < 0
Lemma atan_bound_lt0 : forall x, x < 0 -> - PI / 2 < atan x < 0.
Proof.
  intros. split.
  - pose proof (atan_bound x); ra.
  - rewrite <- atan_0. apply atan_increasing; ra.
Qed.

0 <= atan x < π/2
Lemma atan_bound_ge0 : forall x, x >= 0 -> 0 <= atan x < PI/2.
Proof.
  intros. bdestruct (x =? 0).
  - subst. rewrite atan_0; cbv; ra.
  - assert (x > 0); ra. pose proof (atan_bound_gt0 x H1); ra.
Qed.

  • π/2 < atan x <= 0
Lemma atan_bound_le0 : forall x, x <= 0 -> - PI / 2 < atan x <= 0.
Proof.
  intros. bdestruct (x =? 0).
  - subst. rewrite atan_0; cbv; ra. split; ra. assert (PI > 0); ra.
  - assert (x < 0); ra. pose proof (atan_bound_lt0 x H1); ra.
Qed.

Conversion between R and other types

Remark:
We need two functions commonly used in computer: floor (rounding down), and ceiling (rounding up). Although the function "up" in Coq-std-lib is looks like a rounding up function, but it is a bit different. We need to explicitly define them. Meanwhile, we tested their behaviors on negative numbers
The behavior of "up" is this: 2.0 <= r < 3.0 -> up(r) = 3, and there is a lemma saying this: Check archimed.
But we need the behavior of floor and ceiling are these below exactly: 1. floor 2.0 <= r < 3.0 -> floor(r) = 2 So, floor(r) = up(r) - 1 2. ceiling 2.0 < r < 3.0 -> ceiling(r) = 3 r = 2.0 -> ceiling(r)=2 So, if IZR(up(r))=r，then ceiling(r)=up(r)-1，else ceiling(r)=up(r).
When talking about negative numbers, their behaviors are below: floor 2.0 = 2 floor 2.5 = 2 floor -2.0 = -2 floor -2.5 = -3
ceiling 2.0 = 2 ceiling 2.5 = 3 ceiling -2.0 = -2 ceiling -2.5 = -2

Properties about up and IZR

Eliminate the up_IZR
Lemma up_IZR : forall z, up (IZR z) = (z + 1)%Z.
Proof.
  intros.
  rewrite up_tech with (r:=IZR z); auto; ra.
  apply IZR_lt. lia.
Qed.

There is a unique integer if such a IZR_up equation holds.
Lemma IZR_up_unique : forall r, r = IZR (up r - 1) -> exists! z, IZR z = r.
Proof.
  intros.
  exists (up r - 1)%Z. split; auto.
  intros. subst.
  rewrite up_IZR in *.
  apply eq_IZR. auto.
Qed.

There isn't any integer z and real number r such that r ∈(IZR z, IZR (z+1))
Lemma IZR_in_range_imply_no_integer : forall r z,
    IZR z < r ->
    r < IZR (z + 1) ->
    ~(exists z', IZR z' = r).
Proof.
  intros. intro. destruct H1. subst.
  apply lt_IZR in H0.
  apply lt_IZR in H. lia.
Qed.

Conversion between R and other types

Conversion between Z and R

Z to R
Definition Z2R (z : Z) : R := IZR z.

Rounding R to z, take the floor: truncate to the nearest integer not greater than it
Definition R2Z_floor (r : R) : Z := (up r) - 1.

Rounding R to z, take the ceiling: truncate to the nearest integer not less than it
Definition R2Z_ceiling (r : R) : Z :=
  let z := up r in
  if Req_EM_T r (IZR (z - 1)%Z)
  then z - 1
  else z.


z <= r < z+1.0 -> floor(r) = z
Lemma R2Z_floor_spec : forall r z,
    IZR z <= r < IZR z + 1.0 -> R2Z_floor r = z.
Proof.
  intros. unfold R2Z_floor in *. destruct H.
  assert (up r = z + 1)%Z; try lia.
  rewrite <- up_tech with (z:=z); auto.
  rewrite plus_IZR. lra.
Qed.

(r=z -> ceiling r = z) /\ (z < r < z + 1.0 -> ceiling r = z+1)
Lemma R2Z_ceiling_spec : forall r z,
    (r = IZR z -> R2Z_ceiling r = z) /\
      (IZR z < r < IZR z + 1.0 -> R2Z_ceiling r = (z+1)%Z).
Proof.
  intros. unfold R2Z_ceiling in *. split; intros.
  - destruct (Req_EM_T r (IZR (up r - 1))).
    + rewrite H. rewrite up_IZR. lia.
    + rewrite H in n. destruct n.
      rewrite up_IZR. f_equal. lia.
  - destruct H. destruct (Req_EM_T r (IZR (up r - 1))).
    + apply IZR_in_range_imply_no_integer in H; auto.
      * destruct H. exists (up r - 1)%Z; auto.
      * rewrite plus_IZR. ra.
    + rewrite up_tech with (r:=r); auto; ra.
      rewrite plus_IZR. ra.
Qed.

Z2R (R2Z_floor r) is less than r
Lemma Z2R_R2Z_floor_le : forall r, Z2R (R2Z_floor r) <= r.
Proof.
  intros. unfold Z2R,R2Z_floor. rewrite minus_IZR.
  destruct (archimed r). ra.
Qed.

r-1 is less than Z2R (R2Z_floor r)
Lemma Z2R_R2Z_floor_gt : forall r, r - 1 < Z2R (R2Z_floor r).
Proof.
  intros. unfold Z2R,R2Z_floor. rewrite minus_IZR.
  destruct (archimed r). ra.
Qed.

Conversion between nat and R


Definition nat2R (n : nat) : R := Z2R (nat2Z n).
Definition R2nat_floor (r : R) : nat := Z2nat (R2Z_floor r).
Definition R2nat_ceiling (r : R) : nat := Z2nat (R2Z_ceiling r).

Conversion from Q to R

Section Q2R.
  Import Rdefinitions.
  Import Qreals.
  Import QExt.


  Lemma Q2R_eq_iff : forall a b : Q, Q2R a = Q2R b <-> Qeq a b.
  Proof. intros. split; intros. apply eqR_Qeq; auto. apply Qeq_eqR; auto. Qed.

  Lemma Q2R_add : forall a b : Q, Q2R (a + b) = (Q2R a + Q2R b)%R.
  Proof. intros. apply Qreals.Q2R_plus. Qed.

End Q2R.

Conversion from Qc to R

Section Qc2R.
  Import Rdefinitions.
  Import Qreals.
  Import QcExt.

  Section QcExt_additional.

    Lemma this_Q2Qc_eq_Qred : forall a : Q, this (Q2Qc a) = Qred a.
    Proof. auto. Qed.

  End QcExt_additional.

  Definition Qc2R (x : Qc) : R := Q2R (Qc2Q x).

  Lemma Qc2R_add : forall a b : Qc, Qc2R (a + b) = (Qc2R a + Qc2R b)%R.
  Proof.
    intros. unfold Qc2R,Qc2Q. rewrite <- Q2R_add. apply Q2R_eq_iff.
    unfold Qcplus. rewrite this_Q2Qc_eq_Qred. apply Qred_correct.
  Qed.

  Lemma Qc2R_0 : Qc2R 0 = 0%R.
  Proof. intros. cbv. ring. Qed.

  Lemma Qc2R_opp : forall a : Qc, Qc2R (- a) = (- (Qc2R a))%R.
  Proof.
    intros. unfold Qc2R,Qc2Q. rewrite <- Q2R_opp. apply Q2R_eq_iff.
    unfold Qcopp. rewrite this_Q2Qc_eq_Qred. apply Qred_correct.
  Qed.

  Lemma Qc2R_mul : forall a b : Qc, Qc2R (a * b) = (Qc2R a * Qc2R b)%R.
  Proof.
    intros. unfold Qc2R,Qc2Q. rewrite <- Q2R_mult. apply Q2R_eq_iff.
    unfold Qcmult. rewrite this_Q2Qc_eq_Qred. apply Qred_correct.
  Qed.

  Lemma Qc2R_1 : Qc2R 1 = (1)%R.
  Proof. intros. cbv. field. Qed.

  Lemma Qc2R_inv : forall a : Qc, a <> 0 -> Qc2R (/ a) = (/ (Qc2R a))%R.
  Proof.
    intros. unfold Qc2R,Qc2Q. rewrite <- Q2R_inv. apply Q2R_eq_iff.
    unfold Qcinv. rewrite this_Q2Qc_eq_Qred. apply Qred_correct.
    intro. destruct H. apply Qc_is_canon. simpl. auto.
  Qed.

  Lemma Qc2R_eq_iff : forall a b : Qc, Qc2R a = Qc2R b <-> a = b.
  Proof.
    split; intros; subst; auto. unfold Qc2R, Qc2Q in H.
    apply Qc_is_canon. apply eqR_Qeq; auto.
  Qed.

  Lemma Qc2R_lt_iff : forall a b : Qc, (Qc2R a < Qc2R b)%R <-> a < b.
  Proof.
    intros. unfold Qc2R, Qc2Q,Qclt in *. split; intros.
    apply Rlt_Qlt; auto. apply Qlt_Rlt; auto.
  Qed.

  Lemma Qc2R_le_iff : forall a b : Qc, (Qc2R a <= Qc2R b)%R <-> a <= b.
  Proof.
    intros. unfold Qc2R, Qc2Q,Qclt in *. split; intros.
    apply Rle_Qle; auto. apply Qle_Rle; auto.
  Qed.

  #[export] Instance Qc_ConvertToR
    : ConvertToR Qcplus (0%Qc) Qcopp Qcmult (1%Qc) Qcinv Qclt Qcle Qcltb Qcleb Qc2R.
  Proof.
    constructor; intros.
    apply Qc2R_add. apply Qc2R_0. apply Qc2R_opp. apply Qc2R_mul. apply Qc2R_1.
    apply Qc2R_inv; auto. apply Qc_Order. apply Qc2R_eq_iff.
    apply Qc2R_lt_iff. apply Qc2R_le_iff.
  Qed.

End Qc2R.

Approximate of two real numbers

r1 ≈ r2, that means |r1 - r2| <= diff
Definition Rapprox (r1 r2 diff : R) : Prop := |r1 - r2| <= diff.

boolean version of approximate function
Definition Rapproxb (r1 r2 diff : R) : bool := |r1 - r2| <=? diff.

Mathematical Structure


Well-defined (or compatible, or proper morphism) of operations on R.


Lemma Rplus_wd : Proper (eq ==> eq ==> eq) Rplus.
Proof. simp_proper. intros; subst; ring. Qed.

Lemma Ropp_wd : Proper (eq ==> eq) Ropp.
Proof. simp_proper. intros; subst; ring. Qed.

Lemma Rminus_wd : Proper (eq ==> eq ==> eq) Rminus.
Proof. simp_proper. intros; subst; ring. Qed.

Lemma Rmult_wd : Proper (eq ==> eq ==> eq) Rmult.
Proof. simp_proper. intros; subst; ring. Qed.

Lemma Rinv_wd : Proper (eq ==> eq) Rinv.
Proof. simp_proper. intros; subst; ring. Qed.

Lemma Rdiv_wd : Proper (eq ==> eq ==> eq) Rdiv.
Proof. simp_proper. intros; subst; ring. Qed.

Hint Resolve
  Rplus_wd Ropp_wd Rminus_wd Rmult_wd Rinv_wd Rdiv_wd
  : wd.

Useful structures


#[export] Instance R_Order : Order Rlt Rle Rltb Rleb.
Proof.
  constructor; intros; try lra.
  destruct (total_order_T a b) as [[H|H]|H]; auto.
  apply Rltb_reflect. apply Rleb_reflect.
Qed.

#[export] Instance R_ARing : ARing Rplus R0 Ropp Rmult R1.
Proof.
  repeat constructor; intros; ring.
Qed.

#[export] Instance R_OrderedARing
  : OrderedARing Rplus 0 Ropp Rmult 1 Rlt Rle Rltb Rleb.
Proof.
  constructor. apply R_ARing. apply R_Order.
  - intros. lra.
  - intros. apply Rmult_lt_compat_r; auto.
Qed.

#[export] Instance R_Field : Field Rplus R0 Ropp Rmult R1 Rinv.
Proof.
  constructor. apply R_ARing. intros. field; auto. lra.
Qed.

#[export] Instance R_OrderedField
  : OrderedField Rplus 0 Ropp Rmult 1 Rinv Rlt Rle Rltb Rleb.
Proof.
  constructor. apply R_Field. apply R_OrderedARing.
Qed.

Additional properties

(a * c + b * d)² <= (a² + b²) * (c² + d²)
Lemma Rsqr_mult_le : forall a b c d : R, (a * c + b * d)² <= (a² + b²) * (c² + d²).
Proof.
  intros. unfold Rsqr. ring_simplify.
  rewrite !associative. apply Rplus_le_compat_l.
  rewrite <- !associative. apply Rplus_le_compat_r.
  autorewrite with R.
  replace (a² * d²) with (a * d)²; [|ra].
  replace (c² * b²) with (c * b)²; [|ra].
  replace (2 * a * c * b * d) with (2 * (a * d) * (c * b)); [|ra].
  apply R_neq1.
Qed.

Lemma Rdiv_le_1 : forall x y : R, 0 <= x -> 0 < y -> x <= y -> x / y <= 1.
Proof.
  intros. unfold Rdiv. replace 1 with (y * / y); ra.
  apply Rmult_le_compat_r; ra. apply Rinv_r; ra.
Qed.

Lemma Rdiv_abs_le_1 : forall a b : R, b <> 0 -> |a| <= |b| -> | a / b | <= 1.
Proof.
  intros. unfold Rdiv. rewrite Rabs_mult. rewrite Rabs_inv.
  apply Rdiv_le_1; auto; ra. apply Rabs_pos_lt; auto.
Qed.

#[export] Hint Resolve
  Rdiv_le_1
  : R.

#[export] Instance R_ConvertToR
  : ConvertToR Rplus 0 Ropp Rmult 1 Rinv Rlt Rle Rltb Rleb id.
Proof. constructor; intros; unfold id; auto; try easy. apply R_Order. Qed.

b <> 0 -> a * b = b -> a = 1
Lemma Rmult_eq_r_reg : forall a b : R, b <> 0 -> a * b = b -> a = 1.
Proof.
  intros. replace b with (1 * b)%R in H0 at 2 by lra.
  apply Rmult_eq_reg_r in H0; auto.
Qed.

a <> 0 -> a * b = a -> b = 1
Lemma Rmult_eq_l_reg : forall a b : R, a <> 0 -> a * b = a -> b = 1.
Proof.
  intros. replace a with (a * 1)%R in H0 at 2 by lra.
  apply Rmult_eq_reg_l in H0; auto.
Qed.

Absolute function
Lemma Rabs_pos_iff : forall x, |x| = x <-> x >= 0.
Proof.
  intros. split; intros.
  - bdestruct (x >=? 0). lra. exfalso.
    assert (x <= 0); try lra.
    apply Rabs_left1 in H1. lra.
  - apply Rabs_right. auto.
Qed.

Lemma Rabs_neg_iff : forall x, |x| = - x <-> x <= 0.
Proof.
  intros. split; intros.
  - destruct (Rleb_reflect x 0); auto.
    assert (x >= 0); try lra.
    apply Rabs_right in H0. lra.
  - apply Rabs_left1. auto.
Qed.

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

Lemma mult_PI_gt0 : forall r, 0 < r -> 0 < r * PI.
Proof. ra. Qed.

算术-几何平均值不等式，简称 “算几不等式”

平均数不等式，或称平均值不等式、均值不等式。是算几不等式的推广

Lemma Rineq2 : forall a b : R,
    0 <= a -> 0 <= b ->
    (a + b) / 2 >= sqrt(a * b).
Abort.

Lemma Rineq3 : forall a b c : R,
    0 <= a -> 0 <= b -> 0 <= c ->
    (a + b + c) / 3 >= sqrt(a * b).
Abort.