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:sma, connector, electronics

Source:https://en.wikipedia.org/wiki/SMA_connector

Software Foundations

Enumerated Type Definition

The following defines the type <code>day</code> with members monday, tuesday, etc.

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

The return type <code>day</code> can be inferred instead of being explicitly specified.

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

Tags:sma, connector, electronics

Source:https://en.wikipedia.org/wiki/SMA_connector

Software Foundations

Compute

Use the <code>Compute</code> command to evaluate a compound expression:

Tags:sma, connector, electronics

Source:https://en.wikipedia.org/wiki/SMA_connector

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:sma, connector, electronics

Source:https://en.wikipedia.org/wiki/SMA_connector

Software Foundations

If..then..else

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

Tags:sma, connector, electronics

Source:https://en.wikipedia.org/wiki/SMA_connector

Software Foundations

Admitted

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

Tags:sma, connector, electronics

Source:https://en.wikipedia.org/wiki/SMA_connector

Software Foundations

Type Checking

Expressions' return types can be checked using the <code>Check</code> command like so:

Tags:sma, connector, electronics

Source:https://en.wikipedia.org/wiki/SMA_connector

Software Foundations

Type Checking of Functions

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

This checks that the function takes <code>bool</code> type and returns a <code>bool</code> type.

Tags:sma, connector, electronics

Source:https://en.wikipedia.org/wiki/SMA_connector

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., <ul><li>red</li><li>true</li><li>primary red</li><li>etc.</li></ul>

But not<ul><li>red primary</li><li>true red</li><li>primary (primary red)</li><li>etc.</li></ul>

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