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.

Add

The addition operator for unsigned integers is defined in UInt.pf and the one for integers is defined in Int.pf.

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)

The proof (apply X to Y) proves formula Q so long as

• X proves (if P then Q),
• Y proves P.

Example:

Arbitrary (Forall Introduction)

A proof of the form

is a proof of all x1:T1, ..., xn:Tn. P so long as

• 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 so long as

• X is a proof of Q.

The proof X may use the given 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.

Auto auto (Automatic Reduction)

To tell Deduce to automatically apply an equation, left to right, use the auto statement with the name of the theorem. For example, in UInt.pf we prove that zero multiplied by anything is zero and follow this theorem with an auto statement to register it for automatic reduction.

From here on, anytime Deduce sees a term containing a 0 multiplied by something, Deduce replaces it with 0.

Some care is needed when selecting equations for use with auto. For example, we do not register the uint_mult_commute theorem with auto because that would cause Deduce to go into an infinite loop.

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 (Proof)

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.

Compose (Functions)

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

Example:

The composition of the add1 with itself produces a function that adds 2. So applying that 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 so long as

• 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
• Contradict
• Expand-In
• Equations
• Evaluate
• Evaluate-In
• Help
• Identifier
• Induction
• Instantiation
• Period
• Question Mark
• Recall
• Sorry
• Switch
• Symmetric
• Transitive

Conjunct

A proof of the form

is a proof of Pn so long as

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

Example:

Contradict (Proof)

• The contradict proof expects a proof of some formula P and its negation, not P.
• The result of contradict is a proof of false.

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 of an equality with different constructors on the left and right-hand side, such as

or

then you can implicitly use X to prove false:

(2) If you have a proof of P and a proof of not P, then you can prove false using contradict.

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 an unsigned integer, so its type is UInt.

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

Divide

The division function for UInt is defined in UInt.pf. The main theorem is uint_div_mod which states, assuming m is positive, that

Example:

Expand (Proof)

In the current goal formula, expand the occurrences of the specified names with their definitions. 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.

Expand-In (Proof)

In the formula of the given proof, expand the occurrences of the specified names with their definitions, resulting in the formula that is proved by this expand-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.

In the example below, we write expand length in A to transform the formula

to

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.

When using replace or expand for one of the reasoning steps in equations, the transformation is, by default, applied to the left-hand side of the equation (and not the right-hand side). However, if you would like to apply a transformation to the right-hand side, use hash marks (#) around the region of the right-hand side that you want to change.

Example:

In the following example, the hash marks tell Deduce to expand the definition of length in the right-hand side of the second equation.

Evaluate (Proof)

The evaluate proof method simplifies the goal formula by expanding all definitions (except for opaque ones). 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 expanding all definitions (except for opaque ones), 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.)

See the entry for Contradiction for an example of both proving false and using false to prove something else.

Formula

A formula is any term of type bool.

Function (Term)

Functions are created with a fun expression. Their syntax starts with fun, 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.

To add type parameters to a function (to make it generic), see Generic Function.

Function (Statement)

The fun statement is for defining a function (non-recursive). The function statement begins with its visibility, then the fun keyword, followed by the type parameters enclosed in < and > (if generic), then the parameter list enclosed in ( and ), and finally the body of the function enclosed in { and }.

Function Type

A function type classifies a function. This includes both recursive functions (recursive) and non-recursive 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 recursive functions can be defined using the recursive statement (see Recursive Function).

Generic Function (Term)

To make a Function generic, add type parameters surrounded by < and >. For example, the following function declares two type parameters with the syntax <T, U>.

Given

An assumption or fact that is known to be true at a specific step within a proof.

Greater-Than

The greater-than operator on unsigned integers is defined in UInt.pf and is defined in terms of less-than as follows

Example:

Greater-Than or Equal

The greater-than-or-equal operator on unsigned integers is defined in UInt.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.

Inside the proof X the goal changes to P.

After the have statement, 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.

Identifier List Bar

A bar-separated sequence of identifiers used in the syntax for Expand and Expand-Int to specify which definitions to expand. To tell Deduce to expand a definition multiple times (e.g. for a recursive function), preceed the identifier by a number and the multiplication sign.

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 X_i is a proof of P where x is replaced by c_i(e_i1,...,e_ij). The type T must be a union type. Each proof X_i may use its induction hypotheses IH_i. For each term e_in whose type is T (so it is recursive), the induction hypothesis is the formula P with x replaced by the constructor argument e_in.

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. In the following example, at the bottom of the proof, we instantiate len_node_1 with the type UInt and then the term 42, with the syntax len_node_1<UInt>[42].

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 unsigned integers is defined in UInt.pf. To find theorems about the less-than operator in UInt.thm, search for theorems with less in the name.

Example:

Less-Than or Equal

The less-than-or-equal operator on unsigned integers is defined in UInt.pf. To find theorems about the less-than operator in UInt.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 replace or expand proof to only apply to that subterm.

The equations feature, by default, places marks around the entire left-hand side of each equation. However, you can override this default by placing explicit marks.

Modulo

The modulo operator is defined in UInt.pf as follows.

Example:

Modus Ponens

See the entry for Apply-To.

Multiply

Multiplication on unsigned integers is defined in UInt.pf. To find theorems about multiplication, search for mult in UInt.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.

Natural Number

An natural number literal is the symbol ℕ followed by a sequence of one or more digits.

The operations on natural numbers and theorems about them are in Nat.thm.

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 (Proof)

A proof of the form

is a proof of formula Q so long as

• Y proves Q.
• Xproves some x1:T1,...,xn:Tn. P.

The proof Y may use the given label as a proof of P and it may also refer to the proof of P by writing recall P.

Example:

Opaque (Visibility)

See Visibility.

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

Private (Visibility)

See Visibility.

Public (Visibility)

See Visibility.

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 Replace (Proof).

Proof Statement

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

• Arbitrary
• Assume
• Choose
• Define
• Expand
• Extensionality
• Have
• Injective
• Obtain
• Replace
• Show
• 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.

Reason

Recall (Proof)

A proof of the form

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.

Recursive Function (Statement)

The recursive 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 recursive 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 unsigned integers.

There are two clauses in the body of length because the UIntList 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.

Reflexive (Proof)

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

Replace (Proof)

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

Replace-In (Proof)

In the formula of the given proof, replace according to the equalities proved by the specified Proof List, resulting in the formula that is proved by this replace-in statement. The algorithm for rewriting described in the entry for Replace (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.

Show (Proof)

Use show to document the current goal formula. Deduce checks to make sure that the given formula matches the current goal.

Some (Formula)

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.

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.

Example:

Subtract (Producing Integers)

Subtraction of Unsigned Integers (aka. monus or truncated subtraction)

The monus operator is different from ordanary subtraction on integers because there are no negative unsigned integers. If you subtract a larger unsigned integer from a smaller one, the result of monus is 0.

To search for theorems about monus in UInt.thy, search for theorems with monus 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 uint_add_zero from UInt.thm.

Suppose

See the entry for Assume.

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:

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:

Unsigned Integer

An unsigned integer literal is a sequence of one or more digits.

Variable List

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

Visibility

The visibility of a statement controls how the defined name can be used outside of the current module.

• The default visibility is public, which means the name can be freely used outside the current module.
• A private name cannot be mentioned outside of the current module.
• An opaque name can be mentioned in other modules but it cannot be expanded (via the expand or evaluate statements). The constructors of an opaque union are always private.