I'm writing a fairly involved combinatorial function (Murnaghan–Nakayama rule). Before even trying to prove anything, I'd like to test it. I'd also like to keep the tests in the likely case I need to change the function, either to correct it or to improve its code for ease of proof or efficiency. Currently, I'm writing things like
Goal add_ribbon_start_stop [:: 2; 2; 1; 1] 0 0 2 = [:: 4; 2; 1; 1]. Proof. by . Qed. Goal add_ribbon_start_stop [:: 2; 2; 1; 1] 1 1 2 = [:: 2; 4; 1; 1]. Proof. by . Qed.
which fits the need, except that when I search for
add_ribbon_start_stop, the answer is cluttered with all the unnamed lemmas. Is there a recomanded practice for that ?
End with Abort rather than Qed.
Or, if you want to test for potential universe issues, end with
Fail Fail Qed. This is like
Qed without the side effects.
Thanks for the tip. For the
Fail Fail Qed. solution, I'm a little puzzled by the error message:
The command has indeed failed with message: The command has not failed!
Florent Hivert said:
I'm a little puzzled by the error message:
Well, the command
Fail Fail Qed. reports that the command
Fail Qed. has indeed failed with a message stating that the command
Qed. has not failed. :smile:
We will now have the
Succeed vernac command in 8.14 by the way. https://coq.github.io/doc/master/refman/proof-engine/vernacular-commands.html#coq:cmd.Succeed
Last updated: Feb 08 2023 at 08:02 UTC