Why S n' =? S n' simplifies to n' =? n' in Coq?

Question

I'm a beginner in Coq, and I've seen other examples when, if you have S n' on both sides of an equality, using the tactics simpl removes the successor function of both sides and simplifies them to n'.

Although it seems "obvious", I'm wondering why it happens with this specific function (successor). Is this behavior stated by any axiom or something like that?

Answer

That's because _ =? _ is defined by structural recursion on both arguments.

Require Import Arith.
Locate "_ =? _".
Notation "x =? y" := (Nat.eqb x y) : nat_scope
  (default interpretation)
Print Nat.eqb.
Nat.eqb = 
fix eqb (n m : nat) {struct n} : bool :=
  match n with
  | 0 => match m with
         | 0 => true
         | S _ => false
         end
  | S n' =>
      match m with
      | 0 => false
      | S m' => eqb n' m'
      end
  end
     : nat -> nat -> bool

Arguments Nat.eqb (_ _)%nat_scope

When you use simpl, you're computing _ =? _, same as you're computing every other function that simplifies.

Note that there are two equalities for natural numbers: _ = _ lives in Prop and checks whether two terms are exactly the same, "character for character", so to say. _ =? _ is defined as above. They behave exactly the same [*], as the following theorem states:

Nat.eqb_eq
     : forall n m : nat, (n =? m) = true <-> n = m

However, they aren't defined in the same way (they don't even have the same type signature).