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)))$
Best Answer
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:
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.