## Stream: math-comp users

### Topic: computation with `exact:`

#### Pierre Rousselin (Aug 18 2023 at 15:07):

I am currently following this file from the Math Comp School 2022. I am confused by the 4th reminder which is:

``````Goal forall m n, m.+1 == n.+1 -> m == n.
Proof.
move=> m n mEn.
exact: mEn.
Qed.
``````

I would not have thought of using `exact:` (probably by lack of habit) to simplify an hypothesis and conclude the proof in one go.
So my first question is how much more powerful is this `exact:` compared to `exact`? I also noticed that it also allows for silent unification.
The other thing which troubles me is that I could not compute more explicitly with `simpl` or `/=` in `mEn`. Maybe I did the wrong thing.

#### Pierre Roux (Aug 18 2023 at 15:41):

In fact, the power is not really in `exact: sth` which is just `by apply: sth` (so apply then ensure that this solves the goal) but in the computation power of `==` (in bool, compared to `=` in Prop). If you do

``````Goal forall m n, m.+1 == n.+1 -> m == n.
Proof.
move=> m n.
rewrite /eq_op/=.
(* eqn m n -> eqn m n *)
(* or with Set Printing All: is_true (eqn m n) -> is_true (eqn m n) *)
``````

and indeed if you `Print eqn`, you will see that `m.+1 == n.+1` computes to `m == n`. More generally, this is an example of the "small scale reflection" in the ssreflect name.

#### Pierre Rousselin (Aug 20 2023 at 09:29):

Thank you for your answer. So, if I understand correctly, `==` cannot be `simpl`ed manually, but Coq will silently compute that the types `m.+1 == n.+1` and `m == n` are convertible. Hence any proof stating that `mEn` is already a proof of the goal will be accepted.

#### Pierre Roux (Aug 21 2023 at 14:51):

Exactly. I guess the reason no simplification is done by default is that this requires unfolding `eq_op` (the function behind the notation `==`) and we don't have an easy way to refold it after the fact. So since we don't want `/=` to turn `m == n` into `eqn m n` we don't simplify anything.

Last updated: Jul 15 2024 at 20:02 UTC