(*|
-----------------
Self-evaluation 3
-----------------

:Authors: Yannick Forster, Théo Winterhalter
:Files:
  - `Source <../files/self_eval3.v>`_

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

.. default-role:: coq

.. important::

  The following exercises are easily solved by Rocq or here by hovering the
  results. This is useful for you to check your answers, but we urge you to
  resist the temptation and do it on paper!

^^^^^^^^^^
Exercise 1
^^^^^^^^^^

Write down the induction principle for `even`.

|*)

Inductive even : nat -> Prop :=
| evenO : even 0
| evenS n : even n -> even (S (S n)).

(*|

^^^^^^^^^^
Exercise 2
^^^^^^^^^^

We give you the definition of disjunction as a reminder.

.. code-block:: coq

  Inductive or (A B : Prop) : Prop :=
  | or_introl : A -> A \/ B
  | or_intror : B -> A \/ B.

  Notation "A \/ B" := (or A B).

Complete the following definition with a proof term.

|*)

#[refine]
Definition or_imp :
  forall (P Q R : Prop), (P -> R) -> (Q -> R) -> P \/ Q -> R
:= _.
Proof. Admitted.

(*|

^^^^^^^^^^
Exercise 3
^^^^^^^^^^

What is the goal after the following script?

|*)

Lemma true_false :
  true <> false.
Proof.
  intro e.
  change (if true then False else True).
  rewrite e.
  (* HERE *)
Abort.

(*|

^^^^^^^^^^
Exercise 4
^^^^^^^^^^

.. code-block:: coq

  Inductive le (n : nat) : nat -> Prop :=
  | le_n : n <= n
  | le_S : forall m, n <= m -> n <= S m.

What is the goal after the following script?
|*)

Lemma le_n_S :
  forall n m,
    n <= m ->
    S n <= S m.
Proof.
  intros n m h.
  induction h as [| m h ih].
  - constructor.
  - (* HERE *)
Abort.