Recursive definitions and structural induction:

A binary tree is:
  - (make-empty-tree)
  - (make-branch [any] [tree] [tree])

(define-struct empty-tree ())
(define-struct branch (datum left right))


Prove: for any binary tree, there is one more leaf than branch.

NOT the way to argue the inductive step:
 "take any binary tree of size k;
  i'll splice out a leaf and add a branch with two leaves.
  this gives me a binary tree of size k+1, which has one more
  branch and (net) one more leaf."
Problem: this gives you *some* binary tree of size k+1,
but can you guarantee that all such binary trees were created through
this method?

To be clear, start with an arbitrary binary tree of size k+1,
and show that it has the property
(knowing that any way you trim it down gives you a binary tree
of size k, for which the inductive hypothesis will hold).



We'll define the size of a binary tree as the number of branches:
  For an empty binary tree, 0.
  For a branch, 1+size(left)+size(right).

We'll define the height of a binary tree as:
  For an empty binary tree, 0.
  For a branch, it's 1+max(height(left),height(right)).


Prove:  For any binary tree,
  size(t)+1 ≤ 2height(t)




Similarly, structural induction on WFFs of first-order logic:
A WFF is:
  - T or F,        } "atoms"
  - a proposition, }
  - ¬φ,
  - (φ ∧ ψ),
  - (φ ∨ ψ),
  - (φ → ψ)
  - ∀ x.φ
  - ∃ x.φ
This is a recursive definition of structure;
proof on WFF will have eight cases (two base, 6 recursive).

Prove: for any WFF, the number of connectives ≥ 
is equal to the number of atoms minus 1.

(More generally, we can include not: #conns ≥ #props-1.)



Here is a def'n of string: 
For a set Σ (the alphabet), the set 
Σ* ("strings over Σ") contains:
  - lambda (empty string)
  - wa, where a ∈ Σ, and w ∈ Σ*.

How to further define concat?
  For v,w ∈ Σ*, vw ∈ Σ* as follows:
   - If w=lambda, vw = v.
   - if w=ua (for a letter a and a string u),
     vw = (vu)a.
     
Th'm (book): length(vw) = length(v) + length(w).
  Define length on def'n.
  Then, induct on *w only*!
  That is, P(w) = "length(vw) = ..." (for arbitrary string v).
  Then just look at the two cases for w being empty or not.
  (This is an example in Rosen.)

Give a def'n of "string of even length".
Give a def'n of "stuttering string", each letter duplicated -- e.g.  aabbzzzzyy.
Give a def'n of wR:  
   - if w=lambda, lambdaR = lambda.
   - if w=ua,  wR = auR.

Book (and a hw problem) talks about reversal wR of a string w.
What is skeleton for showing
  (vw)R = wRvR ?
Again, make P() about w only, with a "forall v ∈ Σ* ...".
Use the Def'n of concatenation!




Proof: a string contains at most one more occurrence of 01 than of 10.
Notation, to help: for a string s, #01(s) is the number of 01's, and #10(s) corresponding.

Let P(s) be "#01(s) ≤ #10(s)+1".
Proof by structural induction:
- base case: if s = lambda, 0 ≤ 0+1, check.
- Inductive step, s=wa: 
   case a=0: inductive hypothesis:   #01(w) ≤ #10(w) + 1.
      Thus #01(s) = #01(w0) = #01(w);
           #10(s) = #10(w0) = #10(w) + {0 or 1} ≥ #10(w).
        So, #01(s) = #01(w) ≤ #10(w)+1 ≤ #10(w0)+1 = #10(s)+1.
   case a=1: is harder.  Look at the subcases of w:
      subcase w=lambda: check
      subcase w=v0: s=w1=v01. 
          Then  #01(s) = #01(v01)= #01(v0)+1 = #01(v)+1 ≤ #10(v)+2 
              #10(s) = #10(
      subcase w=v1: s=w1=v11.
     
      
[The first time I wrote out this proof, I didn't use this notation "#01()".
 As i was repeating the same words over and over, I went back
 and re-wrote it with notation.

 By the way, deciding what things to give special shorthand/names to
 is part of the art of writing a good proof...
 just as deciding precisely what tasks to include as separate functions
 is part of the art of writing a good program.

 Beware adding too *much* new notation -- this can result in
 a more-confusing proof.  Using "standard" names like
 x,y for real numbers, m,n for natnums, i,j for indices
 can also make your notation more accessible.
 ]



   



------------  Why all these different forms of induction?
For you to ponder:
If I restricted you to only use a single base case,
would this suffice to still solve the problem?
That is, is
    strong-induction-with-multiple-premises
a truly more powerful inference rule than
    strong-induction-with-single-premise?
For that matter, introduced mathematical (non-strong) induction
as a new rule of inference; then sneakily slipped in strong-induction
as well.
Are we justified to throw in stronger and stronger rules of
inference whenever we feel like it?
(Rosen even has a couple of exercises in this vein: sect 3.3, #55,56.)