Reasoning-level modules

A reasoning-level module is a parameterized namespace of kinds, constants, predicates, definitions, axioms, and theorems. Modules let a development share a theory across several type instances without repeating the declarations and proofs. They are stored in .thmod files or defined inline in .thm files.

Modules are a development-version feature. The released 2.0.8 documentation does not describe them.

Module files

A .thmod file contains exactly one top-level Module/End block. The module name must match the file base name:

List.thmod

Module List[T].
  Kind lst type.
  Type lnil lst.
  Type lcons T -> lst -> lst.
  Type contains T -> lst -> prop.
End List.

The parameter list [T] declares schematic type variables. They are replaced by the type arguments supplied at each import. Parameters are not exported as items.

The Kind lst type declaration creates a fresh internal type in every module instance. Two imports of the same module therefore have distinct lst types, while the parameter occurrences are instantiated at the supplied types.

Nested modules use the same Module/End form and may have their own parameters:

Module Nested[T].
  Type p T -> prop.
  Module Inner[U].
    Kind inner type.
    Type mk U -> inner.
    Type q U -> prop.
  End Inner.
  Import Module I = Inner[T].
End Nested.

Items of a nested module are reached through the import alias, as in N.I.inner.

Importing a module

Import Module loads a module into the current development. A quoted target names a .thmod file without its extension:

Import Module N = "List"[nat].
Import Module B = "List"[bool].

The name before = is an alias and becomes the prefix for the imported items. Without an alias, the target module's name is used as the prefix. A parameterized module requires a type argument list in the order of its parameters. A non-parameterized module is imported without brackets.

An unquoted target names a module already in scope, such as a nested module or an existing instance:

Module Counter.
  Kind counter type.
  Type zero counter.
  Type succ counter -> counter.
  Type positive counter -> prop.
End Counter.

Import Module C = Counter.

An existing instance is already instantiated, so supplying brackets to it is an error.

After import, items are selected with a qualified name. If N is the alias for List at type nat, the declarations are N.lst, N.lnil, N.lcons, and N.contains.

The same module may be imported several times. Each instance has its own internal kind types, so N.lst and B.lst in the example above are different types even though both come from List.

Mapping predicates and axioms

A with clause substitutes declared predicates and axiom items in the imported module:

Module Eq[T].
  Type eq T -> T -> prop.
  Axiom refl : forall (x:T), eq x x.
End Eq.

Module EqUse.
  Kind nat type.
  Type z nat.
  Define nat_eq : nat -> nat -> prop by
    nat_eq X X.
  Theorem nat_eq_refl : forall (x:nat), nat_eq x x.
  intros. search.
  Import Module E = "Eq"[nat] with eq := nat_eq, refl := nat_eq_refl.
End EqUse.

Mapped predicates are removed from the imported instance and their values are not re-exported. Mapped axioms become aliases that carry the value's tag: an axiom may be mapped to a theorem, or to another axiom. Unmapped declared predicates and axioms remain as keys and may be mapped by a later aliased re-import.

Key names are relative to the target, including dotted names for modules that the target imported.

Inline modules

A .thm file, or interactive input, may define modules directly:

Module Counter.
  Kind counter type.
  Type zero counter.
  Type succ counter -> counter.
  Type positive counter -> prop.
  Axiom one_pos : positive (succ zero).
End Counter.

Import Module C = Counter.
Type one C.counter.

Inline modules are local to the file or session. They are not exported by the .thc artifact, so another development cannot import them from the compiled file.

Showing a module

Show Module prints a summary of a module:

Show Module Counter.
Show Module C.
Show Module "List".

The first form shows an in-scope module, the second an imported instance, and the third a module loaded from a .thmod file. The summary lists kinds, types, definitions, axioms, and theorem statements without proofs.

Restrictions

Modules enforce several restrictions:

• Specification, ordinary Import, Close, Suspend, Quit, and Abort are not allowed inside a module.
• Declared predicates may not take an argument of type prop.
• Stratification findings are hard errors.
• A .thmod file may not use specification-logic sequents ({ ... }). An inline module in a .thm file may use them.

Imports check that substituted predicates and axioms have the same types and statements as the keys they replace. A compiled .thmod is stored in a .thmodc file beside the source.

Examples

The distribution contains the following module examples in examples/modules/:

• List.thmod and ListUse.thm: a parameterized list theory imported at two element types.
• Box.thmod and BoxUse.thmod: two instances of a module with an internal kind, showing distinct internal types.
• Nested.thmod and NestedUse.thmod: a nested parameterized module.
• Eq.thmod, EqUse.thmod, and EqUseDecl.thmod: an abstract predicate and axiom mapped to defined and declared predicates and theorems or axioms.
• PropKey.thmod and PropKeyUse.thmod: zero-argument predicate keys.
• Keys.thmod and KeysUse.thmod: unmapped keys and an aliased re-import.
• ShowModule.thm: inline and imported module summaries.

The examples/modules/README.md file has further details and a list of expected error cases.