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