(*|
-------------------------------
Introduction to the Rocq Prover
-------------------------------

:Authors: Yannick Forster, Théo Winterhalter
:Files:
  - `Source <../files/lesson1_part1.v>`_
  - `Test file <../files/test_file.v>`_
  - `Test file rendered <test_file.html>`_
  - `Exercise sheet <../files/tp1.v>`_
  - `Exercise sheet solutions <tp1c.html>`_
  - `Self evaluation <self_eval1.html>`_
  - `Slides <https://docs.google.com/presentation/d/e/2PACX-1vQK8ATweUrqhqTHvVwZ2uCKv3-WCM9JkKf_lPKMd_n_tqECyTkZ1DgiSYAjS00Kd2-veIKep2qKU3Gl/pub?start=false&loop=false>`_

.. role:: coq(code)
   :language: coq
   :class: highlight

.. default-role:: coq

.. contents:: Table of Contents
   :depth: 2
   :local:

This course teaches you how to use one proof assistant (Rocq), with the goal to

- be able to use Rocq in other courses,
- use Rocq in an internship,
- learn other proof assistants or become an expert user of Rocq via self study,
- ultimately use or study proof assistants as part of a PhD.

In particular, we believe that taking this course will allow you to learn other
proof assistants, e.g. `Agda`_, `Isabelle`_, or `Lean`_, via self study, very
quickly. Note that the `MPRI HOTT`_ course teaches Agda in more detail, relying
on you having learnt about proof assistants in this course.

.. _MPRI HOTT: https://mpri-master.ens.fr/doku.php?id=cours:hott

.. _Agda: https://agda.readthedocs.io/en/latest/getting-started/what-is-agda.html

.. _Isabelle: https://isabelle.in.tum.de/

.. _Lean: https://lean-lang.org/

.. important::

  You should have installed Rocq before attending, but in case you haven't,
  please consult `our page about installing Rocq`_.

.. _our page about installing Rocq: ../installrocq.html

In this first lecture, we will introduce fundamentals of Rocq and proof
assistants in general:

* propositional logic
* proofs by case analysis
* proofs by induction

.. raw:: html

  <hr>

.. raw:: html

  Note that this document is being interpreted from Rocq files by
  <a href="https://github.com/cpitclaudel/alectryon/">Alectryon</a>.
  Bubbles (<span class="alectryon-bubble"></span>) indicate interactive
  fragments: hover for details, click to reveal contents.
  Use <kbd>Ctrl+↑</kbd> and <kbd>Ctrl+↓</kbd> to navigate,
  <kbd>Ctrl+🖱️</kbd> to focus.
  On macOS, use <kbd>⌘</kbd> instead of <kbd>Ctrl</kbd>.

  You are welcome to play with this file in Rocq directly, by clicking on
  "Source" in the bar above.

.. raw:: html

  <hr>

^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Getting started with propositional logic
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Let's get started with proving a first simple fact about propositional logic:
If `P` holds, then `P` holds, i.e., an implication.
Implications are written `->` in Rocq.

To prove a fact, one writes `Lemma name : statement.`
Lemmas can be parameterized, our first lemma is parametric in an arbitrary
proposition `P`. We denote this by writing `(P : Prop)`.

|*)

(*| .. coq:: none |*)

Axiom REPLACE_ME : forall {A : Type}, A.

(*| |*)

Lemma P_imp_P (P : Prop) : P -> P.
Proof.
(*|
If you interpret this script live, you will see the so-called goal: `P -> P`.
Verbally: `P` implies `P`.
To prove it, we can assume we have a proof of `P`, we call it `h`.
|*)
  intro h.
(*| The command `intro` is called a *tactic*. |*)
(*|
The goal is now `P`, but notice we have some extra assumption
`h : P`.
To use an assumption, one can use the `apply` tactic:
|*)
  apply h.
(*| Proof finished! All that's left to do is to type `Qed`. |*)
Qed.

(*|
Try to see what happens if one types `Qed` before the proof is finished.
|*)

(*|
We now have a new fact that can be used in other proofs:
`P_imp_P` which is a proof of `P -> P`.
You can check this fact using the `Check` command.
|*)
Check P_imp_P.

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Implication</summary>

..
|*)

