10.00–10.50 Monday (lecture)
11.10–12.00 Monday (tutorial)
10.00–10.50 Thursday (lecture)
11.10–12.00 Thursday (tutorial)
10.00–10.50 Friday (lecture)
11.10–12.00 Friday (tutorial)
All lectures and tutorials in AT 5.08.
Note: Lectures begin Monday of Week 1.
Coursework is worth 25% of your mark. There are five coursework assignments, each worth 5%.
For each assignment you will be given a list of exercises to
complete in the textbook. Copy the relevant files and fill in your
answers. Include a comment at the beginning, listing your
name and which exercises you completed. Mark every
completed exercise by writing (* !!! *)
just before
it. E-mail your files to the instructor. Send all relevant
files: .v, .vo, and .glob. Please ensure your files execute correctly
under Coq!
Some exercises are labeled 'stretch'. These are optional exercises for students who wish an additional challenge.
Note: The coursework is not a light load! But everyone who does the work gets perfect on the exam. (Literally. 100%. That's what proof is for.)
Basics.v
):
factorial
blt_nat
, defined in terms of previously given functions.
blt_nat'
, this time defined directly using recursion.
andb_eq_orb
binary
(stretch)
Induction.v
):
double_plus
Theorem plus_swap : forall m n p, n + (m + p) = m + (n + p).
(Hint: this requires only plus_assoc
and plus_comm
.)
Theorem mult_S_r : forall m n, m * S n = m + (m * n).
Theorem mult_comm : forall m n, m * n = n * m.
Theorem beq_nat_refl : forall n, beq_nat n n = true.
binary
, prove
Theorem binary_comm : forall b, bin_to_nat (incr b) = S (bin_to_nat b).
(stretch)
Lists.v
):
list_funs
list_exercises
update_eq
(stretch)
update_neq
(stretch)
Poly.v
):
poly_exercises
: app_length
more_poly_exercises
fold_length
Tactics.v
):
beq_nat_true
beq_nat_sym
beq_nat_trans
(stretch)
forall_exists_challenge
(stretch)
Logic.v
):
contrapositive
not_both_true_and_false
or_distributes_over_and
dist_not_exists
not_exists_dist
(stretch)
classical_axioms
(stretch)
IndProp.v
):
le_exercises
, first five theorems:
le_trans
O_le_n
n_le_m__Sn_le_Sm
Sn_le_Sm__n_le_m
le_plus_l
palindromes
(stretch)
Maps.v
):
t_update_shadow
t_update_permute
(stretch)
Imp.v
).
ceval_example2
extend_repeat
REPEAT c UNTIL b END
c ;; WHILE ~b DO c END
~b
is the logical negation
of b
. Put the copy in a nested module called
extend_repeat
, so that
you can reuse all the constructor names.
bevalR
no_whiles_terminating
stack_compiler
(stretch)
stack_compiler_correct
(stretch) -->
Equiv.v
):
swap_if_branches
assign_aequiv
CIf_congruence
fold_constants_com_sound
(stretch)
Hoare.v
):
swap_exercise
hoare_repeat
REPEAT
construct introduced earlier.
{{P}}c{{Q}} Q /\ ~b ->> P
-------------------------------------
{{P}}REPEAT b UNTIL c END{{Q /\ b}}
Hoare2.v
)
factorial
factorial_dec
(stretch)
Smallstep.v
):
eval__multistep
step__eval
(stretch)
multistep__eval
(stretch)
par_body_n__Sn
par_body_n
(stretch)
Types.v
)
Stlc.v
):
step_example5
typing_example2_full
StlcProp.v
):
types_unique
(stretch)
progress_preservation_statement
MoreStlc.v
):
halve_fix
STLC_extensions
, you can write it out formally.
STLC_extensions
You are provided with the implementations for
T ::= ... | Empty
t ::= ... | case t of {}
t ==> t'
--------------------------------
case t of {} ==> case t' of {}
Gamma |- t : Empty
-------------------------
Gamma |- case t of {} : T
Admitted
in any lemmas or theorems on which you depend.
In particular, for STLC_extensions you will need to complete the following:
Typechecking.v
):
typechecker_extensions
(stretch)STLC_extensions
.
Please remember the University requirement as regards all assessed work. Details about this can be found at:
Furthermore, you are required to take reasonable measures to protect your assessed work from unauthorised access. For example, if you put any such work on a public repository then you must set access permissions appropriately (generally permitting access only to yourself, or your group in the case of group practicals).
Induction.v
):
Basics.v
to Basics.vo
induction
, proof by cases destruct
plus_n_O
plus_n_Sm
plus_comm
plus_assoc
Induction.v
):
double_plus
Theorem plus_swap : forall m n p, n + (m + p) = m + (n + p).
(Hint: this requires only plus_assoc
and plus_comm
.)
Theorem mult_S_r : forall m n, m * S n = m + (m * n).
Theorem mult_comm : forall m n, m * n = n * m.
Tactics.v
):
inversion
double_injective
generalise dependent
Logic.v
):
intro
, elim apply
split
, elim destruct H as [HA HB]
left
, right
, elim destruct H as [HA|HB]
I
, elim not possible.
destruct H as []
or exfalso
unfold
and then as for implication
PaT.v
.
Imp.v
):
ceval_example2
extend_repeat
REPEAT c UNTIL b END
c ;; WHILE ~b DO c END
~b
is the logical negation
of b
. Put the copy in a nested module
called extend_repeat
, so that
you can reuse all the constructor names.
bevalR
no_whiles_terminating
stack_compiler
(stretch)
stack_compiler_correct
(stretch)
Equiv.v
):
eapply
works.
See "Digression: The eapply Tactic" in the next chapter.
aequiv
, bequiv
, cequiv
skip_left
, IFB_true
, WHILE_true_nonterm
functional_extensionality
CWhile_congruence
Hoare.v
):
Assertion
, hoare_triple
,
valid_triples
, hoare_post_true
assn_sub
, hoare_asgn
assert_implies
, hoare_consequence
hoare_skip
hoare_seq
bassn
, hoare_if
hoare_while
Example better_assn_example :
{{fun st => st X <= 4}}
(X ::= (APlus (AId X) (ANum 1)))
{{fun st => st X <= 5}}.
Proof.
eapply hoare_consequence_pre.
apply hoare_asgn.
unfold assn_sub. simpl.
unfold t_update. simpl.
unfold assert_implies. intro st.
omega.
Qed.
Church.v
):
(λx.N) M = N[x := M]
λx.L x = L
(if x
not free in L
)
zero = λs. λz. z
one = λs. λz. s z
two = λs. λz. s (s z)
three = λs. λz. s (s (s z))
succ = λn. λs. λz. s (n s z)
plus = λm. λn. λs. λz. m s (n s z)
times = λm. λn. m (plus n) zero
plus' = λm. λn. m succ n
times' = λm. λn. m (plus' n) zero
true = λt. λf. t
false = λt. λf. f
not = λb. λt. λf. b f t
and = λa. λb. λt. λf. a (b t f) f
not' = λb. b false true
and' = λa. λb. a b false
isZero = λn. n (λb. false) true
create = λx. λy. λk. k x y
fst = λp. p (λx. λy. x)
snd = λp. p (λx. λy. y)
pred = λn.
fst (n (λp create (snd p) (succ (snd p))) (create zero zero)).
fix = λf. (λx. f (x x)) (λx. f (x x))
factorial = fix (λfact. λn. isZero n one (times n (fact (pred n))))
zero = λs. λz. z
one = λs. λz. s zero
two = λs. λz. s one
three = λs. λz. s two
succ = λn. λs. λz. s n
pred = λn. n (λp. p) zero
plus = fix (λplu. λm. λn. m (λp. succ (plu p n)) n)
times = fix (λtim. λm. λn. m (λp. plus n (tim p n)) zero)
Smallstep.v
):
tm
, eval
, step
relation
, deterministic
value
strong_progress
, nf_same_as_value
multi
, normalising
eval_multistep
astep
, bstep
, cstep
CImp
Smallstep.v
):
par_body_n__Sn
eval__multistep
Stlc.v
):
subst
value
step
has_type
Locate "[ _ := _ ] _".
MoreStlc.v
):
Maps.v
)
Types.v
)
Stlc.v
)
step_example5
MoreStlc.v
):
STLC_extensions
StlcProp.v
):
canonical_forms_bool
,
canonical_forms_fun
progress
appears_free_in
,
free_in_context
context_invariance
substitution_preserves_typing
preservation
The final examination is worth 75% of your mark.
Because you will be working with Coq throughout the course, you should also have access to Coq for the exam. Unlike most courses with a written exam, TSPL has an online exam where you use the Coq proof assistant to assist and confirm your exam work. If anyone has any questions or concerns, please contact the instructor.
The final exam for TSPL is in December 2017
Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, E-mail: school-office@inf.ed.ac.uk Please contact our webadmin with any comments or corrections. Logging and Cookies Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh |