The Coq mailing list

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

Hi,

> Indeed there was a proposal recently to remove axioms from the usual
> Require Import Program, but
> that in turn will force anyone who uses dependent destruction to
> explicitly Require Import Program.Equality.
> It's only Program.Tactics and Program.Wf that are necessary for Program
> to function correctly (IIRC, for 
> the default program_simpl tactic and well-founded fixpoint combinators).
> -- Matthieu

I would argue that this is a question of a slightly more general policy:
 Should libraries strive to provide as much functionality as possible
without importing any axioms?  Not just "Program" is affected here, but
also, e.g., Psatz and Eqdep_dec (the latter importing
Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq).  For the latter two, I currently
don't know of any way to obtain their functionality without importing
axioms, which makes them worse than Program.

If the answer is "yes", then being able to filter things in coqchk
becomes less pressing.  There's still the concern of libraries not
following this policy to the letter and having axiom-free useful stuff
in an "axiom-infected" module; maybe that's sometimes just easier to
structure.

Kind regards,
Ralf