COQ FILE NAMING CONVENTIONS

REVISED: Tuesday, December 17, 2024

1. COQ'S FILE NAMING CONVENTIONS

Coq doesn't require any special naming conventions for files to import or export modules. The connection between files and modules is established through the Require and Require Import commands within Coq code, not through filename matching.

Here's a breakdown:

File Organization: You can organize your Coq code into any files you like (conventionally using the .v extension). For example, you might have MyModule.v, AnotherModule.v, and MainFile.v.

Module Definition: Within each .v file, you define modules using the Module ... End The name you give to the module within the Module declaration is crucial, not the filename.

Importing Modules: To use a module defined in another file, you use the Require or Require Import commands.

Require MyModule.: This command loads the file containing the MyModule definition. It makes the module name MyModule available, but you still need to use the qualified name (e.g., MyModule.my_nat) to access its contents.

Require Import MyModule.: This command loads the file and also imports the module into the current scope. This allows you to use the unqualified names (e.g., my_nat) directly.

Example:

Let's say you have two files:

MyModule.v:

Module MyModule.

  Definition my_nat : nat := 5.

End MyModule.

MainFile.v:

Require Import MyModule. (* Or Require MyModule. *)

Compute my_nat. (* If you used Require Import *)

Compute MyModule.my_nat. (* Always works, even with just Require *)

In this example, the filename MyModule.v is arbitrary. You could rename it to SomethingElse.v as long as you change the Require command in MainFile.v accordingly:

(* If MyModule.v is renamed to SomethingElse.v *)

Require Import SomethingElse. (* Coq will look for SomethingElse.vo or SomethingElse.v *)

Compute MyModule.my_nat. (* Module name remains MyModule *)

Compilation:

When you compile your Coq project (using coqc), Coq creates compiled files (.vo files) that are used for faster loading. The Require commands instruct Coq to find these compiled files (or the source .v files if the .vo files are not available). Coq searches in the current directory and in directories specified by the -I flag (include paths).

2. CONCLUSION

Filenames are not directly used to resolve module names during import.

The Require (or Require Import) command, along with the module name specified in the Module declaration, is what connects files to modules.

Coq looks for .vo (compiled) or .v (source) files based on the required module name and the specified search paths.

This decoupling of filenames and module names provides flexibility in organizing your Coq projects.

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 MODULE SYSTEM PART 2

REVISED: Wednesday, December 18, 2024

1. COQ'S MODULE SYSTEM PART 2

Require Import ZArith. 

Require Import Lia.

Module MyModule.

  (* A simple definition within the module. *)

  Definition my_nat : nat := 5.

  (* A function definition. *)

  Definition increment_by_two (n : nat) : nat := n + 2.

  (* A theorem (or lemma) within the module. *)

  Theorem add_two_positive : forall n : nat, increment_by_two n > n.

  Proof.

     intros n.

     simpl. (* Simplifies increment_by_two n to n + 2. *)

     lia. (* Uses the lia tactic to prove the inequality. *)

  Qed.

  (* Another definition, using the previous one. *)

  Definition my_other_nat : nat := increment_by_two my_nat.

  (* A record definition (like a struct or class). *)

  Record point : Type := {

     x : nat;

     y : nat

  }.

  (* A function operating on records. *)

  Definition move_point (p : point) (dx dy : nat) : point :=

     {| x := p.(x) + dx; y := p.(y) + dy |}.

  (* Example usage of the record and function. *)

  Definition my_point : point := {| x := 3; y := 7 |}.

  Definition moved_point : point := move_point my_point 1 2.

End MyModule.

(* Using the definitions from the module. *)

Compute MyModule.my_nat. (* Output: 5 *)

Compute MyModule.add_two 10. (* Output: 12 *)

Compute MyModule.my_other_nat. (* Output: 7 *)

Compute MyModule.moved_point. (* Output: {| x := 4; y := 9 |} : point *)

(* Demonstrating module inclusion/import. *)

Module AnotherModule.

     Import MyModule. (* Brings all definitions from MyModule into scope. *)

    Compute my_nat. (* Now accessible directly. Output: 5 *)

    Compute move_point my_point 5 5. (* Output: {| x := 8; y := 12 |} : point *)

  

  (* Showing that you can redefine things locally without affecting the original module. *)

    Definition my_nat : nat := 100. (* This only redefines my_nat *within* AnotherModule. *)

    Compute my_nat. (* Output: 100 *)

    Compute MyModule.my_nat. (* Output: 5 (MyModule is unchanged) *)

End AnotherModule.

(* Demonstrating module types (interfaces). *)

Module Type PointInterface.

     Parameter point : Type.

     Parameter make_point : nat -> nat -> point.

     Parameter get_x : point -> nat.

     Parameter get_y : point -> nat.

