Reference Manual

This is a comprehensive reference for Deduce. It describes each feature in alphabetical order by keyword. It gives the grammar rule (syntax) and describes its meaning and/or how it is used in a proof.

In the grammar rules, an unquoted asterisk means zero-or more repetitions of the grammar item that it follows. The symbol ε means the empty string. A vertical bar separates alternatives right-hand sides in a grammar rule.

Add

The addition function for natural numbers is defined in Nat.pf as follows.

Example:

Add (Multiset)

Addition on multisets is defined in MultiSet.pf. The main theorem about multiset addition is cnt_sum, which says that the count for each item in A ⨄ B is the sum of (1) the count for that item in A and (2) the count for that item in B.

Example:

All (Universal Quantifier)

A formula of the form all x1:T1,...,xn:Tn. P is true when P is true for all possible choices of x1...xn.

To prove an all formula, use arbitrary (see entry for Arbitrary) or induction (see entry for Induction). Induction is only allowed when the all has a single variable, as in all x:T. P, and the type T must be a union type.

A proof of all x1:T1,...,xn:Tn. P can be used to prove the formula P where the x1,...,xn have been replaced by terms of your choice. Use square brackets to enclose your comma-delimited choices.

And (logical conjunction)

The formula P and Q is true when both P and Q are true.

Example:

Use comma to combine a proof of P and a proof of Q into a proof of P and Q.

A proof of P and Q can be used implicitly to prove P and to prove Q.

Append

The append function, i.e., operator ++, is defined in List.pf as follows.

Example:

Apply-To Proof (Modus Ponens)

A proof of the form

is a proof of formula Q if X is a proof of (if P then Q) and Y is a proof of P.

Example:

Arbitrary (Forall Introduction)

A proof of the form

is a proof of the formula all x1:T1, ..., xn:Tn. P if X is a proof of P. The variables x1, ..., xn may appear in the formula P and the proof X.

Example:

Assert (Statement)

The assert statement evaluates a term and reports an error if the result is false. For example, the following assert does nothing because the term evaluates to true.

Assume

A proof of the form

is a proof of the formula if P then Q if X is a proof of Q. The proof X may use the label as a proof of P and it may also refer to the proof of P by writing recall P.

Assumption and Assumption List

See the entry for Assume to see how assumptions are used.

At Symbol @

See the entry for Instantiation.

Biconditional (if and only if)

The biconditional formula P ⇔ Q is syntactic sugar for (if P then Q) and (if Q then P).

Bool (Type)

The type bool classifies the values true and false. A formula is a term of type bool.

Braces (Proof)

A proof may be surrounded in curly braces.

Call (Term)

A term of the form t0(t1, ..., tn) calls the function indicated by term t0 on the arguments t1,...,tn.

Cases (Disjunction Elimination)

In Deduce, you can use an or fact by doing case analysis with the cases statement. There is one case for each subformula of the or.

In the following example, we prove that x ≤ y or y < x from the trichotomy law: x < y or x = y or y < x.

Choose (Exists Introduction)

A proof of the form

is a proof of the formula some x1,...xn. P if X is a proof of formula P where the x's replaced by the e's.

Example:

Comma (Logical And Introduction)

See the entry for And (logical conjunction).

Compose (Functions)

The composition of two functions g ∘ f is defined in Maps.pf so that (g ∘ f)(x) = g(f(x)).

Example:

Applying the successor function suc (add 1) to 3 yields 5.

Conclude (Proof)

This proof statement is useful when you wish to emphasize the end of a proof by stating the formula that is being proved.

A proof of the form

is a proof of formula P if X is a proof of P.

Example:

Conclusion (Proof)

The last statement in a proof (the conclusion symbol in the grammar) must be one of the following:

• Cases
• Comma (Logical-And Introduction)
• Conclude
• Conjunct
• Definition
• Definition-In
• Definition and Rewrite
• Equations
• Evaluate
• Evaluate-In
• Help
• Identifier
• Induction
• Instantiation
• Period
• Question Mark
• Recall
• Rewrite
• Sorry
• Switch
• Symmetric
• Transitive

