(*|
------------------------
Modelling and automation
------------------------

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

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

.. default-role:: coq

.. contents:: Table of Contents
   :depth: 2
   :local:
|*)

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

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

(*| |*)

From Stdlib Require Import Lia List ZArith.
Import ListNotations.

(*|
^^^^^^^
Records
^^^^^^^

In Rocq you can write structures using what we call "records".
They consist of various fields that each contain data of a given type.

For instance, a (bad) type of rationals:
|*)

Record bad_rational1 := {
  numerator : nat ;
  denominator : nat
}.

(*| Under the hood, Rocq will define an inductive type with one constructor
called `Build_bad_rational1`. |*)
Print bad_rational1.
About Build_bad_rational1.

(*| We can produce values as follows: |*)

Definition half := {|
  numerator := 1 ;
  denominator := 2
|}.

(*| The names of the fields also correspond to what we call projections.
They let us access the various values of a record. |*)

Compute (numerator half).
Compute (denominator half).

Record bad_rational2 := {
  numerator' : Z ;
  denominator' : nat
}.
(*| We need to give different names because `numerator` is a global definition. |*)

(*|
.. note::

   To write integers in `Z`, we can use numeral notations as long as we
   add `%Z` at the end to indicate that we don't mean a `nat`.
|*)

Definition half' := {|
  numerator' := 1%Z ;
  denominator' := 2
|}.

(*| We can also produce values interactively. |*)
Definition quarter : bad_rational2.
Proof.
  (*| `constructor` will ask us to provide the values for all the fields |*)
  constructor.
  - exact 1%Z.
  - exact 4.
Defined.

Record rational := {
    numerator'' : Z ;
    denominator'' : nat ;
    den_not_zero : denominator'' <> 0
  }.

About Build_rational.

Print quarter.

(*| We can also produce values interactively. |*)
Definition quarter'' : rational.
Proof.
  refine (Build_rational _ _ _).
  (*| `refine` will turn arguments that can be derived from other arguments into
so-called existential variables (evars) |*)
Abort.
Definition quarter'' : rational.
  (*| the tactic `constructor` fails because it cannot introduce evars |*)
  Fail constructor.
  (*| `econstructor` can |*)
  econstructor.
Abort.
Definition quarter'' : rational.
  (*| same for `apply`: |*)
  Fail apply Build_rational.
  (*| `eapply` works |*)
  eapply Build_rational.
  - exact 1%Z.
  - assert (4 <> 0) as H by lia.
    exact H.
Abort.
Definition quarter'' : rational.
   eapply (Build_rational 1).
   instantiate (1 := 4). lia.
Abort.
Definition quarter'' : rational.
  refine {| numerator'' := 1 ; denominator'' := 4 |}.
  lia.
Defined.

(*| Actually, products, which we defined using an inductive type,
can also be defined as records. For this we use parameters to records.
They work like inductive parameters.

In fact, records are syntactic sugar over inductive types with one
constructor that takes all the fields as arguments, and we can even give
a name to that constructor. |*)

Record prod' (A B : Type) := mkpair {
  fst' : A ;
  snd' : B
}.

Definition some_pair := mkpair _ _ 12 bool.
Print some_pair.