End PointInterface.

Module PointImplementation : PointInterface.

     Record point : Type := { x : nat; y : nat }.

     Definition make_point x y := {| x := x; y := y |}.

     Definition get_x p := p.(x).

     Definition get_y p := p.(y).

End PointImplementation.

Module AnotherPointImplementation : PointInterface.

     (* A different implementation of points using lists *)

     Definition point := list nat.

     Definition make_point x y := [x;y].

     Definition get_x p := List.nth 0 p 0. (* Default 0 if out of bounds *)

     Definition get_y p := List.nth 1 p 0.

End AnotherPointImplementation.

Explanation:

Module MyModule. and End MyModule.: These keywords define the beginning and end of a module named MyModule. Modules act as namespaces, grouping related definitions (constants, functions, theorems, records, etc.) together.

Definition my_nat : nat := 5.: This defines a constant my_nat of type nat (natural number) with the value 5.

Definition increment_by_two (n : nat) : nat := n + 2.: This defines a function increment_by_two that takes a natural number n as input and returns a natural number n + 2.

Theorem add_two_positive : forall n : nat, increment_by_two n > n.: This declares a theorem named add_two_positive. forall n : nat means "for all natural numbers n." The theorem states that for any natural number n, increment_by_two n is greater than n.

Proof. ... Qed.: This block contains the proof of the theorem.

intros n. introduces the universal quantifier n into the context.

simpl. simplifies the expression increment_by_two n to n + 2.

lia. is a powerful tactic that automatically proves inequalities in Presburger arithmetic (linear arithmetic over integers and natural numbers).

Record point : Type := { ... }.: This defines a record type called point. Records are similar to structs or classes in other programming languages. They allow you to group related data together. In this case, a point has two fields: x and y, both of type nat.

p.(x): This is the syntax for accessing the field x of a record p.

{| x := ...; y := ... |}: This is the syntax for constructing a record value.

Compute MyModule.my_nat.: This command computes the value of my_nat within the MyModule namespace. The output will be 5.

Import MyModule.: This statement within AnotherModule imports all definitions from MyModule into the current scope of AnotherModule, allowing you to use them directly without the MyModule. prefix.

Redefinition within a module: As shown in AnotherModule, you can redefine names (like my_nat) locally within a module after importing another. This creates a shadowing effect. The local definition takes precedence within the module where it's redefined, without altering the original definition in the imported module.

Module Types (Interfaces): Module Type PointInterface. defines an interface for a point module. It specifies the signatures (types) of the functions and parameters that a module implementing this interface must provide. Module PointImplementation : PointInterface. and Module AnotherPointImplementation : PointInterface. show two different ways of implementing such interface. This is very powerful for code organization, modularity, and abstraction, as it allows you to swap implementations without changing the code that uses these modules.

2. CONCLUSION

Coq modules are crucial for developing larger and more complex Coq projects, enabling better organization, maintainability, and reusability of code.

Key Takeaways about Coq Modules:

Namespaces: Modules provide namespaces to organize code and avoid name collisions.

Encapsulation: They encapsulate definitions, preventing accidental modification from outside the module (unless explicitly imported).

Code Reusability: Modules promote code reusability by allowing you to import and use definitions in other modules.

Abstraction and Interfaces: Module types enable abstraction by defining interfaces that different modules can implement, promoting modularity and code maintainability.

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 MODULE SYSTEM PART 1

REVISED: Tuesday, December 17, 2024

1. COQ'S MODULE SYSTEM PART 1

Coq's module system is a powerful tool for organizing and structuring large-scale formal developments. By breaking down complex proofs and definitions into smaller, modular components, modules promote code reusability, maintainability, and modularity.

Basic Module Structure:

A Coq module typically consists of:

Module Declaration:

Module MyModule. (* START MYMODULE *)

(* Module Body *)

End MyModule. (* END MYMODULE*)

Module MyModule. (* START MYMODULE *)

Module Body:

Definitions: Definition, Fixpoint, Inductive

Theorems: Theorem, Lemma, Proposition

Tactics: Proof, Qed

Other Modules: Nested modules

Importing and Exporting Definitions:

Import:

Import MyModule.

Imports all definitions from MyModule into the current scope.

Export:

Export MyModule.

Exports all definitions from MyModule to any module that imports it.

Example: A Simple Module for Natural Numbers

End MyModule. (* END MYMODULE *)

Module NatModule. (* START NATMODULE *)

(* Inductive definition of natural numbers *)

Inductive nat : Type :=

   | O : nat

   | S : nat -> nat.

(* Definition of addition on natural numbers *)

