Reflexive tactics for algebra, revisited

This archive corresponds to the paper "Reflexive tactics for algebra, revisited" by Kazuhiko Sakaguchi, accepted for publication in proceedings of ITP 2022. It contains the following supplementary materials. Note that CC-BY 4.0 applies only to the first two items below. zmodule.v contains the running example and other illustrations that appeared in Section 2.1, 2.3, 2.4, 3, 4, and 5.2. parametricity.v demonstrates that reification by small-scale reflection (Section 3.2) can be adapted to reification by parametricity as mentioned in Section 6. algebra-tactics/ is Algebra Tactics release 1.0.0, licensed under the CeCILL-B free software license agreement, also available on GitHub. apery/ is a snapshot of the formal proof of Apery's theorem (commit hash: 16f2cbe8e9415817bf012ee5de4ae9700429a599) authored by Chyzak, Mahboubi, and Sibut-Pinote, and licensed under the CeCILL-C free software license agreement. This is also available on GitHub. apery-remove-tests.patch and apery-algebra-tactics.patch are patch files (licensed under CeCILL-C) for the formal proof of Apery's theorem, required to reproduce the result of the performance comparison presented in Section 5.3. We recommend using Coq Platform 2022.04.0 to install dependencies. Particularly, using the following versions of packages is critical to achieving the expected performance: coq.8.15.1, coq-elpi.1.13.0, coq-mathcomp-ssreflect.1.14.0. Before following the instructions below, set the OPAM switch to one created by the Coq Platform: $ opam switch __coq-platform.2022.04.0~8.15~2022.04 $ eval $(opam env) To install Algebra Tactics 1.0.0: $ (cd algebra-tactics && opam install .) OR $ opam install coq-mathcomp-algebra-tactics.1.0.0 To compare the performance of two compilations of Apery, follow the instruction below: $ cd apery/ $ # Remove test suite for tactics: $ patch -p1 < ../apery-remove-tests.patch $ # Measure the compilation time, without Algebra Tactics: $ make make-pretty-timed-before $ # Make use of our ring and field tactics: $ patch -p1 < ../apery-algebra-tactics.patch $ # Make sure all .vo files will be rebuilt: $ touch theories/*.v $ # Measure the compilation time, with Algebra Tactics: $ make make-pretty-timed-after $ # Print the table of timing changes between the two compilations: $ make print-pretty-timed-dif