REVISED: Tuesday, December 17, 2024
1. INTRODUCTION
What are Coq Constructors?
Building Blocks of Inductive Types:
In Coq, inductive types define new data structures. Constructors are the fundamental components used to construct values (or terms) of these inductive types.
Defining New Data:
Think of constructors as blueprints for creating specific instances of a data type. For example:
bool:
This built-in inductive type has two constructors: true and false. These are the only ways to create a value of type bool.
nat:
The natural numbers are defined inductively with two constructors:
O: Represents the number zero.
S: Represents the successor function (e.g., S O is 1, S (S O) is 2, and so on).
2. HOW TO USE CONSTRUCTORS
Define an Inductive Type:
Inductive my_list (A : Type) : Type :=
| Nil : my_list A
| Cons : A -> my_list A -> my_list A.
Nil is the constructor for an empty list.
Cons is the constructor to add an element (A) to the beginning of an existing list (my_list A).
This defines a new type called my_list.
A is a type parameter, meaning my_list can be a list of any type.
Compiling:
Inductive my_list (A : Type) : Type :=
| Nil : my_list A
| Cons : A -> my_list A -> my_list A.
The Messages window of CoqIDE shows:
my_list is defined
my_list_rect is defined
my_list_ind is defined
my_list_rec is defined
my_list_sind is defined
When you define an inductive type in Coq, the system automatically generates several useful definitions and principles:
my_list_rect: This is the general recursion principle for my_list. It allows you to define functions recursively on my_list by providing cases for Nil and Cons.
my_list_ind: This is the induction principle for my_list. It's used to prove properties about my_list by induction on its structure.
my_list_rec: This is a specialized recursion principle for defining functions on my_list. It's often more convenient to use than my_list_rect in many cases.
my_list_sind: This is a specialized induction principle for proving properties about my_list. It's often more convenient to use than my_list_ind in many cases.
In essence, the my_list type is a fundamental building block for defining various list-based data structures and algorithms in Coq.
Construct Values:
(* Example list of integers *)
Definition my_list_example : my_list nat :=
Cons 1 (Cons 2 (Cons 3 Nil)).
This creates a list containing the integers 1, 2, and 3.
Pattern Matching:
Constructors are essential for pattern matching in Coq, which allows you to define functions that operate on inductive types.
Fixpoint my_list_length (l : my_list A) : nat :=
match l with
| Nil => 0
| Cons _ tl => S (my_list_length tl)
end.
This function calculates the length of a list. It uses pattern matching to distinguish between the Nil case (empty list) and the Cons case (non-empty list).
3. CONCLUSION
By understanding the inductive definition and the generated principles, you can effectively work with lists in Coq proofs and program development.
Constructors are fundamental for defining and working with inductive types in Coq. They provide a structured way to create and manipulate data.
Pattern matching on constructors is crucial for defining functions that operate on inductive types.
Example:
Let's define a simple binary tree:
Inductive tree (A : Type) : Type :=
| Leaf : tree A
| Node : A -> tree A -> tree A -> tree A.
Leaf: Represents a leaf node (no children).
Node: Represents an internal node with a value (A) and two child subtrees.
4. 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.
