Certified Programming with Dependent Types, CAS 763, 2019

• Installing Ubuntu (or other distribution) packages will usually give you old, but matching versions of the standard library.

  You then may need to follow the section “Until Agda-2.4: Setting up the Emacs mode for use with the library” on the Agda standard library page.

• If you follow the instructions linked from the Agda Download page, then you need to install also a matching version (typically the latest version) of the Agda standard library and follow the installation instructions which link to the library management section in the Agda documentation. Read that whole page.
• In any case, be aware that typechecking the standard library normally needs write access to its installation directories.

Get started with the textbook Programming Language Foundations in Agda (PLFA).

Download the source:

git clone https://github.com/plfa/plfa.github.io.git

The files corresponding to the early sections of the book are in the sub-directory src/plfa/part1, see the ``Source'' links at the top of the web pages corresponding to each section.

Work through the first four sections and complete at least all “recommended” exercises: For each section, produce a copy of the source file and complete at least the indicated exercises:

1. Naturals: _^_ (power) and ∸-examples (monus-examples)
2. Induction: +-swap, times-distrib-plus, +-assoc — try also at least *-comm, 0∸n≡0, and ∸-+-assoc
3. Relations: <-trans, trichotomy, and ≤-iff-<

4. Equality: After the repeated proof of commutativity (and the explanations for it), insert a proof for

   +-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
   

   that proceeds by induction on n. (If you get stuck, you may find some inspiration in the proof of +-rearrange in Induction.)

You may remove explanations except for parts about which you insert questions into the document, and except the Exercise descriptions. You are encouraged to insert your own documentation, questions, descriptions of problems you encountered and how you solved them as literate documentation between the code fragments.

Do not remove Agda code!

(The PLFA source files are literate Agda files using MarkDown for the documentation parts; this is one of the acceptable formats for this course. After loading such a *.lagda.md file in Emacs, you may need to manually start M-x agda2-mode to activate the special Emacs mode for Agda, which will also give you an ``Agda'' menu in the Emacs menubar.)