%%% Assignment 9 %%% Out: Mon 26 Nov %%% Due: Mon 3 Dec %%% Author : Brigitte Pientka % % This assignment is to be submitted on paper. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % 1. Consider the statement: % % "for every natural number n, the product n * (n + 1) is even". % % Give an informal inductive proof of the corresponding formula: % Specify clearly what lemmas you are using. % % !x:nat ?y:nat . y + y = x * (s x) % We will make use of the following lemmas: trans : !u:nat.!v:nat.!w:nat. u = v => v = w => u = w PlusL : !u:nat.!v:nat. u + u * v = u * (s v) DistL : !u:nat.!v:nat.!w:nat. u + w + v + w = u + v + w + w EqL : !u:nat.!v:nat.!w:nat. u = v => w + u = w + v Proof by induction on x. Case : x = 0 by eq0 : 0 = 0 by exI [0/y] : 0 + 0 = 0 * (s 0) to show : ?y:nat . y + y = 0 * (s 0) Case : x = s x' by IH : ?y:nat. y + y = x' * (s x') by exE : y + y = x' * (s x') by eqL [y+y/u, (s x') + (s x')/v, x' * (s x')/w] y + y = x' * (s x') => (s x') + (s x') + y + y = (s x') + (s x') + x' * (s x') by impE : (s x') + (s x') + y + y = (s x') + (s x') + x' * (s x') by DistL [s x'/u, s x'/v, y/w] s x' + y + s x' + y = s x' + s x' + y + y by trans [s x' + y + s x' + y/u, s x' + s x' + y + y/v, (s x') + (s x') + x' * (s x') / w] s x' + y + s x' + y = s x' + s x' + y + y => (s x') + (s x') + y + y = (s x') + (s x') + x' * (s x') => s x' + y + s x' + y = (s x') + (s x') + x' * (s x') by impE (twice) s x' + y + s x' + y = (s x') + (s x') + x' * (s x') by def. of plus s x' + y + s x' + y = (s x') + (s x') * (s x') by plusL [s x'/u, s x'/v] : (s x') + (s x') * (s x') = (s x') * (s s x') by trans : [s x' + y + s x' + y /u, (s x') + (s x') * (s x') /v, (s x') * (s s x') /w] s x' + y + s x' + y = (s x') + (s x') * (s x') => (s x') + (s x') * (s x') = (s x') * (s s x') => s x' + y + s x' + y = (s x') * (s s x') by impE (twice): s x' + y + s x' + y = (s x') * (s s x') by exI [s x' + y/ y] ?y:nat. y + y = (s x') * (s s x') % % 2. Give a proof term corresponding to your informal proof from part 1. % Also give an equational specification of the term. % fn x => rec x of f 0 => (0, eq0) | f (s x') => let (y, ih) = f x' in (s x' + y, trans (s x' + y + s x' + y) ((s x') + (s x') * (s x')) ((s x') * (s s x')) (trans (s x' + y + s x' + y) (s x' + s x' + y + y) ((s x') + (s x') + x' * (s x')) (distL (s x') (s x') y) (eqL (y+y) ((s x') + (s x')) (x' * s x') ih)) (plusL (s x') (s x'))) end Specification: even 0 = (0, eq0) even (s x') = (s x' + y, trans (s x' + y + s x' + y) ((s x') + (s x') * (s x')) ((s x') * (s s x')) (trans (s x' + y + s x' + y) (s x' + s x' + y + y) ((s x') + (s x') + x' * (s x')) (distL (s x') (s x') y) (eqL (y+y) ((s x') + (s x')) (x' * s x') ih)) (plusL (s x') (s x'))) % % 3. Now bracket irrelevant parts of the proof term, % according to the following bracketing of the proposition: % % !x:nat ?y:nat . [y + y = x * (s x)] % fn x => rec x of f 0 => (0, [eq0]) | f (s x') => let (y, [ih]) = f x' in (s x' + y, [trans (s x' + y + s x' + y) ((s x') + (s x') * (s x')) ((s x') * (s s x')) (trans (s x' + y + s x' + y) (s x' + s x' + y + y) ((s x') + (s x') + x' * (s x')) (distL (s x') (s x') y) (eqL (y+y) ((s x') + (s x')) (x' * s x') [ih])) (plusL (s x') (s x'))]) end the version where we leave out the actual instantiations used for the lemmas: fn x => rec x of f 0 => (0, [eq0]) | f (s x') => let (y, [ih]) = f x' in (s x' + y, [trans (trans distL (eqL [ih])) plusL]) end % % 4. Convert the bracketed formula in part 3 into a type, and simplify it. % Also simplify the bracketed proof term, to arrive at a recursive function % of the corresponding type. % even' : nat -> (nat + 1) fn x => rec x of f 0 => 0 | f (s x') => (s x') + (fst (f x')) end % % 5. Consider the function in part 4, extracted from the proof in part 2. % What does it compute? Give an equational specification for it. % % even' 0 = 0 even' (s x') = x' * (s x') / 2 Thus even'(n) is the sum of the first n natural numbers. %%%