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.
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
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
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.
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
formula ::= formula "and" formula
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
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]
conclusion ::= "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
proof_stmt ::= "arbitrary" var_list
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
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
proof_stmt ::= "assume" assumption
| "suppose" assumption
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 ::= 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.
@See the entry for Instantiation.
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).
type ::= "bool"
The type bool classifies the values true annd false.
A formula is a term of type bool.
proof ::= "{" proof "}"
A proof may be surrounded in curly braces.
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
conclusion ::= "cases" proof case_list
case_list ::= case | case case_list
case ::= "case" identifier "{" proof "}"
| "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 rewrite 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
}
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:
theorem choose_example: some x:Nat. 6 = 2 * x
proof
choose 3
enable {operator*, operator+, operator+, operator+}
conclude 6 = 2 * 3 by .
end
conclusion ::= proof "," proof
See the entry for And (logical conjunction).
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
conclusion ::= "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
The last statement in a proof (the conclusion symbol in the grammar)
must be one of the following:
conclusion ::= "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
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
have X: empty = Node(3, empty) by ...
then you can implicitly use X to prove false:
conclude false by X
(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.)
have X: P by ...
have Y: not P by ...
conclude false by apply Y to X
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.
term ::= "define" identifier "=" term ";" term
This associates a name with a term for use in the term after the semicolon.
assert 5 = (define x = 3; 2 + x)
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.)
theorem define_proof_example: all x:Nat. 2 * (x + x + x) = (x + x + x) + (x + x + x)
proof
arbitrary x:Nat
define y = x + x + x
suffices y + (y + 0) = y + y
by definition {operator*,operator*,operator*}
rewrite add_zero[y]
end
conclusion ::= "definition" identifier
| "definition" "{" identifier_list "}"
In the current goal formula, replace the occurences 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.
theorem length_list2: length([0,1]) = 2
proof
suffices 1 + length([1]) = 2
by definition length
suffices 1 + (1 + 0) = 2
by definition {length, length}
definition {operator+, operator+}
end
conclusion ::= "definition" "{" identifier_list "}" "and" "rewrite" proof_list
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.
conclusion ::= "definition" identifier "in" proof
conclusion ::= "definition" "{" identifier_list "}" "in" proof
In the formula of the given proof, replace the occurences 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.
theorem definition_in_example: all ls:List<Nat>. if length(ls) = 0 then ls = []
proof
arbitrary ls:List<Nat>
switch ls {
case [] {
.
}
case node(x, ls') {
assume A: length(node(x, ls')) = 0
have B: 1 + length(ls') = 0 by definition length in A
have C: suc(length(ls')) = 0 by definition operator+ in B
conclude false by C
}
}
end
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
term ::= "∅"
The empty set ∅ does not contain any elements and is defined in
Set.pf.
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.)
conclusion ::= "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
conclusion ::= "evaluate"
The evaluate proof method simplies the goal formula by applying all
definitions. It succeeds if the formula is simplified to true.
conclusion ::= "evaluate" "in" proof
The evaluate-in proof method simplies the formula of the given
proof by applying all definitions, producing a proof of the simplified
formula.
proof_stmt ::= "extensionality"
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
formula ::= "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.)
A formula is any term of type bool.
formula ::= 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.
statement ::= "function" identifier type_params_opt "(" type_list ")" "->" type "{" fun_case* "}"
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.
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.
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 >.
formula ::= "<" identifier_list ">" formula
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
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).
An assumption or fact that is already proved.
formula ::= 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)
formula ::= term "≥" term
formula ::= 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)
proof_stmt ::= "have" identifier ":" term "by" proof
| "have" ":" term "by" 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.
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.
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..
A comma-separated sequence of identifiers.
identifier_list ::= identifier
identifier_list ::= identifier "," identifier_list
See the entry for Biconditional.
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.)
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
statement ::= "import" identifier
Import all of the definitions and theorems from the specified file (without the file extension).
formula ::= term "∈" term
formula ::= 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)
conclusion ::= "induction" type ind_case*
ind_case ::= "case" pattern "{" proof "}"
| "case" pattern "assume" assumption_list "{" proof "}"
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
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:
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
conclusion ::= proof '<' type_list '>'
| 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
term ::= @ term '<' type_list '>'
Instantiates a generic function or constructor, replaces its type parameters with the given type arguments.
define empty_nat_list = @empty<Nat>
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)
formula ::= 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)
formula ::= 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)
term ::= "[" term_list "]"
Deduce treats [t1,t2,...,tn] as syntactic sugar for
node(t1, node(t2, ... node(tn, empty))).
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)))
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
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
See the entry for Apply-To.
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
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.
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).
formula ::= term "≠" term
formula ::= term "/=" term
Deduce treats x ≠ y as syntactic sugar for not (x = y).
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 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
formula ::= formula "or" formula
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)
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_intro2: 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
To use a given of the form P or Q, use
Cases (Disjunction Elimination).
term ::= "(" term ")"
formula ::= "(" formula ")"
proof ::= "(" proof ")"
A term, formula, or a proof may be surrounded in parentheses.
pattern ::= identifier | "0" | "true" | "false" | identifier "(" identifier_list ")"
This syntax is used in Switch (Term), Switch (Proof), and Function (Statement) via Pattern List.
param_list ::= ε | pattern | 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).
conclusion ::= "."
A period is a proof of the formula true in Deduce.
The type of positive integers Pos is defined in Nat.pf.
proof ::= proof_stmt proof
| conclusion
A proof is a sequence of zero or more proof statements that finishes with a conclusion.
proof_list :: proof
proof_list ::= proof "|" proof_list
A list of proofs separated by vertical bars. This syntax is used in Rewrite (Proof).
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).
statement ::= "print" term
You can ask Deduce to print a value to standard output using the
print statement.
print five
The output is 5.
? (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.
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.
conclusion ::= reflexive
The proof reflexive proves that a = a for any term a.
conclusion ::= "rewrite" proof_list
Rewrite the current goal formula according to the equalities proved by
the specified Proof List. For each equality, any term
in the goal formula that is equal to its left-hand side is replaced by
its right-hand side. If all the rewriting simplifies the goal formula
to true, then this statement proves the goal. Otherwise, Deduce
signals an error.
theorem rewrite_example: all x:Nat,y:Nat. if (x = y) then (1 + x = 1 + y)
proof
arbitrary x:Nat,y:Nat
assume prem: x = y
suffices 1 + y = 1 + y by rewrite prem
.
end
conclusion ::= "rewrite" proof_list "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. In
particular, for each equality, any term in the formula that is equal
to the left-hand side of the equality is replaced by the right-hand
side of the equality.
theorem rewrite_in_example: all x:Nat, y:Nat.
if x < y then not (x = y)
proof
arbitrary x:Nat, y:Nat
assume: x < y
assume: x = y
have: y < y by rewrite (recall x = y) in (recall x < y)
conclude false by apply less_irreflexive[y] to (recall y < y)
end
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.
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
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.
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)
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:
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
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:
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
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.
proof_stmt ::= "suffices" formula "by" 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
See the entry for Assume.
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.
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.
A term list is a comma-separated sequence of zero or more terms.
term_list ::= ε | term | term "," term_list
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.
formula ::= "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
type ::= "bool" // type of a Boolean
| identifier // type of a union
| identifier "<" type_list ">" // type of a generic union
| "fn" type_params_opt type_list "->" type // type of a function
| "(" type ")"
type_list ::= ε | type | type "," type_list
A type list is a comma-separated list of zero or more types.
type_params_opt ::= ε | "<" identifier_list ">"
Specifies the type parameters of a generic union or generic function.
statement ::= "union" identifier type_params_opt "{" constructor* "}"
constructor ::= identifier | 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 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)
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')
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.