The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi all,

I am working on a large-ish axiom-free Coq development. We recently got
coqchk to work on it (there were some stack overflows where coqchk
needed help to do the right conversions), and it outputs the following
(Coq 8.5pl2):

> CONTEXT SUMMARY
> ===============
> 
> * Theory: Set is predicative
>   Theory: Stratified type hierarchy
> 
> * Axioms:
>     Coq.Reals.Raxioms.total_order_T
>     Coq.Reals.Raxioms.Rmult_comm
>     iris.program_logic.model.iProp_solution.iProp_unfold_fold
>     Coq.Reals.Raxioms.Rmult_plus_distr_l
>     iris.program_logic.model.iProp_solution.iProp_fold_unfold
>     iris.program_logic.model.iProp_solution.iProp_unfold
>     Coq.Reals.Raxioms.completeness
>     Coq.Logic.ProofIrrelevance.proof_irrelevance
>     iris.program_logic.model.iProp_solution.iPreProp
>     Coq.Reals.Raxioms.Rlt_asym
>     Coq.Reals.Raxioms.Rplus_0_l
>     Coq.Logic.FunctionalExtensionality.functional_extensionality_dep
>     Coq.Reals.Raxioms.Rmult_assoc
>     Coq.Reals.Raxioms.Rlt_trans
>     Coq.Reals.Raxioms.R1_neq_R0
>     Coq.Reals.Raxioms.Rinv_l
>     Coq.Reals.Raxioms.Rmult_lt_compat_l
>     Coq.Reals.Rdefinitions.Rplus
>     Coq.Reals.Rdefinitions.Rmult
>     Coq.Reals.Rdefinitions.Ropp
>     Coq.Reals.Rdefinitions.Rinv
>     Coq.Reals.Rdefinitions.Rlt
>     Coq.Reals.Rdefinitions.up
>     Coq.Reals.Rdefinitions.R1
>     Coq.Reals.Rdefinitions.R0
>     Coq.Reals.Rdefinitions.R
>     Coq.Reals.Raxioms.Rmult_1_l
>     Coq.Reals.Raxioms.Rplus_comm
>     Coq.Reals.Raxioms.archimed
>     Coq.Logic.JMeq.JMeq_eq
>     Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq
>     Coq.Reals.Raxioms.Rplus_lt_compat_l
>     Coq.Reals.Raxioms.Rplus_opp_r
>     Coq.Reals.Raxioms.Rplus_assoc
>     iris.program_logic.model.iProp_solution.iProp_fold

For an axiom-free development, that's lots of axioms. Some of them
(those is iris.program_logic.model.iProp_solution) are actually names
sealed through an opaque module. I believe not showing them has been
discussed not-too-long-ago here on coq-club, but I don't recall the
consensus. Has this been fixed for 8.6, or should we report a bug?
Showing module names of a properly instantiated module interface as
"axioms" is at best confusing (and "Print Assumptions" doesn't show them).

What I am more surprised about is all these other axioms. I verified
using "Print Assumptions" that we're not actually using any of these, so
I think what's happening here is that "Program" (and potentially other
libraries) are importing axioms like PI or FE which we are not using,
but coqchk is still picking them up. (We're not doing anything with
reals, so I have no idea why they show up.) Is that correct? In that
case, coqchk would not be very useful as a tool to verify that no axioms
are used. (And with some tactics, like "dependent destruct", implicitly
using axioms, such a tool would indeed be useful!)

Is it even possible to use "Program", not use any axioms, and get coqchk
to report that no axioms are used?

My proposal here would be to only show axioms which are actually used by
a name exported by one of the modules passed to coqchk. Alternatively,
Program could provide means of importing the base functionality without
needlessly importing modules. What do you think?

Kind regards,
Ralf