REVISED: Tuesday, December 17, 2024
1. COQ'S MODULE SYSTEM PART 1
Coq's module system is a powerful tool for organizing and structuring large-scale formal developments. By breaking down complex proofs and definitions into smaller, modular components, modules promote code reusability, maintainability, and modularity.
Basic Module Structure:
A Coq module typically consists of:
Module Declaration:
Module MyModule. (* START MYMODULE *)
(* Module Body *)
End MyModule. (* END MYMODULE*)
Module MyModule. (* START MYMODULE *)
Module Body:
Definitions: Definition, Fixpoint, Inductive
Theorems: Theorem, Lemma, Proposition
Tactics: Proof, Qed
Other Modules: Nested modules
Importing and Exporting Definitions:
Import:
Import MyModule.
Imports all definitions from MyModule into the current scope.
Export:
Export MyModule.
Exports all definitions from MyModule to any module that imports it.
Example: A Simple Module for Natural Numbers
End MyModule. (* END MYMODULE *)
Module NatModule. (* START NATMODULE *)
(* Inductive definition of natural numbers *)
Inductive nat : Type :=
| O : nat
| S : nat -> nat.
(* Definition of addition on natural numbers *)
Fixpoint plus (n m : nat) : nat :=
match n with
| O => m
| S p => S (plus p m)
end.
End NatModule. (* END NATMODULE *)
Using the Module:
Import NatModule.
(* Example usage of the `plus` function *)
Theorem plus_comm : forall n m : nat, plus n m = plus m n.
Proof.
(* ... proof using the `plus` function from NatModule *)
Qed.
Advanced Module Features:
Module Parameters:
Module MyModule (A : Type). (* START MYMODULE *)
(* Module body using A *)
End MyModule. (* END MYMODULE *)
Allows for generic modules that can be instantiated with different types.
Module Signatures:
Define interfaces for modules, specifying the signatures of exported definitions.
Functors:
Higher-order modules that can transform other modules.
Example: A Generic List Module
Module ListModule (A : Type). (* START LISTMODULE *)
Inductive list : Type :=
| nil : list
| cons : A -> list -> list.
(* ... other list operations *)
End ListModule. (* END LISTMODULE *)
Using the Generic List Module:
Import ListModule.
(* Instantiate the module for natural numbers *)
Module NatList := ListModule(nat).
(* Use the `nil` and `cons` constructors for natural number lists *)
Definition my_list : NatList.list := NatList.cons 1 (NatList.cons 2 NatList.nil).
2. CONCLUSION
By effectively utilizing Coq's module system, you can organize your formal developments into well-structured, reusable components, making your proofs more modular, maintainable, and easier to understand.
3. REFERENCES
Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.
Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.
Goerzen, J. & O'Sullivan, B. & Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.
Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.
Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.
Pierce, Benjamin C., et al., editors. Logical Foundations. Vol. 1 of Software Foundations. Electronic Textbook, 2024. Version 6.7, http://softwarefoundations.cis.upenn.edu.
Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.
