deduce

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 astericks 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

term ::= term "+" term

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

function operator +(Nat,Nat) -> Nat {
  operator +(0, m) = m
  operator +(suc(n), m) = suc(n + m)
}

Example:

assert 2 + 3 = 5

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:

define A = m_one(5) ⨄ m_one(3) ⨄ m_one(5)
assert cnt(A)(3) = 1
assert cnt(A)(5) = 2
assert cnt(A)(7) = 0

All (Universal Quantifier)

term ::= "all" var_list "." term

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.

theorem all_example_bool: all P:bool. P = true or P = false
proof
  arbitrary P:bool
  switch P {
    case true { . }
    case false { . }
  }
end

theorem all_example_intro: all x:Nat,y:Nat,z:Nat. x + y + z = z + y + x
proof
  arbitrary x:Nat, y:Nat, z:Nat
  equations
    x + y + z = (x + y) + z by symmetric add_assoc[x][y, z]
          ... = (y + x) + z by rewrite add_commute[x][y]
          ... = z + y + x by add_commute[y+x][z]
end

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.

theorem all_example_elim: 1 + 2 + 3 = 3 + 2 + 1
proof
  all_example_intro[1, 2, 3]
end

And (logical conjunction)

term ::= term "and" term

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

Example:

assert true and true
assert not (true and false)
assert not (false and true)
assert not (false and false)

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

theorem and_example_intro: (1 = 0 + 1) and (0 = 0 + 0)
proof
  have eq1: 1 = 0 + 1 by definition operator+
  have eq2: 0 = 0 + 0 by definition operator+
  conclude (1 = 0 + 1) and (0 = 0 + 0) by eq1, eq2
end

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

theorem and_example_elim: all P:bool, Q:bool. if P and Q then Q and P
proof
  arbitrary P:bool, Q:bool
  assume prem: P and Q
  have p: P         by prem   // P and Q  used to prove  P
  have q: Q         by prem   // P and Q  used to prove  Q
  conclude Q and P  by p, q
end

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:

assert [1,2] ++ [3,4] = [1,2,3,4]

Apply-To Proof (Modus Ponens)

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

A proof of the form

apply X to Y

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

Example:

theorem apply_to_example: all P:bool, Q:bool, R:bool.
  if (if P then Q) and (if Q then R) and P
  then R
proof
  arbitrary P:bool, Q:bool, R:bool
  suppose prem: (if P then Q) and (if Q then R) and P
  have pq: if P then Q  by prem
  have p: P             by prem
  have q: Q             by apply pq to p
  have qr: if Q then R  by prem
  conclude R            by apply qr to q
end

Arbitrary (Forall Introduction)

proof ::= "arbitrary" var_list  proof

A proof of the form

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

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:

theorem arbitrary_example: all x:Nat,y:Nat. if x = y then y = x
proof
  arbitrary x:Nat,y:Nat
  conclude if x = y then y = x by
    assume: x = y
    symmetric (recall x = y)
end

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.

assert (if true then 7 else 5+6) = 7

Assume

proof ::= "assume" assumption proof
        | "suppose" assumption proof

A proof of the form

assume label: P
X

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.

theorem assume_example: all x:Nat,y:Nat. if (x = y) then (1 + x = 1 + y)
proof
  arbitrary x:Nat,y:Nat
  assume prem: x = y
  conclude 1 + x = 1 + y  by rewrite prem
end

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.

Biconditional (if and only if)

term ::= term "⇔" term
       | term "<=>" term
       | term "iff" term

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 annd false. A formula is a term of type bool.

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.

assert length(list_example) = 3

Choose (Exists Elimination)

proof ::= "choose" term_list  proof

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:

theorem choose_example: some x:Nat. 6 = 2 * x
proof
  choose 3
  enable {operator*, operator+, operator+, operator+}
  conclude 6 = 2 * 3   by .
end

Comma (Conjunction/And Introduction)

term ::= term "," term

See the entry for And (logical conjunction).

Compose (Functions)

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:

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

assert (suc ∘ suc)(3) = 5

Conclude

proof ::= "conclude" formula "by" 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

conclude P by X

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

Example:

theorem conclude_example: 1 + 1 = 2
proof
  conclude 1 + 1 = 2 by definition {operator+,operator+}
end

Conjunct

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

A proof of the form

conjunct n of X

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

Example:

theorem conjunct_example: all P:bool, Q:bool. if P and Q then Q and P
proof
  arbitrary P:bool, Q:bool
  assume prem: P and Q
  have p: P         by conjunct 0 of prem
  have q: Q         by conjunct 1 of prem
  conclude Q and P  by p, q
end

Define (Statement)

