identities

Algebraic trigonometric identities over the reals or complexes, and where they fail (sqrt of a square).

Case set `7a1dcfa636ed`

case	sympy best	sympy-ask	sympy-refine	sympy-simplify	wolfram best	wolfram-fullsimplify	wolfram-refine	wolfram-simplify
trig-double-01 true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	no verdict	true ✓
trig-double-02 false	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
trig-pyth-01 true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	no verdict	true ✓
trig-sqrt-01 contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
trig-tan-01 true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓

trig-double-01

Given

\(z \in \mathbb{C}\)

Claim

\(\displaystyle \sin\left(2 \, z\right) = 2 \, \sin z \, \cos z\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

(case trig-double-01 (category identities)
  (var z complex)
  (ask (= (sin (* 2 z)) (* 2 (* (sin z) (cos z)))))
  (expect true))

trig-double-02

Given

\(x \in \mathbb{R},\quad x > 0,\quad x < 1\)

Claim

\(\displaystyle \sin\left(2 \, x\right) \neq 2 \, \sin x\)

Expected

false unequal at every admissible point (e.g. at \(x = \frac{1}{2}\))

the two sides differ at every admissible point

witness (false): \(x = \frac{1}{2}\)

sin 2x = 2 sin x iff sin x (cos x - 1) = 0: never on (0, 1).

(case trig-double-02 (category identities)
  (note "sin 2x = 2 sin x iff sin x (cos x - 1) = 0: never on (0, 1).")
  (var x real)
  (assume (positive x)) (assume (< x 1))
  (ask (= (sin (* 2 x)) (* 2 (sin x))))
  (expect false)
  (witness false (x 1/2)))

trig-pyth-01

Given

\(z \in \mathbb{C}\)

Claim

\(\displaystyle \sin z \, \sin z + \cos z \, \cos z = 1\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

(case trig-pyth-01 (category identities)
  (var z complex)
  (ask (= (+ (* (sin z) (sin z)) (* (cos z) (cos z))) 1))
  (expect true))

trig-sqrt-01

Given

\(x \in \mathbb{R}\)

Claim

\(\displaystyle \sqrt{1 - \sin x \, \sin x} \overset{?}{=} \cos x\)

Expected

contingent true at \(x = 0\); false at \(x = 3\)

equal at some admissible points, different at others

witness (true): \(x = 0\)

witness (false): \(x = 3\)

sqrt(cos^2) is |cos x|, which is cos x only where cos x >= 0.

(case trig-sqrt-01 (category identities)
  (note "sqrt(cos^2) is |cos x|, which is cos x only where cos x >= 0.")
  (var x real)
  (ask (= (sqrt (- 1 (* (sin x) (sin x)))) (cos x)))
  (expect contingent)
  (witness true (x 0))
  (witness false (x 3)))

trig-tan-01

Given

\(x \in \mathbb{R},\quad \cos x \neq 0\)

Claim

\(\displaystyle \tan x = \frac{\sin x}{\cos x}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

(case trig-tan-01 (category identities)
  (var x real)
  (assume (nonzero (cos x)))
  (ask (= (tan x) (/ (sin x) (cos x))))
  (expect true))

Case set `1e4dbd2f7d86`

case	sympy best	sympy-ask	sympy-refine	sympy-simplify	wolfram best	wolfram-fullsimplify	wolfram-refine	wolfram-simplify
trig-double-01 true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	no verdict	true ✓
trig-double-02 false	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
trig-pyth-01 true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	no verdict	true ✓
trig-sqrt-01 contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
trig-tan-01 true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓

trig-double-01

Given

\(z \in \mathbb{C}\)

Claim

\(\displaystyle \sin\left(2 \, z\right) = 2 \, \sin z \, \cos z\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

(case trig-double-01 (category identities)
  (var z complex)
  (ask (= (sin (* 2 z)) (* 2 (* (sin z) (cos z)))))
  (expect true))

trig-double-02

Given

\(x \in \mathbb{R},\quad x > 0,\quad x < 1\)

Claim

\(\displaystyle \sin\left(2 \, x\right) \neq 2 \, \sin x\)

Expected

false unequal at every admissible point (e.g. at \(x = \frac{1}{2}\))

the two sides differ at every admissible point

witness (false): \(x = \frac{1}{2}\)

sin 2x = 2 sin x iff sin x (cos x - 1) = 0: never on (0, 1).

(case trig-double-02 (category identities)
  (note "sin 2x = 2 sin x iff sin x (cos x - 1) = 0: never on (0, 1).")
  (var x real)
  (assume (positive x)) (assume (< x 1))
  (ask (= (sin (* 2 x)) (* 2 (sin x))))
  (expect false)
  (witness false (x 1/2)))

trig-pyth-01

Given

\(z \in \mathbb{C}\)

Claim

\(\displaystyle \sin z \, \sin z + \cos z \, \cos z = 1\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

(case trig-pyth-01 (category identities)
  (var z complex)
  (ask (= (+ (* (sin z) (sin z)) (* (cos z) (cos z))) 1))
  (expect true))

trig-sqrt-01

Given

\(x \in \mathbb{R}\)

Claim

\(\displaystyle \sqrt{1 - \sin x \, \sin x} \overset{?}{=} \cos x\)

Expected

contingent true at \(x = 0\); false at \(x = 3\)

equal at some admissible points, different at others

witness (true): \(x = 0\)

witness (false): \(x = 3\)

sqrt(cos^2) is |cos x|, which is cos x only where cos x >= 0.

(case trig-sqrt-01 (category identities)
  (note "sqrt(cos^2) is |cos x|, which is cos x only where cos x >= 0.")
  (var x real)
  (ask (= (sqrt (- 1 (* (sin x) (sin x)))) (cos x)))
  (expect contingent)
  (witness true (x 0))
  (witness false (x 3)))

trig-tan-01

Given

\(x \in \mathbb{R},\quad \cos x \neq 0\)

Claim

\(\displaystyle \tan x = \frac{\sin x}{\cos x}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

(case trig-tan-01 (category identities)
  (var x real)
  (assume (nonzero (cos x)))
  (ask (= (tan x) (/ (sin x) (cos x))))
  (expect true))

Case set `45d6b9056f06`

case	sympy best	sympy-ask	sympy-refine	sympy-simplify	wolfram best	wolfram-fullsimplify	wolfram-refine	wolfram-simplify
trig-double-01 true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	no verdict	true ✓
trig-double-02 false	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
trig-pyth-01 true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	no verdict	true ✓
trig-sqrt-01 contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
trig-tan-01 true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓

trig-double-01

Given

\(z \in \mathbb{C}\)

Claim

\(\displaystyle \sin\left(2 \, z\right) = 2 \, \sin z \, \cos z\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

(case trig-double-01 (category identities)
  (var z complex)
  (ask (= (sin (* 2 z)) (* 2 (* (sin z) (cos z)))))
  (expect true))

trig-double-02

Given

\(x \in \mathbb{R},\quad x > 0,\quad x < 1\)

Claim

\(\displaystyle \sin\left(2 \, x\right) \neq 2 \, \sin x\)

Expected

false unequal at every admissible point (e.g. at \(x = \frac{1}{2}\))

the two sides differ at every admissible point

witness (false): \(x = \frac{1}{2}\)

sin 2x = 2 sin x iff sin x (cos x - 1) = 0: never on (0, 1).

(case trig-double-02 (category identities)
  (note "sin 2x = 2 sin x iff sin x (cos x - 1) = 0: never on (0, 1).")
  (var x real)
  (assume (positive x)) (assume (< x 1))
  (ask (= (sin (* 2 x)) (* 2 (sin x))))
  (expect false)
  (witness false (x 1/2)))

trig-pyth-01

Given

\(z \in \mathbb{C}\)

Claim

\(\displaystyle \sin z \, \sin z + \cos z \, \cos z = 1\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

(case trig-pyth-01 (category identities)
  (var z complex)
  (ask (= (+ (* (sin z) (sin z)) (* (cos z) (cos z))) 1))
  (expect true))

trig-sqrt-01

Given

\(x \in \mathbb{R}\)

Claim

\(\displaystyle \sqrt{1 - \sin x \, \sin x} \overset{?}{=} \cos x\)

Expected

contingent true at \(x = 0\); false at \(x = 3\)

equal at some admissible points, different at others

witness (true): \(x = 0\)

witness (false): \(x = 3\)

sqrt(cos^2) is |cos x|, which is cos x only where cos x >= 0.

(case trig-sqrt-01 (category identities)
  (note "sqrt(cos^2) is |cos x|, which is cos x only where cos x >= 0.")
  (var x real)
  (ask (= (sqrt (- 1 (* (sin x) (sin x)))) (cos x)))
  (expect contingent)
  (witness true (x 0))
  (witness false (x 3)))

trig-tan-01

Given

\(x \in \mathbb{R},\quad \cos x \neq 0\)

Claim

\(\displaystyle \tan x = \frac{\sin x}{\cos x}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

(case trig-tan-01 (category identities)
  (var x real)
  (assume (nonzero (cos x)))
  (ask (= (tan x) (/ (sin x) (cos x))))
  (expect true))

identities

Case set 7a1dcfa636ed

Case set 1e4dbd2f7d86

Case set 45d6b9056f06

Case set `7a1dcfa636ed`

Case set `1e4dbd2f7d86`

Case set `45d6b9056f06`