I'm studying the Logical Foundations textbook on my own, and in chapter 1, (https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html) there are a bunch of unit tests that look like:

```
Example test_orb1: (orb true false) = true.
Proof. simpl. reflexivity. Qed.
```

and, for another example,

```
Example test_odd1: odd 1 = true.
Proof. simpl. reflexivity. Qed.
```

My confusion comes on the simpl. step. For example test_orb1, (a test for testing a binary or definition) on the proof step, the subgoal looks like :

```
1 goal
______________________________________(1/1)
orb true false = true
```

and after the simpl step it looks like

```
1 goal
______________________________________(1/1)
true = true
```

This leads me to beleive that simpl runs the (orb true false) function and returns the result. Since orb true false simplifies to true, it makes sense to me that reflexivity would finish the proof, since reflexivity compares two sides to see if they are the same.

but for test odd 1, a test for testing if a number is odd, nothing happens on the simpl. step.

```
1 goal
______________________________________(1/1)
odd 1 = true
```

Why is it that (orb true false) can evaluate to true on the simpl. step, but (odd 1) can't evaluate to true on the simpl. step? What exactly is simpl. doing here, if it's not for evaluating a function? the two sides don't look equal on the subgoal, but after I run the reflexivity tactic the subgoal disappears, which, I guess, means that coq decided that odd 1 and true evaluated to the same thing?

In short, why did simpl change the subgoal when working with the orb defintion, and did not change the subgoal for the odd definition? More generally, why is simpl in all the testing examples in chapter 1 when a lot of the time nothing happens on that step?

And the answer to my question was a couple of paragraphs down: from `odd 1`

to quote the book,

```
(** (You may notice if you step through these proofs that
[simpl] actually has no effect on the goal -- all of the work is
done by [reflexivity]. We'll discuss why that is shortly.)
```

`simpl`

doesn't fully evaluate terms in a goal but rather heuristically simplifies the goal. Roughly, if there are more terms after unfolding and beta reducing (substituting function arguments) then `simpl`

won't progress. You can unfold terms in a goal directly with `unfold odd`

for example. If you want to fully evaluate the goal, you can use `cbv`

(which stands for call by value).

Here is some documentation on applying conversion rules from the Coq reference manual: https://coq.inria.fr/refman/proofs/writing-proofs/equality.html#applyingconversionrules

Last updated: Jun 18 2024 at 23:01 UTC