Lemma P_imp_P' (P : Prop) : P -> P.
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
We can also write conjunctions (``/\``) and disjunctions (``\/``) of
propositions. For instance, we can show that conjunction is symmetric.
|*)

Lemma and_comm (P Q : Prop) : P /\ Q -> Q /\ P.
Proof.
(*| We have an implication so we use `intro`. |*)
  intro h.
(*|
We now have `h : P /\ Q` as assumption and we need to prove `Q /\ P`.

First we need to have a look at `P /\ Q`, we would like to turn it into
two different hypotheses: one for `P` and one for `Q`.
If you have taken a course in logic, you would have said that we need to apply
the elimination rule(s) for conjunctions.
They are sometimes written as follows in natural deduction.

.. math::

   \cfrac{P \land Q}{P} \qquad \cfrac{P \land Q}{Q}

Expressed with a context this can be stated as only one rule:

.. math::

   \cfrac{\Gamma \vdash P \land Q \quad \Gamma, P, Q \vdash R}{\Gamma \vdash R}

.. tip::

  To see the connection with tactics, you have to read those rules bottom-up,
  from the conclusion to the premises. You view the goal as
  :math:`\Gamma \vdash P` where :math:`\Gamma` is the list of hypotheses —
  what appears above the bar in the goal pane — and `P` is the proposition you
  have to prove — below the bar.
  Applying the tactic yields the goals that are above the bar of the inference
  rule.

We can use elimination rules in general using the `destruct` tactic to
decompose an hypothesis into all possible proofs of it. In the case of
`P /\ Q`, there is just one:
|*)
  destruct h as [hP hQ].
(*|
The `as` clause above is used to give a name to the resulting
hypotheses. Here we name `hP : P` and `hQ : Q`.
|*)
(*|
To prove a conjunction we can use the `split` tactic to get two goals:
|*)
  split.
(*|
In logical terms, this corresponds to applying the introduction rule for
conjunctions:

.. math::

   \cfrac{\Gamma \vdash P \quad \Gamma \vdash Q}{\Gamma \vdash P \land Q}

Notice we now have two goals, `P` and `Q`.
We use bullets to focus on the goals one by one.
|*)
  - (*| Now proving `Q` is easy. |*)
    apply hQ.
  - apply hP.
Qed.

(*|
Here `apply` plays the role of the axiom rule of natural deduction.

.. math::

   \cfrac{P \in \Gamma}{\Gamma \vdash P}

|*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Conjunction</summary>

..
|*)

Lemma and_comm' (P Q : Prop) : P /\ Q -> Q /\ P.
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*| Let us look at a slightly different example: disjunction. |*)

Lemma or_comm (P Q : Prop) : P \/ Q -> Q \/ P.
Proof.
  intro h.
  (*|
Now we first need to do a case analysis on whether `P` or `Q` holds.
This should again be reminiscent of natural deduction rules, this time for
disjunction elimination:

.. math::

   \cfrac{\Gamma \vdash P \lor Q \quad \Gamma, P \vdash R \quad \Gamma, Q \vdash R}{\Gamma \vdash R}

This is done using the `destruct` tactic again, doing a case analysis
on all possible proofs of `P \/ Q`. There are two:
|*)
  destruct h as [hP | hQ].
  (*| Notice how we used a pipe to separate the two cases. |*)
  -
(*|
Now we have `P` and we want to prove `Q \/ P`.
We can use the tactic `right` to say we want to prove the right case.
|*)
    right.
    apply hP.
  - (*| Unsurprisingly, the dual tactic is called `left`. |*)
    left.
    apply hQ.
Qed.

(*|
We can once again see the connection with natural deduction rules: we have two
introduction rules for disjunction that correspond to `left` and `right`
respectively.

.. math::

   \cfrac{\Gamma \vdash P}{\Gamma \vdash P \lor Q} \qquad
   \cfrac{\Gamma \vdash Q}{\Gamma \vdash P \lor Q}

|*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Disjunction</summary>

..
|*)

Lemma or_comm' (P Q : Prop) : P \/ Q -> Q \/ P.
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
We also have the usual ⊤ and ⊥ which in Rocq are called `True` and
`False`.
|*)

Lemma truetrue : True.
Proof.
(*|
To prove it, you can also use `split`!
It's like the nullary conjunction.
`split` will work with all logical constructions that only have one
introduction rule.
|*)
  split.
