# Proving a function is a fixed point

I'm taking a class in University which involves proving the correctness of computer programs and I'm really bad a proofs, I don't really understand them at all.

Can anyone tell me if my proof actually makes any sense, I frequently think I've written a proof but usually I've proved nothing.

Given this (T1 is a function that takes another function (F) as one of its parameters):

T1(F,x,y) == if y = 0 then x else F(x−1,y−1)

I had to suggest a fixed point solution, I suggested:

f1(x,y) == x - y

Because T1 is a recursive function that implements subtraction. And below I had to prove my suggestion was correct.

To show T1(f1) = f1

T1(f1, x, y) == if y = 0 then x else f1(x−1,y−1)

if y = 0 then x
else (x-1) - (y-1)

if y = 0 then x
else x - y - 2

x - y - 2 = f1(x-1,y-1)

x - y = f1(x,y)

Does my proof have some obvious hole in it that I'm not seeing or is there some mistake I can't see, I think it works but I'm not really sure why it proves anything?

You are thinking of the map: $$T_1(f,x,y) =\begin{cases} x & \text{if } y=0 \\f(x-1,y-1) & \text{otherwise} \end{cases},$$ and want to show that the function $$f(x,y)=x-y$$ is a fixed point. This amounts to showing $$T_1(f,x,y)=f(x,y)=x-y\$$ for any $$x$$ and $$y$$.
There are only two cases one has to check, $$y=0$$ and $$y\neq 0$$. If $$y=0$$, then $$T_1(f,x,0)=x=x-0=f(x,0)$$, just as we want. If $$y\neq 0$$, then $$T_1(f,x,y)=f(x-1,y-1)=x-1-y+1=x-y=f(x,y)$$, and the proof is done.
I don't fully understand the programmatic notation you are using, but I think this is what you are trying to do. However you have evaluated $$f(x-1,y-1)$$ to $$x-y+2$$ rather than $$x-1-y+1=x-y$$, possibly you have forgotten to distribute the minus sign. I hope this helps!
Your idea is correct, but in the way it's written I don't recognize it as a proof. You want to show that $$T_1(f_1,x,y)=f_1(x,y)$$ for all $$x$$ and $$y$$ in whatever your domain is. So start with $$x$$ and $$y$$, distinguish cases for $$y=0$$ and $$y\neq0$$, and then show that in both cases $$T_1(f_1,x,y)=f_1(x,y)$$.