Is structural induction on terms applicable when a function is involved?

Assume an evaluation-relation on terms $t \Downarrow v$. If I want to prove correctness of a function $\phi$ w.r.t. evaluation, I have to show that the following implication always holds:

$$\frac{\phi(t) \Downarrow \phi(v)}{t \Downarrow v}$$

Naturally, this is a candidate for structural induction. But on what structure? Is it sufficient to run the induction over terms, or do I have to run it over the derivation tree? Structural induction is usually only allowed for direct sub-terms, but the function could, in principle, yield completely different results.

Is it sensible to consider $\phi$ part of the promise or do I have to consider it a part of the recursive structure?

You probably shouldn't write $\cfrac{\phi(t)\Downarrow \phi(u)}{t\Downarrow u}$ for "For any terms $t,u$, $\phi(t)\Downarrow \phi(u)$ implies $t\Downarrow u$".

I'll take a concrete example: Terms are made using $0,S,+$. And there are six rules:

$$\cfrac{}{0 \Downarrow 0}(0)\hspace{2em}\cfrac{x\Downarrow y}{Sx \Downarrow Sy}(S)\hspace{2em}\cfrac{x\Downarrow y}{x+0 \Downarrow y}(+0)\hspace{2em}\cfrac{x\Downarrow y}{0+x \Downarrow y}(0+)\hspace{2em}\cfrac{x+y\Downarrow z}{x+Sy \Downarrow Sz}(+S)\hspace{2em}\cfrac{x+y\Downarrow z}{Sx+y \Downarrow Sz}(S+)$$

Note that $(0+)$ and $(S+)$ are superfluous (but do not break the uniqueness of the normal form).

I'll provide three examples where different proof techniques apply.

Let's take $\phi(x)=Sx$.

Suppose that for some $a$, $Sa=\phi(a)\Downarrow \phi(b)=Sb$. The only rule that allows you to prove this is the rule $(S)$ with $x=a$ and $y=b$ (because it's the only rule that can have successor on both sides of $\Downarrow$ in the conclusion), so you must have $a\Downarrow b$, which is what you want. So you can prove that "For any terms $t,u$, $\phi(t)\Downarrow \phi(u)$ implies $t\Downarrow u$".

You were able to prove it without even using induction because the definition of $\phi$ wasn't inductive.

Remark

But you can not compose rules to get $\cfrac{St\Downarrow Su}{t\Downarrow u}$ (because there are more $S$ in the conclusion than in the premise and all rules have at most as many $S$ in the conclusion as in the premise).

Your result is a meta-theorem but not a theorem (because it's not just a combination of the rules).

A theorem would, for example, be $\cfrac{}{S0\Downarrow S0}$ (that you get by composing $(0)$ and $(S)$ or $\cfrac{x\Downarrow y}{x+S0\Downarrow Sy}$ (that you get by composing $(+0)$ and $(+S)$).

Let's take another example: $\varphi(0)=0$, $\varphi(Sx)=SSx$ and $\varphi(x+y)=\varphi(x)+\varphi(y)$.

Now suppose that $\varphi(a)\Downarrow \varphi(b)$.

We'll prove $a\Downarrow b$ by induction on the size of the proof of $\varphi(a)\Downarrow \varphi(b)$.

If it's of size $1$, then it has to be just an application of $(0)$ so $\varphi(a)=0=\varphi(b)$ and so $a=0=b$ and $(0)$ gives us the proof we want.

If it's of size $>1$, the last rule is not $(0)$ so you do case analysis and apply the induction hypothesis on the premise of the rule. You'll have to do case analysis, but you should be able to prove that it works.

There should be some case where you can do induction on terms to prove the thing but I couldn't find one. It feels more natural when you have a small step transition system $\to$ and define a big step one $x\Downarrow y$ by $x\to^* y$ and for any $z$, $y\not\to z$. Then, it you manage to prove that $\phi(x)\to \phi(y)$ implies $x\to^+ y$ and that $x\to y$ implies $\phi(x)\to^+\phi(y)$, you will get that $\phi(x)\Downarrow \phi(y)$ implies $x\Downarrow y$.

The main thing you should remember is that "case analysis" < "induction on terms" < "induction on proofs" in terms of what you can proove but often, the number of cases you have to handle often grows. So you should try the proofs techniques in that order until you get one that works.

StackExchange Computer Science Q#64832, answer score: 3