Qed.

(*|
Looking at natural deduction again, it makes sense, on the top of the inference
line we see no premises.

.. math::

   \cfrac{}{\Gamma \vdash \top}


Now, let's look at `False`.
|*)

Lemma falsefalse : False.
Proof.
(*|
Of course, one cannot prove `False` without assumptions.
So we give up:
|*)
Abort.

(*|
Rocq will now not add `falsefalse` to the environment, and thus the `Check`
command will fail:
|*)
Fail Check falsefalse.

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Truth</summary>

..
|*)

Lemma truetrue' : True.
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
However, `False` implies anything: *ex falso quodlibet*.
|*)

Lemma anything_goes P : False -> P.
Proof.
  intro bot.
  (*|
The `exfalso` tactic concludes anything as long as you can prove
`False`.
|*)
  exfalso.
  apply bot.
Qed.

(*|
The corresponding rule is as follows.

.. math::

   \cfrac{\Gamma \vdash \bot}{\Gamma \vdash A}

|*)

(*| Let's do the proof again, with an alternative approach. |*)
Lemma anything_goes_again P : False -> P.
Proof.
  (*|
Namely, we can do case analysis on all possible proofs of `False`
directly — of which there are none.
|*)
  intro bot.
  destruct bot.
Qed.

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Ex falso</summary>

..
|*)

Lemma anything_goes' (P : Prop) : False -> P.
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
Let us have a look at negation now.
`~ P` is a notation for the negation of `P`.
In fact it is defined as `P -> False`, so we can use intro to prove a
negation.
|*)

Lemma nofalse : ~ False.
Proof.
  intro contra. apply contra.
Qed.

(*|
The corresponding rules are:

.. math::

   \cfrac{\Gamma, P \vdash \bot}{\Gamma \vdash \neg P}
   \qquad
   \cfrac{\Gamma \vdash \neg P \quad \Gamma \vdash P}{\Gamma \vdash \bot}

By the way, we have implicitly used the introduction and elimination rules for
implication from the very beginning (including for negation since it is defined
in terms of implications):

.. math::

   \cfrac{\Gamma, Q \vdash P}{\Gamma \vdash Q \Longrightarrow P}
   \qquad
   \cfrac
     {\Gamma \vdash Q \Longrightarrow P \quad \Gamma \vdash Q}
     {\Gamma \vdash P}

They are invoked through `intro` and `apply` respectively.
|*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Negation</summary>

..
|*)

(*| `~ A` (negation) is a notation for `A -> False` below. |*)

Lemma nofalse' : ~ False.
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

Lemma impl_trans P Q R :
  (P -> Q) -> (Q -> R) -> (P -> R).
Proof.
(*|
The following is equivalent to `intro hPQ. intro hQR. intro hP.`
Notice the `s`.
|*)
  intros hPQ hQR hP.
(*| We now use elimination twice in a row. |*)
  apply hQR.
  apply hPQ.
  apply hP.
Qed.

(*|
Finally, let's end this part of the lesson by having a look at logical
equivalence: :math:`P \iff Q`.
In Rocq, this is unsurprisingly defined as the conjunction of the two
implications: `P <-> Q` is the same as `(P -> Q) /\ (Q -> P)`.

We can for instance prove that equivalence is symmetric (it is in fact an
equivalence relation… shocking.)
|*)

Lemma equiv_sym P Q :
  (P <-> Q) -> (Q <-> P).
Proof.
  intros h.
  destruct h as [hPQ hQP].
  split.
  - apply hQP.
  - apply hPQ.
Qed.

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Propositional logic</summary>

..
|*)

(*| Now some new exercises about propositional logic. |*)

Lemma imp_trans (P Q R : Prop) : (P -> Q) -> (Q -> R) -> (P -> R).
Proof.
Admitted.

Lemma to_not_not (P : Prop) : P -> ~~ P.
Proof.
Admitted.

(*|
For this one, note that if you already separated a case distinction
with dashes (`-`) then you can use `+` at the next level.
The following level is marked with `*`.
|*)

Lemma distr (P Q R : Prop) : (P \/ Q) /\ R -> (P /\ R) \/ (Q /\ R).
Proof.
Admitted.

Lemma contrad (P : Prop) : P /\ ~ P -> False.
Proof.
Admitted.

