Skip to content

Home

Jump to bottom
Jeremy Avigad edited this page May 2, 2020 · 14 revisions

Notes

  • There is a start on a TOC below. It can change, but this will let us get started with the writing.

  • We agree: lots of exercises.

  • We need Gabriel and Bryan to provide this functionality in VS Code:

    • try it! button: creates a folder in a hierarchy with a snippet, or open if it is already there
    • show more! button: opens a read-only file We need to come up with a general mechanism to specify where the files go.

  • We need a mechanism for generating stable tags for exercises.

  • The emphasis should be on mathematics rather than logic; we teach students the logic only insofar as they need to do mathematics. But we will use logical terminology and schematic presentation of logical rules when it is helpful.

  • Some sections should focus on basic skills: equational reasoning, proof by induction, etc. Others should be substantial mathematical examples, showing students how to use basic concepts in mathematics and how to write serious proofs.

  • The current site is here.

  • Patrick's tutorial is here.

  • Kevin's Lagrange gist is here, Jeremy's follow up is here.

  • Kevin's propositional exercises are here

  • There are also exercises in TPIL and Logic and Proof.

  • A glossary and a cheat sheet like this one will be helpful.

  • Some sample uses of norm_num and dec_trivial are here.

Ideas for a table of contents

Basic skills

  • equational reasoning
  • universal quantifiers and implication
  • conjunction and negation
  • disjunctions
  • existential quantifiers

(JA: I think I know how to do this now. I'll have a draft soon. I will use examples of proving ring identities and proving general facts from lattice axioms. These are a good way to introduce the basics, they are mathematically interesting, and the information will be useful later on. Also complete lattices: using lubs to define a glb is a good example of something that little more than pure logic.)

Fundamentals

  • sets (union, Union, sUnion, bUnion...)
  • relations (order relations and equivalence relations)
  • functions (injective / surjective, inverses, etc.)
  • finite sets and cardinality (a bit of combinatorics with finsets)
  • the finite (Cantor Bernstein)

Numbers

  • proof by induction
  • there exist infinitely many primes
  • integers, rationals, and reals
  • fighting coercion hell; test case: proving that 1/(n+1) tends to zero (with home brewed limit definition, no filters).

Other ideas: Fibonacci numbers, Catalan numbers, binomial coefficients, irrationality of sqrt 2, sums of four squares, congruences.

Algebra

  • some elementary group theory
  • some specific groups, like the dihedral group?
  • Lagrange (and Euler-Fermat as a corollary)?
  • Cauchy's theorem (if p divides o(G), then G has an element of order p)?
  • First isomorphism theorem?
  • Sensitivity conjecture?
  • linear algebra?
  • lattices and Galois connections

Give background on declaring a structure and extending structures, using notation like * and <.

This is crucial because it is a huge barrier to using mathlib. You cannot do subgroups, ideals, or any topology or analysis without lattices. Galois connections are less necessary to use those theories, but they are crucial for anyone who wants to get even a tiny bit of understanding of how things are set up.

Topology

  • filters
  • topological spaces and metric spaces (with a pinch of uniform spaces). The forgetful inheritance pattern
  • big example: IVT

Calculus

  • derivatives
  • integrals
  • find some nice example that brings everything together
Clone this wiki locally