# Structural Induction proof on binary search trees

Below is the problem I am struggling with. I understand the format of structural induction but I am having trouble with the base case right now. I can't seem to make the jump from assuming the first part of the implication to the end. Where does the insert() come from? I think that if I could figure out the base case I could probably puzzle out the rest but right now I'm stuck on that. Any help is appreciated!

Consider the following definition of a (binary)Tree:

Bases Step: Nil is a Tree.

Recursive Step: If L is a Tree and R is a Tree and x is an integer, then Tree(x, L, R) is a Tree.

The standard Binary Search Tree insertion function can be written as the following:

insert(v, Nil) = Tree(v, Nil, Nil)

insert(v, Tree(x, L, R))) = (Tree(x, insert(v, L), R) if v < x Tree(x, L, insert(v, R)) otherwise.

Next, define a program less which checks if an entire Binary Search Tree is less than a provided integer v:

less(v, Nil) = true

less(v, Tree(x, L, R)) = x < v and less(v, L) and less(v, R)

Prove that, for all b ∈ Z, x ∈ Z and all trees T, if less(b, T) and x < b, then less(b, insert(x, T)). In English, this means that, given an upper bound on the elements in a BST, if you insert something that meets that upper bound, it is still an upper bound. You should use structural induction on T for this question, but there are a few tricky bits that are worth pointing out up-front:

• You are proving an implication by induction. This means, in your Base Case, you assume the first part and prove the second one.

• Because of this, there will be two implications going on in your Induction Step. This can be very tricky. You will assume both your IH and the left side of what you’re trying to prove. You will end up needing to use both of them at some point in your proof.

Edit: I've solved the base case thanks to help, but now I am stuck on the inductive step. This is my "best" attempt at it so far:

Inductive Hypothesis: Assume $$L,R \in Trees$$ and P(L) and P(R) is true Inductive Step: Goal: Prove P(Tree(a,L,R)) / $$(less(b, Tree(a,L,R)) > \land x < b) \rightarrow less(b, insert(x, Tree(a,L,R)))$$ where $$a\in > Z$$ Assume $$less(b, Tree(a,L,R))$$ and $$x < b$$ Then, by definition of less, $$a < b \land less(b,L) \land less(b,R)$$ Then, by Inductive Hypothesis, $$a < b \land less(b, insert(a,L)) \land less(b, > insert(a,R))$$ Then, by definition of less, $$less(b, Tree(x, insert(a, > L), insert(a,R)))$$ Then, by definition of insert, $$less(b, > insert(Tree(x, insert(a, L), R)))$$ Then, by definition of insert, $$less(b, insert(insert(Tree(x, L, R)))$$

• I'm not sure what you mean by "where does the insert() come from?" It is defined right there in your quote. Feb 23, 2020 at 18:18

You are proving this over induction on the Tree $$T$$, not the variables $$b, x$$, so we can assume we are just given values of $$b$$ and $$x$$, with $$x < b$$.

The base case of the induction is when $$T = \text{Nil}$$. So you have to prove:

• if $$\text{less}(b, \text{Nil})$$, then $$\text{less}(b, \text{insert}(x, \text{Nil}))$$.

So assume $$\text{less}(b, \text{Nil})$$. (Actually this much is true from the definition of "less" - but even if it were not always true, since it is your hypothesis, you can assume it here.)

By the definition of "insert", $$\text{insert}(x, \text{Nil}) = \text{Tree}(x, \text{Nil}, \text{Nil})$$

So you need to prove $$\text{less}(b, \text{Tree}(x, \text{Nil}, \text{Nil}))$$. By the definition of "less", that statement is $$\text{less}(b, \text{Tree}(x, \text{Nil}, \text{Nil})) = x < b \text{ and }\text{less}(b, \text{Nil})\text{ and }\text{less}(b, \text{Nil})$$

Since $$x < b$$ and $$\text{less}(b, \text{Nil})$$ are both true, so is $$\text{less}(b, \text{Tree}(x, \text{Nil}, \text{Nil}))$$ and therefore $$\text{less}(b, \text{insert}(x, \text{Nil}))$$.

This proves the base case. I'll leave you to figure out how to do the induction step.

On the inductive step, again, you can assume that $$x, b \in \Bbb Z$$ with $$x < b$$. What you need to show is that for a tree $$T \ne \text{Nil}, \text{less}(b, T) \implies \text{less}(b, \text{insert}(x,T))$$. Because $$T \ne \text{Nil}$$, you know that $$T = \text{Tree}(a, L, R)$$ for some $$a \in \Bbb Z$$ and trees $$L, R$$.

The inductive hypothesis is (since we are given $$x < b$$), "$$\text{less}(b, L) \implies \text{less}(b, \text{insert}(x,L))$$ and $$\text{less}(b, R) \implies \text{less}(b, \text{insert}(x,R))$$"

So you start by assuming $$\text{less}(b, T)$$. From this, demonstrate that $$\text{less}(b, L)$$ and $$\text{less}(b, R)$$. By the induction hypothesis, you then know that $$\text{less}(b, \text{insert}(x,L))$$ and $$\text{less}(b, \text{insert}(x,R))$$. From those two facts, you then demonstrate that $$\text{less}(b, \text{insert}(x,T))$$ also holds. Once you've supplied the indicated demonstrations, this proves $$\text{less}(b, T) \implies \text{less}(b, \text{insert}(x,T))$$, finishing the inductions step.

• Thank you so much for your help with the base case, I think I've got it now. However, I am now lost on the inductive step, I've edited the question with my best shot at it but I don't think its right. Any help is appreciated, thank you so much Feb 23, 2020 at 23:43
• @user65909 - I've added an outline of how the inductive step should go. Feb 24, 2020 at 3:41
• Thanks so much for the outline, I think I understand it I'm just slightly confused on how to make the transition from less(b,insert(x,L)) and less(b,insert(x,R)) to less(b, insert(x,T)). What definitions and steps facilitate that transformation? Feb 24, 2020 at 19:04
• "insert(v, Tree(x, L, R))) = (Tree(x, insert(v, L), R) if v < x Tree(x, L, insert(v, R)) otherwise." Feb 25, 2020 at 0:04
• T =Tree(a, L, R), so insert(x,T) = insert(x, Tree(a, L, R)). If $x < a$, this is Tree(a, insert(x,L), R), if $a < x$, then it is Tree(a, L, insert(x, R}}. So, less(b, insert(x, T)) either is equal to less(b, Tree(a, insert(x, L), R)) or is equal to less(b,Tree(a, L, insert(x,R))). That is how you do it. You don't jump to conclusions. It is not intuition. It is just mechanically applying the definitions. And there is only one way to do it. You see the expression you need to work on next. You go to the list of definitions and find that expression, and you handle it according to that definition. Feb 26, 2020 at 0:26