COQ RECURSIVE FUNCTION EXAMPLE

REVISED: Saturday, September 6, 2025

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.

COQIDE PROOF BY INDUCTION

REVISED: Saturday, September 6, 2025

1. COQIDE PROOF BY INDUCTION

If [P(n)] is some proposition P, involving a natural number [n], and we want to show that [P] holds for all numbers, we can reason like this:

  - Show that [P(O)], the base case,  holds.

  

  - Show that, if [P(n')] holds, then so does [P(S n')], the successor of n', 1+n'. The inductive case holds.

  

  - Conclude by the principle of induction that [P(n)] holds for all [n]. All cases hold.

Example:

Theorem add_O_r : forall n : nat,

     n + O = n.

Proof.

     intros n. induction n as [ | n' IHn' ].

      - (* n = O *) reflexivity.

      - (* n = S n' *) simpl. rewrite -> IHn'. reflexivity.

Qed.

Compile:

Theorem add_O_r : forall n:nat,

     n + O = n.

As you can see, the above Theorem named add_O_r says that for all n that are Natural Numbers n + O = n, (Recall, if you will, Coq represents the number zero as O.)

Depending on the selections you made in your CoqIDE "view" drop-down tab, when the above Theorem compiles in the CoqIDE and turns green, the goals window will show the following:

1 goal

______________________________________(1/1)

forall n : nat, n + 0 = n

Compile:

Proof.

   intros n. 

After Proof. and intros n. compile and turn green the goals window will show the following:

1 goal

n : nat

______________________________________(1/1)

n + 0 = n

The tactic intros n. is used to introduce new variables, in this case, n.  When compiled, n : nat moves above the line as an assumption.

Compile:

 induction n as [ | n' IHn'].

The induction n. tactic takes an as... clause, called an intros pattern, that specifies the names of the variables to be introduced in the subgoals. Since there are two subgoals, the as... clause, intros pattern,  has two parts, separated by |. 

Coq uses IHn' (i.e., the Induction Hypothesis for n').

When induction n as [ | n' IHn']. compiles the goals window will show the following:

2 goals

______________________________________(1/2)

0 + 0 = 0

______________________________________(2/2)

S n' + 0 = S n'

Compile:

     - (* n = O *) reflexivity.

The - is a bullet used to separate the induction subgoal cases. Coq has been designed so that its induction tactic generates the same sub-goals, in the same order, as the bullet points that a mathematician would write. 

Coq comments are shown using (* ... *) with the comment typed, as shown above, between the two *. 

The above shows we are using the tactic reflexivity to work on the first goal which is n = O.

When the above tactic reflexivity code compiles the goals window will show the following:

This subproof is complete, but there are some unfocused goals:

______________________________________(1/1)

S n' + 0 = S n'

The goal window comments above the line shows we have proved the first goal; however, information below the line shows we have another subgoal to complete.

Compile:

     - (* n = S n' *) simpl.

As shown in the above comment (* n = S n' *), we are working on the second goal n = S n' using simpl. After it is compiled, the goal window shows. 

1 goal

n' : nat

IHn' : n' + 0 = n'

______________________________________(1/1)

S (n' + 0) = S n'

As shown above IHn' : n' + 0 = n' has moved above the line as an assumption named IHn' which equals n'.

Compile:

 rewrite -> IHn'.

When the rewrite -> IHn'. code compiles,  (n' + 0) below the line becomes n' and the goals window will show the following:

1 goal

n' : nat

IHn' : n' + 0 = n'

______________________________________(1/1)

S n' = S n'

Compile:

reflexivity.

Notice below the line S n' = S n' ; we can now compile reflexivity and the goals window will show:

No more goals.

When Qed. compiles the goals window will be blank and the proof is complete.

2. CONCLUSION

To prove interesting facts about numbers, lists, and other inductively defined sets, we often need a more powerful reasoning principle: induction.

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.