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.

COQ

REVISED: Saturday, September 6, 2025

1. INTRODUCTION

Imagine you're building a really cool LEGO structure. You have all the bricks and pieces, and you have a plan (instructions) on how to build it. Coq is like a super smart friend who helps you make sure you're following the plan perfectly and that your LEGO structure is strong and sturdy.

Here's how it works:

Proof Assistant:

Coq is a proof assistant. That means it helps you write proofs, which are like arguments or explanations that show something is true.

Math and Programming:

Coq can be used for math and programming. In math, it can help you prove theorems, like proving that 2 + 2 always equals 4. In programming, it can help you write programs that are correct and work the way they should.

Formal Verification:

Coq is used for formal verification. This means it can check if your math or programming is correct, just like your friend checks your LEGO building.

So, Coq is a powerful tool that helps people be sure that their math and programming is accurate and reliable. It's like having a super-smart friend who can help

2. COQIDE

Imagine CoqIDE as a special kind of word processor, but instead of writing stories or essays, it helps you build logical arguments and proofs. It's like having a super smart friend who can check your work and tell you if your reasoning is correct.

Here's what it does:

Proof Editing:

You can type in your proofs, and CoqIDE will help you by suggesting steps or pointing out mistakes.

Auto-Completion: 

It can finish your sentences for you, just like your phone does when you text!

Highlighting: 

It highlights important parts of your proof to make it easier to read and understand.

Checking: 

CoqIDE checks your proof step-by-step to make sure it's logically sound.

So, CoqIDE is a tool that helps you build strong, accurate proofs. It's like having a helpful assistant who makes sure your logical thinking is top-notch.

3. COQ-SHELL

Imagine Coq-Shell as a magical text box where you can type in math problems and proofs. It's like having a super smart calculator that not only gives you answers but also checks if your thinking is correct.

Here's how it works:

Typing: 

You type in your math problems and proofs using special commands.

Checking: 

Coq-Shell checks your work step-by-step to make sure it's logically sound.

Feedback: 

It gives you feedback, like if you made a mistake or if your proof is correct.

So, Coq-Shell is a tool that helps you explore math and logic in a fun and interactive way. It's like having a math wizard by your side, guiding you through your calculations and helping you discover new things!

4. CONCLUSION

In this tutorial, you have received a brief overview of Coq, Coq-IDE, and Coq-Shell.

5. 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.