Refine

Simplify $expr$ using $cond$ (or, with no $cond$ , whatever is already assumed) as a fact — the same fact-driven simplification Assuming scopes for a whole subcomputation, but applied once. Provided by @enumeratio/analytic.

✓ checked against that system · ! checked, with disagreements (hover a chip)Wolfram LanguageRefine!

Refine(expr, cond)simplify

expr

under

cond

(a single condition, a List, or an And), then forget it.

Refine(expr)simplify

expr

under whatever is already assumed (e.g. inside an enclosing Assuming).

Typed signatures

Type	Package	Applies
`(expression, expression?) -> expression`	`analytic`	always

Domain: Analytic

Details

Delegates entirely to compute-engine's own simplify() under a scoped assumption (see Assuming for the scoping mechanism) — this covers exactly the sign/domain reasoning simplify() already does: $\sqrt{x^2} \to x$ under $x>0$ (and $\to -x$ under $x<0$ ), $|x| \to x$ , $\ln(e^x) \to x$ , $\operatorname{sign}(x) \to 1$ .
A condition that simplify() has no rule for is left alone, same as Wolfram's Refine declines a fact it can't use — this is not a general decision procedure for arbitrary predicates.

Examples

Basic #

$\sqrt{x^2} \to x$ under $x > 0$

In

\mathrm{Refine}(\sqrt{x^2}, x\gt0)

Out

x

$\sqrt{x^2} \to -x$ under $x < 0$

In

\mathrm{Refine}(\sqrt{x^2}, x\lt0)

Out

-x

$|x| \to x$ under $x > 0$

In

\mathrm{Refine}(\vert x\vert, x\gt0)

Out

x

$\operatorname{sign}(x) \to 1$ under $x > 0$

In

\mathrm{Refine}(\mathrm{sgn}(x), x\gt0)

Out

1

$\ln(e^x) \to x$ once $x$ is known real

In

\mathrm{Refine}(\ln(e^{x}), x∈ℝ)

Out

x

For real $x$ , $\sqrt{x^2}=|x|$

In

\mathrm{Refine}(\sqrt{x^2}, x∈ℝ)

Out

\vert x\vert

In

\mathrm{Assuming}(x≥0∧y\lt0, \text{if }\mathrm{IsTrue}(\mathrm{Refine}(x-y\gt0))\text{ then }\mathrm{Refine}(\sqrt{x^2y^2})\text{ else }0)

Out

-(xy)

Scope #

With $x\ge0$ the cube root of the cube is $x$

In

\mathrm{Refine}(\sqrt[3]{x^3}, x≥0)

Out

x

This assumption does not make $(a^b)^c$ collapse, so it stays

In

\mathrm{Refine}((a^{b})^{c}, -1\lt b\lt1)

Out

(a^{b})^{c}

Assumptions on positivity do not merge the powers here

In

\mathrm{Refine}(a^{p}b^{p}, a\gt0∧b\gt0)

Out

a^{p}b^{p}

A negative argument gives no simplification of the log

In

\mathrm{Refine}(\ln(x), x\lt0)

Out

\ln(x)

For $|p|<1$ , $\ln x^p$ becomes $p\ln x$

In

\mathrm{Refine}(\ln(x^{p}), -1\lt p\lt1)

Out

p\ln(x)

Assumptions on sums are not used to rewrite this equation

In

\mathrm{Refine}(a^2-b^2+1=0, a+b=0)

Out

a^2-b^2+1=0

An unrelated inequality is not used

In

\mathrm{Refine}((x-1)^2+(y-2)^2\lt\frac{3}{2}, x^2+y^2≤1)

Out

(x-1)^2+(y-2)^2\lt\frac{3}{2}

A ceiling is left alone given a range for $x$

In

\mathrm{Refine}(\lceil x\rceil, \mathrm{Inequality}(2, \mathrm{Less}, x, \mathrm{LessEqual}, 3))

Out

\lceil x\rceil

Conditions on residues do not change the fractional part

In

\mathrm{Refine}(\mathrm{FractionalPart}(a), a\lt0∧a\bmod1=\frac{1}{3})

Out

\mathrm{FractionalPart}(a)

The assumption $x>0$ makes $\sqrt{x^2}=x$

In

\mathrm{Assuming}(x\gt0, \mathrm{Refine}(\sqrt{x^2}))

Out

x

Integers make the sine of $k\pi$ vanish

In

\mathrm{Refine}(\sin(kπ), k∈ℤ)

Out

0

The cosine shift is not simplified for integer $k$ , only reordered

In

\mathrm{Refine}(\cos(x+kπ), k∈ℤ)

Out

\cos(πk+x)

Positivity assumptions leave this real-valued test unchanged

In

\mathrm{Refine}(\frac{2x+x^{p}}{xΓ(x+2)}∈ℝ, x\gt0∧p\gt0)

Out

\frac{2x+x^{p}}{xΓ(x+2)}∈ℝ

A product of integers is not reduced further

In

\mathrm{Refine}(2k^3\lfloor x\rfloor^{k}∈ℤ, k∈ℤ∧k\gt0∧x∈ℝ)

Out

2k^3\lfloor x\rfloor^{k}∈ℤ

Floor of integer-affine expression stays

In

\mathrm{Refine}(\lfloor2a+1\rfloor, a∈ℤ)

Out

\lfloor2a+1\rfloor

Divisibility assumptions do not simplify the mod

In

\mathrm{Refine}(a\bmod4, \frac{a+3}{4}∈ℤ)

Out

a\bmod4

With no assumption, $\sqrt{x^2}=|x|$

In

\mathrm{Refine}(\sqrt{x^2})

Out

\vert x\vert

Together with $y<0$ , $\sqrt{x^2y^2}=-xy$

In

\mathrm{Assuming}(x\gt0, \mathrm{Refine}(\sqrt{x^2y^2}, y\lt0))

Out

-(xy)

The range of $\mathrm{Re}\,x$ does not rewrite $\arctan\tan x$

In

\mathrm{Refine}(\arctan(\tan(x)), -\frac{π}{2}\lt\mathrm{Re}(x)\lt\frac{π}{2})

Out

\arctan(\tan(x))

In

\mathrm{Refine}(\arctan(\tan(x)), -\frac{π}{2}\lt\Re(x)\lt\frac{π}{2})

Out

\arctan(\tan(x))

Properties #

With $x>0$ real $y$ , $\ln x^y = y\ln x$

In

\mathrm{Refine}(\ln(x^{y}), x\gt0∧y∈ℝ)

Out

y\ln(x)

A sum $x+y\ge0$ lets the perfect square root become $|x+y|$

In

\mathrm{Refine}(\sqrt{x^2+2xy+y^2}, x+y≥0)

Out

\vert x+y\vert

Possible issues #

$x^2 > 0$ is left alone with no assumption — it fails exactly at $x=0$

In

\mathrm{Refine}(x^2\gt0)

Out

0\lt x^2

The assumption does not decide membership, so this stays

In

\mathrm{Refine}(x∈ℝ, x^2\lt1)

Out

x∈ℝ

In

\mathrm{Refine}(-1\lt x\lt1, x^2\lt1)

Out

-1\lt x

About

Examples	32
Checked against	Wolfram Language 17 agree15 differ
Crosswalk	Wolfram Language