# Ideas for Logical Verification 2019–2020

Let us use _LoVe_ as the abbreviation, and _LoVers_ (pronounced "Lofers" in true Dutch style) for the students (or _LoVebirds_?).


## Tactic cemetery

    split
    left
    right
    injection(s?) (?)

  * * *

    norm_num
    linarith

  * * *

    refine
    suffices
    change [at]?
    simpa
    cc
    congr
    convert (also for debugging)
      and conv, see https://github.com/leanprover-community/mathlib/blob/master/docs/extras/conv.md
    tidy
      and tidy?  (debugging)
    squeeze_simp (debugging)
    assoc_rw


## Lecture Notes

Create a 150-or-so-page book called

    Logical Verification in Lean

that will serve as lecture notes. The book should have 13 chapters following the first 13 lectures below. Authorship: perhaps

    AB, JCB, JH, RYL

Things to mention:

  * sporty attitude

  * series of cliffs

  * at the end of course: know the basics and are in a position to formalize anything (with the proper mentor or local expertise; see also Zulip)

Most of the examples in the book would be quoted from `loveXX_YYY_demo.lean`, using some preprocessor trick (similar to `qdoc`'s quoting commands).

Go through the exams and explain things student got wrong better.


## Exercises

We should get proper lecture rooms instead of the computer labs. We would answer questions during the first half and solve the problems together during the second half.


## Homework

Check if it is possible to count the homework for e.g. 20% of the final grade, and enforce the deadlines. Or make it optional.


## Lean Setup

* Keep using Lean 3.4.1

* Require `mathlib` all along (and `elan`)

* Provide our own instructions for installation

* Provide a basic library with some convenience, including
  * a proper `cases` tactic
  * a `find_theorem` command
  * a `solve_direct` command
  * some kind of basic Lean Hammer?
  * some kind of Nunchaku?
  * some kind of predicate compiler?


## Files Associated with the Course

These files would be stored in a `git` repository, which students could clone and update (instead of downloading the files one by one from a web site). The files would appear gradually in the repository.

* `love_lib.lean`: basic library imported by all other `.lean` files

For each lecture (where `XX` = `01` to `14`):

* `loveXX_YYY_lecture.md`: the "slides"

* [`loveXX_YYY_lib.lean`: when appropriate, contains some boring lecture-specific material]

* `loveXX_YYY_demo.lean`: the demo that accompanies the lecture

* `loveXX_YYY_exercise.lean`: group exercises (master file)

* `loveXX_YYY_homework.lean`: homework (master file)

From each master files, two files will be generated, e.g.,

* `loveXX_YYY_exercise_sheet.lean`

* `loveXX_YYY_exercise_solution.lean`

Each file would live in its own namespace, with the same name as the file (e.g., `love01_demo`).


## Plan

### 1. Definitions and Lemma Statements

Keep roughly the same as lecture 1.1 from 2018–2019, but kick structures out (leave them for lecture 4). Spend more time on the inductive definitions and basic functional programming material (moving it from 2.1), including the correspondence with Java and C.

### 2. Tactical Proofs

Bring together all the tactical proof material from lectures 1.2 and 1.3, including intro and elim rules for the connectives. Describe more `simp` features, e.g. the ability to work on premises. Introduce more commands for working comfortably with hypotheses (e.g. for trimming needless hypotheses).

### 3. Type Theory, Proof Terms, and Structured Proofs

Similar with lecture 1.3, but with less focus on tactical proofs and more on proof terms and structured proofs. Cleanly distinguish between the three proof styles, and show how they can be translated into each other. Explain clearly that everything is a proof term ultimately (and explain how to view them).

Exploiting Curry–Howard, even show how we can define a program using tactics?

### 4. Functional Programming

Cover not only lists here (lecture 2.1) but also trees (lecture 2.2). No inductive predicates yet, though.

Mention a few basic things about efficiency:

  * cons `::` versus append `@`

  * tail-recursion, accumulators

The induction tactic, and its connection to pattern matching, should be introduced properly here.

Give some instructions on how to choose the induction principle.

Dependently typed functional programming would seem to belong here. E.g. a precondition on a function (as in `huffman`).

Explain how to perform inductions following a well-founded function definition.

Put some focus on basic arithmetic reasoning (needed e.g. for the well-founded proofs).

Nested and mutual inductive definitions and proofs.

Explain induction intuitively as a program printing a proof with input _n_. Then explain this is exactly how it works in Lean (and also elsewhere, e.g. Dafny).

Explain how to perform equational proofs "lhs = rhs" by simpifying both sides (instead of switching into reverse in the middle of the proof). Get some inspiration from Info2 course at TUM for examples.

Have an example with if and only if (e.g. question 2b of final exam of 2018) and show that it is a bad idea to perform a knee-jerk `iff.intro`. Quote Dijkstra and Knuth ("unity where there is unity").

### 5. Logic Programming

Inductive predicates appear here. Show how to reason about them, including elimination, induction, etc. Transitive closure and its variants should be introduced here and drilled into the students' heads.

Dependent type matching should also be introduced properly here, but we should point out that `cases` can be used instead (in the context of the course).

Mention lack of executability as a major disadvantage.

Spend more time on the (reflexive) transitive closure etc. and on induction (cf. the final exam of 2018).

### 6. Monads

Roughly like lecture 2.3.

### 7. Metaprogramming

Roughly like lecture 2.4, but with much more information upfront in the course and a rich `love07_demo.lean` file with more examples.

### 8. Logical Foundations of Mathematics

Like lecture 4.1.

### 9. Algebraic and Order Structures

Like lecture 4.2 but extended with order/lattices.

### 10. Operational Semantics

Rougly like lecture 3.1.

And how about a functional big-step semantics? How is that different from a denotational semantics?

Show some paper proofs and some diagrams to keep one's sanity. Emphasize that there is a time for mindless proofs and a time for mindfull proofs.

### 11. Hoare Logic

Roughly like lecture 3.2. Put more focus on total correctness.

Give some heuristics for coming up with loop invariants.

Total correctness: define it properly so it also works with nondetermistic languages.

Put more examples in `love10_demo.lean`.

Explain much better forward, backward, etc., rules, and VCG.

Show how to derive new rules for new language constructs (e.g. `do while`).

### 12. Denotational Semantics

Based on lecture 3.3, but do the relational denotational semantics using an inductive predicate like the transitive closure instead of the complicated `lfp` construction. Move `lfp` to the end.

Using the saved time, do a functional (?) denotational semantics, following Nipkow & Klein, and/or using clocks/fuel? Get inspiration from final exam from 2018.

### 13. Rationals and Reals

Like lecture 4.3.

### 14. _p_-Adic Numbers

Like lecture 4.4, with a special guest speaker (RYL) if possible. Coincides with project.

We include _p_-adic numbers directly in the book, and add Rob Lewis as coauthor.


## Random Notes

TODO: if and only if, two directions, not always a good idea.

Backward proof development, with sorrys. Advantage: focus on main thing, see
what's needed. Disadvantage: What if a sorry isn't provable?
