Section 1 : Logic
=================

By "logic" here we mean the study of propositions. A proposition is a
true/false statement. For example ``2+2=4``, ``2+2=5``, and the statement
of the Riemann Hypothesis are all propositions.

Basic mathematics with propositions involves learning about how
functions like ``→``, ``¬``, ``∧``, ``↔`` and ``∨`` interact with
propositions like ``true`` and ``false``.

In Lean we can prove mathematical theorems using *tactics* such as ``intro``
and ``apply``. The purpose of this section is to teach you ten or so basic
tactics which can be used to solve logic problems.

Fire up a Lean session, open up the ``formalising-mathematics-2022``
Lean repository, find ``section01`` within the ``src`` directory of
the repository, and try doing the problem sheets! If you need help
getting started, you can read the below, or you can watch the
video **TODO** make a video and link to it here.

Lean's notation for logic.
--------------------------

In Lean, ``P : Prop`` means "``P`` is a proposition", and ``P → Q`` is the
proposition that "``P`` implies ``Q``". Note that Lean uses a single arrow ``→``
rather than the double arrow ``⇒``.

The notation ``h : P`` means any of the following equivalent things:

* ``h`` is a proof of ``P``;
* ``h`` is the assumption that ``P`` is true;
* ``P`` is true, and this fact is called ``h``.

Here ``h`` is just a variable name. We will often call proofs of ``P`` things like ``hP`` but you can call them pretty much anything.

WARNING: do not confuse ``P : Prop`` with ``hP : P``. The former means
that ``P`` is a true-false statement; the latter means that it is a true
statement (and ``hP`` is its proof).

Lean's tactic state.
--------------------

Lean's "tactic state", or "local context", is what you see on the right
hand side of the screen when you have Lean up and running. In the middle
of a proof it might look something like this:

.. code-block::

   P Q : Prop
   hP : P
   hPQ : P → Q
   ⊢ Q

The proposition after the "sideways T" at the bottom (it's called a "turnstile" apparently) is the thing you
are supposed to be *proving* -- this is the *goal* of the level of
the game. The stuff above the turnstile is the stuff you are *assuming*.
In the example above, `P` and `Q` are propositions, and we are assuming
that `P` is true and that `P` implies `Q`, and we are supposed to be
proving that `Q` is true. If you succeed in proving the goal, Lean
will display a "goals accomplished 🎉" message and, assuming you
didn't use `sorry` at any point (which is cheating), you've solved the level.

How then do we manipulate the tactic state? We do this using tactics,
which you type in on the left hand side of the screen, between a
``begin`` and an ``end``. Take a look at some of the tactic documentation
in Part C of this book to learn more about tactics. If you're
just getting started, then try reading about :ref:`intro <tac_intro>`,
:ref:`apply <tac_apply>` and :ref:`exact <tac_exact>`. Those are the tactics
you'll need to solve the levels in the first problem sheet of the course,
logic sheet 1 in section 1.