Conjunct

A proof of the form

is a proof of Pn if X is a proof of P1 and ... and Pk and 1 ≤ n ≤ k.

Example:

Contradiction

During a proof, one sometimes encounters assumptions that contradict each other. In these situations, you can prove false and from that, anything else (the Principle of Explosion). Here are two ways to prove false from contradictions.

(1) If you have a proof X of an equality with different constructors on the left and right-hand side, such as

then you can implicitly use X to prove false:

(2) If you have a proof X of P and a proof Y of not P, then you can prove false using apply-to. (Because not P is shorthand for if P then false.)

Define (Statement)

The define feature of Deduce associates a name with a value. For example, the following definitions associate the name five with the natural number 5, and the name six with the natural number 6.

Optionally, the type can be specified after the name, following a colon. In the above, six holds a natural number, so its type is Nat.

Define (Term)

This associates a name with a term for use in the term after the semicolon.

Define (Proof)

This associates a name with a term for use in the following proof. (Note: there is no semicolon after the term when using define in a proof.)

Definition (Proof)

In the current goal formula, replace the occurrences of the specified names with their definitions and then check whether the formula has simplified to true. If a definition is recursive, only one expansion is performed per time the definition's name is mentioned in the list. If one of the specified names does not appear in the goal formula, Deduce signals an error.

Definition and Rewrite (Proof)

Apply the specified definitions to the current goal (see Definition (Proof)), then the specified rewrites (see Rewrite (Proof)). If this simplifies that formula to true, then this statement proves the goal. Otherwise, Deduce signals an error.

Definition-In (Proof)

In the formula of the given proof, replace the occurrences of the specified names with their definitions, resulting in the formula that is proved by this definition-in statement. If a definition is recursive, only one expansion is performed per time the definition's name is mentioned in the list. If one of the specified names does not appear in the formula, Deduce signals an error.

Divide

The division function for Nat and Pos is defined in Nat.pf. The main theorem is division_remainder which states that

Example:

Empty Set

The empty set ∅ does not contain any elements and is defined in Set.pf.

Equal

The formula a = b is true when the left-hand side and right-hand are the same.

(In Deduce, there is no distinction between identity and deep equality as there is in Java because there is no concept of identity in Deduce.)

Equations

Combining a sequence of equations using transitive is quite common, so Deduce provides equations to streamline this process. After the first equation, the left-hand side of each equation is written as ... because it is just a repetition of the right-hand side of the previous equation.

Example:

Evaluate (Proof)

The evaluate proof method simplifies the goal formula by applying all definitions. It succeeds if the formula is simplified to true.

Evaluate-In (Proof)

The evaluate-in proof method simplifies the formula of the given proof by applying all definitions, producing a proof of the simplified formula.

Extensionality

To prove that two functions are equal, it is sufficient to prove that they always produce equal outputs given equal inputs.

False

One can prove false when there are assumptions that contradict each other, such as x = 0 and x = 1, or not P and P.

A proof of false can be used to prove anything else! (This is known as the Principle of Explosion.)

Formula

A formula is any term of type bool.

Function (Term)

Functions are created with a λ expression. Their syntax starts with λ, followed by parameter names and their types, then the body of the function enclosed in braces. For example, the following defines a function for computing the area of a rectangle.

To call a function, apply it to the appropriate number and type of arguments.

The output is 12.

Function (Statement)

The function statement is for defining recursive functions that operate on union types. Recursive functions in Deduce are somewhat special to make sure they always terminate.

• The first parameter of the function must be a union.
• The function definition must include a clause for every constructor in the union.
• The first argument of every recursive call must be a sub-part of the current constructor of the union.

A recursive function begins with the function keyword, followed by the name of the function, then the parameters types and the return type. The body of the function includes one equation for every constructor in the union of its first parameter. For example, here's the definition of a length function for lists of natural numbers.

