<p>What <code>simpl</code> does is compute the result of expressions that can be computed with the available information. For example, <code>Eval simpl in (1 + 1).</code> returns <code>2</code>, but <code>Eval simpl in (n + m).</code> doesn't change anything because there is not enough information about <code>n</code> and <code>m</code>.</p>
<p>In order to answer your question about <code>_ &lt;=? _</code>, check its definition. One way to find it is [*]:</p>
<pre><code>Locate &quot;_ &lt;=? _&quot;.
(* Notation &quot;x &lt;=? y&quot; := (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 =&gt; true
  | S n' =&gt; match m with
            | 0 =&gt; false
            | S m' =&gt; leb n' m'
            end
  end
     : nat -&gt; nat -&gt; bool
*)
</code></pre>
<p>Here we see that <code>Nat.leb</code> is defined recursively on the first argument and then on the second in such a way that the computation of <code>S n &lt;=? S m</code> reduces to the computation of <code>n &lt;=? m</code>. Not knowing anything else about <code>n</code> and <code>m</code>, <code>simpl</code> stops here.</p>
<hr />
<p>[*] With <code>Require Import PeanoNat.</code> beforehand.</p>

CC BY-SA 4.0
2024-06-07T00:03:41.187Z
2024-06-07T00:03:41.187Z
Ana Borges
<p>I am working through Software Foundations, I had a question about the leb_refl theorem from the induction chapter. Here is my solution:</p>
<pre><code>Theorem leb_refl : forall n:nat,
  (n &lt;=? n) = true.
Proof.
  intros n. induction n as [| n' IHn'].
  + simpl. reflexivity.
    (* Question: how does it know how to simplify? here *)
  + simpl. rewrite -&gt; IHn'. reflexivity.
</code></pre>
<p>In the inductive step, the simpl command appears to rewrite the goal  (S n' &lt;=? S n') = true to (n' &lt;=? 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?</p>

<coq>
Simple Coq simplification question
whatisit
# Simple Coq simplification question

(Asked by: username_0 on 2024-06-06)

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?

**Tags:** coq


---

## 1 answers

### Answer by username_1 on 2024-06-07. Score: 0 | Accepted answer

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.


---

