Stream: math-comp users

Topic: Best practice : keeping tests


view this post on Zulip Florent Hivert (Sep 04 2021 at 07:48):

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 ?

view this post on Zulip Enrico Tassi (Sep 04 2021 at 20:09):

End with Abort rather than Qed.

view this post on Zulip Janno (Sep 06 2021 at 09:14):

Or, if you want to test for potential universe issues, end with Fail Fail Qed. This is like Qed without the side effects.

view this post on Zulip Florent Hivert (Sep 14 2021 at 14:48):

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!

;-)

view this post on Zulip Christian Doczkal (Sep 14 2021 at 15:06):

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:

view this post on Zulip Ali Caglayan (Sep 14 2021 at 23:12):

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