# Simple Coq simplification question

I am working through Software Foundations, I had a question about the leb_refl theorem from the induction chapter. Here is my solution:

Theorem leb_refl : forall n:nat,
(n <=? n) = true.
Proof.
intros n. induction n as [| n' IHn'].
+ simpl. reflexivity.
(* Question: how does it know how to simplify? here *)
+ simpl. rewrite -> IHn'. reflexivity.


In the inductive step, the simpl command appears to rewrite the goal (S n' <=? S n') = true to (n' <=? n') = true using simplification. Intuitively, this is obvious (simply subtract one from both sides), but I was wondering what is happening in internally to make that jump? In general, how can I demystify what is happening when I use simpl?

What simpl does is compute the result of expressions that can be computed with the available information. For example, Eval simpl in (1 + 1). returns 2, but Eval simpl in (n + m). doesn't change anything because there is not enough information about n and m.

In order to answer your question about _ <=? _, check its definition. One way to find it is [*]:

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


Here we see that Nat.leb is defined recursively on the first argument and then on the second in such a way that the computation of S n <=? S m reduces to the computation of n <=? m. Not knowing anything else about n and m, simpl stops here.

[*] With Require Import PeanoNat. beforehand.