►7400:   i  PPL (Spring 2020)
►Working with Redex
▼Lecture 3
    ← prev  up  next → 

9 Inductive Proofs

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:

  1. 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.

  2. s = overlay(stop,sbot) Here you may assume that

    1. area(bb(stop)) >= area(stop)

    2. area(bb(sbot)) >= area(sbot)

    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.

The outer (numeric) enumeration sets up the case analysis for s; the inner (alphabetical) enumeration is the essence of the induction proof strategy. End of organization

Proof Let us fill in the gaps:

  1. 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.

  2. 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(overlay(stop,sbot)))

    >= area(bb(stop)) + area(bb(sbot))

    with some reasonably straightforward simple claims about max and min.

    If you now compose these two calculations, you get the desired conclusion.

    ← prev  up  next →