%%% 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
%
% B. !k: t-list .!l: t-list . !m: t-list .
% rev (rev k l) m = rev l (app k 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 .
%
%
% 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.)
%
% B. Use finite types to define the type DATE , the terms of which have the form
%
% >
%
% 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.
%
%%%