Stream: Coq users

Topic: ✔ How to hide definitions of propositions?

view this post on Zulip Tiago Cogumbreiro (Oct 27 2022 at 14:20):

I want to distribute a theory, but I want to hide how it's internally defined. Are module types the way to go?

For instance, let us say I have the following module and I want to hide from my users that Even was defined inductively, is the "proper" way to do this by declaring a module type?

Module A.
  Inductive Even : nat -> Prop :=
  | even_z: Even 0
  | even_s_s n: Even n -> Even (S (S n)).

End A.

Module Type IA.
  Parameter Even : nat -> Prop.
  Axiom even_z : Even 0.
  Axiom even_s_s: forall n, Even n -> Even (S (S n)).
End IA.

Module A_Impl : IA.
  Inductive t : nat -> Prop :=
  | t1: t 0
  | t2 n: t n -> t (S (S n)).
  Definition Even := t.
  Definition even_z := t1.
  Definition even_s_s := t2.
End A_Impl.

view this post on Zulip Michael Soegtrop (Oct 27 2022 at 14:59):

This is definitely a good option. Another possible approach is to use a Record / typeclass / canonical structure with the same information. You can then open a section, where you add a Variable of this Record type. The lemmas you prove in this section get the record as parameter when you close the section.

view this post on Zulip Michael Soegtrop (Oct 27 2022 at 15:04):

IMHO Modules are easier to get started with, while a Record / typeclass / canonical structure approach is more flexible, since Records can be computed by Coq (Gallina) functions, while the Module system is on top of Gallina.

view this post on Zulip Michael Soegtrop (Oct 27 2022 at 15:05):

For large developments Modules are easier to handle, though. I personally frequently use Modules to instantiate complicated Records.

view this post on Zulip Tiago Cogumbreiro (Oct 27 2022 at 15:30):

Thank you, @Michael Soegtrop!

view this post on Zulip Paolo Giarrusso (Oct 27 2022 at 22:58):

Modules are the best technology for "sealing", indeed: in your example, you can replace Even by Even n := True and rest assured client proofs will still typecheck (except maybe with universe constraints)

view this post on Zulip Michael Soegtrop (Oct 28 2022 at 08:04):

To add a bit on what Paolo said: with the Module system you can decide to hide certain aspects even when the module is instantiated (not abstract). That is you can restrict the signature of an instantiated module to a Module Type and strip away all details not mentioned in the Module Type. With Records you can't do this - if you have an instantiated record you can unfold the definitions in it (unless you play some extra tricks).

But what you can do with Records, as I said, is to work with a Record Variable in a Section. Then the Record is abstract and you obviously can't look into it.

Usually one wants this kind of abstraction for two reasons:

IMHO one can achieve both equally well with Records and Modules.

Typeclasses and Canonical Structures are btw. mechanisms to automatically supply records for implicit record parameters e.g. created by a Variable Record in a Section.

view this post on Zulip Notification Bot (Oct 28 2022 at 17:01):

Tiago Cogumbreiro has marked this topic as resolved.

view this post on Zulip Tiago Cogumbreiro (Oct 28 2022 at 17:03):

@Michael Soegtrop thank you for the detailed and clear answer!

view this post on Zulip Paolo Giarrusso (Oct 28 2022 at 21:54):

Michael's discipline with records works, but it seems less robust in one regard: it's only opt-in abstraction, so Coq won't tell you if in fact some module chooses to break it. It's probably not a problem if all devs are disciplined.

view this post on Zulip Paolo Giarrusso (Oct 28 2022 at 21:54):

(which is harder in larger teams, but YMMV).

view this post on Zulip Michael Soegtrop (Oct 29 2022 at 09:03):

Yes this is true. With Records you explicitly have to abstract things with e.g. a Section Variable or simply a premise, while with Modules you cannot access things the designer of a library denied to give you.

I guess the main reason I ended up using records - and using modules mostly for constructing complicated records with 10s of lemmas - is that when I do reflective automation at some point I need a gallina function which returns the record corresponding to a certain construct based on on the abstraction of this construct. Say I have an inductive which enumerates the various integer types in C (short, int, long, int128 X signed, unsigned ...) and have records with definitions and lemmas about the arithmetic in this type and a function which matches over the inductive and returns the corresponding record. Another example are the records which describe the various rings and fields in Coq and are used by the ring and field tactic. With modules the only way to do this is to integrate the tactic into the module. With rings and fields this would probably work - one would end up with separate tactics for Q and R which is not nice but OK. But things get tough when there are recursive dependencies - say mixing different int types in one C expression. One would need recursively dependent modules to write a tactic which can handle this, which does not work. With records this is not much of an issue.

So at some point I always needed the additional flexibility offered by records in one way or another.

Having said that, it is a good idea to start with modules - when you create records say for a ring or a C integer arithmetic you will anyway need modules to create such records. Doing this directly is quite a pain (there is currently another thread discussing this). When you find you need the records, it is relatively pain free to just construct a record from the contents of the module inside the module and use the module system to instantiate your complicated records. You can still use gallina record functions to construct derived records from these module generated records.

Please note that there are also developments which create complicated records directly - e.g. the mathematical components library. I am not an expert here, but I would say they build deep hierarchical structures of not too complicated records to manage the complexity. Meanwhile there is a dedicated tool for that, though: Hierarchy Builder. I can't really tell from which level of complexity on HB is better than the module system for creating records. I didn't reach the level where the module system is painful for creating records. I can see it at the horizon, but not necessarily in the direction I am walking.

Last updated: Jun 18 2024 at 20:02 UTC