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


%%%