Software Foundations

Functional Programming

In functional programming, a procedure is considered functional if it has no side effects and its inputs map to outputs. It's a concerete method for computing a mathematical function.

Functions are first-class values: Functions can be passed to other functions as arguments, returned from functions or included in data structures.

Other features of functional programming include algebraic data types, pattern matching and polymorphic type systems. All these are supported by Coq.

Tags:Software Foundations, Logical Foundations, functional

Source:https://softwarefoundations.cis.upenn.edu/

Software Foundations

Enumerated Type Definition

The following defines the type day with members monday, tuesday, etc.

Having defined the type, we can now write functions that operate on it:

The return type day can be inferred instead of being explicitly specified.

The individual elemens (monday, tuesday, etc.) are called constructors

Tags:Software Foundations, Logical Foundations, enumeration, constructor, type

Source:https://softwarefoundations.cis.upenn.edu/

Software Foundations

Compute

Use the Compute command to evaluate a compound expression:

Tags:Software Foundations, Logical Foundations, compute

Source:https://softwarefoundations.cis.upenn.edu/

Software Foundations

Example + Proof

Examples serve as assertions using example input and output values to verify expectted behavior of an expression.

Examples can be named so that they can be referenced later.

We can ask Coq to verify the assertion like this:

Tags:Software Foundations, Logical Foundations, proof, example

Source:https://softwarefoundations.cis.upenn.edu/

Software Foundations

If..then..else

If..then..else conditional expressions are support for any inductively defined type with exactly two clauses in its definition.

Tags:Software Foundations, Logical Foundations, if, then, else

Source:https://softwarefoundations.cis.upenn.edu/

Software Foundations

Admitted can be used as a placeholder for an incomplete proof. Without it, the following example would throw an error.

Tags:Software Foundations, Logical Foundations, if, then, else

Source:https://softwarefoundations.cis.upenn.edu/

Software Foundations

Type Checking

Expressions' return types can be checked using the Check command like so:

Tags:Software Foundations, Logical Foundations, check

Source:https://softwarefoundations.cis.upenn.edu/

Software Foundations

Type Checking of Functions

Types of functions' clauses and return values can be checked using the Check command with the => syntax like so:

This checks that the function takes bool type and returns a bool type.

Tags:Software Foundations, Logical Foundations, if, then, else

Source:https://softwarefoundations.cis.upenn.edu/

Software Foundations

Constructor Arguments

Enumerated types can have constructors that take arguments:

Constructor expressions are formed by applying a constructor to zero or more other constructors or constructor expressions, obeying the declared number and types of the constructor arguments. E.g.,

• red
• true
• primary red
• etc.

But not

• red primary
• true red
• primary (primary red)
• etc.

If p is a constructor expression belonging to the set rgb, then primary p (pronounced "the constructor primary applied to the argument p") is a constructor expression belonging to the set color.

We can define functions on colors using pattern matching:

Since the primary constructor takes an argument, a pattern matching primary should include either a variable (as above -- note that we can choose its name freely) or a constant of appropriate type (as below).

A proof involving a constructor expression looks like this:

Tags:Software Foundations, Logical Foundations, constructor argument, constructor

Source:https://softwarefoundations.cis.upenn.edu/

Software Foundations

Modules

Modules can be used to limit the scope of definition:

Tags:Software Foundations, Logical Foundations, module

Source:https://softwarefoundations.cis.upenn.edu/

Software Foundations

Tuples

A single constructor with multiple parameters defines a tuple. This is a tuple with 4 values of type bit is defined and checked:

Tags:Software Foundations, Logical Foundations, tuple

Source:https://softwarefoundations.cis.upenn.edu/

Software Foundations

Tuple Matching

This is how variable of type tuple is created and matched for:

Tags:Software Foundations, Logical Foundations, tuple

Source:https://softwarefoundations.cis.upenn.edu/

Software Foundations

Definition of Unary Number

Unary (as opposed to binary or decimal) numbers are defined as:

0 is represented by 0, 1 by S 0, 2 by S (S 0) and so on.

The S stands for "successor".

0 and S are arbitrary; they define a representation of numbers. Other marks could have been used instead.

Tags:Software Foundations, Logical Foundations, unary, nat

Source:https://softwarefoundations.cis.upenn.edu/

Software Foundations

n - 2

A definition of a function that returns n - 2:

Tags:Software Foundations, Logical Foundations, nat

Source:https://softwarefoundations.cis.upenn.edu/

Software Foundations

Fixpoint, Recursion

Recursion is defined using the Fixpoint keyword:

Tags:Software Foundations, Logical Foundations, fixpoint

Source:https://softwarefoundations.cis.upenn.edu/