FinMatrix.CoqExt.RExt.RExtSqr

Require Export RExtBase.
Require Export RExtBool RExtPlus RExtMult.

Basic automation

#[export] Hint Rewrite
  Rsqr_0
  Rsqr_1
  Rsqr_mult
  : R.

#[export] Hint Resolve
  Rle_0_sqr
  Rsqr_pos_lt
  Rplus_sqr_eq_0
  : R.

Convert between x², x^n, and x*x

r * r = r²

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. unfold Rsqr. ring. Qed.
#[export] Hint Rewrite Rpow2_Rsqr : R.

r ^ 4 = (r²)²

Lemma Rpow4_Rsqr_Rsqr r : r ^ 4 = r ²².
Proof. unfold Rsqr. ring. 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; try lra.
apply Rsqr_eq in H1; try lra.
Qed.

0 <= r * r

Lemma Rsqr_ge0 : forall r, 0 <= r * r.
Proof. ra. Qed.
#[export] Hint Resolve Rsqr_ge0 : R.

r <> 0 -> r² <> 0

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

Additional properties

R0² = 0

Lemma Rsqr_R0 : R0 ² = 0.
Proof. rewrite <- Rsqr_0. auto. Qed.
#[export] Hint Rewrite Rsqr_R0 : R.

(R1)² = 1

Lemma Rsqr_R1 : (R1 )² = 1.
Proof. ra. Qed.
#[export] Hint Rewrite Rsqr_R1 : R.

r1² + r2²

r1² + r2² = 0 -> r1 = 0 /\ r2 = 0

Lemma Rplus2_sqr_eq0_imply : forall r1 r2, r1 ² + r2 ² = 0 -> r1 = 0 /\ r2 = 0.
Proof. ra. Qed.
#[export] Hint Resolve Rplus2_sqr_eq0_imply : R.

r1 = 0 /\ r2 = 0 -> r1² + r2² = 0

Lemma Rplus2_sqr_eq0_if : forall r1 r2, r1 = 0 /\ r2 = 0 -> r1 ² + r2 ² = 0.
Proof. ra. Qed.
#[export] Hint Resolve Rplus2_sqr_eq0_if : R.

r1 = 0 /\ r2 = 0 <-> r1² + r2² = 0

Lemma Rplus2_sqr_eq0 : forall r1 r2, r1 = 0 /\ r2 = 0 <-> r1 ² + 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.
#[export] Hint Resolve Rplus2_sqr_eq0_l : R.

r1² + r2² = 0 -> r2 = 0

Lemma Rplus2_sqr_eq0_r : forall r1 r2, r1 ² + r2 ² = 0 -> r2 = 0.
Proof. ra. Qed.
#[export] Hint Resolve Rplus2_sqr_eq0_r : R.

r1² + r2² <> 0 -> r1 <> 0 \/ r2 <> 0

Lemma Rplus2_sqr_neq0_imply : forall r1 r2, r1 ² + r2 ² <> 0 -> r1 <> 0 \/ r2 <> 0.
Proof. intros. rewrite <- Rplus2_sqr_eq0 in H. tauto. Qed.
#[export] Hint Resolve Rplus2_sqr_neq0_imply : R.

r1 <> 0 \/ r2 <> 0 -> r1² + r2² <> 0

Lemma Rplus2_sqr_neq0_if : forall r1 r2, r1 <> 0 \/ r2 <> 0 -> r1 ² + r2 ² <> 0.
Proof. intros. rewrite <- Rplus2_sqr_eq0. tauto. Qed.
#[export] Hint Resolve Rplus2_sqr_neq0_if : R.

r1 <> 0 \/ r2 <> 0 <-> r1² + r2² <> 0

Lemma Rplus2_sqr_neq0 : forall r1 r2, r1 ² + r2 ² <> 0 <-> r1 <> 0 \/ r2 <> 0.
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.