REVISED: Thursday, December 5, 2024
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.
