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

term ::= term "+" term

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

Example:

Add (Multiset)

term ::= term "⨄" term
term ::= term "[+]" term

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.

cnt_sum: all T:type. all A:MultiSet<T>, B:MultiSet<T>, x:T.
  cnt(A ⨄ B)(x) = cnt(A)(x) + cnt(B)(x)

Example:

All (Universal Quantifier)

formula ::= "all" var_list "." formula

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)

formula ::= formula "and" formula

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

term ::= term "++" term

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

function operator ++ <E>(List<E>, List<E>) -> List<E> {
  operator ++(empty, ys) = ys
  operator ++(node(n, xs), ys) = node(n, xs ++ ys)
}

Example:

Apply-To Proof (Modus Ponens)

conclusion ::= "apply" proof "to" proof

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

Example:

Arbitrary (Forall Introduction)

proof_stmt ::= "arbitrary" var_list

A proof of the form

arbitrary x1:T1, ..., xn:Tn
X

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

The variables x1, ..., xn may appear in the formula P and the proof X.

Example:

Assert (Statement)

statement ::= "assert" term

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

proof_stmt ::= "assume" assumption
proof_stmt ::= "suppose" assumption

A proof of the form

assume label: P
X

is a proof of the formula if P then Q so long as

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

assumption ::= identifier
assumption ::= identifier ":" formula
assumption ::= ":" formula



assumption_list ::= assumption
assumption_list ::= assumption "," assumption_list

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

At Symbol @

See the entry for Instantiation.

Auto auto (Automatic Reduction)

statement ::= "auto" identifier

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.

theorem uint_zero_mult: all n:UInt. 0 * n = 0
proof
  ...
end



auto uint_zero_mult

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.

theorem uint_mult_commute: all m:UInt, n:UInt.
  m * n = n * m

Biconditional (if and only if)

formula ::= formula "⇔" formula
formula ::= formula "<=>" formula
formula ::= formula "iff" formula

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

Bool (Type)

type ::= "bool"

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

Braces (Proof)

proof ::= "{" proof "}"

A proof may be surrounded in curly braces.

Call (Term)

term ::= term "(" term_list ")"

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

Cases (Disjunction Elimination)

conclusion ::= "cases" proof case_list
case_list ::= case | case case_list
case ::= "case" identifier "{" proof "}"
case ::= "case" identifier ":" term "{" proof "}"

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.

have tri: x < y or x = y or y < x by trichotomy[x][y]
cases tri
case x_l_y: x < y {
  have x_le_y: x ≤ y by apply less_implies_less_equal[x][y] to x_l_y
  conclude x ≤ y or y < x by x_le_y
}
case x_eq_y: x = y {
  have x_le_y: x ≤ y by
      suffices y ≤ y  by replace x_eq_y.
      less_equal_refl[y]
  conclude x ≤ y or y < x by x_le_y
}
case y_l_x: y < x {
  conclude x ≤ y or y < x by y_l_x
}

Choose (Proof)

proof_stmt ::= "choose" term_list

A proof of the form

choose e1,...,en
X

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)

conclusion ::= proof "," proof

See the entry for And.

Compose (Functions)

term ::= term "∘" term
term ::= term "[o]" term

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)

conclusion ::= "conclude" formula reason

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

conclude P by X

is a proof of formula P so long as

Example:

Conclusion (Proof)

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

Conjunct

conclusion ::= "conjunct" number "of" proof 

A proof of the form

conjunct n of X

is a proof of Pn so long as

Example:

Contradict (Proof)

conclusion ::= "contradict" proof "," proof

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

have X: empty = node(3, empty) by ...

or

have X: 0 = 1 by ...

then you can implicitly use X to prove false:

conclude false by X

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

have X: P by ...
have Y: not P by ...
conclude false by contradict Y, X

Define (Statement)

statement ::= visibility "define" ident ":" type "=" term
            | visibility "define" ident "=" term

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)

term ::= "define" identifier "=" term ";" term

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