statement ::= "define" ident ":" type "=" term
            | "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.

define five = 2 + 3
define six : Nat = 1 + five

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)

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

This associates a name with a term for use in the subsequent term.

assert 5 = (define x = 3
            2 + x)

Divide

term ::= term "/" term

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

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

Example:

define three = succ(succ(one))
assert 6 / three = 2
assert 7 / three = 2
assert 8 / three = 2
assert 9 / three = 3

Empty Set

term ::= "∅"

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

Equal

term ::= 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

proof ::= "equations" equation equation_list
equation ::= term "=" term "by" proof
half_equation ::= "..." "=" term "by" proof
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.

Example:

theorem equations_example: all x:Nat, y:Nat, z:Nat.
  x + y + z = z + y + x
proof
  arbitrary x:Nat, y:Nat, z:Nat
  equations
    x + y + z = x + z + y      by rewrite add_commute[y][z]
          ... = (x + z) + y    by rewrite symmetric add_assoc[x][z,y]
          ... = (z + x) + y    by rewrite symmetric add_commute[z][x]
          ... = z + x + y      by rewrite add_assoc[z][x,y]
          ... = z + y + x      by rewrite add_commute[x][y]
end

Extensionality

term ::= "extensionality" proof

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

define inc = fun x:Nat { pred(suc(suc(x))) }

theorem extensionality_example: inc = suc
proof
  extensionality
  arbitrary x:Nat
  conclude inc(x) = suc(x) by definition {inc, pred}
end

False

term :: = "false"

One can prove false when there are assumptions that contradict eachother, 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.

formula ::= term

Function (Term)

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

define area = λ h:Nat, w:Nat { h * w }

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

print area(3, 4)

The output is 12.

Function (Statement)

statement ::= "function" identifier type_params_opt "(" type_list ")" "->" type "{" fun_case_list "}"
fun_case_list ::= fun_case | fun_case fun_case_list
fun_case ::= identifier "(" pattern_list ")" "=" term

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.

function length(NatList) -> Nat {
  length(Empty) = 0
  length(Node(n, next)) = 1 + length(next)
}

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

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

term ::= "<" identifier_list ">" term

This parameterizes a formula by a list of type paremeters. 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.

define operator ∘ = generic T,U,V { λ g:fn U->V, f:fn T->U {
                        λ x:T { g(f(x)) } } }

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

Greater-Than

term ::= term ">" term

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

x > y = y < x

Example:

assert 2 > 1
assert not (1 > 1)
assert not (0 > 1)

Greater-Than or Equal

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

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

x ≥ y = y ≤ x

Example:

assert 2 ≥ 1
assert 1 ≥ 1
assert not (0 ≥ 1)

Have (Forward Proof)

proof ::= "have" identifier ":" term "by" proof proof
        | "have" ":" term "by" proof proof

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. The formula P becomes a given and can be used inside the proof Y.

Help (Proof)

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

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:

assert (if true then 1 else 2) = 1
assert (if false then 1 else 2) = 2

theorem if_then_else_example: all P:bool.
  (if P then 1 else 2) = (if not P then 2 else 1)
proof
  arbitrary P:bool
  switch P {
    case true { . }
    case false { . }
  }
end

Import (Statement)

statement ::= "import" identifier

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

In (Set Membership)

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

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

Example:

define S = single(1) ∪ single(2) ∪ single(3)
assert 1 ∈ S and 2 ∈ S and 3 ∈ S and not (4 ∈ S)

Induction

proof ::= "induction" type ind_case*

A proof of the form

induction T
case c1(e11,...,e1k) assume IH1, ... { X1 }
...
case cn(en1,...,enj) assume IH1, ... { Xn }

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:

theorem induction_example: all n:Nat.
  n + 0 = n
