← suite trig

periodicity

Shifts by multiples of pi: periods, half-periods, and where a shifted value coincides.

Case set 7a1dcfa636ed

casesympy bestsympy-asksympy-refinesympy-simplifywolfram best wolfram-fullsimplify wolfram-refine wolfram-simplify
trig-period-01 truetrue ✓true ✓true ✓true ✓true ✓true ✓true ✓true ✓
trig-period-02 contingentno verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓
trig-period-03 contingentno verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓
trig-shift-01 contingentno verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓

trig-period-01

Given
\(z \in \mathbb{C}\)
Claim
\(\displaystyle \sin\left(z + 2 \, \pi\right) = \sin z\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case trig-period-01 (category periodicity)
  (var z complex)
  (ask (= (sin (+ z (* 2 pi))) (sin z)))
  (expect true))

trig-period-02

Given
\(x \in \mathbb{R}\)
Claim
\(\displaystyle \cos\left(x + \pi\right) \overset{?}{=} \cos x\)
Expected
contingent true at \(x = \frac{1}{2} \, \pi\); false at \(x = 0\)

equal at some admissible points, different at others

witness (true): \(x = \frac{1}{2} \, \pi\)

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

cos(x + pi) = -cos x, so the claim holds exactly where cos x = 0.

(case trig-period-02 (category periodicity)
  (note "cos(x + pi) = -cos x, so the claim holds exactly where cos x = 0.")
  (var x real)
  (ask (= (cos (+ x pi)) (cos x)))
  (expect contingent)
  (witness true (x (* 1/2 pi)))
  (witness false (x 0)))

trig-period-03

Given
\(x \in \mathbb{R},\quad x > 0\)
Claim
\(\displaystyle \cos\left(x + \pi\right) \overset{?}{=} \cos x\)
Expected
contingent true at \(x = \frac{1}{2} \, \pi\); false at \(x = 1\)

equal at some admissible points, different at others

witness (true): \(x = \frac{1}{2} \, \pi\)

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

(case trig-period-03 (category periodicity)
  (var x real)
  (assume (positive x))
  (ask (= (cos (+ x pi)) (cos x)))
  (expect contingent)
  (witness true (x (* 1/2 pi)))
  (witness false (x 1)))

trig-shift-01

Given
\(x \in \mathbb{R}\)
Claim
\(\displaystyle \sin\left(x + \pi\right) \overset{?}{=} \sin x\)
Expected
contingent true at \(x = 0\); false at \(x = 1\)

equal at some admissible points, different at others

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

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

(case trig-shift-01 (category periodicity)
  (var x real)
  (ask (= (sin (+ x pi)) (sin x)))
  (expect contingent)
  (witness true (x 0))
  (witness false (x 1)))

Case set 1e4dbd2f7d86

casesympy bestsympy-asksympy-refinesympy-simplifywolfram best wolfram-fullsimplify wolfram-refine wolfram-simplify
trig-period-01 truetrue ✓true ✓true ✓true ✓true ✓true ✓true ✓true ✓
trig-period-02 contingentno verdictno verdictno verdictno verdictno verdictno verdictno verdictno verdict
trig-period-03 contingentno verdictno verdictno verdictno verdictno verdictno verdictno verdictno verdict
trig-shift-01 contingentno verdictno verdictno verdictno verdictno verdictno verdictno verdictno verdict

trig-period-01

Given
\(z \in \mathbb{C}\)
Claim
\(\displaystyle \sin\left(z + 2 \, \pi\right) = \sin z\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case trig-period-01 (category periodicity)
  (var z complex)
  (ask (= (sin (+ z (* 2 pi))) (sin z)))
  (expect true))

trig-period-02

Given
\(x \in \mathbb{R}\)
Claim
\(\displaystyle \cos\left(x + \pi\right) \overset{?}{=} \cos x\)
Expected
contingent true at \(x = \frac{1}{2} \, \pi\); false at \(x = 0\)

equal at some admissible points, different at others

witness (true): \(x = \frac{1}{2} \, \pi\)

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

cos(x + pi) = -cos x, so the claim holds exactly where cos x = 0.

