The Coq mailing list

[Peter Aczel <petera AT cs.man.ac.uk>]

Dear coq-club and coqdev members,

I would like to raise an issue concerning the standard library from a
different perspective.

I am sorry for the length of this email, which may not be of interest
to the more practically
preoccupied users of coq.

Let me first confess that, although I am familiar with dependent type
theory and have had
some interaction with coq (but more with lego) some time in the past,
it is only in the last
2,3 weeks that I have had the strong motivation to work with coq
again, because of the
mathematically very exciting developments of Vladimir Voevodsky, Steve
Awodey (the
independent originators) and others involving the interactions between
homotopy theory
and type theory and coq developments of machine checked proofs in type
theory based
on intuitions from homotopy theory.

For some years now I have suggested that it would be good if a
computer system like coq
implemented a (uninterpreted) logic enrichment of a basic type theory,
rather than having a
fixed treatment of logic.  At present the coq system has the fixed
interpretation of logic
using the impredicative sort Prop and the libraries are based on that
interpretation.
Propositions are types of sort Prop, implication is the -> operation
on the sort, universal
quantification is the Pi operation and the other logical operations
are inductive types.  But
there are many other ways of interpreting logic that may be
potentially important.for some
researchers.  Another interpretation would be to use a predicative
sort, following the
Martin-Lof treatment of logic.  Yet another would be to use a type
Bool, following the
classical treatment of logic.  But there are potentially many more via
re-interpretations of logic
via a J modal operator, only one example being the double negation
re-interpretation.

Voevodsky, in his coq files, wants to avoid the use of the sort Prop
and the standard library
treatment of logic and there are suggestions in his theoretical ideas
that a different
interpretation of logic, where propositions are his homotopy level 1
types.may be the way to
go.  Altthough this is still rather speculative, I am convinced that
it would be excellent if coq
could be modified so as to base its libraries, as much as possible, on
a logic-enriched type
theory.  This would enable some users to carry out experiments with
alternative interpretations
of logic.  I should add that, by logic I have in mind intuitionistic
dependently sorted logic with
equality, the sorts being the types of the basic type theory, the
basic type theory being
essentially the part of the type theory implemented in Coq, that does
not involve Prop.  Of
course, as well as the rules of inference for predicate logic one
would need to add the logical
induction rules for the inductive forms of type.

I do not expect that the coq team will want to modify the coq
treatment of logic in the short term,
but I hope that the issue can be kept open for discussion.  I suspect
that if the modification were
made it might be possible to re-adapt the libraries with a manageable effort.

In the meantime I have started to experiment with the implementation
of the notion of a logic in
coq, as it is.  At present I am not sure whether I want a module type,
record type or type class,
but am trying to develop a module type.  I am still learning to work
with notations and
interpretation scopes and other features of coq.

My main problem has been the need to avoid the standard library.

Is there a simple way to bypass the standard library??

Any suggestions for how to proceed would be welcome.  I want to have a
module type/record type/type class for the notion of a logic, relative
to a sort of the types for
the free and bound variables of the logic.  This would have Parameter
declarations for the logical
operations and rules of inference and proofs of logic theorems and
then implement different logics
as instances of the logic module type/record type/type class.

Best wishes,

Peter Aczel