Close a goal

To solve the goal, so that the goal disappears. To create a term of the type specified by the goal.

Definitional equivalence

To a mathematician, x + 0 = x and 0 + x = x, and these are both thought of as lemmas. However if x : ℕ then the definition of x + 0 is “it’s defined to be x”, and the definition of 0 + x is “it is defined recursively, with 0 + 0 := 0 and 0 + succ x := succ (0 + x), so it is a very easy lemma (proof by induction) that 0 + x = x but it is not true by definition.

Definitional equivalence is a notion in computer science – it is a strong kind of equality, one that you can just prove by looking at definitions of the various functions. The change tactic can be used to change a hypothesis or goal to something definitionally equivalent.

Universe

Types like nat and FLT have types too; these are universes. Examples are Prop and Type. Whilst, strictly speaking, all universes are types, and all types are terms, in practice it’s useful to maintain the distinction between universes, types which are not universes, and terms which are not types.

Propositions

Informally, a proposition is a true-false statement in Lean. Do not confusion a proposition with its proof.

A proposition P is a Type, which lives in the universe called Prop. Because P is a type, it makes sense to talk about terms of type P. A term of type P is called a proof of P.

In the Lean code below we define two propositions, and check that they are in the Prop universe.

try it!

definition P : Prop := 2 + 2 = 4
definition Q : Prop := 2 + 2 = 5

#check P -- P : Prop
#check Q -- Q : Prop

It is impossible to construct a term of type Q – this would be a proof of 2 +2 = 5. However we can construct a term of type P:

try it!

definition P : Prop := 2 + 2 = 4

definition HP : P :=
begin
  refl -- lean magic
end

#check (HP : P)
#check (P : Prop)

Local context

This is the assumptions, also known as hypotheses, which are currently known to Lean – the stuff before the turnstyle and the goal. For example in the following code

try it!

example (P Q : Prop) (HP : P) : P ∨ Q :=
begin
  sorry
end

the tactic state at the sorry is

P Q : Prop,
HP : P
⊢ P ∨ Q

meaning that the local context is

P Q : Prop,
HP : P

and the goal is P ∨ Q.

Turnstyle

Or turnstile. This is the ⊢ symbol in the tactic state which appears just before the goal.

Goal

This is the type (often a proposition) which you are trying to construct a term of (i.e., trying to prove, if the goal is a proposition). There can sometimes be more than one goal, although use of { and } is encouraged to keep the number of goals down to one at any one time. The goal is the type after the ⊢ turnstyle symbol in the tactic state.

Tactic state

The tactic state looks something like this:

P Q : Prop,
HP : P
⊢ P ∨ Q

It consists of our hypotheses (the local context) and, after a turnstyle, the goal or goals. The window containing the tactic state can be opened in VS Code with ctrl-shift-enter (i.e. hold down the Ctrl key, then hold down the Shift key, and with them both held down press the Enter key). If VS Code has a Lean file open then it should open another window displaying the tactic state (note that the tactic state might well be empty if we are not in tactic mode).