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

10 Improving Claims

(define-language Lon
  (l (n ...))
  (n number))
 
; a simple demonstration of a syntax rule
(define-syntax-rule
  (t x)
  ; ==>> (rewrite to)
  (term x))
 
; act like cons for Redex
(define-metafunction Lon
  mcons : n l -> l
  [(mcons n l) ,(cons (term n) (term l))])
 
; act like + for Redex
(define-metafunction Lon
  m+ : n n -> n
  [(m+ n_1 n_2) ,(+ (t n_1) (t n_2))])

(define-metafunction Lon
  abs.v1 : l -> l
  [(abs.v1 ()) ()]
  [(abs.v1 (n_h n_r ...))
   (mcons
     n_h
     (+* n_h
         (abs.v1 (n_r ...))))])
 
(define-metafunction Lon
  +* : n l -> l
  [(+* n l)
   ,(map (λ (x) (+ x (t n)))
         (t l))])

(define-metafunction Lon
  abs.v2 : l -> l
  [(abs.v2 l) (aux l 0)])
 
(define-metafunction Lon
  aux : l n -> l
  [(aux () n) ()]
  [(aux (n_h n_r ...) n)
   (mcons (m+ n n_h)
     (aux (n_r ...)
          (m+ n n_h)))])

Figure 3: Two ways of computing absolute distances

On occasion, structural induction is not quite enough. To illustrate this point, let us study the claim that the two versions of the abs function in figure 3—one plain structural, one in accumulator-style—are equal. That is, given the same list of relative distances they produce the same list of absolute distances.

Claim: for all Lists of numbers l, abs.v1(l) = abs.v2(l)

Since abs.v2(l0) = aux(l0,0), we really mean

Claim: for all Lists of numbers l, abs.v1(l) = aux(l,0)

What you may not see from the definition of Lon is that lists have an inductive definition. Here it is:
; A Lon (list of numbers) is one of:
; – empty or ()
; – (cons Number #, Lon)
It has the two obvious clauses, and it is inductive in the expected case (the cons case) and position (cons consumes a number and a list). Hence we can adapt the proof organization from above:

Proof Organization By induction on the structure of the definition of Lists and by case analysis on the construction of l:

  1. l = () In this so-called base case, you must prove that abs.v1( () ) = aux( () ,0), without any further assumptions.

  2. s = (nfirst nrest ...) Here you may assume that

    abs.v1( (nrest ...) ) = aux((nrest ...), 0)

    which is the induction hypothesis for an inductive definition with a single self-reference.

    From the inductive hypothesis, you must prove that abs.v1( (nfirst nrest ...) ) = aux((nfirst nrest ...), 0) and you may use the definitions of the functions.

Again, the enumeration sets up the case analysis for l; the nested math display enumeration is the essence of the induction proof strategy. End of organization

You can probably see that the first item follows from a trivial calculation. The problem is the second item, the inductive step. Let us start by simplifying the left side of the goal:

abs.v1( (nfirst nrest ...) )

= cons(nfirst,+*(nfirst, abs.v1(nrest ...)))

= cons(nfirst,+*(nfirst, aux( (nrest ...), 0)))

The last step of the calculation follows from the induction hypothesis. But as you can easily see from any example, this last line is not equational equal to aux( (nfirst nrest ...), 0) because it unfolds like this:

aux( (nfirst nrest ...), 0 ) = cons (nfirst, aux( (nrest ...) nfirst))

What this means that we need to improve our claim so that the induction goes through:

for all lists l and for any number n, +*(n,abs.v1(l)) = aux(l,n)

The first case, l = () works out easily again.

The second case, l = (nfirst nrest ...) relies on the induction hypothesis:

+*(n,abs.v1( (nfirst nrest ...) ))

= +*(n,cons(nfirst,+*(nfirst,abs.v1( (nrest ...) )))) by def. of abs.v1

= cons(n+nfirst,+*(n,+*(nfirst,abs.v1( (nrest ...) )))) by ’laws’ of +*

= cons(n+nfirst,+*(n+nfirst,abs.v1( (nrest ...) ))) by ’laws’ of +*

= cons(n+nfirst,aux( (nrest ... ),n+nfirst)) by IH

= aux( (nfirst nrest ... ),n) by def. if aux

Naturally, what we called ’laws’ of +* are claims about this auxiliary function, and these claims deserve a proof. They are good practice proof and follow from straightforward structural induction.

P.S. Yes, an alternative way to proceed would have been to prove

+*(n,aux(l)) = aux(l,n)

    ← prev  up  next →