Define (Proof)

proof_stmt ::= "define" identifier "=" term  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.)

Expand (Proof)

proof_stmt ::= "expand" identifier_list_bar

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)

conclusion ::= "expand" identifier_list_bar "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

length(node(x, ls')) = 0

to

1 + length(ls') = 0

Divide

term ::= term "/" term

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

(n / m) * m + (n % m) = n

Example:

Empty Set

term ::= "∅"

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

Equal

formula ::= term "=" term

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

conclusion ::= "equations" equation equation_list
equation ::= term "=" term reason
half_equation ::= "..." "=" term reason
equation_list ::= half_equation
equation_list ::= half_equation equation_list
equation_list ::= "$" equation equation_list

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)

conclusion ::= "evaluate"

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)

conclusion ::= "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

proof_stmt ::= "extensionality"

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

False

formula ::= "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.

formula ::= term

Function (Term)

term ::= "fun" var_list "{" term "}"
term ::= "λ" var_list "{" 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)

statement ::= visibility "fun" ident type_params_opt "(" var_list ")" "{" term "}"

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

type ::= "fn" type_params_opt type_list "->" 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)

formula ::= "<" identifier_list ">" 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.

<T> all xs:List<T>. if length(xs) = 0 then xs = empty

Generic (Term)

term ::= "generic" identifier_list "{" term "}"

A term of the form

generic T1, ..., Tn { X }

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)

term ::= "fun" type_params_opt var_list "{" term "}"
term ::= "λ" type_params_opt var_list "{" 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

formula ::= term ">" term

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

x > y = y < x

Example:

Greater-Than or Equal

formula ::= term "≥" term
formula ::= term ">=" term

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

x ≥ y = y ≤ x

Example:

Have (Proof Statement)

proof_stmt ::= "have" identifier ":" term reason 
proof_stmt ::= "have" ":" term reason 

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

A proof of the form

have label: P by X
Y

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)

conclusion ::= "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

term ::= identifier
formula ::= identifier
conclusion ::= 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 ::= identifier
identifier_list ::= identifier "," identifier_list

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.

identifier_list_bar ::= identifier
identifier_list_bar ::= natural_number "*" identifier
identifier_list_bar ::= identifier "|" identifier_list_bar
identifier_list_bar ::= natural_number "*" identifier "|" identifier_list_bar

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

if a then b else c

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

Example:

Import (Statement)

statement ::= "import" identifier

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

In (Set Membership)

formula ::= term "∈" term
formula ::= term "in" term

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

Example:

Induction

conclusion ::= "induction" type ind_case*
ind_case ::= "case" pattern "{" proof "}"
ind_case ::= "case" pattern "assume" assumption_list "{" proof "}"

A proof of the form

induction T
case c_1(e_11,...,e_1k) assume IH_1, ... { X_1 }
...
case c_n(e_n1,...,e_nj) assume IH_n, ... { X_n }

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)

proof_stmt ::= "injective" term 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)

conclusion ::= proof '<' type_list '>'
conclusion ::= proof '[' term_list ']'

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)

term ::= @ term '<' type_list '>'

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

Intersection

term ::= term "∩" term
term ::= term "&" term

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

formula ::= term "<" term

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

formula ::= term "≤" term
formula ::= term "<=" term

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)

term ::= "[" term_list "]"

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.

union List<T> {
  empty
  node(T, List<T>)
}

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

Mark

term ::= "#" term "#"

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

term ::= term "%" term

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

n % m = n ∸ (n / m) * m

Example:

Modus Ponens

See the entry for Apply-To.

Multiply

term ::= term "*" term

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

natural_number ::= ℕ[0-9]+
term ::= 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

formula ::= "not" formula

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

Not Equal

formula ::= term "≠" term
formula ::= term "/=" term

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

Obtain (Proof)

proof_stmt ::= "obtain" identifier_list "where" assumption "from" proof

A proof of the form

obtain x1,...,xn where label: P from X
Y