Lemma lem_pl (P Q : Prop) : P \/ ~ P -> ((P -> Q) -> P) -> P.
Proof.
Admitted.

Lemma lem_dns (P : Prop) : P \/ ~ P -> ~~ P -> P.
Proof.
Admitted.

(*|
To introduce several variables at once, you can use the `intros` tactic.
|*)

Lemma dn_functorial P Q : (P -> Q) -> ~~ P -> ~~ Q.
Proof.
  intros hPQ hnnP.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
^^^^^^^^^^^^^^^^^^^^^^^^^^^
Case analysis and induction
^^^^^^^^^^^^^^^^^^^^^^^^^^^

Let us consider the type of Booleans, with elements `true` and `false`.
We also refer to the `negb` function from the standard library which sends
`true` to `false` and vice versa.
|*)
Lemma negb_true :
  negb true = false.
Proof.
(*| Here we have computation, so we can ask Rocq to simplify things. |*)
  simpl.
(*|
Equality is then proven with the following tactic which solves goals
of the form `x = x`.
|*)
  reflexivity.
Qed.

(*| We show that Boolean negation is involutive. |*)

Lemma negb_invol (b : bool) :
  negb (negb b) = b.
Proof.
(*|
Similar to how `destruct` can be used to do case analysis on hypotheses,
it can be used to do case analysis on Booleans. There are two cases:
|*)
  destruct b.
  - simpl. reflexivity.
  - simpl. reflexivity.
Qed.

(*| We now turn to Boolean conjunction. |*)

Lemma andb_comm b1 b2 :
  andb b1 b2 = andb b2 b1.
Proof.
  destruct b1.
  - simpl. destruct b2.
    + simpl. reflexivity.
    + simpl. reflexivity.
  - simpl. destruct b2.
    + simpl. reflexivity.
    + simpl. reflexivity.
Qed.

Lemma andb_comm' b1 b2 :
  andb b1 b2 = andb b2 b1.
Proof.
  (*| We can also ask Rocq to do two case analyses at the same time. |*)
  destruct b1, b2.
  -
(*|
No need to use `simpl` every time, `reflexivity` does it on its own.
|*)
    reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity.
Qed.

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Booleans</summary>

..
|*)

(*|
Let us switch to Booleans again.

`andb` is conjunction, `orb` is disjunction, `negb` is negation.
Both `andb` and `orb` look at the first Boolean before simplifying.
|*)

Lemma andb_orb_distr (b1 b2 b3 : bool) :
  andb b1 (orb b2 b3) = orb (andb b1 b2) (andb b1 b3).
Proof.
Admitted.

Lemma de_morgan (b1 b2 : bool) :
  negb (andb b1 b2) = orb (negb b1) (negb b2).
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*| Let us switch to natural numbers. |*)

Lemma calc_12_3 : 12 + 3 = 15.
Proof.
(*|
Here we have computation again, so we can ask Rocq to simplify things.
|*)
  simpl.
(*|
Now we have to prove `15 = 15`, this is true by reflexivity of equality.
|*)
  reflexivity.
Qed.

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Computation</summary>

..
|*)

(*| Let us switch to natural numbers. |*)

Lemma calc_12_3' : 12 + 3 = 15.
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

Lemma double_eq n : n + n = 2 * n.
Proof.
(*| Functions in Rocq have computation rules. |*)
  simpl.
(*|
The `+ 0` at the end might seem surprising.
This has to do with the definition of multiplication:

    0 * m := 0

    (n + 1) * m := m + n * m

So `2 * m = m + 1 * m = m + (m + (0 * m)) = m + (m + 0)`.

Note that `n + 0` also does not simplify by computation, because the defining
rules are:

    0 + m := m

    (n + 1) + m := (n + m) + 1

However, we can prove that `n + 0 = n`. We do so with a lemma first.

|*)
Abort.

Lemma plus_zero n : n = n + 0.
Proof.
(*|
Case analysis is no longer sufficient to prove such a result, instead we're
going to perform induction on natural numbers. We do so with the following
tactic.
|*)
  induction n.
  (*|
We have two cases to prove, the case `n = 0` and the case `n + 1`.
In Rocq, the successor of `n` is written `S n`, like in Peano
arithmetic.
|*)
  - (*| Now, `0 + 0` computes to `0`: |*)
    simpl. reflexivity.
  - simpl.
