Tara Roys (Mar 14 2022 at 20:05): Tara Roys (Mar 14 2022 at 20:05):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?
Tara Roys (Mar 14 2022 at 20:16):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: Oct 03 2023 at 04:02 UTC