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