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