# 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. Feb 20 '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. Feb 20 '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? Feb 21 '20 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. Feb 21 '20 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. Feb 21 '20 at 9:45
• It seems you've deferred one notion of membership for another, then @Nicolas will have to prove that definition is correct ;-) Feb 21 '20 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 '20 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 '20 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 '20 at 18:37