Coq: Proving simple theorem using Fixpoints and Induction

Question

I am learning to use Coq right now and I have stumbled on a theorem I can't seem to prove. Below is the theorem and my current attempt.

  Fixpoint nateq (n m : nat) : bool :=
    match n with
      | O => match m with
              | O => true
              | S _ => false
            end
      | S n' => match m with
                 | O => false
                 | S m' => nateq n' m'
                end
    end.

  Theorem nateq_is_eq : ∀ n m : nat, nateq n m = true → n = m.
  Proof.
     admit.
  Admitted.

My attempt

  Theorem nateq_is_eq : ∀ n m : nat, nateq n m = true → n = m.
  Proof.
    intros n m H.
    induction n as [| n' IHn'].
    - induction m as [| m' IHm'].
      + reflexivity.
      + inversion H.
    - induction m as [| m' IHm'].
      + inversion H.
      + 
  Admitted.

My problem is in the final inductive step. The current state of my subgoals says the following:

1 subgoal
n', m' : nat
H : nateq (S n') (S m') = true
IHn' : nateq n' (S m') = true → n' = S m'
IHm' : nateq (S n') m' = true → (nateq n' m' = true → n' = m') → S n' = m'
______________________________________(1/1)
S n' = S m'

This all seems a bit convoluted. I would really appreciate any advice in the right direction.

Answer 1

Your induction hypothesis on n' is not general enough: to get the proof to go through, it needs to work for arbitrary m. The generalize dependent tactic can be used to solve this problem:

Require Import Coq.Unicode.Utf8.

Fixpoint nateq (n m : nat) : bool :=
    match n with
      | O => match m with
              | O => true
              | S _ => false
            end
      | S n' => match m with
                 | O => false
                 | S m' => nateq n' m'
                end
    end.

Theorem nateq_is_eq : ∀ n m : nat, nateq n m = true → n = m.
Proof.
intros n m H.
generalize dependent m.
induction n as [|n IH].
- destruct m; easy.
- destruct m as [|m]; try easy.
  simpl. intros H. specialize (IH _ H). congruence.
Qed.

In this case, you can avoid the problem altogether simply by leaving m on the context:

Theorem nateq_is_eq' : ∀ n m : nat, nateq n m = true → n = m.
Proof.
intros n. induction n as [|n IH].
- destruct m; easy.
- destruct m as [|m]; try easy.
  simpl. intros H. specialize (IH _ H). congruence.
Qed.

The Software Foundations book has a more detailed explanation on the generalize dependent tactic.