Stream: Coq users

Topic: ✔ How to hide definitions of propositions?


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: Feb 05 2023 at 22:03 UTC