(*|
We have `S` on both sides.
We can use the `f_equal` tactic to prove that `f x = f y` if `x = y`.
|*)
    f_equal.
(*|
Here we can apply our induction hypothesis.
Since we did not chose its name, we can use a different tactic
that finds a matching hypothesis on its own:
|*)
    assumption.
Qed.

(*|
The lemma we wanted to prove earlier is now easy, we just have to make use of
`plus_zero` we just proved.
|*)

Lemma double_eq n : n + n = 2 * n.
Proof.
  simpl. f_equal. apply plus_zero.
Qed.

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Addition</summary>

..
|*)

(*|
Let us make a lemma out of the `n + 0 = n` property.

You can then apply this lemma by using `apply n_plus_0` like for hypotheses!
|*)

Lemma n_plus_0 (n : nat) : n + 0 = n.
Proof.
Admitted.

Lemma double_eq' (n : nat) : n + n = 2 * n.
Proof.
Admitted.

Lemma plus_S (n m : nat) : n + S m = S n + m.
Proof.
Admitted.

Lemma plus_comm (n m : nat) : n + m = m + n.
Proof.
  induction n.
  - simpl.
    (* Try the command below, it gives information about a constant. *)
    About n_plus_0.
    rewrite n_plus_0.
    (* You should manage the rest *)
Admitted.

(*| Show associativity of addition. |*)

Lemma plus_assoc (k n m : nat) : k + n + m = k + (n + m).
Proof.
Admitted.

(*|
We can also show commutativity of multiplication.
Try to come up with the lemmas yourself.
Note that you can also use `rewrite` in the opposite direction by using:

.. code-block:: coq

    rewrite <- n_plus_0

for instance.
You can also use `rewrite` with hypotheses you have.

If you ever find yourself with `x = y` to prove, when you think you can
prove `y = x`, you can also use the `symmetry` tactic.
|*)

(*|
.. raw:: html

   </details>

..
|*)

(*|
^^^^^^^^^^^^^^^^^^
Defining functions
^^^^^^^^^^^^^^^^^^

In Rocq you can also write your own definitions and they can be recursive.
In models a recursive function corresponds to a fixed point so such functions
are introduced with the keyword `Fixpoint`.
It corresponds roughly to OCaml's `let rec` syntax, but compared to OCaml,
functions must be total (defined on all inputs) so in particular, they must be
terminating.

Here, we define a function `double` which doubles its argument by duplicating
all occurrences of `S` in it. For instance, `double (S (S 0))` will compute
to `S (S (double (S 0)))` and then to `S (S (S (S (double 0))))` which is
`S (S (S (S 0)))`. In other words `double 2 = 4`.
|*)

Fixpoint double (n : nat) :=
  match n with
  | 0 => 0
  | S n => S (S (double n))
  end.

(*|
Note that the definition contains the `match` construct which performs
pattern matching, or case analysis. If you know OCaml then it is the same syntax
with the exception that a `match` block has to end with the keyword `end`
and that branches are marked with `=>` instead of `->`.
The `end` makes it easier to parse for both humans and machines, in particular
when several `match` are nested.

We can now prove by a simple induction that `double n` is the same as
`n * 2`.
|*)

Lemma double_eq2 n : double n = n * 2.
Proof.
  induction n as [ | m ihm].
(*|
This time we decided to give names to the extra hypotheses produced by the
`induction` tactic. As with `destruct` before, there is a pipe (`|`)
separating the two cases (`0` and `S m`).
In the first case, there is no induction hypothesis so we do not need to
introduce any name.
In the successor case, we need to provide a name for the induction hypothesis
`ihm` but also for the natural number that appears below `S`, here we chose
`m`.
|*)
  - simpl. reflexivity.
  - simpl.
(*|
Now we have `ihm : double m = m * 2` in the context, and `double m` in the
goal. So we would like to replace it with `m * 2`.
There is a tactic to do just that: `rewrite`!
|*)
    rewrite ihm. reflexivity.
Qed.

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Minimum</summary>

..
|*)

(*|
Fill in the cases for the following function.

We use a placeholder `REPLACE_ME` that you need to replace.
|*)