There are two clauses in the body of length because the NatList union has two constructors. The clause for Empty says that its length is 0. The clause for Node says that its length is one more than the length of the rest of the linked list. Deduce approves of the recursive call length(next) because next is part of Node(n, next).

Recursive functions may have more than one parameter but pattern matching is only supported for the first parameter. If you need to pattern match on a parameter that is not the first, you can use a switch statement.

Function Type

A function type classifies a function. This includes both recursive functions (function) and anonymous functions (fun or λ). If the function is generic, its function type includes type parameters enclosed in < and >.

Generic (Formula)

This parametrizes a formula by a list of type parameters. For example, the following formula states that if the length of a list is 0, then the list must be empty. The type parameter <T> means that this formula applies to lists with any element type.

Generic (Term)

A term of the form

produces a generic function with type parameters T1, ..., Tn, if term X produces a function (e.g., using fun).

An example use of generic is in Maps.pf, in the definition of function composition.

Generic functions can also be defined using the function statement (see Function).

Given

An assumption or fact that is already proved.

Greater-Than

The greater-than operator on natural numbers is defined in Nat.pf and is defined in terms of less-than as follows

Example:

Greater-Than or Equal

The greater-than-or-equal operator on natural numbers is defined in Nat.pf and is defined in terms of less-than-or-equal as follows

Example:

Have (Proof Statement)

Use have to prove a formula that may help you later to prove the goal.

A proof of the form

is a proof of Q as long as Y is a proof of Q and X is a proof of P. The formula P becomes a given and can be used inside the proof Y.

Help (Proof)

This halts Deduce and prints advice regarding how to use the formula of the supplied proof. Typically the supplied proof is the label for a given.

Identifier

Identifiers are used in Deduce to give names to functions and values and to label theorems and facts.

An identifier is a sequence of characters that starts with an upper or lower-case letter or an underscore, and is followed by letters, digits, or the special characters !, ?, and '. An identifier can also be an operator, which starts with the keyword operator and is then followed by one of the following operators: +, -, *, /, %, =, ≠, /=, <, ≤, <=, ≥, >= ++, ∩, &, ∈, in, ∪, |, ⨄, .+., ⊆, (=, ∘, .o..

Identifier List

A comma-separated sequence of identifiers.

If and only if (iff)

See the entry for Biconditional.

If Then (Conditional Formula)

A formula if P then Q is true when both P and Q are true and it is true when P is false.

To prove a conditional formula, use assume. (See the entry for Assume.)

To use a given that is a conditional formula, use apply-to. (See the entry for Apply-To.)

If Then Else (Term)

A term of the form

is equal to b when a is true and equal to c when a is false.

Example:

Import (Statement)

Import all of the definitions and theorems from the specified file (without the file extension).

In (Set Membership)

The formula x ∈ S is true when element x is contained in the set S.

Example:

Induction

A proof of the form

is a proof of the formula all x:T. P if each Xi is a proof of P where x is replaced by ci(ei1,...,eij). The type T must be a union type. Each proof Xi may use its induction hypotheses IH1, .... For each term ein whose type is T (so it is recursive), the induction hypothesis is the formula P with x replaced by the constructor argument ein.

Example:

Injective (Proof)

The injective proof rule allows you to conclude that the inputs to a constructor are equal if the outputs are equal. For example, if suc(x) = suc(y) then x = y.

Example:

Instantiation (Proof)

Use square brackets [ and ] to instantiate an all formula with terms and use angle brackets < and > to instantiate an all formula with types.

Example:

Instantiation (Term)

Instantiates a generic function or constructor, replaces its type parameters with the given type arguments.

Intersection

Set intersection is defined in Set.pf. The intersection of sets A and B, written A ∩ B, contains the items that occur both sets.

Example:

Less-Than

The less-than operator on natural numbers is defined in Nat.pf as follows.

To find theorems about the less-than operator in Nat.thm, search for theorems with less in the name.

Example:

Less-Than or Equal

The less-than-or-equal operator on natural numbers is defined in Nat.pf as follows.

