Pierre Rousselin (Aug 18 2023 at 15:07): 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 simpled 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: Oct 13 2024 at 01:02 UTC