REVISED: Wednesday, December 18, 2024
1. COQ'S MODULE SYSTEM PART 2
Require Import ZArith.
Require Import Lia.
Module MyModule.
(* A simple definition within the module. *)
Definition my_nat : nat := 5.
(* A function definition. *)
Definition increment_by_two (n : nat) : nat := n + 2.
(* A theorem (or lemma) within the module. *)
Theorem add_two_positive : forall n : nat, increment_by_two n > n.
Proof.
intros n.
simpl. (* Simplifies increment_by_two n to n + 2. *)
lia. (* Uses the lia tactic to prove the inequality. *)
Qed.
(* Another definition, using the previous one. *)
Definition my_other_nat : nat := increment_by_two my_nat.
(* A record definition (like a struct or class). *)
Record point : Type := {
x : nat;
y : nat
}.
(* A function operating on records. *)
Definition move_point (p : point) (dx dy : nat) : point :=
{| x := p.(x) + dx; y := p.(y) + dy |}.
(* Example usage of the record and function. *)
Definition my_point : point := {| x := 3; y := 7 |}.
Definition moved_point : point := move_point my_point 1 2.
End MyModule.
(* Using the definitions from the module. *)
Compute MyModule.my_nat. (* Output: 5 *)
Compute MyModule.add_two 10. (* Output: 12 *)
Compute MyModule.my_other_nat. (* Output: 7 *)
Compute MyModule.moved_point. (* Output: {| x := 4; y := 9 |} : point *)
(* Demonstrating module inclusion/import. *)
Module AnotherModule.
Import MyModule. (* Brings all definitions from MyModule into scope. *)
Compute my_nat. (* Now accessible directly. Output: 5 *)
Compute move_point my_point 5 5. (* Output: {| x := 8; y := 12 |} : point *)
(* Showing that you can redefine things locally without affecting the original module. *)
Definition my_nat : nat := 100. (* This only redefines my_nat *within* AnotherModule. *)
Compute my_nat. (* Output: 100 *)
Compute MyModule.my_nat. (* Output: 5 (MyModule is unchanged) *)
End AnotherModule.
(* Demonstrating module types (interfaces). *)
Module Type PointInterface.
Parameter point : Type.
Parameter make_point : nat -> nat -> point.
Parameter get_x : point -> nat.
Parameter get_y : point -> nat.
End PointInterface.
Module PointImplementation : PointInterface.
Record point : Type := { x : nat; y : nat }.
Definition make_point x y := {| x := x; y := y |}.
Definition get_x p := p.(x).
Definition get_y p := p.(y).
End PointImplementation.
Module AnotherPointImplementation : PointInterface.
(* A different implementation of points using lists *)
Definition point := list nat.
Definition make_point x y := [x;y].
Definition get_x p := List.nth 0 p 0. (* Default 0 if out of bounds *)
Definition get_y p := List.nth 1 p 0.
End AnotherPointImplementation.
Explanation:
Module MyModule. and End MyModule.: These keywords define the beginning and end of a module named MyModule. Modules act as namespaces, grouping related definitions (constants, functions, theorems, records, etc.) together.
Definition my_nat : nat := 5.: This defines a constant my_nat of type nat (natural number) with the value 5.
Definition increment_by_two (n : nat) : nat := n + 2.: This defines a function increment_by_two that takes a natural number n as input and returns a natural number n + 2.
Theorem add_two_positive : forall n : nat, increment_by_two n > n.: This declares a theorem named add_two_positive. forall n : nat means "for all natural numbers n." The theorem states that for any natural number n, increment_by_two n is greater than n.
Proof. ... Qed.: This block contains the proof of the theorem.
intros n. introduces the universal quantifier n into the context.
simpl. simplifies the expression increment_by_two n to n + 2.
lia. is a powerful tactic that automatically proves inequalities in Presburger arithmetic (linear arithmetic over integers and natural numbers).
Record point : Type := { ... }.: This defines a record type called point. Records are similar to structs or classes in other programming languages. They allow you to group related data together. In this case, a point has two fields: x and y, both of type nat.
p.(x): This is the syntax for accessing the field x of a record p.
{| x := ...; y := ... |}: This is the syntax for constructing a record value.
Compute MyModule.my_nat.: This command computes the value of my_nat within the MyModule namespace. The output will be 5.
Import MyModule.: This statement within AnotherModule imports all definitions from MyModule into the current scope of AnotherModule, allowing you to use them directly without the MyModule. prefix.
Redefinition within a module: As shown in AnotherModule, you can redefine names (like my_nat) locally within a module after importing another. This creates a shadowing effect. The local definition takes precedence within the module where it's redefined, without altering the original definition in the imported module.
Module Types (Interfaces): Module Type PointInterface. defines an interface for a point module. It specifies the signatures (types) of the functions and parameters that a module implementing this interface must provide. Module PointImplementation : PointInterface. and Module AnotherPointImplementation : PointInterface. show two different ways of implementing such interface. This is very powerful for code organization, modularity, and abstraction, as it allows you to swap implementations without changing the code that uses these modules.
2. CONCLUSION
Coq modules are crucial for developing larger and more complex Coq projects, enabling better organization, maintainability, and reusability of code.
Key Takeaways about Coq Modules:
Namespaces: Modules provide namespaces to organize code and avoid name collisions.
Encapsulation: They encapsulate definitions, preventing accidental modification from outside the module (unless explicitly imported).
Code Reusability: Modules promote code reusability by allowing you to import and use definitions in other modules.
Abstraction and Interfaces: Module types enable abstraction by defining interfaces that different modules can implement, promoting modularity and code maintainability.
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.