To find theorems about the less-than operator in Nat.thm, search for theorems with less_equal in the name.

Example:

List (Term)

Deduce treats [t1,t2,...,tn] as syntactic sugar for node(t1, node(t2, ... node(tn, empty))).

List (Type)

The List type represents a singly-linked list of items and is defined in List.pf as follows.

The sequence 3,8,4 can be represented as a List by creating three nodes that are composed in the following way.

Mark

Marking a subterm with hash symbols restricts a rewrite or definition proof to only apply to that subterm.

Modulo

The modulo operator is defined in Nat.pf as follows. The first argument is a natural number (of type Nat) and the second argument is a positive number (of type Pos).

Example:

Modus Ponens

See the entry for Apply-To.

Multiply

Multiplication on natural numbers is defined in Nat.pf as follows.

To find theorems about multiplication, search for mult in Nat.thm.

Example:

MultiSet (Type)

The MultiSet<T> type represents the standard mathematical notion of a multiset, which is a set that may contain duplicates of an element. The MultiSet<T> type is defined in MultiSet.pf.

Not

The formula not P is true when P is false. Deduce treats not P as syntactic sugar for (if P then false).

Not Equal

Deduce treats x ≠ y as syntactic sugar for not (x = y).

Obtain (Exists Elimination)

A proof of the form

is a proof of formula Q if Y is a proof of Q. The X must be a proof of the form some x1:T1,...,xn:Tn. P. The proof Y may use the label as a proof of P and it may also refer to the proof of P by writing recall P.

Example:

Or (logical disjunction)

The formula P or Q is true when either P is true or Q is true.

Example:

To prove P or Q it is enough to just prove P or to just prove Q.

To use a given of the form P or Q, use Cases (Disjunction Elimination).

Parentheses

A term, formula, or a proof may be surrounded in parentheses.

Pattern

This syntax is used in Switch (Term), Switch (Proof), and Function (Statement) via a Pattern List.

Parameter List

A parameter list begins with a pattern (for the first function parameter) and then continues with a comma-separated sequence of zero or more identifiers (for the rest of the function parameters).

Period (Proof of True)

A period is a proof of the formula true in Deduce.

Pos (Positive Integers)

The type of positive integers Pos is defined in Nat.pf.

Proof

A proof is a sequence of zero or more proof statements that finishes with a conclusion.

Proof List

A list of proofs separated by vertical bars. This syntax is used in Rewrite (Proof).

Proof Statement

The following are proof statements (proof_stmt symbol in the grammar). A proof may begin with zero or more proof statements, but it must end with a Conclusion (not a proof statement).

• Arbitrary
• Assume
• Choose
• Define
• Extensionality
• Have
• Injective
• Obtain
• Suffices
• Suppose

Print (Statement)

You can ask Deduce to print a value to standard output using the print statement.

The output is 5.

Question Mark ? (Proof)

A proof can be left incomplete by placing a ? in the part that you don't know. Deduce halts at the ? and prints an error message with the location of the ? and the formula that needs to be proved, as well as some advice about how to prove it.

Recall (Proof)

A proof of the form !!! recall P1, ..., Pn !!! is a proof of the formula P1 and ... and Pn. The formulas P1,...,Pn must be in the givens at the current point in the proof.

Reflexive (Proof)

The proof reflexive proves that a = a for any term a.

Rewrite (Proof)

Rewrite the current goal formula according to the equalities proved by the specified Proof List. Each equality may be a literal equality (has the form LHS = RHS) or it can be a generalized equality (has the form all x1:T1,...,xn:Tn. LHS = RHS).

For each equality going left-to-right in the proof list, any subterm in the goal formula that matches the left-hand side of the equality (LHS) is replaced by the right-hand side of the equality (RHS). Once a subterm is rewritten by an equality, the resulting subterm is not rewritten further by the same equality. On the other hand, rewriting with an equality may apply to multiple disjoint locations in a formula.

