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 4: 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 4—
Claim: for all Lists of numbers l, abs.v1(l) = abs.v2(l)
Claim: for all Lists of numbers l, abs.v1(l) = aux(l,0)
; A Lon (list of numbers) is one of: ; – empty or () ; – (cons Number #, Lon)
Proof Organization By induction on the structure of the definition of Lists and by case analysis on the construction of l:
l = () In this so-called base case, you must prove that abs.v1( () ) = aux( () ,0), without any further assumptions.
- 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.
abs.v1( (nfirst nrest ...) )
= cons(nfirst,+*(nfirst, abs.v1(nrest ...)))
= cons(nfirst,+*(nfirst, aux( (nrest ...), 0)))
aux( (nfirst nrest ...), 0 ) = cons (nfirst, aux( (nrest ...) nfirst))
for all lists l and for any number n, +*(n,abs.v1(l)) = aux(l,n)
The first case, l = () works out easily again.
+*(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
+*(n,aux(l)) = aux(l,n)