(*| Actually it's annoying to have the underscores in `mkpair _ _ 12 bool`;
we're going to change that with the `Arguments` command. |*)

Arguments mkpair {A B}.

Definition some_other_pair := mkpair false true.

(*| You can also do pattern matching using this constructor. |*)

Definition to_prod {A B} (p : prod' A B) : A * B :=
  match p with
  | mkpair a b => (a, b)
  end.

(*| Since there is only one constructor, we can also use `let`. |*)

Definition to_prod_alt {A B} (p : prod' A B) : A * B :=
  let 'mkpair a b := p in (a, b).

(*| We can also use a more generic notation that doesn't require remembering
the name of `mkpair`. It's maybe not as explicit so it's up to you to decide
which version you prefer. |*)

Definition to_prod_alt2 {A B} (p : prod' A B) : A * B :=
  let (a, b) := p in (a, b).

(*| Generally, one uses the projections directly.
They take the parameters as arguments so for convenience we declare them
as implicit. |*)

Arguments fst' {A B}.
Arguments snd' {A B}.

Definition to_prod_alt3 {A B} (p : prod' A B) : A * B :=
  (fst' p, snd' p).

(*|
.. raw:: html

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

..
|*)

(*| Show that `to_prod` and `to_prod_alt3` produce the same result. |*)

Lemma to_prod_eq :
  forall A B (p : prod' A B),
    to_prod p = to_prod_alt3 p.
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*| We can use records to represent more complex mathematical structures.
See for instance the following record representing monoids. |*)

Record monoid := {
  m_ty : Type ;
  m_ne : m_ty ;
  m_op : m_ty -> m_ty -> m_ty ;
  m_l_ne : forall x, m_op m_ne x = x ;
  m_r_ne : forall x, m_op x m_ne = x ;
  m_assoc : forall x y z, m_op (m_op x y) z = m_op x (m_op y z)
}.

(*| Again we can build these structures interactively using `refine`. |*)

Definition nat_monoid : monoid.
Proof.
  refine {|
    m_ty := nat ;
    m_ne := 0 ;
    m_op n m := n + m
  |}.
  - intro. reflexivity.
  - intro. rewrite <- plus_n_O. reflexivity.
  - intros x y z. rewrite Nat.add_assoc. reflexivity.
Defined. (*| We need `Defined` to access the fields! |*)

Compute nat_monoid.(m_ne). (*| Notation for `m_ne nat_monoid` |*)
Check nat_monoid.(m_op).

(*| We can prove things generically about monoids. |*)

Notation "a ** b" := (m_op _ a b) (at level 11, left associativity).

Check m_assoc.

Lemma monoid_fact :
  forall (M : monoid) (x y : M.(m_ty)),
    x ** M.(m_ne) ** y = x ** y.
Proof.
  intros M x y.
  (*| More complicated than necessary of course |*)
  rewrite m_assoc. rewrite m_l_ne. reflexivity.
Qed.

Lemma nat_fact :
  forall (x y : nat),
    x + 0 + y = x + y.
Proof.
  intros x y.
  apply monoid_fact with (M := nat_monoid).
Qed.

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Groups as records</summary>

..
|*)

(*|
Define a record for groups, building on the record for monoids.
Then show that `monoid_fact` also holds in groups.
|*)

Check monoid_fact.

(*|
.. raw:: html

   </details>

..
|*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Lists form a monoid</summary>

..
|*)

(*|
Show that lists form a monoid using `++` as operation.
How does `monoid_fact` translate to lists?
Note that, unlike `**` or `+`, `++` associates to the right,
meaning `x ++ y ++ z` stands for `x ++ (y ++ z)`.
|*)

Definition list_monoid (A : Type) : monoid.
Proof.
Admitted.

Lemma list_fact :
  forall A (x y : list A),
    (x ++ []) ++ y = x ++ y.
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*| Products of monoids also yield a monoid. |*)

Definition prod_monoid (M1 M2 : monoid) : monoid.
Proof.
  refine {|
    m_ty := M1.(m_ty) * M2.(m_ty) ;
    m_ne := (M1.(m_ne), M2.(m_ne)) ;
    m_op '(x,y) '(u,v) := (x ** u, y ** v)
  |}.
  - intros [x y]. rewrite !m_l_ne. reflexivity.
  - intros [x y]. rewrite !m_r_ne. reflexivity.
  - intros [x y] [u v] [a b]. rewrite !m_assoc. reflexivity.
Defined.

(*|
^^^^^^^^^^^^
Type classes
^^^^^^^^^^^^

Say we want to use our `monoid_fact` on pairs of natural numbers.
We can write the following:
|*)

Check monoid_fact (prod_monoid nat_monoid nat_monoid).

(*| But this doesn't tell us much.
If we want to write it by hand, it actually doesn't really work because
Rocq can't find the monoid structure on its own. |*)

Fail Lemma nat_nat_fact :
  forall (a b c d : nat),
    (a, b) ** (0, 0) ** (c, d) = (a, b) ** (c, d).

Lemma nat_nat_fact :
  forall (a b c d : nat),
    ((prod_monoid nat_monoid nat_monoid).(m_op) (a, b) (0, 0)) ** (c, d) =
    (prod_monoid nat_monoid nat_monoid).(m_op) (a, b) (c, d).
Proof.
  (*| It prints in a readable way, but we had to suffer to write our lemma! |*)
  intros a b c d.
  apply monoid_fact.
Qed.

(*|
The solution to this problem is called classes. It adapts the notion of
type classes one finds in functional programming languages such as Haskell.

Syntax is the same as for records but it is registered as a
special structure for Rocq. We move the carrier, neutral and operation as
parameters because Rocq will use them to guess which monoid structure we
mean. |*)

Class Monoid (A : Type) (neu : A) (op : A -> A -> A) := {
  mon_left_neutral : forall x, op neu x = x ;
  mon_right_neutral : forall x, op x neu = x ;
  mon_assoc : forall x y z, op (op x y) z = op x (op y z)
}.

(*|
`Instance` is a special command for definitions that register them as
things Rocq will use automatically if it has to find a value for
`Monoid nat 0 plus`.

Don't worry too much about the `export` thing. This is called an attribute
and it just means that if someone imports the file, then the instance will
still be available. We could instead use `#[local]` to restrict the instance
to the module. It does not matter for the course. |*)
#[export] Instance MonoidNat : Monoid nat 0 plus.
Proof.
  split.
  - intro. reflexivity.
  - intro. lia.
  - intros. lia.
Qed.

(*| A lemma we can prove using only the monoid structure on (ℕ,0,+).
See how Rocq infers which proofs we are talking about. |*)
Lemma test_nat :
  forall k n m, k + n + m + 0 = k + (n + m).
Proof.
  intros.
  rewrite mon_right_neutral.
  rewrite mon_assoc. reflexivity.
Qed.

(*| We can prove it in general on monoids with the same proof. |*)
Lemma test_monoid :
  forall M neu op `{Monoid M neu op} k n m,
    op (op (op k n) m) neu = op k (op n m).
Proof.
  intros.
  rewrite mon_right_neutral.
  rewrite mon_assoc. reflexivity.
Qed.

Lemma test_nat' :
  forall k n m, k + n + m + 0 = k + (n + m).
Proof.
  intros. apply test_monoid.
  (*| Rocq can use type class search to find instances on its own when we use `_` |*)
  exact _.
Qed.

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Product instance</summary>

..
|*)

(*| Complete the product instance. |*)

#[export] Instance MonoidProd :
  forall A B na nb opa opb,
    Monoid A na opa ->
    Monoid B nb opb ->
    Monoid (A * B) (na,nb) (fun '(xa,xb) '(ya,yb) => (opa xa ya, opb xb yb)).
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*| Now you can see that Rocq can infer complex monoid structures on its own! |*)
Definition foo : Monoid (nat * nat * nat) _ _ := _.
Print foo.

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Monoid instance for lists</summary>

..
|*)

(*|
Define an instance for lists and apply `test_monoid` to it.
Then check that Rocq can now find a monoid structure on
`list bool * nat * list nat`.

Hint: If asked for an instance of `Monoid`, you can always write `exact _`.
It will trigger class resolution and find it automatically (if you have a
corresponding instance).
|*)

Check test_monoid.

#[export] Instance MonoidList : forall A, Monoid (list A) [] (@app A).
Proof.
Admitted.

Lemma test_list :
  forall A (k n m : list A), ((k ++ n) ++ m) ++ [] = k ++ n ++ m.
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*| Here is another example of a class: decidable equality. |*)

Class Eq A := {
  eqb : A -> A -> bool ;
  eqb_iff : forall x y, eqb x y = true <-> x = y
}.

(*| Note: `` `{Eq A} `` is short for `{_ : Eq A}` -- i.e. we don't have to give it a
name. Indeed we don't care about the name of the instance because we don't
need to refer to it explicitly, Rocq finds it on its own. |*)

Fixpoint memb {A} `{Eq A} (x : A) (l : list A) : bool :=
  match l with
  | [] => false
  | y :: l => eqb x y || memb x l
  end.

Search (nat -> nat -> bool).

(*| Another useful tool is the `refine` attribute that also lets us give only
partial instances. Note that it only works for `Instance`, not `Definition`. |*)

#[export, refine] Instance Eq_nat : Eq nat := {|
  eqb := Nat.eqb
|}.
Proof.
  Search Nat.eqb.
  apply Nat.eqb_eq.
Defined. (*| We still need to use `Defined` though. |*)

Compute (eqb 0 1).
Compute (eqb 12 12).

Compute (memb 1 [ 3 ; 5 ; 1 ]).
Compute (memb 12 [ 3 ; 5 ; 1 ]).

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Specification of memb</summary>

..
|*)

(*|
Give `memb` a specification using the `In` predicate and show it correct with
respect to it.
|*)

Check memb.

(*|
.. raw:: html

   </details>

..
|*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Groups as a class</summary>

..
|*)

(*|
Define a class of groups and show uniqueness of neutral and inverse for all
groups.

Apply this result to a group of your choosing (you will have to provide an
instance). To apply a lemma, sometimes `apply` is not enough.
In this case you can use `eapply` which is more permissive. It creates
existential variables (starting with a question mark) corresponding to values
it couldn't guess. They are typically resolved as you prove the various
goals.

Can you show that every group forms a monoid (again, provide a generic
instance)?
|*)

(*|
.. raw:: html

   </details>

..
|*)

(*|
^^^^^^^^^^
Automation
^^^^^^^^^^

Classes are one form of automation. There are others in Rocq, the main one
being tactics. Indeed they can be used to derive properties automatically.
We will start by looking again at the `In` predicate.

We'll start by proving some easy lemmas. |*)

Lemma In_hd :
  forall A (x : A) l,
    In x (x :: l).
Proof.
  intros A x l.
  simpl. left. reflexivity.
  (*| Ok, this we already know, but we can use the `auto` tactic to deal with
      some of this. |*)
Abort.
Lemma In_hd :
  forall A (x : A) l,
    In x (x :: l).
Proof.
  intros A x l.
  simpl. auto.
Qed.

Lemma In_tl :
  forall A (x y : A) l,
    In x l ->
    In x (y :: l).
Proof.
  intros A x y l h.
  simpl. auto.
Qed.

(*| Now we would like `auto` to deal with `In` without the need to use `simpl`.
It should also be able to deal with more complex examples like the
following. |*)

Lemma In_4 :
  forall A (x a b c d : A) l,
    In x l ->
    In x (a :: b :: c :: d :: l).
Proof.
  intros A x a b c d l h.
  auto. (*| You can see it does nothing. |*)
  apply In_tl. apply In_tl. (*| This is annoying; let's use `repeat`: |*)
  repeat apply In_tl.
  auto.
Abort. (*| We don't need this lemma, so I abort in order not to save it. |*)

(*| Applying the lemma by hand is not very nice, and rather tedious.
We're going to declare hints so that `auto` knows how to use them.

In fact, we're first going to declare a new database of hints dedicated
to `In`. We call it `indb`, because why not? |*)

Create HintDb indb.

(*| We then add hints to the database using the `Hint Resolve` command.
Like for instances, we need to specify a locality. It doesn't matter so
we're going to go with `export` as before.
We then give it the name of a definition (or lemma etc.) and after the
colon the databases to which we want to add the hint. |*)

#[export] Hint Resolve In_hd : indb.

Lemma In_hd' :
  forall A (x : A) l,
    In x (x :: l).
Proof.
  intros A x l.
  auto. (*| It still doesn't work, because `auto` doesn't use `indb` by default. |*)
  auto with indb. (*| Now it does! |*)
Abort.

(*| If we do not use a `HintDb` Rocq automatically uses `core`, but this
behaviour is deprecated and will be removed. Instead, one should do so explicitly: |*)

#[export] Hint Resolve In_hd : core.

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Extending the hint database</summary>

..
|*)

(*|
Expand the database so that `auto with indb` is enough to solve the following
goals.

Note: `Goal` is like `Lemma` but it doesn't require a name. You won't be able to
reuse the proven goal afterwards, but it's useful to test things.

Recall the following lemmas from the lecture.
|*)

Check In_hd.
Check In_tl.

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

#[export] Hint Resolve In_tl : indb.

(*| |*)

Goal forall A (x a b c d : A) l,
  In x l ->
  In x (a :: b :: c :: d :: l).
Proof.
Admitted.

Goal forall A (x a b c d : A) l,
  In x (a :: b :: x :: c :: d :: l).
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Membership in concatenations</summary>

..
|*)

(*|
Show that `In x l` implies `In x (l ++ r)` and that `In x r` implies
`In x (l ++ r)`.

Now add both lemmas to `indb`. For the first time, we are introducing a choice
for `auto`: presented with the goal `In x (l ++ r)` it has to choose whether to
go left or right. It has no way to know in advance which one is better so it
will pick one and backtrack if it doesn't work.

Use it to solve the following two goals.
|*)

Lemma In_app_l :
  forall A (x : A) l r,
    In x l ->
    In x (l ++ r).
Proof.
Admitted.

Lemma In_app_r :
  forall A (x : A) l r,
    In x r ->
    In x (l ++ r).
Proof.
Admitted.

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

#[export] Hint Resolve In_app_l : indb.
#[export] Hint Resolve In_app_r : indb.

(*| |*)

Goal forall A (x a b c d : A) l l',
  In x l ->
  In x ([ a ; b ; c ] ++ l' ++ d :: l).
Proof.
Admitted.

Goal forall A (x a b c d : A) l l',
  In x l ->
  In x (l ++ [ a ; b ; c ] ++ l' ++ [ d ]).
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Equal elements</summary>

..
|*)

(*|
What if the element in my list is not syntactically what I'm looking for
but only equal to it?

Prove a lemma for this particular case and add a hint for it.
It should solve the following goal.
|*)

Goal forall A (x y a b c d : A) l l',
  x = y ->
  In x ([ a ; b ; c ] ++ l' ++ d :: y :: l).
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Domain-specific automation tactics
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|*)

(*| * `lia` |*)
(*| For linear integer arithmetic. Solves goals about `nat` / `Z` and addition,
sometimes multiplication. |*)

(*| * `congruence` |*)
(*| For equality. Solves goals about equality, knows about injectivity and
disjointness of constructors. |*)

(*| * `tauto` |*)
(*| For propositional logic. Solves (intuitionistic) propositional tautologies. |*)
(*| However, it's easy to use it for classical propositional logic as well: |*)

Axiom DNE : forall P : Prop, ~~ P -> P.

Goal forall p, p \/ ~ p.
Proof.
  intros. Fail tauto. apply DNE. tauto.
Defined.

(*| Or without manual work |*)
From Stdlib Require Import Classical.

Goal forall p, p \/ ~ p.
Proof.
  intros. tauto.
Defined.

(*| * `intuition` / `firstorder` |*)
(*| Uses the `tauto` algorithm and calls a tactic on the leaves.
`tauto` is `intuition fail`, i.e. no leaves allowed.
`intuition` is `intuition auto with core` |*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: The arith database</summary>

..
|*)

(*|
The equality in the exercise "Equal elements" is not always going to be an
assumption in the context. But it could be handled by some more automation.
There is for instance the `arith` database that can deal with arithmetic.

You can give two (or more) databases to `auto`. Check that it indeed succeeds
in the following goal with `arith` but not without.
|*)

Goal forall (a b c d : nat) l l',
  In (a + b) ([ b ; c ] ++ l' ++ d :: (b + a) :: l).
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Limits of arith</summary>

..
|*)

(*|
Sadly, it has its limits: check that it isn't sufficient for the following
goal even though you should be able to prove it (do it).

Hint: `lia` is stronger than `auto with arith` on that one.
|*)

Goal forall (a b c d : nat) l l',
  In (a + b + c) ([ a ; b ; c ] ++ l' ++ d :: (c + 0 + a + b) :: l).
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Using lia in auto (advanced)</summary>

..
|*)

(*|
There is a way to use `lia` with `auto` actually. For this we have to provide
a different kind of hint.
Using the command `Hint Extern` we can tell Rocq what tactic to try when
encountering a goal of the form `n = m` where `n, m : nat`.

Below what we do is say that when the goal is of the shape `@eq nat _ _`
then we apply `lia`. We add this to `indb`.
The 3 is something called cost. `auto` is actually cost-based and each action
it takes has a cost attached to it. `auto` will start by picking the actions
with the lowest cost when it has a choice. When it runs out of money, it
gives up.

Check that you can solve the previous goal using `auto with indb`.
Can you also make it so that the other goal works?
|*)

#[export] Hint Extern 3 (@eq nat _ _) => lia : indb.

Goal forall (a b c d : nat) l l',
  In (a + b + c) ([ a ; b ; c ] ++ l' ++ d :: (c + 0 + a + b) :: l).
Proof.
Admitted.

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

#[export] Hint Extern 3 (@eq Z _ _) => lia : indb.

(*| |*)

Goal forall (a b c d : Z) l l',
  In (a + b + c)%Z ([ a ; b ; c ] ++ l' ++ d :: (c + d + 0 + a - d + b) :: l)%Z.
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
^^^^^^^^^^^^^^^^^^^^^
Existential variables
^^^^^^^^^^^^^^^^^^^^^

We have seen `eapply` already. But many tactics come with an `e` version.
One such example is the `eexists` tactic that is very convenient. See below.
|*)

Goal forall n, n = 0 \/ exists m, n = S m.
Proof.
  intro n.
  destruct n.
  - auto.
  - right. eexists. reflexivity.
  (*| We're going to show the proof to see what value was picked for the
  existential variable. |*)
  Show Proof.
Qed.

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Existential variables</summary>

..
|*)

(*|
Solve the following goal without using any lemma or variable in the context
explicitly.
|*)

Goal forall A (x : A) l l',
  exists y, In y (l ++ x :: l').
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*| `auto` also has an `eauto` variant. You can use it when applying a
hypothesis requires guessing a variable that doesn't appear in the goal (like
`y` below).
It is generally slower than `auto` so you can use it when `auto` fails. |*)

Goal forall (P : nat -> nat -> Prop) (Q : nat -> Prop),
  P 4 2 ->
  (forall x y, P x y -> Q x) ->
  Q 4.
Proof.
  intros P Q hP h.
  apply h with (y := 2). assumption.
Qed.
Goal forall (P : nat -> nat -> Prop) (Q : nat -> Prop),
    P 4 2 ->
    (forall x y, P x y -> Q x) ->
    Q 4.
Proof.
  intros P Q hP h.
  eapply h.
  eassumption. (*| Notice how we need the `e` here too! |*)
Qed.
Goal forall (P : nat -> nat -> Prop) (Q : nat -> Prop),
    P 4 2 ->
    (forall x y, P x y -> Q x) ->
    Q 4.
Proof.
  eauto.
Qed.

(*|
.. raw:: html

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

..
|*)

(*| Solve the following goal. |*)

Goal forall A (P : A -> A -> Prop) (Q : A -> Prop),
  (forall x, exists y, P x y) ->
  (forall x y, P x y -> Q x) ->
  (forall x, Q x).
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Logical equivalences (advanced)</summary>

..
|*)

(*|
Another interesting feature of Rocq is the ability to rewrite on other things
rather than just equality.

For instance, we can use rewrite for logical equivalences.
Let us go through it step by step.

To begin, prove the following logical equivalences.
|*)

Lemma and_AA :
  forall A, A /\ A <-> A.
Proof.
Admitted.

Lemma or_AA :
  forall A, A \/ A <-> A.
Proof.
Admitted.

Lemma and_com :
  forall A B,
    A /\ B <-> B /\ A.
Proof.
Admitted.

Lemma or_com :
  forall A B,
    A \/ B <-> B \/ A.
Proof.
Admitted.

Lemma and_assoc :
  forall A B C,
    (A /\ B) /\ C <-> A /\ B /\ C.
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Rewriting with equivalences (advanced)</summary>

..
|*)

(*|
Now you can solve the following goals just by using rewrite on equivalences.
No more need for split!

Note that you can also use `reflexivity`, `symmetry` and `transitivity` on those.
Under the hood, this is using class resolution to find the proper instances.
For `iff` (logical equivalence) they are already registered so we can freely
use them.
|*)

Goal forall (A B C D : Prop),
  A /\ (B /\ B) /\ (C -> D) /\ (C -> D) <-> A /\ B /\ (C -> D).
Proof.
Admitted.

Goal forall (A B : Prop),
  (B /\ A /\ B) \/ (A /\ B) <-> B /\ A.
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Set equality on lists (advanced)</summary>

..
|*)

(*|
Ok, this is getting old. We're going to switch to another relation which isn't
already registered in the standard library.
First we're going to introduce a relation on lists that relates two lists
if they have the same elements (regardless of how many times they appear),
i.e., if they represent the same set.

Complete the following definition.
|*)

Definition list_set_eq {A} (u v : list A) : Prop :=
  REPLACE_ME.

Notation "u ~ v" := (list_set_eq u v) (at level 70).

(*|
We first need to show that the relation is reflexive, symmetric and
transitive. We do so by instantiating the right classes so that we can use
the corresponding tactics (as for `iff`).

Check it works with the provided goal.
|*)

From Stdlib Require Import Setoid.

#[export] Instance list_set_eq_refl :
  forall A, Reflexive (list_set_eq (A := A)).
Proof.
Admitted.

#[export] Instance list_set_eq_sym :
  forall A, Symmetric (list_set_eq (A := A)).
Proof.
Admitted.

#[export] Instance list_set_eq_trans :
  forall A, Transitive (list_set_eq (A := A)).
Proof.
Admitted.

Goal forall A (u v w : list A),
  v ~ u ->
  (u ~ u -> v ~ w) ->
  u ~ w.
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Rewriting with set equality (advanced)</summary>

..
|*)

(*|
We will use the following command to register this relation to use with
rewrite. Rocq will find the instances of equivalence relation we provided
above. Otherwise we could provide them manually.
Look up the documentation if you want to do that:
https://rocq-prover.org/doc/master/refman/addendum/generalized-rewriting.html

On the left of the colon we give the list of parameters, here there is only
one which is the type of values. We call it `A` and we can refer to it after
the colon.
The next argument is the type of elements we compare with the relation:
`list A`.
Then we give the relation itself: `list_set_eq`.
Finally we give a name to the setoid relation. This is for Rocq's internal use.

Prove the following goal using rewrite. This is just transitivity again but
this is to show you how it works on a simple example.
|*)

Add Parametric Relation A : (list A) list_set_eq as list_set_rel.

Goal forall A (u v w : list A),
  u ~ v ->
  v ~ w ->
  u ~ w.
Proof.
Admitted.

(*| Prove that `u ++ v ~ v ++ u`. |*)

Lemma list_set_eq_app :
  forall A (u v : list A),
    u ++ v ~ v ++ u.
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)

(*|
.. raw:: html

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

..
|*)

(*|
In order to rewrite this relation inside, *e.g.*, `In`, we have to first show
that `In` is invariant under `~`. In other words, that `u ~ v` implies
`In x u <-> In x v`.
We can use the following command to declare it. This will in turn let us
rewrite inside `In`.

Prove that we indeed have a morphism.
Prove the given goals using rewrite.
|*)

Add Parametric Morphism A (x : A) : (In x)
  with signature list_set_eq ==> iff
  as In_morph.
Proof.
Admitted.

Goal forall A (x : A) u v,
  In x (u ++ v) ->
  In x (v ++ u).
Proof.
Admitted.

Goal forall A (x a b c : A) u v,
  In x (u ++ [ a ; b ; c ] ++ x :: v).
Proof.
Admitted.

(*|
Look up the `Forall` predicate. Show that it is a morphism for `list_set_eq`.
Proceed to solve the following goal.
|*)

Goal forall u v w,
  let P n := exists m, n = 2 * m in
  Forall P (w ++ u ++ v) ->
  Forall P (u ++ v ++ w).
Proof.
Admitted.

(*|
.. raw:: html

   </details>

..
|*)