REVISED: Tuesday, November 12, 2024
1. COQ RECURSIVE FUNCTION EXAMPLE
Fixpoint even (n:nat) : bool :=
match n with
| O => true
| S O => false
| S (S n') => even n'
end.
To understand the Coq program's Vernacular Commands and Tactics let's break down the above Coq program and explain each component:
1.1. Fixpoint even (n:nat) : bool :=
Fixpoint: This keyword declares a recursively defined function. In this case, we're defining a function named even that takes a natural number n as input and returns a boolean value.
(n:nat): This specifies that the input parameter n is of type nat, which represents Natural Numbers in Coq.
: bool: This indicates that the function even returns a value of type bool, which represents boolean values (true or false).
1.2. match n with
match: This keyword introduces a pattern-matching construct. It allows us to define the behavior of the function based on different cases of the input n.
1.3. | O => true
| O: This is a pattern that matches the case when n is zero.
=> true: If the pattern matches, the function returns true.
1.4. | S O => false
| S O: This pattern matches the case when n is the successor of zero, i.e., one.
=> false: If the pattern matches, the function returns false.
1.5. | S (S n') => even n'
| S (S n'): This pattern matches the case when n is the successor of the successor of some natural number n'.
=> even n': If the pattern matches, the function recursively calls itself with the argument n'.
2. Reasoning Behind the Program
The even function is designed to determine whether a given natural number is even or odd. It works as follows:
2.1. Base Cases:
If n is zero, it's considered even, so the function returns true.
If n is one, it's considered odd, so the function returns false.
2.2. Recursive Case:
If n is greater than one, we can express it as the successor of another natural number n'.
The parity of n is the opposite of the parity of n'. Therefore, we can recursively call the even function on n' and negate the result.
In essence, the even function recursively checks if a number is even by repeatedly subtracting 2 until it reaches 0 or 1.
2. CONCLUSION
This is a classic example of a recursive function in Coq, demonstrating how pattern matching and recursion can be used to define complex functions in a concise and elegant manner.
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.
