Agda,
a beautiful proof assistant

second part of the course teoria dei tipi • begin April 22th, 2022 • by Ingo Blechschmidt

Welcome to our joint course on Agda. :-)

Agda is a programming language. But Agda is much more than that: Agda is also a proof language. We can write up mathematical proofs in Agda, even proofs concerning infinite or uncomputable objects. Furthermore, Agda is not static: Agda is also a proof assistant helping us devise proofs. With Agda, we can …:

• develop proofs and ensure their correctness,
• practically explore type theory
• appreciate mathematics from a new point of view and
• verify the correctness of programs.

I hope you will enjoy the course. Questions and suggestions are always welcome!

via Zoom

Zoom: https://unipd.zoom.us/j/85250849100?pwd=MHo4K0NBb240SjlUWG42ME44bkRLdz09
Meeting ID: 852 5084 9100
Passcode: 123456

Thursdays from 4.30 pm till 6.30 pm (Italian time)
Fridays from 2.30pm till 4.30 pm

Exercise sheets

Suggested exercises and their solutions will be posted here.

• Sheet 1. basic functions with booleans and natural numbers
• Sheet 2. functions with vectors and lists
• Sheet 3. first steps in proving properties of natural numbers
• Sheet 4. equality of functions, numbers, lists and vectors
• Sheet 5. equational reasoning, relations
• Sheet 6. correctness of insertion sort
• Sheet 9. sets as trees
• Sheet 10. termination and well-founded recursion

Transcripts

• Transcript of session 1. Booleans, natural numbers, basic functions
• Transcript of session 2. Partial solutions to exercise sheet 1, vectors, basic functions with vectors
• Transcript of session 3. First steps in proving: even and odd numbers
• Transcript of session 4. First steps in proving: equality of natural numbers
• Transcript of session 5. More on equality of natural numbers; also polymorphic equality
• Transcript of session 7. Correctness of insertion sort
• Transcript of session 9. Sets as trees: introduction to one of the most important models of CZF and to the connection between set theory and type theory
• Transcript of session 10. On termination and well-founded recursion
• Transcript of session 11. Function extensionality, quotients, setoids
• Transcript of session 12. Cubical type theory
• Transcript of session 13. Extracting constructive content from classical proofs (illustrated with Dickson's lemma)

Syllabus

First draft based on earlier Agda workshops. After the basics are cleared, we can explore lots of different tangents. Your input is very much welcome.

1. Agda as a programming language
   • Bool, id, neg, ¬_, and
   • Nat, add2, pred, recursion
   • "types are first-class", "everything has a type"
   • Weird
   • NatList
   • List
   • Vector
2. Agda as a proof language
   • de Morgan
   • relations
   • equality type, zero = zero, neg² = id, function extensionality
   • lemmas about natural numbers
   • general induction
3. Exploring Agda
   • certified sorting
   • sets as trees, Russell's paradox
   • simply typed lambda calculus
   • minima of sets of natural numbers, Higman's Lemma
   • setoids
   • cubical Agda
   • your suggestion here

References

• Programming Language Foundations in Agda (by Wadler, Kokke and Siek)
• Programming and Proving in Agda (by Cockx)
• Introduction to Univalent Foundations of Mathematics with Agda (by Escardó)
• Dependent Types at Work (by Bove and Dybjer)

Contact

mail: iblech@speicherleck.de
phone: +49 176 95110311 (also Telegram)