← suite trig

inverse

asin(sin x) = x and friends: true exactly on the principal range of the inverse.

Case set 7a1dcfa636ed

casesympy bestsympy-asksympy-refinesympy-simplifywolfram best wolfram-fullsimplify wolfram-refine wolfram-simplify
trig-acos-01 trueno verdictno verdictno verdictno verdicttrue ✓true ✓true ✓true ✓
trig-asin-01 contingentno verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓
trig-asin-02 trueno verdictno verdictno verdictno verdicttrue ✓true ✓true ✓true ✓
trig-atan-01 trueno verdictno verdictno verdictno verdicttrue ✓true ✓true ✓true ✓

trig-acos-01

Given
\(x \in \mathbb{R},\quad x > 0,\quad x < 3\)
Claim
\(\displaystyle \arccos\left(\cos x\right) = x\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case trig-acos-01 (category inverse)
  (var x real)
  (assume (positive x)) (assume (< x 3))
  (ask (= (acos (cos x)) x))
  (expect true))

trig-asin-01

Given
\(x \in \mathbb{R}\)
Claim
\(\displaystyle \arcsin\left(\sin x\right) \overset{?}{=} 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\)

(case trig-asin-01 (category inverse)
  (var x real)
  (ask (= (asin (sin x)) x))
  (expect contingent)
  (witness true (x 0))
  (witness false (x 3)))

trig-asin-02

Given
\(x \in \mathbb{R},\quad x > -1,\quad x < 1\)
Claim
\(\displaystyle \arcsin\left(\sin x\right) = x\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case trig-asin-02 (category inverse)
  (var x real)
  (assume (> x -1)) (assume (< x 1))
  (ask (= (asin (sin x)) x))
  (expect true))

trig-atan-01

Given
\(x \in \mathbb{R},\quad x > -1,\quad x < 1\)
Claim
\(\displaystyle \arctan\left(\tan x\right) = x\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case trig-atan-01 (category inverse)
  (var x real)
  (assume (> x -1)) (assume (< x 1))
  (ask (= (atan (tan x)) x))
  (expect true))

Case set 1e4dbd2f7d86

casesympy bestsympy-asksympy-refinesympy-simplifywolfram best wolfram-fullsimplify wolfram-refine wolfram-simplify
trig-acos-01 trueno verdictno verdictno verdictno verdicttrue ✓true ✓true ✓true ✓
trig-asin-01 contingentno verdictno verdictno verdictno verdictno verdictno verdictno verdictno verdict
trig-asin-02 trueno verdictno verdictno verdictno verdicttrue ✓true ✓true ✓true ✓
trig-atan-01 trueno verdictno verdictno verdictno verdicttrue ✓true ✓true ✓true ✓

trig-acos-01

Given
\(x \in \mathbb{R},\quad x > 0,\quad x < 3\)
Claim
\(\displaystyle \arccos\left(\cos x\right) = x\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case trig-acos-01 (category inverse)
  (var x real)
  (assume (positive x)) (assume (< x 3))
  (ask (= (acos (cos x)) x))
  (expect true))

trig-asin-01

Given
\(x \in \mathbb{R}\)
Claim
\(\displaystyle \arcsin\left(\sin x\right) \overset{?}{=} 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\)

(case trig-asin-01 (category inverse)
  (var x real)
  (ask (= (asin (sin x)) x))
  (expect contingent)
  (witness true (x 0))
  (witness false (x 3)))

trig-asin-02

Given
\(x \in \mathbb{R},\quad x > -1,\quad x < 1\)
Claim
\(\displaystyle \arcsin\left(\sin x\right) = x\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case trig-asin-02 (category inverse)
  (var x real)
  (assume (> x -1)) (assume (< x 1))
  (ask (= (asin (sin x)) x))
  (expect true))

trig-atan-01

Given
\(x \in \mathbb{R},\quad x > -1,\quad x < 1\)
Claim
\(\displaystyle \arctan\left(\tan x\right) = x\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case trig-atan-01 (category inverse)
  (var x real)
  (assume (> x -1)) (assume (< x 1))
  (ask (= (atan (tan x)) x))
  (expect true))

Case set 45d6b9056f06

casesympy bestsympy-asksympy-refinesympy-simplifywolfram best wolfram-fullsimplify wolfram-refine wolfram-simplify
trig-acos-01 trueno verdictno verdictno verdictno verdicttrue ✓true ✓true ✓true ✓
trig-asin-01 contingentno verdictno verdictno verdictno verdictno verdictno verdictno verdictno verdict
trig-asin-02 trueno verdictno verdictno verdictno verdicttrue ✓true ✓true ✓true ✓
trig-atan-01 trueno verdictno verdictno verdictno verdicttrue ✓true ✓true ✓true ✓

trig-acos-01

Given
\(x \in \mathbb{R},\quad x > 0,\quad x < 3\)
Claim
\(\displaystyle \arccos\left(\cos x\right) = x\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case trig-acos-01 (category inverse)
  (var x real)
  (assume (positive x)) (assume (< x 3))
  (ask (= (acos (cos x)) x))
  (expect true))

trig-asin-01

Given
\(x \in \mathbb{R}\)
Claim
\(\displaystyle \arcsin\left(\sin x\right) \overset{?}{=} 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\)

(case trig-asin-01 (category inverse)
  (var x real)
  (ask (= (asin (sin x)) x))
  (expect contingent)
  (witness true (x 0))
  (witness false (x 3)))

trig-asin-02

Given
\(x \in \mathbb{R},\quad x > -1,\quad x < 1\)
Claim
\(\displaystyle \arcsin\left(\sin x\right) = x\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case trig-asin-02 (category inverse)
  (var x real)
  (assume (> x -1)) (assume (< x 1))
  (ask (= (asin (sin x)) x))
  (expect true))

trig-atan-01

Given
\(x \in \mathbb{R},\quad x > -1,\quad x < 1\)
Claim
\(\displaystyle \arctan\left(\tan x\right) = x\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case trig-atan-01 (category inverse)
  (var x real)
  (assume (> x -1)) (assume (< x 1))
  (ask (= (atan (tan x)) x))
  (expect true))