If the rewriting done by all of the equalities simplifies the goal formula to true, then this statement proves the goal. Otherwise, Deduce signals an error.

Rewrite-In (Proof)

In the formula of the given proof, rewrite according to the equalities proved by the specified Proof List, resulting in the formula that is proved by this rewrite-in statement. The algorithm for rewriting described in the entry for Rewrite (Proof).

Set (Type)

The Set<T> type defined in Set.pf represents the standard mathematical notion of a set. The empty set is written ∅ and the usual set operations such as union ∪, intersection ∩, membership ∈, and subset-or-equal ⊆ are all defined in Set.pf. The Set.thm file provides a summary of the many theorems about sets that are proved in Set.pf.

Some (Existential Quantifier)

The formula some x1:T1,...,xn:Tn. P is true when there exists a choice for x1,...,xn such that P is true.

To prove a some formula, see the entry for Choose.

To use a some formula, see the entry for Obtain

Sorry (Proof)

sorry is the get-out-of-jail free card. It can prove anything. However, it prints a warning message with the location of the sorry.

Switch (Term)

(See the entry for Pattern for the syntax of pattern.)

The subject of the switch must be of union type or bool (e.g., not a function). The body of the switch must have one case for every constructor in the union, or for bool, the cases are true and false. The body of each case is a term and they all must have the same type. The switch evaluates the subject and compares it to each case, then evaluates the body of the case that matched.

Switch (Proof)

(See entry for Assumption List for the syntax of assumption_list.)

A proof of the form

is a proof of formula R if X1,...,Xn are all proofs of R. The fact t = p1 is a given that can be used in X1 and similarly for the other cases.

Example:

Subset or Equal

The formula A ⊆ B is true when every element of set A is contained in set B. That is, given A and B of type Set<T>, the definition of A ⊆ B is as follows. !!! A ⊆ B = (all x:T. if x ∈ A then x ∈ B) !!!

Example:

Subtract

Subtraction for natural numbers is defined in Nat.pf as follows

Note that subtraction on natural numbers is different from subtraction on integers, as they are no negative natural numbers. If you subtract a larger natural number from a smaller natural number, the result is 0.

To search for theorems about subtraction in Nat.thy, search for theorems with sub in the name.

Suffices (Proof Statement)

A proof of the form

is a proof of the formula Q if X is a proof that P implies Q and Y is a proof of Q.

Use suffices to transform the goal formula into a simpler formula. Thus, the suffices feature enables reasoning backwards from the goal.

Example:

One often wants to transform the goal by using a definition or equation. For example, in the following theorem we change the goal from

into

by two uses of the definition of length. We then prove the new goal with theorem add_zero from Nat.thm.

Suppose

See the entry for Assume.

Symmetric (Proof)

If X is a proof of a = b, then symmetric X is a proof of b = a for any terms a and b.

Theorem (Statement)

A theorem (or lemma) proves that a formula is true. The theorem's name can then be used later when one needs to prove the formula again.

A theorem has the form

The proof X must prove the formula P. After the theorem, the label can be used as a proof of P.

Term List

A term list is a comma-separated sequence of zero or more terms.

Transitive (Proof)

If X is a proof of a = b and Y is a proof of b = c, then transitive X Y is a proof of a = c, for any terms a, b, and c.

True (Formula)

There's not much to say about true. It's true! Proving true is easy. Just use a period.

Type

Type List

A type list is a comma-separated list of zero or more types.

Type Parameters

Specifies the type parameters of a generic union or generic function.

Union (Statement)

The union statement defines a new type whose values are created by invoking one of the constructors declared inside the union.

Example:

The following union statement defines a Tree type that has two kinds of nodes, Leaf nodes with zero children and Internal nodes with two children. We create a three-node tree T3 by using the constructors Leaf and Internal to create the nodes.

Union (Operator on Sets)

Set union is defined in Set.pf. The union of sets A and B, written A ∪ B, contains the items that occur in either set.

Example:

Variable List

A comma-separated list of variable declarations. Each variable may optionally be annotated with its type.