liamoc / holbert Goto Github PK

Support for multi-document "books" and libraries is becoming necessary, but a number of design options present themselves.

• Book-style: Each document is a chapter in the book, and Chapters 1 through N-1 are implicitly imported by Chapter N. Simple to implement but not very flexible. Also heavily pollutes the namespace of later chapters and may cause performance issues if large-scale formalisations are conducted.
• Isabelle-style: Each module is in a flat namespace. Modules can be imported by other modules, but the import graph is always a DAG and the order of processing is linearised into topological order. The book table of contents is just an ordering on these modules, and doesn't have any impact on the import graph.
• More sophisticated options: First class or parameterised modules/locales, etc. This could be integrated with things like typeclasses etc. later too. However, this would stray the furthest from straightforward textbook-style presentation of material, and risks introducing concepts that are too Holbert-specific and would make Holbert materials too focused on Holbert as a tool rather than their intended subject matter.

Some technical considerations: Currently the set of available theorems and syntax declarations is taken just by taking the prefix of the current document before the current entry. Therefore changes to a theorem definition are just propagated to the suffix of the document after its definition (wiping invalidated proofs). To support very large developments, we'd have to extend this mechanism to traverse the entire import graph. This is potentially slow. I'm not sure what solution there is.

Gist demonstrating the issue: https://gist.github.com/plt-amy/a6d38244540ce1c4f5d928c164c6dcbc
Try applying the pi-elim rule; You'll see that the first goal we obtain is for a derivation of

p : (Π (? a A p) (x. T a))

rather than the

p : (Π (? a A p) (x. T (? a A p x)))

I would expect. I wish I could be more specific about the title.