COQ INDUCTION ON LISTS

REVISED: Thursday, December 12, 2024

1. INTRODUCTION

ASSOCIATIVITY OF LIST CONCATENATION 

A list can be either nil or else cons applied to a number and a list. 

Applications of the declared constructors to one another are the only possible shapes that elements of an inductively defined set can have.

This last fact directly gives rise to a way of reasoning about inductively defined sets. A number is either O or S applied to some smaller number. A list is either nil or is cons applied to some number and some smaller list; etc. Thus, if we have in mind some proposition P that mentions a list l and we want to argue that P holds for all lists, we can reason as follows:

First, show that P is true of l when l is nil.

Then show that P is true of l when l is cons n l' for some number n and some smaller list l', assuming that P is true for l'.

Since larger lists can always be broken down into smaller ones, eventually reaching nil, these two arguments establish the truth of P for all lists l.

2. EXAMPLE

(* ++ is constructor for append *)

Theorem app_assoc : forall l1 l2 l3 : list Type,

  (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).

Proof.

  intros l1 l2 l3. induction l1 as [| n l1' IHl1'].

  - (* l1 = nil *)

    simpl. (* Unfold the ++ operator *)

    reflexivity.

  - (* l1 = cons n l1' *)

    simpl.

    rewrite IHl1'.

    reflexivity.

Qed.

Compiling:

(* ++ is constructor for append *)

Theorem app_assoc : forall l1 l2 l3 : list Type,

  (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).

The Goal window of CoqIDE shows:

1 goal

A, B, C : Prop

______________________________________(1/1)

forall l1 l2 l3 : list Type,

(l1 ++ l2) ++ l3 = l1 ++ l2 ++ l3

Theorem Declaration:

Theorem app_assoc : ... : Declares a theorem named app_assoc.

forall l1 l2 l3 : list Type,: Specifies that the theorem holds for any three lists of any type.

(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).: States the property to be proven: associativity of list concatenation.

Compiling:

Proof.

The Goal window of CoqIDE shows:

1 goal

A, B, C : Prop

______________________________________(1/1)

forall l1 l2 l3 : list Type,

(l1 ++ l2) ++ l3 = l1 ++ l2 ++ l3

Proof Initiation:

Proof.: Starts the proof.

Compiling:

  intros l1 l2 l3.

The Goal window of CoqIDE shows:

1 goal

A, B, C : Prop

l1 : list Type

l2 : list Type

l3 : list Type

______________________________________(1/1)

(l1 ++ l2) ++ l3 = l1 ++ l2 ++ l3

Induction Hypothesis:

intros l1 l2 l3.: Introduces the variables l1, l2, and l3 for the three lists.

Compiling:

 induction l1 as [| n l1' IHl1'].

The Goal window of CoqIDE shows:

2 goals

A, B, C : Prop

l2 : list Type

l3 : list Type

______________________________________(1/2)

([] ++ l2) ++ l3 = [] ++ l2 ++ l3

______________________________________(2/2)

((n :: l1') ++ l2) ++ l3 = (n :: l1') ++ l2 ++ l3

induction l1 as [| n l1' IHl1'].: Inducts on the first list l1.

Base Case: l1 = nil

Inductive Case: l1 = cons n l1' with the induction hypothesis IHl1'.

Compiling:

 - (* l1 = nil *)

    simpl. (* Unfold the ++ operator *)

The Goal window of CoqIDE shows:

1 goal

A, B, C : Prop

l2 : list Type

l3 : list Type

______________________________________(1/1)

l2 ++ l3 = l2 ++ l3

Base Case:

simpl.: Simplifies the expression by unfolding the ++ operator.

Compiling:

    reflexivity.

The Goal window of CoqIDE shows:

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

______________________________________(1/1)

((n :: l1') ++ l2) ++ l3 = (n :: l1') ++ l2 ++ l3

reflexivity.: Directly proves the equality by reflexivity, as both sides reduce to the same expression.

Compiling:

- (* l1 = cons n l1' *)

    simpl.

The Goal window of CoqIDE shows:

1 goal

A, B, C : Prop

n : Type

l1' : list Type

l2 : list Type

l3 : list Type

IHl1' : (l1' ++ l2) ++ l3 = l1' ++ l2 ++ l3

______________________________________(1/1)

((n :: l1') ++ l2) ++ l3 = (n :: l1') ++ l2 ++ l3

Inductive Case:

simpl.: Simplifies the expression, again unfolding the ++ operator.

Compiling:

rewrite IHl1'.

The Goal window of CoqIDE shows:

1 goal

A, B, C : Prop

n : Type

l1' : list Type

l2 : list Type

l3 : list Type

IHl1' : (l1' ++ l2) ++ l3 = l1' ++ l2 ++ l3

______________________________________(1/1)

n :: l1' ++ l2 ++ l3 = n :: l1' ++ l2 ++ l3

rewrite IHl1'.: Applies the induction hypothesis IHl1' to simplify the expression further.

Compiling:

  reflexivity.

The Goal window of CoqIDE shows:

No more goals.

reflexivity.: After simplification, the two sides of the equation become identical, allowing for the application of reflexivity.

Compiling:

Qed.

3. CONCLUSION

Induction: The proof uses mathematical induction on the structure of the first list.

Simplification: The simpl tactic is used to unfold definitions and reduce expressions.

Reflexivity: The reflexivity tactic is used to prove equalities directly.

Induction Hypothesis: The IHl1' represents the induction hypothesis, which is the assumption that the property holds for smaller lists.

By following these steps and applying the appropriate tactics, Coq can verify the correctness of the app_assoc theorem.

The core idea of inductive proofs is to break down a complex problem into simpler instances and then use the inductive hypothesis to solve the simpler instances. In this case, we broke down the problem for cons n l1' into a simpler problem for l1' and then used the inductive hypothesis to solve the simpler problem.

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.

COQ PROOF TECHNIQUES; REFLEXIVITY, REWRITE, AND DESTRUCT

REVISED: Saturday, November 30, 2024

Coq is a powerful Proof Assistant that allows you to formally verify mathematical proofs. To effectively use Coq, you'll need to master a few fundamental proof tactics. Let's delve into three of the most common ones: reflexivity, rewrite, and destruct.

1. REFLEXIVITY

The reflexivity tactic is used to prove equalities where both sides of the equation are identical. In essence, it asserts that any term is equal to itself. If you are having problems understanding Coq, preceed reflexivity with simpl. simpl is not necessary; however, it might help with human readability.

Example:

Goal forall x: nat, x = x.

Proof.

  reflexivity.

Qed.

We enter the proof engine by the command Goal, followed by the conjecture we want to verify: forall x: nat, x = x.

In this example, the goal is to prove that for any natural number x, x is equal to itself. The reflexivity tactic directly proves this equality.

Compiling: 

Goal forall x: nat,

  x = x.

The CoqIDE system displays the current goal below a line, local hypotheses (there are none initially) being displayed above the line. We call the combination of local hypotheses with a goal a judgment.

The Goal window of CoqIDE shows: 

1 goal

______________________________________(1/1)

forall x : nat, x = x

Compiling: 

Proof.

  reflexivity.

The Goal window of CoqIDE shows: 

No more goals.

Qed.

2. REWRITE

The rewrite tactic is used to replace one side of an equation with another equivalent expression. This is particularly useful when you have a known equality that can be applied to simplify a proof.

Example:

Theorem plus_id_example :

  forall n m : nat,

  n = m ->

  n + n = m + m.

Proof.

  intros n m.

  intros H.

  rewrite -> H.

  reflexivity.

Qed.

Compiling: 

Theorem plus_id_example :

  forall n m : nat,

  n = m ->

  n + n = m + m.

The Goal window of CoqIDE shows: 

1 goal

______________________________________(1/1)

forall n m : nat, n = m -> n + n = m + m

Compiling: 

Proof.

  intros n m.

The Goal window of CoqIDE shows: 

1 goal

n, m : nat

______________________________________(1/1)

n = m -> n + n = m + m

forall n, m : nat are moved above the line and become assumptions to improve human readability.  Now we more clearly see we have one goal, and we are assuming n and m are both natural numbers.

Compiling: 

intros H.

The Goal window of CoqIDE shows: 

1 goal

n, m : nat

H : n = m

______________________________________(1/1)

n + n = m + m

Compiling: 

rewrite -> H.

The Coq default is left to right; therefore, we could have written rewrite H.

The Goal window of CoqIDE shows: 

1 goal

n, m : nat

H : n = m

______________________________________(1/1)

m + m = m + m

Compiling: 

reflexivity.

The Goal window of CoqIDE shows: 

No more goals.

Qed.

3. DESTRUCT

The destruct tactic is used to break down inductive data types into their constituent cases. This is essential for reasoning about recursive definitions and proofs by induction.

Example:

Theorem andb_commutative : forall b c, andb b c = andb c b.

Proof.

  intros b c.

  destruct b, c.

  - reflexivity.

  - reflexivity.

  - reflexivity.

  - reflexivity.

Qed.

Compiling: 

Theorem andb_commutative : forall b c, andb b c = andb c b.

The Goal window of CoqIDE shows: 

1 goal

______________________________________(1/1)

forall b c : bool,

(b && c)%bool = (c && b)%bool

Compiling:

Proof.

  intros b c.

The Goal window of CoqIDE shows: 

1 goal

b, c : bool

______________________________________(1/1)

(b && c)%bool = (c && b)%bool

Compiling:

destruct b, c.

The Goal window of CoqIDE shows: 

4 goals

______________________________________(1/4)

(true && true)%bool = (true && true)%bool

______________________________________(2/4)

(true && false)%bool = (false && true)%bool

______________________________________(3/4)

(false && true)%bool = (true && false)%bool

______________________________________(4/4)

(false && false)%bool = (false && false)%bool

Compiling:

  - reflexivity.

The Goal window of CoqIDE shows: 

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

______________________________________(1/3)

(true && false)%bool = (false && true)%bool

______________________________________(2/3)

(false && true)%bool = (true && false)%bool

______________________________________(3/3)

(false && false)%bool = (false && false)%bool

Compiling:

  - reflexivity.

The Goal window of CoqIDE shows: 

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

______________________________________(1/2)

(false && true)%bool = (true && false)%bool

______________________________________(2/2)

(false && false)%bool = (false && false)%bool

Compiling:

  - reflexivity.

The Goal window of CoqIDE shows: 

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

______________________________________(1/1)

(false && false)%bool = (false && false)%bool

Compiling:

  - reflexivity.

The Goal window of CoqIDE shows: 

No more goals.

Qed.

Additional information.

Combined Destruct:

Instead of performing two nested destructs, they can be combined into a single destruct b, c. This simultaneously breaks down both b and c into their possible cases, leading to a more concise proof.

Implicit Reflexivity:

In each case, the equality is trivial. Coq's automated tactics can often infer the necessary steps to prove such simple equalities. By simply using reflexivity without explicit argument, we let Coq fill in the details.

Key Points to Remember.

Efficient Destruct:

Use destruct judiciously to break down complex terms into simpler cases.

Leverage Automation: 

Utilize Coq's automated tactics to simplify proofs, especially for trivial equalities.

Readability: 

Write clear and concise proofs. Avoid unnecessary steps and redundant explanations.

4. CONCLUSION

By mastering these three techniques, you can tackle a wide range of proofs in Coq. 

Remember that practice is key, so don't hesitate to experiment and explore more complex examples.

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.

COQ RECURSIVE FUNCTION EXAMPLE

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.

COQIDE PROOF BY INDUCTION

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.