%%% Assignment 10
%%% Out: Mon 3 Dec
%%% Due: Mon 10 Dec 
%
% This assignment is to be submitted on paper.
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% 1. Structural Induction on Lists.
%
% Prove the following propositions using structural induction.
% In each case, give an informal proof and then a proof term.
% You may make use of lemmas already proved.
%
% A. !l: t-list .!k: t-list . l = k => k = l
%
the rules given in the notes are not strong
enough to prove symmetry. We assume the following two elimination
rules:

x::l = y::l'     x::l = y::l'
------------    ---------------
 x=y                l = l'


and


x = y     t = t'
-----------------
x::t = y::t'

Proof by structural induction on l:

Case : l = nil
 Sub-Case: k = nil
       to show : nil = nil => nil = nil
       by impI and eq0

 Sub-Case: k = h::t
       to show : nil = h::t => h::t = nil
       by impI and eqEnc

Case l = h'::t' 
 Sub-Case : k = nil
       to show : h'::t' = nil => nil = h'::t'
       by impI and eqEnc

 Sub-Case : k = h::t
     to show: h'::t' = h::t => h::t = h'::t'
            u : h'::t' = h::t     
     by elimR : h' = h
     by sym  : h = h'
                t = t'
     by IH      t' = t => t = t'
     by impE : t = t'
     by eqLI : h::t = h'::t'
     by impI(u) : h'::t' = h::t => h::t = h'::t'


% B.  !k: t-list .!l: t-list . !m: t-list .
%        rev (rev k l) m = rev l (app k m)
%  
Induction on k:

Case : k = nil
  to show :  rev (rev nil l ) m = rev l (app nil m)
  by def of rev and app : 
             rev l m = rev l m
  by refl

Case : k = h::t

  by IH: 
       !l:t-list.!m:t-list.rev (rev t l) m = rev l (app t m)
  by forallE: [h::l/l, m/m] : 
       rev (rev t (h::l) m = rev (h::l) (app t m)
  by def of rev and app : 
       rev (rev t (h::l) m = rev (h::l) (app t m)
  forallI(twice) : 
       rev (rev (h::t) l) m = rev l (app (h::t) m)
  to show : 
       !l:t-list.!m:t-list.rev (rev (h::t) l) m = rev l (app (h::t) m)
  

%
% 2. Generalizing the Induction Hypothesis.
%
% Using previously proved problems and lemmas,
% give a formal proof of the following:
%
%  !l: t-list . reverse(reverse l) = l .

we need to prove : 
 !l: t-list . rev (rev l nil) nil = l.

by lemma A : 
rev (rev l nil) nil = rev nil (app l nil) 

by applying the app and rev definition: 
rev (rev l nil) nil = rev nil l
rev (rev l nil) nil = l

%
%
% 3. Dependent Types.
%
% A. The finite types n: nat |- nat(n) are to represent the types
%  of natural numbers x such that  x < n .
%  Give introduction and elimination rules, and reductions, for these types.
%  (Hint: use n different introduction rules and one elimination rule
%  with an n-fold case construct.)

                      G |- m : nat n
-------------------  --------------------
G |- 0 : nat (s n)    G |- s m : nat (s n)


G |- m : nat(n)
G |- t0 : sigma(s n', 0)
G, n': nat, m':nat(n'), f(n',m') : sigma(n',m') |- sigma(s n', s m')
---------------------------------------------------------------------
G |- rec m of f(s n', 0) => t0 | f (s n', s m') => tm end : sigma(n,m)

%
% B. Use finite types to define the type DATE , the terms of which have the form
%  
%    <year,<month, day>> 
%
%  where years are natural numbers, months are numbers between 1 and 12,
%  and days are numbers between 1 and the number of days in the respective month.
%  For this, assume that you have a function
%
%    days : YEARS x MONTHS -> nat 
% 
%  that gives the number of days in a given month, taking account of leap years.
%
% C. Define a function,
%
%    nextweek : DATE -> DATE
%
%  that takes each particular date to the one that is one week hence.
%
%
%  3. More Dependent Types.
%
%  Use dependent sum and product types to implement binary product and function types.
%  Specifically, define the latter, and their associated terms, in terms of the former,
%  and verify the corresponding introduction and elimination rules.
% 
%  Specifically, define (A x B) = (Sum a:A . B) and (A -> B) = (Product a:A . B),
%  where B does not depend on A.




   G, a:A |-  M : B                    G |- M : Product a:A.B      G |- N : A
-------------------------------       ----------------------------------------
G |- lam a:A. M : Product a:A.B              G |- M N : B



G |- M : A         G |- N : B       G |- M : Sum a:A . B    G |- M : Sum a:A . B  
------------------------------     -----------------------  ---------------------
G |- <M,N> : Sum a:A. B             G |- fst M : A          G |- snd M : B



%  
%%%