Refactoring using mathematical properties of min

Today I refactored a small piece of code.

Before:

$coupon_amount = self::get_coupon_prop( $coupon, 'amount' ) - $already_applied_coupons;

if ( isset( WC()->cart ) ) {
	$coupon_amount = min( WC()->cart->subtotal - $already_applied_coupons, $coupon_amount );
}

if ( $coupon_amount < 0 ) {
	return $discount;
}

After:

$coupon_amount = self::get_coupon_prop( $coupon, 'amount' );

if ( isset( WC()->cart ) ) {
	$coupon_amount = min( WC()->cart->subtotal, $coupon_amount );
}

$coupon_amount -= $already_applied_coupons;

if ( $coupon_amount < 0 ) {
	return $discount;
}

This was intuitive to me, but I wanted to prove that it really does the same thing. For that, we need to use the property $min(a - c, b - c) = min(a, b) - c$ .

The usual definition for min is:
$min(a, b) = \left\{ \begin{array}{ll} a, & \mbox{if } a < b \\ b, & \mbox otherwise \end{array} \right.$

Now we can use proof by cases to prove our property which will allow us to confidently refactor our code. There are two cases we can assume:

1. Case $a - c > b - c$ :
In this case, $min(a - c, b - c) = b - c$ , and since from $a - c > b - c$ we can conclude that $a > b$ , then $min(a, b) = b$ .
So, we have that $b - c = b - c$ , which proves this case.

2. Case $a - c \le b - c$ :
In this case, $min(a - c, b - c) = a - c$ , and since from $a - c < b - c$ we can conclude that $a < b$ , then $min(a, b) = a$ .
So, we have that $a - c = a - c$ , which proves this case.

Thus, the property $min(a - c, b - c) = min(a, b) - c$ is proven. 🙂

There are also some other properties like $min(a, a) = a$ and $min(a, b) = min(b, a)$ but you can try doing these yourself. Stuff with max is proven analogously.