Fixpoint min (n m : nat) : nat :=
  match n, m with
  | 0, _ => REPLACE_ME
  | _, 0 => REPLACE_ME
  | S n, S m => REPLACE_ME
  end.

Lemma min_comm : forall n m, min n m = min m n.
Proof.
  intro n.
  (* Hint: start the induction before introducing m, or use induction in *)
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
^^^^^^^^^^^
Quantifiers
^^^^^^^^^^^

When using `Check`, `About`, or simply hovering constants in VSRocq, you
have probably seen the keyword `forall` appear.
It corresponds to the universal quantifier, often written `∀`
(and in fact you can tell Rocq to print it like this `if you tell it to use
Unicode <../rocq-faq.html#does-rocq-support-unicode>`_).

Adding quantifiers makes us leave the realm of propositional logic and enter
the world of higher order logic.

Have a look at the lemma we just proved, and see how its statement begins with
`forall (n : nat)`. When we put `n` to the left of the colon (`:`), we
have implicitly quantified over it, universally.
|*)
Check double_eq2.

(*|
To see what looks like in natural deduction, we extend the notion of context so
that besides formulas, it is able to contain also elements of a certain type
such as `n : nat`.

.. math::

   \cfrac{\Gamma, x : A \vdash P}{\Gamma \vdash \forall (x : A).\ P}
   \qquad
   \cfrac{\Gamma, Q \vdash P}{\Gamma \vdash Q \Longrightarrow P}

This is just like the context we see in goals.
Notice the parallel with the introduction rule for implication we have seen
previously.
This introduction rule is materialised in Rocq as the tactic `intro`, exactly
like for implication. See how it works below.
|*)

Lemma n_mul_0 : forall (n : nat), n * 0 = 0.
Proof.
(*|
As before, `intro` takes a name. We could pick `n` but we don't have to.
Let's pick `k` for a change.
|*)
  intro k.
(*|
Nothing prevents me from reusing `k` as a variable name.
Don't do it if you find it confusing.
|*)
  induction k as [| k ih].
  - reflexivity.
  - simpl. assumption.
Qed.

(*|
Of course, the universal quantifier also has an elimination rule, which we put
side by side with the one for implication again, because there is a parallel to
be made.

.. math::

   \cfrac
     {\Gamma \vdash \forall (x : A). P \quad \Gamma \vdash u : A}
     {\Gamma \vdash P[ x := u ]}
   \qquad
   \cfrac
     {\Gamma \vdash Q \Longrightarrow P \quad \Gamma \vdash Q}
     {\Gamma \vdash P}

It is much more complicated than everything we have seen before for two reasons:

1. At the top we wrote :math:`u : A` to the right of the turnstile (:math:`\vdash`) instead of a proposition. This is because the element :math:`u` of type :math:`A` itself matters.
2. At the bottom we wrote :math:`P[ x := u ]` to indicate that in the end we prove :math:`P`, but since :math:`P` is allowed to mention :math:`x` (think of `forall (n : nat), n * 0 = 0` again), we need to replace it with the value :math:`u`.

If it's too hard, don't scratch your head too much and instead look at a
concrete example where we use `n_mul_0` using `apply` (again a parallel
with implication).
|*)

Lemma dummy :
  forall (a b c : nat), (a + b * b + c * a) * 0 = 0.
Proof.
  intros a b c.
(*|
This is just an instance of `n * 0 = 0` where we replace `n` with a bigger
expression. Fortunately, we don't even need to specify it, Rocq will infer that
information for us.
|*)
  apply n_mul_0.
Qed.

(*|
Another way to look at it, is to split it into steps using the `specialize`
tactic.
|*)

Lemma spec :
  (forall n, n + n = 2 * n) ->
  (forall k r, (k + r) + (k + r) = 2 * (k + r)).
Proof.
  intros h k r.
  specialize (h (k + r)).
  apply h.
Qed.

(*|
Let us now move on to the dual operator, the existential quantifier.
First let us look at the natural deduction rules.

.. math::

   \cfrac
     {\Gamma \vdash u : A \quad \Gamma \vdash P[ x := u ]}
     {\Gamma \vdash \exists (x : A). P}
   \qquad
   \cfrac
     {\Gamma \vdash \exists (x : A). P \quad \Gamma, x : A, P \vdash Q}
     {\Gamma \vdash Q}

In the elimination rule (on the right), remember that :math:`P` can refer to
:math:`x`, which is symbolised by having :math:`x` appear *before* :math:`P`.

Let's look first at how to prove an existentially quantified statement.
In Rocq they are written `exists (x : A), P`.
|*)

