The Coq mailing list

["Jevgenijs Sallinens" <jevgenijs AT dva.lv>]

Pierre Casteran wrote:
> Do you mean to put in the module types such informations as
> _ind, _rec, _rect constructions, equalities related to iota-reductions
> and so on ? That can be a lot of information to write.


No, just opposite.
Inductive definitions and fixpoint operators, placed in module types
probably  doing exactly this, only implicitly. The problem with such an
approach,  probably is in the fact (actually I have no sufficient knowledge)
, that reduction mechanism couldn't unify two similar inductive definitions,
encoded in different places (for example one in a module type and another in
an implementation module).

With module type defined as follows there are no any of two problems
mentioned  (but certainly this interface is unusable).
Module Type I_Nat.
Parameter Nat:Set.
Parameter eq_Nat:Nat->Nat->bool.
End I_Nat.



For booleans, natural numbers and lists I have implementation where module
types contains description of these types (together with equality, similar
to Setoids) as parameters.
Additionally others parameters and axioms related with recursion and
induction are described.
As the price, most of standard tactics became unusable for such (maximized)
types.
Nevertheless, it was possible (by using Ltac) to write others tactics, doing
most frequent and complicated manipulation, with no too much additional
effort, compared with traditional proofs.
It is doing the coding more complicated, but (to my mind) harmony and
abstraction achieved are more important: module types are becoming real
interfaces for black boxes, containing implementation written in terms of
inductive types, so that usage of these interfaces in independent on which
inductive type could be used for their implementation.


I just tried to answer your question, but actually, I don’t know proper
answers, possible others more experienced people do.

Best wishes,
Jevgenijs,





________________________________________________
Message sent using UebiMiau 2.7.2