proof
  induction Nat
  case 0 {
    conclude 0 + 0 = 0   by definition operator+
  }
  case suc(n') suppose IH: n' + 0 = n' {
    equations
      suc(n') + 0 = suc(n' + 0)  by definition operator+
              ... = suc(n')      by rewrite IH
  }
end

Injective (Proof)

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

theorem injective_example: all x:Nat, y:Nat, z:Nat.
  if suc(x) = suc(y) and suc(y) = suc(z) then x = z
proof
  arbitrary x:Nat, y:Nat, z:Nat
  suppose prem: suc(x) = suc(y) and suc(y) = suc(z)
  have: x = y by injective suc prem
  have: y = z by injective suc prem
  transitive (recall x = y) (recall y = z)
end

Instantiation (Proof)

proof ::= proof '<' type_list '>'
proof ::= 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:

theorem instantiate_proof_example: length(node(42, empty)) = 1
proof
  have X: all T:type. all x:T. length(node(x, empty)) = 1 by {
    arbitrary T:type arbitrary x:T
    definition {length, length, operator+, operator+}
  }
  conclude length(node(42, empty)) = 1
    by X<Nat>[42]
end

Instantiation (Term)

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

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

define empty_nat_list : List<Nat> = @empty<Nat>

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:

define C = single(1) ∪ single(2)
define D = single(2) ∪ single(3)
assert 2 ∈ C ∩ D
assert not (1 ∈ C ∩ D)
assert not (3 ∈ C ∩ D)

Less-Than

term ::= term "<" term

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

x < y = suc(x) ≤ y

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

Example:

assert 1 < 2
assert not (1 < 1)
assert not (2 < 1)

Less-Than or Equal

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

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

function operator ≤(Nat,Nat) -> bool {
  operator ≤(0, m) = true
  operator ≤(suc(n'), m) =
    switch m {
      case 0 { false }
      case suc(m') { n' ≤ m' }
    }
}

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

Example:

assert 1 ≤ 1
assert 1 ≤ 2
assert not (2 ≤ 1)

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.

define list_example = node(3, node(8, node(4, empty)))

Mark

term ::= "#" term "#"

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

theorem mark_example: all x:Nat. if x = 1 then x + x + x = 3
proof
  arbitrary x:Nat
  suppose: x = 1
  equations
    #x# + x + x = 1 + x + x   by rewrite recall x = 1
  $ 1 + #x# + x = 1 + 1 + x   by rewrite recall x = 1
  $ 1 + 1 + #x# = 1 + 1 + 1   by rewrite recall x = 1
            ... = 3           by definition {operator+,operator+}
end

Modulo

term ::= term "%" term

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

n % m = n - (n / m) * pos2nat(m)

Example:

define two = succ(one)
assert 1 % two = 1
assert 2 % two = 0
assert 3 % two = 1
assert 4 % two = 0

Modus Ponens

See the entry for Apply-To.

Multiply

term ::= term "*" term

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

function operator *(Nat,Nat) -> Nat {
  operator *(0, m) = 0
  operator *(suc(n), m) = m + (n * m)
}

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

Example:

assert 2 * 3 = 6

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

term ::= "not" term

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

Not Equal

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

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

Obtain

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

A proof of the form

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

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:

theorem obtain_example: all n:Nat. 
  if (some x:Nat. n = 4 * x) then (some x:Nat. n = 2 * x)
proof
  arbitrary n:Nat
  assume prem: (some x:Nat. n = 4 * x)
  obtain x where m4: n = 4 * x from prem
  choose 2 * x
  equations
     n = 4 * x          by m4
   ... = #2 * 2# * x    by definition {operator*,operator*,operator*,
                                       operator+,operator+,operator+}
   ... = 2 * (2 * x)    by mult_assoc
end

Or (logical disjunction)

term ::= term "or" term

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

Example:

assert true or true
assert true or false
assert false or true
assert not (false or false)

Prove `P or Q`

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

theorem or_example_intro1: all P:bool, Q:bool. if P then P or Q
proof
  arbitrary P:bool, Q:bool
  assume: P
  conclude P or Q by recall P
end

theorem or_example_intro1: all P:bool, Q:bool. if Q then P or Q
proof
  arbitrary P:bool, Q:bool
  assume: Q
  conclude P or Q by recall Q
end

Pattern

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

Pos (Positive Integers)

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

Print (Statement)

statement ::= "print" term

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

print five

The output is 5.

Question Mark `?` (Proof)

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)

proof ::= "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 of givens at the current point in the proof.

Reflexive (proof)

proof ::= reflexive

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

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)

term ::= "some" var_list "." term

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)

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

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.

define flip = fun x:bool {
  switch x {
    case true { false }
    case false { true }
  }
}
assert flip(false)
assert not flip(true)

Switch (Proof)

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

