2.1.1. Syntax🔗

These two definitions specify the abstract syntax of arithmetic and boolean expressions.

In this chapter, we'll ignore the translation from the concrete syntax that a programmer would actually write to these abstract syntax trees -- the process that, for example, would translate the string "1 + 2 * 3" to the AST .plus (.num 1) (.mult (.num 2) (.num 3)).

For comparison, here's a conventional BNF (Backus-Naur Form) grammar defining the same abstract syntax:

Compared to the Lean version above...

• The BNF is more informal -- for example, it gives some suggestions about the surface syntax of expressions (like the fact that the addition operation is written with an infix +) while leaving other aspects of lexical analysis and parsing (like the relative precedence of +, -, and *, the use of parens to group subexpressions, etc.) unspecified. Some additional information -- and human intelligence -- would be required to turn this description into a formal definition, e.g., for implementing a compiler. The Lean version consistently omits all this information and concentrates on the abstract syntax only.

• Conversely, the BNF version is lighter and easier to read. Its informality makes it flexible, a big advantage in situations like discussions at the blackboard, where conveying general ideas is more important than nailing down every detail precisely.

  Indeed, there are dozens of BNF-like notations and people switch freely among them -- usually without bothering to say which kind of BNF they're using, because there is no need to: a rough-and-ready informal understanding is all that's important.

It's good to be comfortable with both sorts of notations: informal ones for communicating between humans and formal ones for carrying out implementations and proofs.

2.1.2. Evaluation🔗

Evaluating an arithmetic expression produces a number.

Similarly, evaluating a boolean expression yields a boolean.

It's worth noting that ≤ and > are Prop-valued, i.e. a₁.eval st ≤ a₂.eval st is a proposition, but Bexp.eval returns a Bool, so Lean implicitly inserts a decide coercion. You can observe the call to decide by hovering over Bexp.eval_le and Bexp.eval_gt.

Aexp.eval (.plus (.num 3) (.minus (.num 4) (.num 1)))

2.1.3. Optimization🔗

We can now start to get some mileage out of these definitions. Suppose we define a function that takes an arithmetic expression and slightly simplifies it, changing every occurrence of 0 + e (i.e., .plus (.num 0) e) into just e.

To gain confidence that our optimization is doing the right thing, we can test it on some examples and see if the output looks OK.

But if we want to be certain the optimization is correct -- that evaluating an optimized expression always gives the same result as the original -- we should prove it!

Here is a first, deliberately explicit, proof, by induction on a. The interesting case is Aexp.plus: because Aexp.optimize0plus treats plus (num 0) e specially, we case-split on the left operand a₁ -- and, when it is a numeral, on whether that numeral is 0 -- to line the proof up with the function's own branches. Once the constructors are exposed, each case is discharged by essentially the same incantation: unfold Aexp.optimize0plus, rewrite Aexp.eval by its characterizing lemmas, then finish with the induction hypotheses. Notice how repetitive that makes the proof.

We can do much better. The case analysis we performed by hand -- peeling plus apart to reach the plus (num 0) e branch -- is exactly the case analysis that Aexp.optimize0plus itself performs.

The fun_induction tactic inducts along a function's own recursion structure: fun_induction Aexp.optimize0plus a hands us one goal per branch of optimize0plus -- the special plus (num 0) e branch included -- so the nested cases disappear.

Before applying fun_induction to a function as complex as Aexp.optimize0plus, let's see how it works on somthing simpler. Recall the definition of Nat.even and Nat.odd:

Normally, if we perform induction on n, we get two cases - 0 and n' + 1 - one for each of the cases in the inductive definition of natural numbers. Functional induction on Nat.even, however, gives us three cases - 0, 1, and n' + 2 - corresponding to each of the cases of its definition.

Now let's try using fun_induction on Aexp.optimize0plus. When we do this, every goal has the same shape, so we can attack them uniformly with the <;> combinator and a single tactic, simp_all, which rewrites Aexp.eval by the @[simp] characterizing lemmas and uses the induction hypotheses -- which it picks up from the local context automatically -- to close each goal. The whole proof collapses to two lines.