Disclaimer: I'm not a mathematician. I'm a developer (with physics degree).
I'm programming tax form and stumbled on following (simplified) definition of one of the fields, lets name it P: $$a = \dots$$ $$b = \dots$$ $$c = \max(\min(a,b),0)$$ $$ P = \left\{ \begin{matrix} \max(b,0)-c & a \leq 0 \\ \max(b,0)-c & b>a \\ 0 & otherwise & \end{matrix} \right. \land P\geq0 $$
I've checked on Wolframalpha that $\max(b,0)-c=\max(b,0)-\max(\min(a,b),0)$ always meets the required conditions.
$\max(b,0)-\max(\min(a,b),0) \geq 0$ results in $True$ (which I'm assuming means that it's always true)
and
$\max(b,0)-\max(\min(a,b),0) > 0$ have following solutions:
$${a > 0, b > a}$$
$${a <= 0, b > 0}$$
which means that initial conditions are met.
So seems that I just need to type in my program that $P = \max(b,0)-c$ and assume that task is finished, but I'm curious: How can one come from definition of $P$ to $P = \max(b,0)-c$?
How can one get rid of all conditions (ifs) and end up with one simple formula $\max(b,0)-c$?
I've tried to start with something like this:
- $a \leq 0 \implies a=\min(a,0)$
- $b>a \implies b=max(a,b)$
and for each case somehow end up with $\max(b,0)-c\geq0$ but all my attempts failed so far.
Correct me if I'm wrong, but I'm probably asking for a proof that:
$${
{P =
\left\{
\begin{matrix}
\max(b,0)-c & a \leq 0 \\
\max(b,0)-c & b>a \\
0 & otherwise &
\end{matrix}
\right. \land P\geq0}
} \implies \max(b,0)-c\geq0
$$
Edit: Better explanation for what I'm asking for:
In "Material for the course Constructive Logic at Carnegie Mellon University" (15-317) I have found folowing example how we prove $A \lor B$
If we know that A ∨ B is true, we must consider two cases: A true and B true. If we can prove a conclusion C true in both cases, then C must be true! Written as an inference rule:
$$ \frac { \begin{matrix} \\ \\ A \lor B \, true \end{matrix} \begin{matrix}\frac{}{A\,true}u \\ \vdots \\ C\,true \end{matrix} \begin{matrix}\frac{}{B\,true}w \\ \vdots \\ C\,true \end{matrix} }{C\,true} \lor E^{u,w} $$
Translated to my case it's (assuming I correctly understand how inference rules are written): $$ \frac { \begin{matrix} \\ \\ a \leq 0 \lor b>a \, true \end{matrix} \begin{matrix}\frac{}{a \leq 0 \, true}u \\ \vdots \\ \max(b,0)-c \geq 0 \,true \end{matrix} \begin{matrix}\frac{}{b>a \, true}w \\ \vdots \\ \max(b,0)-c \geq 0 \,true \end{matrix} }{\max(b,0)-c \geq 0 \,true} \lor E^{u,w} $$
And I want to know what hides behind every $\vdots$
You can separate the cases.
Case 1: $a\leq 0$.
If $a\leq 0$, then you know that $\min(a,b)\leq 0$, which means that $\max(\min(a,b),0)=0$.
You also know that $\max(b,0)\geq 0$, which means that $$\max(b,0)+\max(\min(a,b),0) = \max(b,0)+0=\max(b,0)\geq 0.$$
Case 2: $a>0$.
In this case, because we know that $b>a\lor a\leq 0$, we know that $b>a$.
Therefore, we know that $\min(a,b)=a$, which means that $\max(\min(a,b),0) = \max(a,0)=a$, because $a>0$.
This means that
$$\max(b,0)-\max(\min(a,b),0)=\max(b,0)-a=b-a,$$ and since we know $b>a$, we also know $b-a>0$, which means the entire expression is positive in this case.
If you want to fully write out the range of values that the expression $\max(b,0)-\max(\min(a,b),0)$ can take, then you need to separate out some more cases. In particular, you have the following $6$ cases:
$$\max(b,0)-\max(\min(a,b),0)=\begin{cases}0&\text{if}&a\leq b\leq 0\\ b&\text{if}&a\leq 0\leq b\\ 0&\text{if}&b\leq a \leq 0\\ 0&\text{if}&b\leq 0\leq a\\ b-a&\text{if}&0\leq a\leq b\\ 0&\text{if}&0\leq b\leq a\end{cases}$$
This also shows that the expression is always positive (i.e., not only when $b<a\lor a\leq 0$).