How come correctness proofs aren't tautological?

Question

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?

Answer 1

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$.