%%% 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 % % > % % 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 > else > else > 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 = p in u snd p = let = p in v and use the same notation for the terms: 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 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. % %%%