.. _tactic.intro:

intro
=====

.. _tactic.intro.implies:

In general, the `intro` tactic changes a goal of type ``P → Q`` into a hypothesis of type ``P`` and a goal of type ``Q``. Here is a simple example.

.. code-block:: lean

   example (P Q : Prop) (HQ : Q) : P → Q :=
   begin
     intro HP,
     exact HQ
   end

When this proof begins, the state is

.. code-block:: python

   P Q : Prop,
   HQ : Q
   ⊢ P → Q

After ``intro HP`` the state is

.. code-block:: python

   P Q : Prop,
   HQ : Q,
   HP : P
   ⊢ Q
		
and the goal is then solved with the :ref:`exact <tactic.exact>` tactic.

.. _tactic.intro.forall:

`∀` is a function
-------------------

Terms of type `∀ x, P x` can be regarded as functions which eat a variable `x` and spit out a proof of `P x`; here is an example of what this looks like.

.. code-block:: lean

   example (X : Type) (a : X) (P : X → Prop) (H : ∀ x, P x) : P a :=
   begin
     /-
     X : Type,
     a : X,
     P : X → Prop,
     H : ∀ (x : X), P x
     ⊢ P a
     -/
     exact (H a), -- H is a function; evaluate it at a
   end

.. _tactic.intro.not:

`¬` is a function
------------------

In Lean, ``¬ P`` is notation for ``not P``, which is defined to mean ``P → false``. So one can work with ``¬ P`` as if it were a function.

.. code-block:: lean
		
   example (P Q : Prop) : ¬ P → ¬ (P ∧ Q) :=
   begin
     intro HnP,
       -- goal is now ⊢ ¬ (P ∧ Q)
     intro HPQ,
       -- state now
       -- HnP : ¬ P
       -- HPQ : P ∧ Q
       -- goal is ⊢ false
     apply HnP, -- think of HnP : P → false
       -- goal now P
     cases HPQ with HP HQ,
     exact HP
   end