Fixpoint plus (n m : nat) : nat :=

   match n with

   | O => m

   | S p => S (plus p m)

   end.

End NatModule. (* END NATMODULE *)

Using the Module:

Import NatModule.

(* Example usage of the `plus` function *)

Theorem plus_comm : forall n m : nat, plus n m = plus m n.

Proof.

  (* ... proof using the `plus` function from NatModule *)

Qed.

Advanced Module Features:

Module Parameters:

Module MyModule (A : Type).  (* START MYMODULE *)

(* Module body using A *)

End MyModule.  (* END MYMODULE *)

Allows for generic modules that can be instantiated with different types.

Module Signatures:

Define interfaces for modules, specifying the signatures of exported definitions.

Functors:

Higher-order modules that can transform other modules.

Example: A Generic List Module

Module ListModule (A : Type). (* START LISTMODULE *)

Inductive list : Type :=

   | nil : list

   | cons : A -> list -> list.

(* ... other list operations *)

End ListModule.  (* END LISTMODULE *)

Using the Generic List Module:

Import ListModule.

(* Instantiate the module for natural numbers *)

Module NatList := ListModule(nat).

(* Use the `nil` and `cons` constructors for natural number lists *)

Definition my_list : NatList.list := NatList.cons 1 (NatList.cons 2 NatList.nil).

2. CONCLUSION

By effectively utilizing Coq's module system, you can organize your formal developments into well-structured, reusable components, making your proofs more modular, maintainable, and easier to understand.

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 CONSTRUCTORS

REVISED:  Tuesday, December 17, 2024

1. INTRODUCTION

What are Coq Constructors?

Building Blocks of Inductive Types: 

In Coq, inductive types define new data structures. Constructors are the fundamental components used to construct values (or terms) of these inductive types.

Defining New Data: 

Think of constructors as blueprints for creating specific instances of a data type. For example:

bool: 

This built-in inductive type has two constructors: true and false. These are the only ways to create a value of type bool.

nat: 

The natural numbers are defined inductively with two constructors:

O: Represents the number zero.

S: Represents the successor function (e.g., S O is 1, S (S O) is 2, and so on).

2. HOW TO USE CONSTRUCTORS

Define an Inductive Type:

Inductive my_list (A : Type) : Type :=

  | Nil : my_list A

  | Cons : A -> my_list A -> my_list A.

  

Nil is the constructor for an empty list.

Cons is the constructor to add an element (A) to the beginning of an existing list (my_list A).

This defines a new type called my_list. 

A is a type parameter, meaning my_list can be a list of any type.

Compiling:

Inductive my_list (A : Type) : Type :=

  | Nil : my_list A

  | Cons : A -> my_list A -> my_list A.

The Messages window of CoqIDE shows:

my_list is defined

my_list_rect is defined

my_list_ind is defined

my_list_rec is defined

my_list_sind is defined

When you define an inductive type in Coq, the system automatically generates several useful definitions and principles:

my_list_rect: This is the general recursion principle for my_list. It allows you to define functions recursively on my_list by providing cases for Nil and Cons.

my_list_ind: This is the induction principle for my_list. It's used to prove properties about my_list by induction on its structure.

my_list_rec: This is a specialized recursion principle for defining functions on my_list. It's often more convenient to use than my_list_rect in many cases.

my_list_sind: This is a specialized induction principle for proving properties about my_list. It's often more convenient to use than my_list_ind in many cases.

In essence, the my_list type is a fundamental building block for defining various list-based data structures and algorithms in Coq. 

Construct Values:

(* Example list of integers *)

Definition my_list_example : my_list nat := 

    Cons 1 (Cons 2 (Cons 3 Nil)). 

  

This creates a list containing the integers 1, 2, and 3.

Pattern Matching:

Constructors are essential for pattern matching in Coq, which allows you to define functions that operate on inductive types.

Fixpoint my_list_length (l : my_list A) : nat :=

   match l with

   | Nil => 0

   | Cons _ tl => S (my_list_length tl) 

   end.

  

This function calculates the length of a list. It uses pattern matching to distinguish between the Nil case (empty list) and the Cons case (non-empty list).

3. CONCLUSION

By understanding the inductive definition and the generated principles, you can effectively work with lists in Coq proofs and program development.

Constructors are fundamental for defining and working with inductive types in Coq. They provide a structured way to create and manipulate data. 

Pattern matching on constructors is crucial for defining functions that operate on inductive types.

Example:

Let's define a simple binary tree:

Inductive tree (A : Type) : Type :=

  | Leaf : tree A

  | Node : A -> tree A -> tree A -> tree A.

  

Leaf: Represents a leaf node (no children).

Node: Represents an internal node with a value (A) and two child subtrees.

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