CAS 707 ─ Formal Specification Techniques ─ Winter 2018

Exercise 2

Exercise 2.1: Using FStar.Constructive, prove the following:

  • p ⇒ p ∧ (p ∨ q)
  • (p ∧ r) ∨ (q ∧ r) ⇒ (p ∨ q) ∧ r
  • (p ∨ q) ∧ r ⇒ (p ∧ r) ∨ (q ∧ r)
  • (p ⇒ q) ⇒ p ∨ r ⇒ q ∨ r
  • p ⇒ ¬ ¬ p

    ─ Can you prove also the opposite implication?

    ¬ ¬ p ⇒ p

  • ∀ x : A • ∃ y : A • x = y
  • (p ∨ ∀ x : A • q x) ⇒ (∀ x : A • p ∨ q x)
  • (∃ x : A • p x ∧ x = t) ⇔ p t           ─ Challenge!

(See either the F* distribution or our gitlab wiki for the contents of FStar.Constructive.)

Exercise 2.2: List suffixes

Develop material for the suffix relationship between lists, at least analogously to what Assignment 1.2 asked for prefixes.

Exercise 2.3: Suffix relation with decode and showS

Explore using your suffix material to strengthen the types for showsHTree and for Huffman decoding.

Recall:

  • Type for “difference strings” in analogy to ShowS of Haskell: 
type showS = list char -> Tot (list char)
  • Function composition (nicer symbol?) that can be used as O(1) concatenation of the “difference strings” as defined above: 
val (~.) : #a:Type -> #b:Type -> #c:Type -> (b -> c) -> (a -> b) -> (a -> c)
let (~.) #a #b #c g f = fun x -> g (f x)