%%% 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,
we need to assume there is a symmetric equality on type t.
We then assume the following two elimination rules:

x::l = y::l'         x::l = y::l'
------------elimL    ---------------elimR
 x=y                    l = l'

and the introduction rule:

x = y     t = t'
-----------------eqLI
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'
     assume u : h'::t' = h::t     
     by elimR : h' = h
     by sym on t : h = h'
     by elimL: 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 B : 
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.)

Option 1 (weak):

Introduction:
                     
------------------- nat(sn)I_0
G |- 0_sn : nat(sn)   

                     
------------------- nat(sn)I_1
G |- 1_sn : nat(sn)  

...
                     
------------------- nat(sn)I_(n)
G |- n_sn : nat(sn)   


Elimination:

G |- m : nat(sn)
G |- t0 : sigma(sn)
G |- t1 : sigma(sn)
...
G |- tn : sigma(sn)
----------------------------------------------------------------------
G |- case m of 0_sn => t0 |  1_sn => t1 | ... | n_sn => tn end : sigma(sn)


Reduction:

(case m_sn of 0_sn => t0 |  1_sn => t1 | ... | n_sn => tn) ==> t_m


Option 2 (strong):

Introduction:

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


Elimination:

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


Reductions:

(rec 0 of f(sn',0) => t0 | f (sn',sm') => tm end) ==> t0

(rec sm of f(sn',0) => t0 | f (sn',sm') => tm end) ==> tm 


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

For convenience, suppose the finite types nat(n) run from 1 to n
(rather than 0 to n-1).

Let:

YEAR = nat
MONTH = nat(12)
days : YEARS => MONTHS => nat 
DATE(n,m) = nat(days(y,m))

Then:

y: YEAR, m : MONTH |- DATE(y,m) type

% C. Define a function,
%
%    nextweek : DATE -> DATE
%
%  that takes each particular date to the one that is one week hence.
%

Define the "tomorrow" function t , taking a date d: DATE(y,m) to the next one, by:

t : Pi y:YEAR. Pi m:MONTH. DATE(y,m) => Sigma y:YEAR. Sigma m:MONTH. DATE(y,m)

t y m d = if d = days y m
          then if m = 12
               then <sy,<1,1>>
               else <y,<sm,1>>
          else <y,<m,sd>>

here sn is the usual successor on YEARS,
and is defined in the obvious way on finite types.

Finally, let

nextweek d = t(t(t(t(t(t(t(d)))))))

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

As suggested, if B does not depend on A, put:

(A x B) = (Sigma x:A . B
(A => B) = (Pi x:A . B)

For terms, put:

fst p = let <u,v> = p in u
snd p = let <u,v> = p in v

and use the same notation for the terms:

<a,b>
fa
lam x.b

This gives the required rules:

G |- a : A         G |- b : B       G |- p : A x B          G |- p : A x B 
------------------------------     -----------------------  ---------------------
G |- <a,b> : A x B                  G |- fst p : A          G |- snd p : B


G, x:A |-  b : B                    G |- f : A => B      G |- a : A
-------------------------------    ----------------------------------------
G |- lam x. b : A => B              G |- fa : B

These can be verified using the rules for dependent types.

%  
%%%