.. _glossary:

.. _glossary.close:

Close a goal
------------

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

.. _glossary.definitional_equivalence:

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 :ref:`change <tactic.change>` tactic can be used to change a hypothesis or goal to something definitionally equivalent.

.. _glossary.universe:

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.

.. _glossary.proposition:

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 :ref:`universe <glossary.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.

.. code-block:: lean

   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``:

.. code-block:: lean

   definition P : Prop := 2 + 2 = 4

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

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

.. _glossary.local_context:

Local context
-------------

This is the assumptions, also known as hypotheses, which are currently known to Lean -- the stuff before the :ref:`turnstyle <glossary.turnstyle>` and the goal. For example in the following code

.. code-block:: lean

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

the tactic state at the sorry is

.. code-block:: python

   P Q : Prop,
   HP : P
   ⊢ P ∨ Q
		
meaning that the local context is

.. code-block:: python

   P Q : Prop,
   HP : P

and the goal is ``P ∨ Q``.

.. _glossary.turnstyle:

Turnstyle
---------

Or turnstile. This is the ``⊢`` symbol in the :ref:`tactic state <glossary.tactic_state>` which appears just before the :ref:`goal <glossary.goal>`.

Goal
----

.. _glossary.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 ``⊢`` :ref:`turnstyle <glossary.turnstyle>` symbol in the :ref:`tactic state <glossary.tactic_state>`.

Tactic state
------------

.. _glossary.tactic_state:

The tactic state looks something like this:

.. code-block:: python

   P Q : Prop,
   HP : P
   ⊢ P ∨ Q
		
It consists of our hypotheses (the :ref:`local context <glossary.local_context>`) and, after a :ref:`turnstyle <glossary.turnstyle>`, the :ref:`goal <glossary.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).