It is time to study the structure of proofs for claims about inductive functions and sets. Here is a mathematical statement of the claim:
Claim: for all Shapes s, area(bb(s)) >= area(s)
The claim is about the elements of an infinitely large set. When such a set is defined by induction, we can usually (but not always) use mathematical induction, specifically, a modification called structural induction. The key to structural induction is that you may assume that the claim holds for all pieces of a compound structure. This is similar to plain mathematical induction where you assume that the claim holds for n and then prove it for n+1. Also, such proofs are usually organized in analogy to the definition. That is, the proof proceeds by case analysis that includes as many cases as the inductive definition and the same kind of shapes.
Here is an outline of the proof of the above claim according to these two principles.
Proof Organization By induction on the structure of the definition of Shapes and by case analysis on the construction of s:
s = square(x,y,r) In this so-called base case, you must prove that area(bb(square(x,y,r))) >= area(square(x,y,r)), without any further assumptions.
- s = overlay(stop,sbot) Here you may assume that
These two statements are called induction hypotheses. From these induction hypotheses, you must prove that area(bb(overlay(stop,sbot))) >= area(overlay(stop,sbot)) and you may use the definitions of the functions.
area(bb(stop)) >= area(stop)
area(bb(sbot)) >= area(sbot)
If s is a square, its bounding box is the same square, meaning the areas of the two shapes are the same. You can perform an algebraic computation using the function definitions for bb and area.
From the two induction hypotheses, you get
area(bb(stop)) + area(bb(sbot))
>= area(stop) + area(sbot)
>= area(stop) + area(sbot) - area(intersection(stop,sbot))
= area(overlay(stop,sbot))because area(intersection(stop,sbot)) >= 0. (An area is positive!)Using the definitions of area and bb, you also get
>= area(bb(stop)) + area(bb(sbot))
If you now compose these two calculations, you get the desired conclusion.