is a proof of formula Q so long as

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)

visibility ::= "opaque"

See Visibility.

Or (logical disjunction)

formula ::= formula "or" formula

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

term ::= "(" term ")"
formula ::= "(" formula ")"
proof ::= "(" proof ")"

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

Pattern

pattern ::= identifier
pattern ::= "true"
pattern ::= "false"
pattern ::= identifier "(" identifier_list ")"

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

Parameter List

param_list ::= ε
param_list ::= pattern
param_list ::= pattern "," identifier_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)

conclusion ::= "."

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

Private (Visibility)

visibility ::= "private"

See Visibility.

Public (Visibility)

visibility ::= "public"

See Visibility.

Proof

proof ::= proof_stmt proof
proof ::= conclusion

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

Proof List

proof_list :: proof 
proof_list ::= proof "|" 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).

statement ::= "print" term

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

The output is 5.

Question Mark ? (Proof)

conclusion ::= "?"

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

reason ::= "by" proof
reason ::= "begin" proof "end"

Recall (Proof)

conclusion ::= "recall" term_list

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.

Recursive Function (Statement)

statement ::= visibility "recursive" identifier type_params_opt "(" type_list ")" "->" type "{" fun_case* "}"
fun_case ::= identifier "(" pattern_list ")" "=" term

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.

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)

conclusion ::= reflexive

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

Replace (Proof)

proof_stmt ::= "replace" proof_list

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)

conclusion ::= "replace" proof_list "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)

proof_stmt ::= "show" formula

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

Some (Formula)

formula ::= "some" var_list "." 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)

conclusion ::= "sorry"

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

formula ::= term "⊆" term
formula ::= term "(=" term

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 (Producing Integers)

term ::= term "-" term

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

term ::= term "∸" term

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)

proof_stmt ::= "suffices" formula reason

A proof of the form

suffices P by X
Y

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

length(node(3, empty)) = 1

into

1 + 0 = 1

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)

term ::= "switch" term "{" switch_case* "}"
switch_case ::= "case" pattern "{" 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)

conclusion ::= "switch" term "{" switch_proof_case* "}"
switch_proof_case ::= "case" pattern "{" proof "}"
switch_proof_case ::= "case" pattern assumptions "{" proof "}"
assumptions ::= "suppose" assumption_list | "assume" assumption_list

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

A proof of the form

switch t {
  case p1 assume eq1: t = p1 {
    X1
  }
  ...
  case pn assume eqn: t = pn {
    Xn
  }
}

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)

conclusion ::= "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)

statement ::= "theorem" IDENT ":" formula reason
statement ::= "lemma" IDENT ":" formula reason

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

theorem label: P
proof
  X
end

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.

term_list ::= ε
term_list ::= term
term_list ::= term "," term_list

Transitive (Proof)

conclusion ::= "transitive" proof 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)

formula ::= "true"

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

Type

type ::= "bool"                                        // type of a Boolean
type ::= identifier                                    // type of a union
type ::= identifier "<" type_list ">"                  // type of a generic union
type ::= "fn" type_params_opt type_list "->" type      // type of a function 
type ::= "(" type ")"

Type List

type_list ::= ε
type_list ::= type
type_list ::= type "," type_list

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

Type Parameters

type_params_opt ::= ε
type_params_opt ::= "<" identifier_list ">"

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

Union (Statement)

statement ::= visibility "union" identifier type_params_opt "{" constructor* "}"
constructor ::= identifier
constructor ::= identifier "(" type_list ")"

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)

term ::= term "∪" term
term ::= term "|" term

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

unsigned_integer ::= [0-9]+
term ::= unsigned_integer

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

Variable List

var_list ::= ε
var_list ::= ident
var_list ::= ident ":" type
var_list ::= ident ":" type "," var_list
var_list ::= ident "," var_list

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

Visibility

visibility ::= ε
visibility ::= "public"
visibility ::= "private"
visibility ::= "opaque"

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