# How come correctness proofs aren't tautological?

Consider the following function on binary trees, which is supposed to tell whether a given int is a member of a binary tree t:

type tree = Leaf | Node of int * tree * tree;;

let rec tmember (t:tree) (x:int) : bool =
match t with
Leaf -> false
| Node (j,left,right) -> j = x || tmember left x || tmember right x
;;


If one wants to prove that this function is correct, one would need to define first what tree membership actually means, but then I can find no formal way of doing this except for saying that x is a member of t if and only if it is either equal to the root of t, or it is a member of the left or right subtree of t. This is essentially saying that x is a member of t if and only if tmember t x outputs true.

What am I missing here?

• Some things have to be taken primitively before properties can be proven, such as tmember. However, you can still prove things about it that you would expect of a membership relation, such as empty trees have no elements and if you insert an element into a tree then tmember gives true. – Musa Al-hassy Feb 20 at 14:04
• This seems to demonstrate the elegance of the functional paradigm: correctness is often “self evident” from the code. Consider the procedural paradigm, where you might want to prove tmember is true if and only if x was added ad some point in the past but not yet removed. – Daniel M Gessel Feb 20 at 17:58
• @MusaAl-hassy do you mean that the membership relation cannot be stated in more general terms, and therefore one should define it as being the output of the tmember function? – Nicolas Feb 21 at 9:51
• Yes, using it as a starting point you can then define subset and equality relationships. Then check the expected properties, such as 'casting' $x \in X \subseteq Y \to x \in Y$; if the usual elementary properties cannot be proven, then you know something's wrong somewhere. – Musa Al-hassy Feb 21 at 18:17

Membership is much more general than this recursive definition you give. At a higher level you could define membership as follows:

A tree can be defined as a collection of nodes, $$V$$, and edges $$E$$ where those edges and nodes satisfy particular constraints.

We say a value $$x$$ is a member of the tree if and only if there is a node $$v$$ in $$V$$ such that the value of $$v$$ is equivalent to $$x$$.

You then prove (probably with induction since it's recursive) that your function is equivalent to this definition. That is to say, your function returns true on value $$x$$ if and only if there is a node $$v$$ in $$V$$ such that the value of $$v$$ is equivalent to $$x$$.

• If I understand correctly, you are suggesting that the specification be written in terms of these graph theoretic notions. But what if one were to use only set theoretic notions, as described here ? I think in that case the specification would correspond roughly to what I wrote in my question. – Nicolas Feb 21 at 9:45
• It seems you've deferred one notion of membership for another, then @Nicolas will have to prove that definition is correct ;-) – Musa Al-hassy Feb 21 at 18:18
• @Musa you don't have to prove definitions are correct, that's why it's a definition. You prove that the function returns true if and only if the definition is satisfied. I guess you could choose whichever definition you want, but set membership is much more general than the definition provided in the question. – ryan Feb 21 at 18:28
• Whatever the case, pick a definition and prove that your function returns true iff that is satisfied. Whether or not the definition is what you want is another question. – ryan Feb 21 at 18:31
• @Nicolas if you stick with your original definition of tree membership then the proof just becomes easier. You prove it for the base case (empty tree), then prove inductively that it holds for a tree of size $n$. – ryan Feb 21 at 18:37