FinMatrix.CoqExt.RExt

Test


Section test.
  Goal 1 = R1. ra. Qed.
  Goal R1² = 1. ra. Qed.
  Goal = R1. ra. Qed.
  Goal /R1 = R1. ra. Qed.
  Goal /R1 = 1. ra. Qed.
  Goal /1 = R1. ra. Qed.
  Goal 0 R1. ra. Qed.
End test.

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.

Section test.
  Goal forall x, cos x * cos x + sin x * sin x = R1. ra. Qed.
  Goal forall x, sin x * sin x + cos x * cos x = R1. ra. Qed.
End test.

Section test.
  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.

Section test.
  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.

Section test.
  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.