1
$\begingroup$

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?

$\endgroup$

1 Answer 1

0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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