Lemma nat_desc n :
  n = 0 \/ (exists m, n = S m).
Proof.
(*| We don't need full induction here. |*)
  destruct n as [| m].
  - left. reflexivity.
  - right.
(*|
Proving an existential can be done using the `exists` tactic, just like
the quantifier itself!
|*)
    exists m. reflexivity.
Qed.

(*|
Using an existentially quantified assumption on the other hand is going to
require the `destruct` tactic, a bit like a conjunction.

To see this, we are going to define two predicates on natural numbers
corresponding to even- and oddness.
|*)

Definition even n := exists m, n = 2 * m.

Definition odd n := exists m, n = S (2 * m).

Lemma even_odd_S n :
  even n ->
  odd (S n).
Proof.
  intro hn.
  destruct hn as [m e].
  rewrite e.
  exists m. reflexivity.
Qed.

(*|
To showcase more handy features. We're going to perform the introduction
of the assumption at the same time as eliminating it.
This is done by using so-called *intropatterns*: the tactic `intros [n e]`
works essentially like `intros h. destruct h as [n e].` while being much
shorter.
|*)

Lemma even_odd_S_again n :
  even n ->
  odd (S n).
Proof.
  intros [m e].
  exists m.
(*| For fun we're going to use `rewrite` from right to left. |*)
  rewrite <- e.
  reflexivity.
Qed.

(*|
Try to do the exercises and ask for help if needed.
It is expected that you can't solve all of them yet before completing the
lesson.
Don't hesitate to `refer to our tactic index when solving exercises
<tactics.html>`_.
|*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Equivalence and forward reasoning (advanced)</summary>

..
|*)

(*|
If you have already used Rocq before or you are done with the exercises,
give the advanced exercises a try.
They hopefully teach you things you have not seen before.

If they are too hard, don't worry too much about it for the exam.
|*)

Section Advanced.

  Context (P Q R : Prop).

(*|
We introduce a new notation `P <-> Q` meaning `P` is equivalent to `Q`.

It is essentially a notation for `(P -> Q) /\ (Q -> P)` so you can use the
tactics split and destruct to prove it and use it.

Here is a trivial example to understand it.
|*)

  Lemma P_iff_P : P <-> P.
  Proof.
    split.
    - intro. assumption.
    - intro. assumption.
  Qed.

(*|
And here is a new tactic that is going to be useful: `assert`.

When you write `assert (h : P)` you are telling Rocq that you want to prove
`P` and that then you are going to use this as an hypothesis named `h`.
This is sometimes called forward reasoning.

See how it works below.
|*)

  Lemma or_imp : (Q -> P) /\ (R -> P) -> Q \/ R  -> ~~ P.
  Proof.
    intros h1 h2.
    assert (hP : P).
    { destruct h1 as [hQP hRP].
      destruct h2 as [hQ | hR].
      - apply hQP. apply hQ.
      - apply hRP. apply hR.
    }
    apply to_not_not. apply hP.
  Qed.

  Lemma Russell : ~ (P <-> ~ P).
  Proof.
  Admitted.

End Advanced.

(*|
.. raw:: html

   </details>

..
|*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Quantifying over propositions (advanced)</summary>

..
|*)

(*|
For even more advanced stuff we are going to use quantifiers
on propositions too. It's basically the same as with natural numbers.

If you have some hypothesis of the form:

.. code-block:: coq

    h : forall x, P x

then know that you can use `specialize (h y)` to obtain `h : P y`.
See the following example.
|*)

Lemma forall_False : (forall (P : Prop), P) -> False.
Proof.
  intro h.
  specialize (h False).
  assumption.
Qed.

(*| Note that it would work with apply directly in this case. |*)

Lemma forall_False' : (forall (P : Prop), P) -> False.
Proof.
  intro h.
  apply h.
Qed.

(*| Prove the converse now. |*)

Lemma False_forall : False -> (forall (P : Prop), P).
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Excluded middle (advanced)</summary>

..
|*)

(*|
Rocq is, at its basis, a system that has nothing but elimination and
introduction rules for disjunctions:

.. math::

  \frac{P}{P \vee Q}

  \frac{Q}{P \vee Q}

  \frac{P \vee Q \qquad P \Longrightarrow R \qquad Q \Longrightarrow R}{R}


In particular, these rules do not allow proving

.. math::

  P \vee \neg P

In other words, Rocq implements intuitionistic logic. This allows

* assuming classical laws of reasoning like the law of excluded middle and
  doing classical math
* not assuming the law of excluded middle, thus being able to have interesting
  proofs of the form `A -> LEM` for a statement `A`.

We will prove `A <-> LEM` for two statements now:
|*)

(*| Law of Excluded Middle |*)
Definition theLEM := forall P, P \/ ~ P.
(*| Double Negation Shift |*)
Definition theDNS := forall P, ~~ P -> P.
(*| Peirce's law |*)
Definition thePL := forall P Q : Prop, ((P -> Q) -> P) -> P.

(*| We can now prove the other direction from before. |*)

Lemma lem_dns_general : theLEM -> theDNS.
Proof.
Admitted.

Lemma lem_pl_general : theLEM -> thePL.
Proof.
Admitted.

Lemma dns_lem : theDNS -> theLEM.
Proof.
Admitted.

Lemma pl_lem : thePL -> theLEM.
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Advanced advanced exercise</summary>

..
|*)

(*|
* Come up with more natural statements equivalent to `LEM`.
* Come up with a statement `S` such that `LEM -> S`, you cannot prove
  `S -> LEM`, but `S` is also not provable without any assumptions in
  Rocq.
* Found one? Great! Now find a statement `S'` such that `S -> S'`, you
  cannot prove `S' -> S`, but `S'` is also not provable without any
  assumptions in Rocq.
* If you force `theDNS` and `theLEM` to talk about the same proposition `P`,
  the implication `theDNS -> theLEM` doesn't work any more, why?
* Can you come up with a hierarchy `S_i` of such statements such that
  `S_0` is the strongest and they get subsequently weaker?
* Can you come up with a hierarchy `S_i` of such statements such that
  `S_0` is the weakest and they get subsequently stronger?

**🗣️ Talk to us if you want to know more about the solution.**
|*)

(*|
.. raw:: html

   </details>

..
|*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Commuting <code class="coq highlight">forall</code> and <code class="coq highlight">\/</code> (advanced)</summary>

..
|*)

(*| An example of commuting `forall` and `\/`. |*)

Lemma forall_or :
  forall P Q,
    (Q \/ ~ Q) ->
    (forall (x : nat), P x \/ Q) ->
    (forall x, P x) \/ Q.
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: More classical reasoning</summary>

..
|*)

Lemma classical_or_contra_r :
  theLEM ->
  forall (P Q : Prop),
    (~ Q -> P) ->
    P \/ Q.
Proof.
Admitted.

(*| For the following do you need LEM for both directions? |*)

Lemma classical_impl :
  theLEM ->
  forall (P Q : Prop),
    (P -> Q) <-> (~ P \/ Q).
Proof.
Admitted.

Lemma contrapositive :
  theLEM ->
  forall (P Q : Prop),
    (~ Q -> ~ P) ->
    P -> Q.
Proof.
Admitted.

(*|
.. tip::

  If you want to use `specialize` on a hypothesis twice, you can use
  `specialize (h x) as hx` to create a new hypothesis instead of replacing `h`.

..
|*)

Lemma twice :
  theLEM ->
  forall (P Q : Prop),
    ((P -> Q) -> Q) ->
    ((Q -> P) -> P).
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: More natural numbers</summary>

..
|*)

Lemma mult_distr :
  forall n m k,
    k * (n + m) = k * n + k * m.
Proof.
Admitted.

(*|
If you thought this kind of proof is extremely annoying, rest assured, most
would agree and in practice you don't have to do them by hand.
We torture you so you understand better how things work.

In practice Rocq users will use the `lia` tactic to solve a lot of integer
arithmetic problems.
|*)

From Stdlib Require Import Lia.

Lemma mult_distr_lia :
  forall n m k,
    k * (n + m) = k * n + k * m.
Proof.
  lia.
Qed.
(*| See? Much better. 😊 |*)

(*|
.. raw:: html

   </details>

..
|*)