7
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ I'm a beginner with Coq. I'm trying to follow along with this example, but I couldn't figure out exactly what to import to prove forall m n : nat , m == n -> m = n. In particular, I'm not sure what to import to get == in scope. Can you please include an MCVE? $\endgroup$ Feb 15 at 20:37
  • 1
    $\begingroup$ @GregoryNisbet done $\endgroup$
    – CrabMan
    Feb 15 at 20:41

2 Answers 2

5
$\begingroup$

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.
$\endgroup$
6
  • $\begingroup$ I don't see how to get n1 = m1 from the two induction hypotheses in the last case. $\endgroup$
    – CrabMan
    Feb 15 at 18:37
  • $\begingroup$ The induction hypotheses are forall n, m1 == n -> m1 = n and S m1 == S n1 but the latter is definitionally equal to m1 == n1 so the former can be applied to n1 and the latter. $\endgroup$
    – Ihar Bury
    Feb 15 at 19:00
  • $\begingroup$ I get different induction hypotheses: forall n0 : nat, (n0 == n -> n0 = n) -> n0.+1 == n -> n0.+1 = n and m == n.+1 -> m = n.+1, while the goal is m.+1 == n.+1 -> m.+1 = n.+1. $\endgroup$
    – CrabMan
    Feb 15 at 19:02
  • $\begingroup$ When doing induction, you can put arguments to the local context instead of keeping them in the goal. SSReflect provides a convenient syntax for that: elim=> [| m1 hm] [| n1 hn]. $\endgroup$
    – Ihar Bury
    Feb 15 at 21:13
  • $\begingroup$ What a weird induction scheme you've proposed. In it, we start at (0, 0), can move any number of times to the right (from (x, 0) to (S x, 0)) OR any number of times up (from (0, y) to (0, S y)), and then any number of times along the main diagonal (from (x, y) to (S x, S y)). How did elim=> [| m1 hm] [| n1 hn]. turn into this? Is it possible to use different induction schemes as easily? Btw, it works, thanks. $\endgroup$
    – CrabMan
    Feb 15 at 21:39
4
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.