sympy-refine

suite trig · 2026-10-12 20:21:45 · CAS sympy 1.15.0.dev, mode fork · machine pi5 · dialect sympy · case set 45d6b9056f06

By category

old report format (graded with a combined score): its nulls are shown as no verdict, because an old report cannot tell a correct decline on a contingent case from no verdict

category	n	solved	no verdict
identities	5	0	5
inverse	4	0	4
periodicity	4	1	3
total	13	1	12

Setup (run once per start, not counted in the per-query times)

measured setup time: 0.415 s

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = refine(Abs(W), Q.positive(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

sympy	`sympy.__version__`	→	`1.15.0.dev`
warm-up	`refine(Abs(W), Q.positive(W))`	→	`W`

Cases

case category outcome query (as sent) answer steps (from the trace) s detail

trig-double-01 true identities no verdict Q.complex(z) ⊢ Eq(sin((2*z)), (2*(sin(z)*cos(z)))) null difference → -2*sin(z)*cos(z) + sin(2*z) · refine → -2*sin(z)*cos(z) + sin(2*z) 0.055 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = refine(Abs(W), Q.positive(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

z = Symbol('z', complex=True)
Assum = And(Q.complex(z))
Residual = sin(2 * z) - (2 * (sin(z) * cos(z)))
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`sin(2 * z) - (2 * (sin(z) * cos(z)))`	→	`-2sin(z)cos(z) + sin(2*z)`
refine	`refine(Residual, Assum)`	→	`-2sin(z)cos(z) + sin(2*z)`
answer			`null`

trig-double-02 false identities no verdict Q.real(x) ∧ Q.positive(x) ∧ (x < 1) ⊢ Eq(sin((2*x)), (2*sin(x))) null difference → -2*sin(x) + sin(2*x) · refine → -2*sin(x) + sin(2*x) 0.044 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = refine(Abs(W), Q.positive(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

x = Symbol('x', real=True)
Assum = And(Q.real(x), Q.positive(x), x < 1)
Residual = sin(2 * x) - (2 * sin(x))
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`sin(2 * x) - (2 * sin(x))`	→	`-2sin(x) + sin(2x)`
refine	`refine(Residual, Assum)`	→	`-2sin(x) + sin(2x)`
answer			`null`

trig-pyth-01 true identities no verdict Q.complex(z) ⊢ Eq(((sin(z)*sin(z)) + (cos(z)*cos(z))), 1) null difference → sin(z)**2 + cos(z)**2 - 1 · refine → sin(z)**2 + cos(z)**2 - 1 0.05 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = refine(Abs(W), Q.positive(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

z = Symbol('z', complex=True)
Assum = And(Q.complex(z))
Residual = sin(z) * sin(z) + cos(z) * cos(z) - 1
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`sin(z) * sin(z) + cos(z) * cos(z) - 1`	→	`sin(z)2 + cos(z)2 - 1`
refine	`refine(Residual, Assum)`	→	`sin(z)2 + cos(z)2 - 1`
answer			`null`

trig-sqrt-01 contingent identities no verdict Q.real(x) ⊢ Eq(sqrt((1 - (sin(x)*sin(x)))), cos(x)) null difference → sqrt(1 - sin(x)**2) - cos(x) · refine → sqrt(1 - sin(x)**2) - cos(x) 0.048 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = refine(Abs(W), Q.positive(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

x = Symbol('x', real=True)
Assum = And(Q.real(x))
Residual = sqrt(1 - sin(x) * sin(x)) - cos(x)
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`sqrt(1 - sin(x) * sin(x)) - cos(x)`	→	`sqrt(1 - sin(x)**2) - cos(x)`
refine	`refine(Residual, Assum)`	→	`sqrt(1 - sin(x)**2) - cos(x)`
answer			`null`

trig-tan-01 true identities no verdict Q.real(x) ∧ (~Q.zero(cos(x))) ⊢ Eq(tan(x), (sin(x)/cos(x))) null difference → -sin(x)/cos(x) + tan(x) · refine → -sin(x)/cos(x) + tan(x) 0.048 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = refine(Abs(W), Q.positive(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

x = Symbol('x', real=True)
Assum = And(Q.real(x), ~Q.zero(cos(x)))
Residual = tan(x) - (sin(x) / cos(x))
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`tan(x) - (sin(x) / cos(x))`	→	`-sin(x)/cos(x) + tan(x)`
refine	`refine(Residual, Assum)`	→	`-sin(x)/cos(x) + tan(x)`
answer			`null`

trig-acos-01 true inverse no verdict Q.real(x) ∧ Q.positive(x) ∧ (x < 3) ⊢ Eq(acos(cos(x)), x) null difference → -x + acos(cos(x)) · refine → -x + acos(cos(x)) 0.041 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = refine(Abs(W), Q.positive(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

x = Symbol('x', real=True)
Assum = And(Q.real(x), Q.positive(x), x < 3)
Residual = acos(cos(x)) - x
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`acos(cos(x)) - x`	→	`-x + acos(cos(x))`
refine	`refine(Residual, Assum)`	→	`-x + acos(cos(x))`
answer			`null`

trig-asin-01 contingent inverse no verdict Q.real(x) ⊢ Eq(asin(sin(x)), x) null difference → -x + asin(sin(x)) · refine → -x + asin(sin(x)) 0.042 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = refine(Abs(W), Q.positive(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

x = Symbol('x', real=True)
Assum = And(Q.real(x))
Residual = asin(sin(x)) - x
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`asin(sin(x)) - x`	→	`-x + asin(sin(x))`
refine	`refine(Residual, Assum)`	→	`-x + asin(sin(x))`
answer			`null`

trig-asin-02 true inverse no verdict Q.real(x) ∧ (x > (-1)) ∧ (x < 1) ⊢ Eq(asin(sin(x)), x) null difference → -x + asin(sin(x)) · refine → -x + asin(sin(x)) 0.046 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = refine(Abs(W), Q.positive(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

x = Symbol('x', real=True)
Assum = And(Q.real(x), x > -1, x < 1)
Residual = asin(sin(x)) - x
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`asin(sin(x)) - x`	→	`-x + asin(sin(x))`
refine	`refine(Residual, Assum)`	→	`-x + asin(sin(x))`
answer			`null`

trig-atan-01 true inverse no verdict Q.real(x) ∧ (x > (-1)) ∧ (x < 1) ⊢ Eq(atan(tan(x)), x) null difference → -x + atan(tan(x)) · refine → -x + atan(tan(x)) 0.041 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = refine(Abs(W), Q.positive(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

x = Symbol('x', real=True)
Assum = And(Q.real(x), x > -1, x < 1)
Residual = atan(tan(x)) - x
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`atan(tan(x)) - x`	→	`-x + atan(tan(x))`
refine	`refine(Residual, Assum)`	→	`-x + atan(tan(x))`
answer			`null`

trig-period-01 true periodicity solved Q.complex(z) ⊢ Eq(sin((z + (2*pi))), sin(z)) true difference → 0 · refine → 0 0.038 true

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = refine(Abs(W), Q.positive(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

z = Symbol('z', complex=True)
Assum = And(Q.complex(z))
Residual = sin(z + 2 * pi) - sin(z)
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`sin(z + 2 * pi) - sin(z)`	→	`0`
refine	`refine(Residual, Assum)`	→	`0`
answer			`true`

trig-period-02 contingent periodicity no verdict Q.real(x) ⊢ Eq(cos((x + pi)), cos(x)) null difference → -2*cos(x) · refine → -2*cos(x) 0.043 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = refine(Abs(W), Q.positive(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

x = Symbol('x', real=True)
Assum = And(Q.real(x))
Residual = cos(x + pi) - cos(x)
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`cos(x + pi) - cos(x)`	→	`-2*cos(x)`
refine	`refine(Residual, Assum)`	→	`-2*cos(x)`
answer			`null`

trig-period-03 contingent periodicity no verdict Q.real(x) ∧ Q.positive(x) ⊢ Eq(cos((x + pi)), cos(x)) null difference → -2*cos(x) · refine → -2*cos(x) 0.041 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = refine(Abs(W), Q.positive(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

x = Symbol('x', real=True)
Assum = And(Q.real(x), Q.positive(x))
Residual = cos(x + pi) - cos(x)
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`cos(x + pi) - cos(x)`	→	`-2*cos(x)`
refine	`refine(Residual, Assum)`	→	`-2*cos(x)`
answer			`null`

trig-shift-01 contingent periodicity no verdict Q.real(x) ⊢ Eq(sin((x + pi)), sin(x)) null difference → -2*sin(x) · refine → -2*sin(x) 0.042 null

code

setup — not timed

from sympy import *
import sympy

SympyVersion = sympy.__version__
# warm-up: a fixed generic expression, never case content
W = Symbol('W')
Warmup = refine(Abs(W), Q.positive(W))
# every query then runs in its own forked process, starting from this state:
# the expression caches are dropped (imported and lazily loaded modules stay)
sympy.core.cache.clear_cache()

x = Symbol('x', real=True)
Assum = And(Q.real(x))
Residual = sin(x + pi) - sin(x)
Result = refine(Residual, Assum)
# true iff the result is 0; false only if it is a definite nonzero number
Answer = True if Result == 0 else False if (Result.is_number and Result.is_finite and Result.is_zero is False) else None
print(Result, Answer, sep='\n')

difference	`sin(x + pi) - sin(x)`	→	`-2*sin(x)`
refine	`refine(Residual, Assum)`	→	`-2*sin(x)`
answer			`null`