theorem switch_proof_example: all x:Nat. x = 0 or 0 < x
proof
  arbitrary x:Nat
  switch x {
    case zero {
      conclude true or 0 < 0 by .
    }
    case suc(x') {
      have z_l_sx: 0 < suc(x')
          by definition {operator <, operator ≤, operator ≤}
      conclude suc(x') = 0 or 0 < suc(x') by z_l_sx
    }
  }
end

Subset or Equal

term ::= term "⊆" term
term ::= 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:

define E = single(1)
define F = single(1) ∪ single(2)

theorem subset_example: E ⊆ F
proof
  suffices all x:Nat. if x ∈ E then x ∈ F  by definition operator ⊆
  arbitrary x:Nat
  assume: x ∈ E
  have: 1 = x       by definition {E, operator∈, single, rep} in recall (x ∈ E)
  suffices 1 ∈ F    by rewrite symmetric (recall 1 = x)
  definition {F, operator∈, single, operator ∪, rep}
end

Subtract

term ::= term "-" term

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

function operator -(Nat,Nat) -> Nat {
  operator -(0, m) = 0
  operator -(suc(n), m) =
    switch m {
      case 0 { suc(n) }
      case suc(m') { n - m' }
    }
}

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.

assert 3 - 2 = 1
assert 3 - 3 = 0
assert 2 - 3 = 0

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

Suffices

proof ::= "suffices" formula "by" proof  proof

A proof of the form

suffices P by X
Y

is a proof of the formula Q if X is a proof that P imples 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 add_zero from Nat.thm.

theorem suffices_example:
  length(node(3, empty)) = 1
proof
  suffices 1 + 0 = 1  by definition {length, length}
  add_zero
end

Suppose

See the entry for Assume.

Symmetric (Proof)

proof ::= "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 ":" term "proof" proof "end"
            |   "lemma" IDENT ":" term "proof" proof "end"

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 | term "," term_list

Transitive (Proof)

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

term ::= "true"

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

theorem true_example: true
proof
  .
end

Union (Statement)

statement ::= "union" identifier type_params_opt "{" constructor_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 Tree {
  Leaf(Nat)
  Internal(Tree, Nat, Tree)
}

/*
            5
           / \
          4   7
*/
define T1 : Tree = Leaf(4)
define T2 : Tree = Leaf(7)
define T3 : Tree = Internal(T1, 5, T2)

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:

define C = single(1) ∪ single(2)
define D = single(2) ∪ single(3)
assert 1 ∈ C ∪ D
assert 2 ∈ C ∪ D
assert 3 ∈ C ∪ D
assert not (4 ∈ C ∪ D)

Variable List

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

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

<!- -

import Nat
import List

<<add_example>>
<<add_multiset_example>>
<<all_example_bool>>
<<all_example_intro>>
<<all_example_elim>>
<<and_example>>
<<and_example_intro>>
<<and_example_elim>>
<<append_example>>
<<apply_to_example>>
<<arbitrary_example>>
<<assert_example>>
<<assume_example>>
<<call_example>>
<<choose_example>>
<<compose_example>>
<<conclude_example>>
<<conjunct_example>>
<<define_example>>
<<define_term_example>>
<<division_example>>
<<equations_example>>
<<greater_example>>
<<greater_equal_example>>
<<if_then_else_example>>
<<membership_example>>
<<induction_example>>
<<instantiate_example>>
<<intersect_example>>
<<less_than_example>>
<<less_equal_example>>
<<list_example>>
<<mark_example>>
<<mod_example>>
<<obtain_example>>
<<or_example>>
<<or_example_intro1>>
<<or_example_intro2>>
<<print_example>>
<<switch_example>>
<<switch_proof_example>>
<<subset_example>>
<<suffices_example>>
<<true_example>>
<<union_example>>

–>

deduce

Add

Add (Multiset)

All (Universal Quantifier)

And (logical conjunction)

Append

Apply-To Proof (Modus Ponens)

Arbitrary (Forall Introduction)

Assert (Statement)

Assume

Assumption and Assumption List

At Symbol @

Biconditional (if and only if)

Bool (Type)

Call (Term)

Choose (Exists Elimination)

Comma (Conjunction/And Introduction)

Compose (Functions)

Conclude

Conjunct

Define (Statement)

Define (Term)

Divide

Empty Set

Equal

Equations

Extensionality

False

Formula

Function (Term)

Function (Statement)

Function Type

Generic (Formula)

Generic (Term)

Greater-Than

Greater-Than or Equal

Have (Forward Proof)

Help (Proof)

Identifier

Identifier List

If and only if (iff)

If Then (Conditional Formula)

If Then Else (Term)

Import (Statement)

In (Set Membership)

Induction

Injective (Proof)

Instantiation (Proof)

Instantiation (Term)

Intersection

Less-Than

Less-Than or Equal

List (Term)

List (Type)

Mark

Modulo

Modus Ponens

Multiply

MultiSet (Type)

Not

Not Equal

Obtain

Or (logical disjunction)

Prove P or Q

Pattern

Pos (Positive Integers)

Print (Statement)

Question Mark ? (Proof)

Recall (Proof)

Reflexive (proof)

Set (Type)

Some (Existential Quantifier)

Sorry (Proof)

Switch (Term)

Switch (Proof)

Subset or Equal

Subtract

Suffices

Suppose

Symmetric (Proof)

At Symbol `@`

Prove `P or Q`

Question Mark `?` (Proof)