Notes on learning Lean (3/?)

Now that I'm done writing and defending my thesis (and submitting the associated paper to a journal), I can dive back into Lean full time (for the next few months at least). I just wrapped up Chapter 5 of MIL, and the final theorem of the chapter, namely the fact that there are infinitely many primes that are equal to \(3\) mod \(4\) was a fun one to formalize: and used an inductive type I had not encountered yet, namely Finsets. This chapter also featured the first use of strong induction on Nat, which modifies the induction tactic to use strong induction.

Working with Finset also led down to the rabbit hole of constructive vs. classical logic. To filter a Finset with some predicate (i.e. a Prop) P, the the predicate has to be in the DecidablePred typeclass. This would make working with Finsets of real numbers quite annoying, since inequalities involving real numbers are not decidable (or semi-decidable, whatever that may mean). Conveniently, one can convince the Lean compiler to work in classical logic, instead of constructive logic, by opening the Classical namespace. I suppose this namespace has the law of excluded middle (or some equivalent notion) as an axiom, which makes all Prop decidable, and makes it possible once again to work with finite sets of reals. This article by Jeremy Avigad on classical vs constructive logic was a fun read.

Going on a tangent, and thinking about Lean as a programming language, I noticed that some of the more general tactics make it seem like tactics form a monad: namely repeat, and <;> which sequences two tactics, as well as some others. Another analogy is how we start a tactic proof using the by keyword, very much like the do notation in Haskell. It makes sense, since a tactic takes the current proof "state", and applies some operation on it to give a new proof "state". Chapter 5 of PIL confirms this observation. I am quite pleased to have identified a familiar monad in a new programming language.

Some more tactics

• contradiction: Closes the current goal if there are contradictory or (decidably) false hypothesis in the environment.
• by_contra h: If the goal is p, it introduces a hypothesis h : \not p, and changes the current goal to False.
• repeat': Similar to repeat, but runs the tactic on the newly produced goals as well, perhaps? The documentation online is somewhat sparse.
• t1 <;> t2: This runs the tactic t1 on the main goal, and then t2 on the subsequent goals.
• push_neg at h: If h has type \not a \leq b, it creates a new hypothesis h with type a > b, and so on.
• interval_cases x : a: Creates cases for x if the x is a natural or an integer, assuming it can find in the ambient hypotheses upper and lower bounds for x. If so, it splits into cases for each possible value of x. I should try and see if there's a variant of this tactic that splits up cases into sub-intervals.
• strong_induction_on: Modifies the induction' tactic to use strong induction instead.
• refine and refine' are generalizations of exact and apply, where you can provide some of the arguments, and it will turn the missing arguments into new goals. More specifically, if you are trying to construct an object of a dependent type, it will let you plug in the pieces you already have.
• ext tactic: The ext tactic applies “extensionality lemmas”. An extensionality lemma says “two things are the same if they are built from the same stuff”. In practice so far, this came up when I was trying to show two sets A and B are equal: calling ext x gave me two cases to deal with: it gave me an x \in A, and the goal was to show x \in B, and second case was the other way around.
• tauto and tauto!: These were useful in dealing with goals that were tautologically true, at least the set-theoretic ones, and these tactics closed them immediately. I need to figure out what contexts do these tactics work in.
• decide: This tactic is useful if the goal is something that Lean has an algorithm to decide: e.g. equality of Nat, primality of Nat, etc.
• let and set: This lets us define new variables in a tactic proof. The set variant will also rewrite all of the ambient hypotheses to use the new variable if possible.
• revert: This is intro backwards.
• by_cases h: This creates two new subgoals, one which assumes h, and one which assumes \not h. This requires that h be decidable (but if we are working with classical logic, this is moot).
• tidy: This is a meta tactic that helps you find the right tactics to solve the goal. Not sure how useful this is in the mathlib context.
• norm-num: If the goal is an arithmetic expression involving the 4 standard operators, equality, and inequalities, this will reduce the expression to a normal form, which is then decidable.

Reading

• On how schemes were formalized, and the perils of universal properties.

Other small notes

• There is a possibly a typo in Section 5.3 (as of 05/09/2024): the line about dsimp is probably stale.