(*|
-----------------
Self-evaluation 2
-----------------

:Authors: Yannick Forster, Théo Winterhalter
:Files:
  - `Source <../files/self_eval2.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 of `expr`.

|*)

Inductive expr (X : Type) :=
| var (x : X)
| add : expr X -> expr X -> expr X.

(*|

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

Prove the following:

|*)

Goal forall X x e1 e2, var X x <> add X e1 e2.
Proof.
Admitted.

(*|

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

Given the following inductive type, identify parameters, non-uniform parameters, and indices:

|*)

Inductive lt X (s : X -> X) (x : X) : X -> Prop :=
| lt_start : lt X s x (s x)
| lt_S y : lt X s (s x) y -> lt X s x y.

(*|

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

|*)

Lemma lt_s_both X s x y :
  lt X s x y -> lt X s (s x) (s y).
Proof.
  induction 1 as [ | y h ih].
  - constructor.
  - (* what is the full goal here? give the types of
       every variable in the assumptions
       and the proof obligation
    *)
Admitted.