CAS 707 ─ Formal Specification Techniques ─ Winter 2018

Exercise 1 continued

Exercise 1.2: Provide natural deduction proofs for:

p ⇒ p ∧ (p ∨ q)
(p ∧ r) ∨ (q ∧ r) ⇒ (p ∨ q) ∧ r
(p ∨ q) ∧ r ⇒ (p ∧ r) ∨ (q ∧ r)
(p ⇒ q) ⇒ p ∨ r ⇒ q ∨ r
∀ x : A • ∃ y : A • x = y

Assignment 1

Please submit the document specified below both as LaTeX source and as PDF to the subversion repository at:

https://websvn.cas.mcmaster.ca/cas707/YourMacID/

in subdirectory A1 by Monday, Jan. 15, morning at 11 a.m..

Assignment 1.1

Continue working through the F* tutorial, at least until section 6 inclusively.

As a log of your activity, produce a LaTeX document that contains (as code listings using the listings package) at least for each exercise in the tutorial the last version of your solution (attempt) before you look at the “exercise answer”.

Document questions and problems, and alternate solutions and solution attempts.

Assignment 1.2

(Make your answers to this part of the same document as above.)

Implement the decision procdure

val isPrefixOf : #a : eqtype -> list a -> list a -> bool

and prove that this is reflexive, transitive, and antisymmetric.

What is the complexity of isPrefixOf?

Can you formulate and prove other useful lemmas about isPrefixOf?