Complex property of sparse horner polynomials by induction I'm following this article to do a formal proof on elliptic curve cryptography. My question here addresses only a property "easily proved by induction".

Definitions (the important part is the addition definition at the bottom)

Let assume the following hierarchy:

abstract class shf;
case class const(c: Integer) extends shf
case class POP(i: nat, p: shf) extends shf
case class POW(i: nat, p: shf, q: shf) extends shf


where nat is the type for naturals including zero. We state also a property on the hierarchy called normality given by the function:

def normal(p: shf) = p match {
 case const(c) =&gt; true
 case POP(i,p) =&gt; i &gt; 0 &amp;&amp; normal(p) &amp;&amp; p = POW(_,_,_)
 case POW(i,p,q) =&gt; i &gt; 0 &amp;&amp; normal(p) &amp;&amp; normal(q) &amp;&amp; p != POW(_,_,0)
}


Assume we have some type shfn to say that we have a shf with the normality property. Then also define these functions:

def pop(i: nat, p: shfn) = {
 case i = 0 or p = const(_) =&gt; p
 case p = POP(j,q) =&gt; POP(i+j,q)
 case _ =&gt; POP(i,p)
}


Denote nat* the naturals without zero:

def pow(i: nat*, p: shfn) = {
 case p = 0 =&gt; pop(1,q)
 case p = POW(j,r,0) =&gt; POW(i+j,r,q)
 case _ =&gt; POW(i,p,q)
}


Finally, define the addition operation:

if (x = const(c1)) {
 if(y = const(c2))       c1+c2 (over the integers)
 else if(y = POP(i,p))   POP(i,x+p)
 else if(y = POW(i,p,q)) POW(i,p,x+q) 
}

if(y = const(c)) y+x

if(x = POP(i,p) &amp;&amp; y = POP(j,q)){
 if(i=j)        pop(i,p+q)
 else if(i &gt; j) pop(j,POP(i-j,p)+q)
 else if(i &lt; j) pop(j,POP(j-i,q)+p)
}

if(x = POP(i,p) &amp;&amp; y = POW(j,q,r)){
 if(i=1) POW(j,q,r+p)
 else    POW(j,q,r+POP(i-1,p))
}

if(y = POP(i,p) &amp;&amp; x = POW(j,q,r)) y+x 

if(x = POW(i,p,q) &amp;&amp; y = POW(j,r,s)){
 if(i=j)        pow(i,p+r,q+s)
 else if(i &gt; j) pow(j,POW(i-j,p,0)+r,q+s)
 else           pow(i,POW(j-i,r,0)+p,s+q)
}


The problem

I'm trying to prove that if $x,y$ are normal then $x+y$ is also normal. But the induction is not trivial to me. 

I tried to split it. First I consider $x$ to be constant and everything went well by using the corresponding induction hypothesis. 

The problem appears when I consider $x$ to be $POP$ and I do induction on $y$. When $y$ is also $POP$ I have to rely on the $POW$ case because note that as $x,y$ are normal and instances of $POP$ then their second components need to be instances of pow. The other cases for this situation then need the $POP-POW$ case. But proving the $POP-POW$ case could potentially lead to a $POP-POP$ case again.

How can I structure my proof to succeed? 

You may want to look at the actual proof on ACL2 here. Also, if you have any ideas to simplify the problem (to make it more easy to reason about and describe it) please let me know.

Intuition

Intuitively a POP construct represents a jump in the list of variables where our shf form is evaluated and a POW represents a polynomial in current variable x of the form $x^i \cdot p + q$. So normality for POP means that the jumping index is as big as possible (there cannot be nested POPs) and normality for POW means the power index $i$ is as big as possible.
You need to use induction on some complexity measure $\mu(x,y)$ (on some well-ordered domain) which has the following property:


  When running the addition procedure on $x,y$, all recursive calls are on pairs $z,w$ for which $\mu(z,w) &lt; \mu(x,y)$.


A complexity measure satisfying this property shows that the addition procedure terminates, and will also allow you to do a proof by induction. Note that you are not splitting into cases according to the coarse structure of $x,y$.

It is often the case that you can take $\mu(x,y)$ to be the total description length of $x,y$, so you might start by checking whether this works here. Another possibility is to take the sum of the total degrees of all monomials in $x,y$.

Finally, how should you approach the problem? I suggest forgetting about the formalism (in particular, ignoring POP completely) and writing out the simplification steps in their barest forms. Using $N(p,q)$ for the normal form of $p+q$ (themselves already in normal form), the rules are:


$N(c_1,c_2) = c_1+c_2$.
$N(c,x_i^jp+q) = x_i^jp+N(c,q)$.
$N(x_i^{j_1}p_1+q_1,x_i^{j_2}p_2+q_2) = x_i^{j_2}N(x_i^{j_1-j_2}p_1+0,p_2)+N(q_1,q_2)$, where $j_1 &gt; j_2$.
$N(x_i^jp_1+q_1,x_i^jp_2+q_2) = x_i^jN(p_1,p_2)+N(q_1,q_2)$.
$N(x_{i_1}^{j_1}p_1+q_1,x_{i_2}^{j_2}p_2+q_2) = x_{i_1}^{j_1}p_1+N(q_1,x_{i_2}^{j_2}p_2+q_2)$, where $i_1 &lt; i_2$.


Here we are conflating POP and POW, which makes things a littler more concrete.

We want to prove that these rules are correct, namely:


  If $p,q$ are in normal form then $N(p,q)$ terminates, is in normal form, and agrees as a function with $p+q$.


This can be split into several tasks. First, assuming that $p,q$ are in normal form, show that they match exactly one rule. Second, show that in each recursive invocation $N(r,s)$ on the right-hand side, (i) $\mu(r,s) &lt; \mu(p,q)$, and (ii) $r,s$ are in normal form. Third, show that the right-hand side agrees with $p+q$ as a polynomials (using the inductive hypothesis). Fourth, show that the right-hand side is in normal form (again using the inductive hypothesis).

Proving that the addition procedure as given is valid is similar, only we need to take into account the different encoding which separates POW and POP.