Style

Good style is essential to making both programs and proofs clear and understandable. While it might feel as though your primary objective is simply to type the right sequence of tactics to make Lean close your goal, you'll have an easier time writing and debugging your code, get better and faster help from TAs, and learn more in the process if you take the time to thoughtfully structure your proofs. Remember that one of our motivations for using a proof assistant in this class is that systems like Lean help you see the structure of a proof as it unfolds, and good style will make this structure clearer and easier to follow!

Naming

Identifiers in Lean (variables, theorem names, functions, and the like) must begin with a lower-case or capital letter and can contain most non-whitespace Unicode characters (except for those that are reserved for infix operations: in particular, for those who have a background working in Pyret or Racket, note that the hyphen cannot appear in Lean identifiers). Lean has several identifier naming conventions you'll see throughout this course: "data" declarations, like functions, numbers, and other pieces of named data declared using def, are typically named in camel case (e.g., myGreatNat or addAndSquare), while theorems are written in snake case (e.g., add_two_two_eq_four or mul_comm). Theorem names generally reflect the key operations that appear in the theorem statement: for instance, a theorem proving that k * (m - n) = (k * m) - (k * n) would likely be called mul_sub or mul_sub_eq_mul_sub_mul.

Arguably the most important matter of naming concerns variables introduced into your context in proofs. Always bear in mind the kind of variable you are introducing when you name it. Variables corresponding to values, like natural numbers or integers, should be given names similar to those that you would give such a value in a paper proof (e.g., n or m for natural numbers). Hypotheses, on the other hand, should be given names beginning with h followed by the variables or facts to which they pertain: for instance, the hypothesis m = n would be appropriately named hmn (or, perhaps, heq or hm_eq_n if there were other hypotheses involving m and n). (The one exception to this rule is that inductive hypotheses may be, or begin with, ih.) Keeping track of what's in your context is essential to understanding the flow of a proof and deciding on next steps, and clear and consistent naming conventions make it substantially easier to understand the values and assumptions you have on hand at a given stage of your proof.

Another important naming guideline is to avoid shadowing. Shadowing occurs when you introduce a variable or hypothesis with the same name as one that already exists. When this happens, the first variable or hypothesis becomes inaccessible—you'll no longer be able to refer to it by name (although tactics like assumption will still be able to find it). When a name has been shadowed, the original variable/hypothesis will display with a dagger symbol (✝) next to its name in your context.

Note that these naming rules apply whenever you're introducing names into your context, regardless of the tactic being used. In addition to assume, tactics like fix, have, and eliminate also allow you to specify names to add to your context.

Goal Management

While every proof starts with a single goal, many tactics will lead to the creation of additional goals over the course of your proof. (split_goal, for instance, is such a tactic, along with most induction tactics, eliminate when applied to a disjunction, and have when used without the := syntax.) By default, when new goals are generated, they appear sequentially in your Infoview, though any tactics you use will only affect the topmost goal in the list. This can lead to clutter and confusion; therefore, to keep your work organized, you should always focus the goal on which you're actively working using the { } syntax. (In general, any tactic that generates multiple goals should immediately be followed by braces.) This also makes it much clearer to someone reading your code (including you!) which tactics are applying to which goal. For instance, in the following example, it's very difficult to tell when we stop working on one goal and start working on another, and how all the exacts and split_goals fit together:

/- This is bad! Don't do this! -/
theorem and_and_swap (p q : Prop) : p ∧ q → q ∧ p ∧ p := by
  assume hpq
  eliminate hpq with hp hq
  split_goal
  assumption
  split_goal
  assumption
  assumption
  done

But by using braces to focus individual sub-goals, the structure of the proof becomes clearer:

/- Do this instead! -/
theorem and_and_swap (p q : Prop) : p ∧ q → q ∧ q ∧ p := by
  assume hpq
  eliminate hpq with hp hq
  split_goal
  {
    assumption
  }
  {
    split_goal
    {
      assumption
    }
    {
      assumption
    }
  }
  done

Note that you may sometimes see us omit the line breaks after the opening brace and before the closing brace, so that

{
  split_goal
  {
    assumption
  }
  {
    assumption
  }
}

would become

{ split_goal
  { assumption }
  { assumption } }

This makes for cleaner-looking demo code on our website, but it causes the Infoview to behave confusingly when you're actually writing a proof. For this reason, we strongly advise including the line breaks when you're using the goal-focusing { } syntax.

Indentation

Lean requires consistent indentation in proofs and within any focused subgoals. If you change indentation levels between successive tactic lines, your proof will likely fail. The error messages caused by indentation issues can be confusing, so be careful about correctly indenting your lines!

Here are some examples of incorrect indentation:

/- Don't do this! -/
theorem implies_self (p : Prop) : p → p  := by
  assume hp  -- A confusing error message about the goal not being an implication (even though it is!) appears on this line
    assumption  -- This line is incorrctly indented
  done

/- Don't do this! -/
theorem and_swap (p q : Prop) : p → p ∧ (p ∨ q) := by
  assume hp
  split_goal
  {
    assumption
  }
  -- An error appears here about an "unexpected identifier"
  {
    left
      assumption  -- This line is incorrectly indented
  }
  done