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.

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.

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.

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