Periods at the end of statements

Stream: Berkeley Lean Seminar

[Kyle Miller]

It appears periods terminate statements in Lean (though I can't find this in the documentation). As was mentioned on Friday, periods apparently help keep Lean from re-evaluating things before what you're currently editing, and it appears this is because it prevents the stuff you're editing from being interpreted as arguments to the previous expression.

[Utensil Song]

See also @Mario Carneiro 's answer here: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Natural.20Numbers.20Game/near/199965171

[Utensil Song]

no doc I found explains the . in the following while I once noticed this in Zulip that's also part of the equation compiler:

example (n : ℕ) : nat.succ n ≠ 0.

That's an empty match
because nat.succ n and 0 are distinct constructors, when you pattern match rfl against the equality, you find there are no cases to handle, and so an empty proof works
Note that the equation compiler sees that goal as \forall (h : nat.succ n = 0), false and effectively does | rfl := <wait a minute, this doesn't typecheck>
from a foundational POV, it's totally a circular proof, we are proving that succ is not zero by appeal to the fact that the equation compiler knows that succ is not zero because it proved it somewhere internally
There are 0 cases, they are obviously mutually exclusive, and they are collectively exhaustive because there are no valid cases

[Kyle Miller]

@Utensil Song If I'm reading lean/src/frontends/lean/definition_cmds.cpp correctly, a period indicates the end of a definition (in particular, that a definition has no more "equations", which are the | ... := ... lines, or a single := ... line). The equation compiler knows some stuff about injectivity so that it can, in general, effectively convert pattern matching into the underlying functions for the inductive type and reason about when the equations are exhaustive. It knows you've exhaustively considered all cases with that example, so it is happy with having no equations in the lemma's definition.

The equation compiler generates this term-mode proof:

example (n : ℕ) : n.succ = 0 → false :=
λ (n : ℕ) (a : n.succ = 0), a.dcases_on (λ (a_1 : 0 = n.succ), nat.no_confusion a_1) (eq.refl 0) (heq.refl a)

It seems roughly similar to the term-mode proof that the equation compiler generates from this:

example (n : ℕ) : nat.succ n = 0 → false
| h := begin
  injection h,
end

You can do something similar with match syntax, which doesn't need the period notation since it has an explicit end token. The equation compiler needs no cases in this match because it knows there can't have been an h:

example (n : ℕ) (h : nat.succ n = 0) : false := match h with end

Also, note that it was important that the example have the nat.succ n after the colon, since that's the thing that is being pattern matched in the equations. The following does not work at all:

example (n : ℕ) (h : nat.succ n = 0) : false.

The following does work, giving both n and the proof of nat.succ n = 0 as things to be pattern matched in the equations:

example : ∀ (n : ℕ), nat.succ n = 0 → false.

[Kyle Miller]

@Utensil Song An example of something the equation compiler is able to deal with (that I was pleasantly surprised about when I'd tried it) is

def from_vector {α : Type*} : vector α 2 → α × α
| ⟨[a, b], h⟩ := (a, b)

Recall that a vector is a list along with a proof that the list has a particular length. The equation compiler works out that since h proves the length is 2, then this single equation exhausts the cases. (I could explicitly indicate there are no more equations with a period if I wanted to, I suppose.)

The definition the equation compiler generates is actually rather lengthy.

[Utensil Song]

How do you print the definition generated by the equation compiler?

[Kyle Miller]

@Utensil Song You use the #print command. Like #print from_vector. With the examples, I had to change them to lemmas and give them names to be able to print them.

[Kyle Miller]

This is also how you can see the definitions that tactic mode generates. Sometimes there are sub-definitions these generate, like foo._proof_1, that you might need to #print out as well.

[Utensil Song]

Sorry I was away from computers. Thank you for the detailed and illuminating explanations.

Previously I thought the period is a special structure for expressing no case to the equation compiler, but it's actually general for saying "the definition ends here" and the empty match is just one of its applications. Your answer also demonstrated what Lean has inferred utilizing this hint, how it works, and its limitations, it also gave me the toolkit to explore on my own. It's really a great answer! :heart:

[Utensil Song]

How do you print the definition generated by the equation compiler?

[Kevin Buzzard]

#print