Trigonometry

The Hilbert compiler knows no trigonometric identities of its own: sin(x)² + cos(x)² is computed term by term unless a law says it is one. This module states five identities as laws, each oriented in the direction that makes a formula smaller. A document that opens it has those patterns reduced before code is generated; as with every law, it is in force across the whole document once any file in it opens the module.

Every law here holds for every real number, with no side conditions. That is a deliberate choice: a rewrite rule cannot check a condition such as \(x > 0\), so an identity that is only conditionally true (for example \(e^{\ln x} = x\)) would silently change what a formula computes where the condition fails, and is not stated in any Prelude module. Identities that make a formula larger, such as the expansion of \(\sin 2x\), are not stated either; the laws here only ever shorten a formula.

The module does not open Arithmetic. A reduction that leaves a neutral factor behind — exp(−x) · 1, say — keeps it unless the document also opens Prelude.Arithmetic.

open Prelude.Trigonometry

Identities

Matching is structural: a law fires where the formula is written in the same form as its left-hand side, with the same expression standing for x in every place.

pythagorean

law pythagorean   = sin(x)² + cos(x)² = 1

For all \(x \in \mathbb{R}\),

\[\sin^2 x + \cos^2 x = 1 .\]

Fires on the sum of a squared sine and a squared cosine of the same argument, in that order. The compiler does not reorder a sum for you, so cos(x)² + sin(x)² is not matched and is computed as written; write the sine first to have it reduced.

Intuition A point at angle \(x\) on the unit circle sits at \((\cos x, \sin x)\), and its squared distance from the centre is always one. Evaluated in floating point the two squares add to something only close to one; the law replaces them with the exact constant and skips both calls.

Use it when a formula computes the length of a rotated unit vector, the total power of an in-phase and quadrature pair, or a normalisation that should be one by construction. Write the sine term first. Open Arithmetic too, so the · 1 it can leave inside a larger product is removed.

symbolic-simplificationnumerical-stabilitygeometry

cos_of_double

law cos_of_double = cos(x)² − sin(x)² = cos(2x)

For all \(x \in \mathbb{R}\),

\[\cos^2 x - \sin^2 x = \cos 2x .\]

Fires on a squared cosine minus the squared sine of the same argument, replacing four function calls with one.

Intuition The \(x\)-coordinate of a point rotated by \(x\) and then by \(x\) again: the difference of squares is the cosine of the doubled angle. Four function calls and two squarings become one call on \(2x\).

Use it when formulas square oscillations or compose rotations, as in energy or polarisation terms, or in the orientation of a principal axis. The order is fixed: cosine squared minus sine squared, of the same written argument; the reverse difference is not matched.

symbolic-simplificationsignal-processinggeometry

sin_of_double

law sin_of_double = 2sin(x) · cos(x) = sin(2x)

For all \(x \in \mathbb{R}\),

\[2 \sin x \cos x = \sin 2x .\]

Fires on twice a sine multiplied by the cosine of the same argument.

Intuition Multiplying a sine by a cosine of the same angle produces a wave at twice the frequency; the factor 2 makes its amplitude exactly one. Two calls and two products become one call.

Use it when products of an oscillation with its own quadrature appear, as in instantaneous power, or projectile range, which is proportional to \(2 \sin\theta \cos\theta\). Write it in the law’s form, 2sin(x) · cos(x): matching is structural, so sin(x) · cos(x) · 2 is computed as written.

symbolic-simplificationsignal-processinggeometry

sin_odd

law sin_odd       = sin(−x) = −sin(x)

For all \(x \in \mathbb{R}\),

\[\sin(-x) = -\sin x .\]

Fires on the sine of a negated argument, moving the negation outside.

Intuition Sine is odd: going round the circle clockwise gives the mirror height of going anticlockwise. Pulling the minus sign out of the argument puts it where sign laws can see it.

Use it when angles arrive negated — a reversed rotation, a time-reversed signal, a phase written as −x. With Arithmetic open, −sin(−x) then reduces all the way to sin(x) through neg_neg.

symbolic-simplificationsign-normalisationsignal-processing

cos_even

law cos_even      = cos(−x) = cos(x)

For all \(x \in \mathbb{R}\),

\[\cos(-x) = \cos x .\]

Fires on the cosine of a negated argument, removing the negation.

Intuition Cosine is even: a clockwise and an anticlockwise turn by the same angle land at the same horizontal position, so the sign of the angle does not matter.

Use it when angles arrive negated, and you want the formula to show that the direction of rotation is irrelevant. Dropping the negation also makes cos(−x) the same term as cos(x), so laws that need matching arguments can fire: sin(x)² + cos(−x)² becomes a case of pythagorean.

symbolic-simplificationsign-normalisationsignal-processing

Examples

The Pythagorean identity disappears at compile time

open Prelude.Trigonometry

fn unity(x) ↦ sin(x)² + cos(x)²

using Examples;

var r = Waves.Unity(0.7);

Output (verified):

The generated real-valued method is 1d; no sine or cosine is evaluated.

Double-angle forms

Both double-angle laws replace a product or difference of calls with a single call.

open Prelude.Trigonometry

fn doubled(x) ↦ 2sin(x) · cos(x)
fn cosDoubled(x) ↦ cos(x)² − sin(x)²

using Examples;

var s = Waves.Doubled(0.5);      // sin(1)
var c = Waves.CosDoubled(0.5);   // cos(1)

Output (verified, rounded to 6 significant digits):

0.841471
0.540302

The generated methods are System.Math.Sin((2d * x)) and System.Math.Cos((2d * x)).

Negated arguments

open Prelude.Trigonometry

fn mirrored(x) ↦ sin(−x) + cos(−x)

using Examples;

var r = Waves.Mirrored(0.5);     // −sin(0.5) + cos(0.5)

Output (verified, rounded to 6 significant digits):

0.398157

The generated method is (-System.Math.Sin(x) + System.Math.Cos(x)).

Combine with Arithmetic to finish the job

Inside a larger formula the identity still fires, but the factor of one it leaves is only removed when Arithmetic’s laws are also in force.

open Prelude.Trigonometry
open Prelude.Arithmetic

fn damped(x) ↦ exp(−x) · (sin(3x)² + cos(3x)²)

using Examples;

var r = Waves.Damped(1.0);       // e^−1

Output (verified, rounded to 6 significant digits):

0.367879

With both modules open the generated method is System.Math.Exp(-x); with Trigonometry alone it is (System.Math.Exp(-x) * 1d).