How to prove `forall m n : nat, m == n -> m = n`?

Question

I am learning Coq with ssreflect. Just to understand things, I've proved forall a b : bool, a == b -> a = b but I can't figure out how to prove forall m n : nat, m == n -> m = n. I've tried using the elim tactic first on m, then on n, but in the end I was left with a subgoal I couldn't prove. I've tried destruct m and then destruct n but the result was the same.

---

A minimal working example to try to prove this is

From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma eqn_impl_eq (m n : nat) (m_eqn_n : is_true (m == n)) : m = n.
Proof.
Admitted.

It uses mathcomp library though.

Answer 1

Induction can be used via elim tactic on both m and n, like this: elim=> [| m1 hm] [| n1 hn]. That results in 4 cases:

• 0, 0 case is trivial
• 0, S m1 case can be solved by contradiction via discriminate tactic applied to the boolean equality
• same for S n1, 0 case
• S n1, S m1 case can be solved by proving n1 = m1 first by applying induction hypothesis for both n and m. S m1 = S m1 can then be proved by f_equal.

Answer 2

SSReflect builds upon the relationship between booleans (m == n) and proposition (m = n); this is called reflection, hence the name. You can go from one to the other using the /eqP construct. In your case, one simple proof is thus to simply call for this functionality:

From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma eqn_impl_eq (m n : nat) (m_eqn_n : is_true (m == n)) : m = n.
Proof. exact/eqP. Qed.

You can learn more about this in the documentation, for instance this tutorial