(case trig-period-02 (category periodicity)
  (note "cos(x + pi) = -cos x, so the claim holds exactly where cos x = 0.")
  (var x real)
  (ask (= (cos (+ x pi)) (cos x)))
  (expect contingent)
  (witness true (x (* 1/2 pi)))
  (witness false (x 0)))

trig-period-03

Given
\(x \in \mathbb{R},\quad x > 0\)
Claim
\(\displaystyle \cos\left(x + \pi\right) \overset{?}{=} \cos x\)
Expected
contingent true at \(x = \frac{1}{2} \, \pi\); false at \(x = 1\)

equal at some admissible points, different at others

witness (true): \(x = \frac{1}{2} \, \pi\)

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

(case trig-period-03 (category periodicity)
  (var x real)
  (assume (positive x))
  (ask (= (cos (+ x pi)) (cos x)))
  (expect contingent)
  (witness true (x (* 1/2 pi)))
  (witness false (x 1)))

trig-shift-01

Given
\(x \in \mathbb{R}\)
Claim
\(\displaystyle \sin\left(x + \pi\right) \overset{?}{=} \sin x\)
Expected
contingent true at \(x = 0\); false at \(x = 1\)

equal at some admissible points, different at others

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

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

(case trig-shift-01 (category periodicity)
  (var x real)
  (ask (= (sin (+ x pi)) (sin x)))
  (expect contingent)
  (witness true (x 0))
  (witness false (x 1)))

Case set 45d6b9056f06

casesympy bestsympy-asksympy-refinesympy-simplifywolfram best wolfram-fullsimplify wolfram-refine wolfram-simplify
trig-period-01 truetrue ✓true ✓true ✓true ✓true ✓true ✓true ✓true ✓
trig-period-02 contingentno verdictno verdictno verdictno verdictno verdictno verdictno verdictno verdict
trig-period-03 contingentno verdictno verdictno verdictno verdictno verdictno verdictno verdictno verdict
trig-shift-01 contingentno verdictno verdictno verdictno verdictno verdictno verdictno verdictno verdict

trig-period-01

Given
\(z \in \mathbb{C}\)
Claim
\(\displaystyle \sin\left(z + 2 \, \pi\right) = \sin z\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case trig-period-01 (category periodicity)
  (var z complex)
  (ask (= (sin (+ z (* 2 pi))) (sin z)))
  (expect true))

trig-period-02

Given
\(x \in \mathbb{R}\)
Claim
\(\displaystyle \cos\left(x + \pi\right) \overset{?}{=} \cos x\)
Expected
contingent true at \(x = \frac{1}{2} \, \pi\); false at \(x = 0\)

equal at some admissible points, different at others

witness (true): \(x = \frac{1}{2} \, \pi\)

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

cos(x + pi) = -cos x, so the claim holds exactly where cos x = 0.

(case trig-period-02 (category periodicity)
  (note "cos(x + pi) = -cos x, so the claim holds exactly where cos x = 0.")
  (var x real)
  (ask (= (cos (+ x pi)) (cos x)))
  (expect contingent)
  (witness true (x (* 1/2 pi)))
  (witness false (x 0)))

trig-period-03

Given
\(x \in \mathbb{R},\quad x > 0\)
Claim
\(\displaystyle \cos\left(x + \pi\right) \overset{?}{=} \cos x\)
Expected
contingent true at \(x = \frac{1}{2} \, \pi\); false at \(x = 1\)

equal at some admissible points, different at others

witness (true): \(x = \frac{1}{2} \, \pi\)

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

(case trig-period-03 (category periodicity)
  (var x real)
  (assume (positive x))
  (ask (= (cos (+ x pi)) (cos x)))
  (expect contingent)
  (witness true (x (* 1/2 pi)))
  (witness false (x 1)))

trig-shift-01

Given
\(x \in \mathbb{R}\)
Claim
\(\displaystyle \sin\left(x + \pi\right) \overset{?}{=} \sin x\)
Expected
contingent true at \(x = 0\); false at \(x = 1\)

equal at some admissible points, different at others

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

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

(case trig-shift-01 (category periodicity)
  (var x real)
  (ask (= (sin (+ x pi)) (sin x)))
  (expect contingent)
  (witness true (x 0))
  (witness false (x 1)))