Versions history

ClearSy : Initial version, 10/03/2008

David Deharbe: First draft version in english, 02/04/2009

ClearSy: review completed, 03/04/2009

Acknowledgements

This document was originally written by Thierry Lecomte (ClearSy).

French to English translation was performed by David Deharbe (Federal University of Rio Grande do Norte).

Introduction

This document is targeted to users of the prover that need to write mathematical rules to facilitate in the verification of the generated proof obligations. As a matter of fact:

the proof in predicate logic is undecidable
the rule base of the prover is finite (it has approximatively 2800 rules)

It may therefore be necessary to add rules, either in a Pmm file or in a PatchProver file.

We draw the attention of the reader on the unfortunate consequences of inadequate rules, that may induce an undesirable behavior of the prover. Particularly, employing false rules enables showing correct false proof obligations and thus jeopardize the development of a correct software.

This document contains advice to write rules that are correct and which verification will be easier to perform.

Bibliography

[1] Writing mathematical rules (this document)

[2] Reference manual of the B language

[3] Reference manual of the interactive prover

Terminology

Abbreviations

PO: proof obligation
RPT: rule proving tools
TRATL: translator of rules written in the theory language
RB: automatic prover rule base

Terms

Proof obligation: logic predicate produced by Atelier B from a component (machine, refinement, implementation), written in the B language and that needs to be proved to guarantee the soundness of this component.
Rule base: Set of mathematical rules written in the theory language that are necessary for the prover to achieve proofs.
Pmm: A file containing user rules that enrich the RB used to process the proof obligations of a component.
PatchProver: A file containing user rules that enriches the RB used to process the proof obligations of a project.

Introduction to the Theory Language

The mathematical rules used by the prover are written in the so-called “theory language”. Without getting into the details of this language, which is similar to PROLOG, the following sections expose the fundamental notions that may be employed to use the theory language for the purpose of defining mathematical rules.

What is a wildcard?

A wildcard is a value that can take any value (literal, expression, etc.) If it is assigned a value, then it is said to be instantiated.

The sole mechanism to represent a variable is the wildcard. A wildcard is denoted as a single (latin) alphabet letter: one cannot have more that 52 wildcards inside a rule (considering both uppercase and lowercase letters).

For instance, the expression

a + bb*cc - d

contains wildcards a and d and literals bb and cc.

Wildcards a and d may be instantiated with ee+1 and 3, respectively. We then obtain the expression:

ee + 1 + bb*cc - 3

What is a formula?

A formula is an expression that is built out of

wildcards,
literals and numbers
logical connectors:
- conjunction : &
- disjunction : or
- implication : =>
- equivalence : <=>
- negation : not
quantifications:
- universal quantification : !
- existential quantification : #
equality : =,
set membership : :,
set inclusion : <:
operators to combine arithmetic, set, boolean, relational, functional and sequence expressions of the B language (see [2] ), obeying the syntax of the B language.

For instance,

0=<aa & 0=<bb => 0<=aa*bb
a=TRUE or b=TRUE => a : BOOL

are syntactically correct formulas.

In summary, the language for formulas is the language of B expressions extended with wildcards.

Matching Formulas

A formula f is said to match a formula g, if it is possible to obtain f by substituting, in g, all the occurences of the same wildcards with some formulas . Recall that a wildcard is an atomic formula composed of a single letter . A wildcard is thus a “formula variable”. For instance the following formula g:

aa + (bb/ee - (cc + dd)*aa) - bb/ee

matches the following formula f:

x + (y - z*x) - y

An assignment of formulas to wildcards is called a filter. A filter is thus a partial function from wildcards to formulas. Applying a filter to a formula g consists in replacing each wildcard occurence in g, that belongs to the domain of the filter, by the corresponding formula. In summary, a formula f matches a formula g if there is a filter such that the application of that filter to g yields f. In the case of the previous matching, we have the following filter:

{ x |-> aa, y |-> bb/ee, z |-> cc + dd }

What is a rule?

A rule is a formula with the following form A => B. A is called the antecedent of the rule, B is called the consequent of the rule. A and B may be conjunctions of predicates. A may be omitted, in that case, the rule is said to be atomic. A rule may be:

inductive (backward)

If the current goal is B, then to prove B it is sufficient to prove A. A is supposed to be simpler, or easier to prove, than B. For instance, with the rule

x = FALSE => not(x = TRUE)

the goal

not (bool(0 <= aa*bb) = TRUE)

is proved if the derived goal

bool(0 <= aa*bb) = FALSE

is proved. Similarly, the atomic rule

not (BOOL = {})

is applied to prove immediately the goal with the same form.

deductive (forward)

If the antecedent A has the following form:

A1 & A2 &... & An

and if A1 is an hypothesis that has just been generated, and if

A2 & ... & An

are in the hypothesis stack then instances of predicates in the conjunction B are generated and, if they do not appear in the hypothesis stack, are pushed onto that stack. For instance, with the rule:

not(a=b) & a=c => not(b=c)

If the hypothesis not(xx = 3) has just been generated, and the hypothesis xx = aa * bb – cc is in the hypothesis stack, then the hypothesis not(3=aa*bb-cc) is generated.

rewrite

In this kind of rules, B has the form C == D. If A is satisfied, then C is rewritten to D. This kind of rules only applies to subformulas of the current goal, or on the current goal itself. For instance, the rule SimplifyIntMaxXY.3:

btest(p<=q)                    /* If p and q are integers */
=>                                 /* such that p <= q */
max({p}/{q}) == q        /* then max({p}/{q}) rewrites to p *

applies to the goal

0 <= max({3}/{5}) - min(1..4)

and rewrites it to

0 <= 5 - min(1..4)

The rules contain wildcards, whereas hypothesis do not.

Application of a rule to a formula

To realize formal proofs, inference rules are applied. This section explains what is meant by applying an inference rule to a formula. The result of the application of a rule r to a formula f yields other formulas that are called the successors of f. The set of successors may be empty. Also note that a rule is not always applicable to a formula. When a rule r is applied to a formula f, r is said to discharge f and produces a number of formulas.

We are now going to state in which conditions a rule is applicable to a formula and, if when it is, define the result of this application. Recall that a rule has the following general form:

a1 & a2 & ... * an => c

where a1, a2,… , an are called the rule antecedents, and c is the rule consequent. To apply a rule to a formula, one must consider two cases, depending on the nature of the consequent c.

Deduction rule

When the consequent of the rule does not have the form g == d, then the rule is a deduction rule. For instance, the following is a deduction rule:

x < z & y < z => x+y < 2*z

A deduction rule is applicable to a formula f when f matches the consequent of r, yielding a filter. The result of the application of r to f is then the application of this filter to the different antecedents of r. This result may be empty when the rule has no antecedent. For instance, the application of the previous rule to the following formula:

aa+bb+cc < 2*(cc+dd)

produces the two following formulas:

aa+bb < cc+dd
cc < cc+dd

Note that the filter resulting from this matching is due to the left-recursive nature of the parser. Indeed, aa+bb+cc matches x + y with x matched to aa+bb and y matched to cc.

So the rule

aa+y

matches aa+bb but not aa+bb+cc, as it is parsed as (aa+bb) + cc.

Rewrite rule

When the consequent c of the rule has the form g == d, then the rule is called a rewrite rule. In such rules, formula g and d are called the left hand side and theright hand side. For instance, the following is a rewrite rule (without antecedent):

x*(y+z) == x*y + x*z

Such rule is applicable to a formula f if there exists a sub-formula h of f such that h matches the left-hand side of the consequent of r, yielding a filter. The result of the application of r to f corresponds first, as in the previous case, to the application of the filter to the antecedents of r, if there is any. The result also contains the formula obtained by replacing, in f, the sub-formula h by the application of the filter to the right-and side of the consequent of r. Consequently, the application of the previous rule to the formula

aa + bb + cc*(ee+ff) < cc + dd

produces the following formula:

aa + bb + (cc*ee + cc*ff) < cc + dd

If several subformulas match the left-hand side of the consequent, the “rightmost” sub-formula is chosen. For instance, when the rule

a+b == b+a

is applied to formula

aa+bb+cc = cc+bb+aa

four subformulas match the left hand side, namely:

aa+bb
aa+bb+cc
cc+bb
cc+bb+aa

The selected sub-formula is thus cc+bb+aa. The rewrite rule results in the following formula:

aa+bb+cc = aa+(cc+bb)

What is a theory?

A theory is a group of rules, written in the theory language. Two consecutive rules are separated by a ‘;’ (semi-colon). The rules are (implicitly) named t.n, where

t is the name of the theory
n : is the position of the rule in the theory, the first position being numbered 1.

Example :

THEORY th1 IS
binhyp(a: B) & /* Rule th1.1 */
binhyp(B<: C)
=>
a: C;

btest(0 <= -t) /* Rule th1.2 */
=>
0<=t**2 - 4*t + 1
END

The prover first tries to apply rules with a higher index before a rule with a lower index (from the bottom to the top of the theory). For instance, when using the command ar(th1) (see [3]), the prover always tries to apply rule th1.2 before th1.1. In the case of this command, a rule th1.n only applies when no rule th1.m (such that n < m) applies. When a rule has been applied, the prover repeats its search from the last rule of the theory.

Proof

Proof of a formula

Given a set of rules, a formula f is said to be formally proved under this set of rules, when the repeated applications of these rules to the initial formula f and its successors, and the successors thereof, and so forth, results in an empty set. Equivalently, the formula f is proved under a set of rules when f and all its descendants are discharged by said these rules.

The initial formula and its descendants are called the goals of the proof. The initial formula is the initial goal, and its descendants are intermediate goals that appear during the course of the proof. By definition, all the goals are proved at the end of the proof.

This definition leaves space to some non-determinism, as we specify neither the order in which the intermediate goals are proved, nor the order in which the rules are chosen to discharge a given goal.

For instance, given the following rules:

x < z & x < z => x+y < 2*z
a-a == 0
x < x+1
0 < x+1

the goal is the following formula:

aa + (bb-bb) < 2*(aa+1)

The first rule may be used to discharge the initial goal, producing two intermediate goals:

aa < aa+1 bb-bb < aa+1

The first goal is discharged with the third rule, without creating any new goal. The second intermediate goal still needs to be proved. It is easy to see that can be done by discharging the second and then the fourth rule. Since neither applications produce new goals, we reach the point where no goal is left to be proved. The initial goal is then formally proved under the enuntiated set of rules.

Special case of conjunctive formulas

When a goal has the form:

f1 & f2 & ... & fn

the proof of this goal is replaced by the proof of each formula f1, f2, … fn, that become new intermediate goals.

How to Write Mathematical Rules

Order of rule applications

Rules may be separated according to the order of their application: forward (generating new hypothesis) and backward (generating new goals or resolution). When a rule is written, such order must be stated, either in the name of the corresponding theory, or through comments. Rules with different application order shall not be grouped in a same theory.

Restricting the application domain of a rule

Mathematical rules contain formulas conforming to the syntax of the B language. It is however possible to restrict the application domain of a rule so that it remains valid, or to parameterize it, by using guards of the theory language. Such guards are presented in Chapter 7. For instance, in the rule

bsearch((x: p..q), P, r) &
(SIGMA(x).(P & 0 <= -E | -E)<=SIGMA(x).(P & 0<=E | E))
=>
(0 <= SIGMA(x).(P | E))

the bsearch guard ensures that P contains the definition domain of variable x as an interval.

In the rule

band(binhyp(n<=size(a)) ,
btest(n>0)) &
(size(a) = 1 => b = c) &
(2<=size(a) => first(a) = c)
=>
(first(a<+{size(a)|->b}) = c)

the two guards express that the sequence a has at least one element.

Principle of equivalence

The fundamental principle to obey when writing rules is to write equivalent rules, that is, when writing a rule a => b, showing a shall be equivalent to showing b. This means that the provability of b is preserved. Otherwise the produced goal may be erroneous and prevent th proof when the rule is applied without control. For instance, the rule

0<=a &
0<=b
=>
0<=a*b

does not obey the principle of equivalence, as it cannot be used to show the goal 0<=a*b when a<0 and b<0.

However, the rule

binhyp(0<=a) &
binhyp(0<=b)
=>
0<=a*b

is an equivalence rule.

It is possible to write rules that are not equivalence rules. Such rules may only be employed in interactive proofs, as a single application. There is no risk of showing a false goal; only to reach an unprovable goal.

Rewrite rules

Application of rewrite rules within the scope of a quantifier must be done with care. In the case of rewrite rules with an antecedent, the application is only correct if the context variables appearing on the left-hand side of the consequent are bound at the rewrite position. For instance, the rule:

binhyp(x=0)
=>
(x == 0)

transforms the expression !x1.P(x1) into !0.P(0) under the hypothesis x1 = 0. The problem comes from the fact that the variable bound to the wildcard x in the guard may not be the same as that of the rewriting position (the rule matches since they are synonymous).

The combination of guards blvar(Q) and Q(H) may be used to prevent erroneous rewriting within quantified formulas. Every rewrite rule that needs a restriction withblvar (beware of the instantiation of H). The correct way to write the preceding rule is

binhyp(x=0) &
bgetallhyp(H) &
blvar(Q) &
Q(H)
=>
(x == 0)

The guard bgetallhyp instantiates H with the current hypothesis, the guard blvar instantiates Q with a list of bound variables at the current rewriting position, and the guard Q(H) succeeds if no element of Q occurs in the free variables of the hypothesis found in H.

Forward rules

The behavior of forward rules is significatively different from that of backward rules; in practice, there is little use of such rules outside of the core of the prover. A forward rule may only apply when the hypothesis have just been generated and before they are pushed onto the stack hypothesis (and before they are reachable through the guard binhyp). For instance, applying the backward rule

(not(X<=0 & Y<=0) => 0<=X & 0<=Y)
=>
(0<=X*Y)

on the goal

0<=(aa+bb)*(cc+3)

results in the new goal

not(aa+bb<=0 & cc+3<=0) => 0<=aa+bb & 0<=cc+3

Using the deduction mechanism, then prover then stacks the hypothesis

not(aa+bb<=0 & cc+3<=0)

and the new goal is:

not(aa+bb<=0 & cc+3<=0)

It is when the hypothesis is pushed on the stack that forward rules are applicable.

A forward rule has the form:

A1 ∧ A2 ∧ . . . ∧ An ⇒ B1 ∧ B2 ∧ . . . ∧ Bp

where A1 is a newly generated hypothesis and

A2 ∧ . . . ∧ An

are in the hypothesis stack. The hypothesis B1, B2,… Bn are then generated and pushed onto the hypothesis stack, if they are not already there.

Examples:

(u/v = w)
=>
u: POW(w) & v: POW(w)

not(b: a) &
not(b..c/a = {})
=>
not(b+1..c/a = {})

Such rule may be restricted by guards that shall obrigatorily be placed after hypothesis A1. For instance,

not(a:POW({x})) &
bgetallhyp(H) &
bfresh(zz,H,z)
=>
#z.(z:a & not(z=x))

Lists

Lists hall be manipulated with extreme care in rules. For instance, formula

[a]

may match

[aa, bb, cc]

and also

[aa]

It is then important to be able to state in a rule if a wildcard shall match a literal or a list. In the previous case, if one wishes to match sequences with a single element, the following guard may be used

bnot(bpattern(a, (u, v))

Some rules that apply to lists may be grouped by pairs, where the first rule handles the general case, i.e. when the list has at least two elements, and where the second rule handles the special case of a list with a single element. The latter rule shall not be applied to a list with multiple elements, as it would yield an unprovable goal. For instance, the prover rules:

bnot(bpattern(a, (u,v))
=>
([a]1 == a);

[a,b]1 == [a]1

are used to simplify expressions selecting the first element of a sequence. Note the recursive application expressed in the second rule, as the matching always selects the rightmost occurrence of a pattern.

Tips for parenthesis

Writing rules requires using parenthesis. Misplacing parenthesis may result in flawed rules. The following tips advise on the correct usage of parenthesis:

Parenthesis and existential quantifiers.

For compatibility with the Linux port of Atelier B, it is required to over-parenthesize formulas under the scope of an existential quantifier.

X. P shall be written (#x. P) to be used under Linux.

Quantified predicates.

Parenthesizing of a quantified predicate is not guaranteed. For instance, the following rule:

Antecedent => (!x.(x: E & P(x)))

is too restrictive as it does not apply to goals such as

!xx. (xx : E & A(xx) & B(xx))

Operator precedence (and implicit parenthesis) in the theory language might be ambiguous to the user. For instance

bsearch (aa, aa => bb, C)

is interpreted and implicitly parenthesized as bsearch((aa, aa) => (bb, c)) in the prover. Also:

- rule a == b & c is interpreted as ((a == b) & C)
- rule a => b => c is interpreted as ((a => b) => c).

To avoid surprises in the application of rules in the prover, it is recommended to be systematic in the use of parenthesis when writing such rules.

Wildcard instantiation

Three types of problems may happen with wildcards:

Non-instantiated jokers in the rule antecedent, or in the right-hand side of a rewrite rule consequent provoke the inclusion of so-called “dead wildcards”. Dead wildcards are wildcards that become identifiers and are no longer part of the pattern matching process. This creates a new variable, not present in the source code

For instance:

e: FIN(s) => card(e): NATURAL

s is a not instantiated and will become a dead wildcard.

Renaming is a special case of a non-instantiated wildcard that happens when two distinct wildcards designate the same mathematic object. For instance,

binhyp(s~: E +-> NATURAL) &
1<=size(f)
=>
(tail(s)~: E +-> NATURAL)

f represents the same sequence as s.

The last problem is the name confusion occurring when the same wildcard represent different mathematical objects. In that case, either the rule is badly typed, or the rule is correct but very restrictive.

band(binhyp(r~: C +-> B)
binhyp(C: FIN(D))) &
(a: POW(r<+{a}))
=>
(a: FIN(r<+[a}))

both occurrences of the wildcard are incompatible from the viewpoint of typing.

When writing a rule, special care must be taken regarding wildcards. “Copy&paste” is specially dangerous regarding to that kind of problem. Coherence in the use of wildcards always need to be checked.

The limited number of available wildcards hinders the readability of rules. However, as long as possible, the following conventions must be applied:

f , g, h for functions,
r for a relation,
A, B, C, D, E, F for sets,
the same letter, lowercase, for an element of the set,
s, t for sequences,
i, j, k, m, n, p for integers,
P, Q, R for predicates,
x, y, z for variables.

Ambiguities

Some notations lead to ambiguities:

– denotes both arithmetic subtraction and set difference;
* denotes both arithmetic product and cartesian product.

The rules that may lead to false proof due to overloading such operators must be corrected or eliminated. Ambiguous expressions need to be correctly typed and disambiguated. If it is not possible to remove ambiguities, the rule must be eliminated.

For instance, consider the following formulas:

0 <= a * b

a={} & b={} => a-b = {}

In both cases, there are no ambiguities. Indeed the operator * is the arithmetic product, and the operator – is the set difference.

However, in the following rule:

g(a) : d & h(b) : e =>  f(a*b) :  c,

there is no way to know if the operator * is the cartesian product or the arithmetic product.

The preceding rule may be disambiguated by adding the following:

a: NAT

Miscellaneous remarks

The exact semantics of guards is defined in Appendix C . Special care must be taken with the following points:

The guards best(a=b) and (btest a/=b), differently from other uses of btest, do not check that a and b are elements of NAT. Beware, if btest(a=b) passes then a=b, however if btest(a/=b) passes, it is not necessarily the case that a /= b. Indeed if x and y are two different wildcards that match the same expression, btest(x /= y) passes but x = y is true.
The guard btest(a+b=b+a) fails since a+b is not an identifier.
The guard bsubfrm is used mainly to guide the proof. This guard shall not be employed for other purposes in rules.
The guard bsearch only performs one extraction. bsearch(a, b, c): b needs to be a list with at least two elements, under the form x op y, where op is an associative and commutative operator. The associative and commutative properties of the operator are fundamental as the give the same importance to the different occurences of a within b. If op does not have these properties, the translation in the language of mathematics is no longer general.

Using Automatic Prover Mechanisms

This section presents different mechanisms of the prover that may be referred to and employed in the mathematical rules. These mechanisms have been validated and may simplify the conception phase of these rules. For each mechanism, the following points will be presented:

syntax to use the mechanism
semantics associated with the mechanism
a textual description of the mechanism
an illustrating example.

Trying a proof

Syntax: bguard(attempt_to_prove: a_t_t_e_m_p_t__t_o__p_r_o_v_e(P | Curr))

Translation: P

Description: This mechanism triggers a sub-proof on P. It is successful if P can be demonstrated by the prover. P must be correctly typed.

Examples

band(binhyp(f: s +-> (t --> u)) ,
bguard(attempt_to_prove: a_t_t_e_m_p_t__t_o__p_r_o_v_e(
(t: POW(a) & u: POW(b)) | Curr)))
=>
(f(x): a +-> b)

bguard(attempt_to_prove: a_t_t_e_m_p_t__t_o__p_r_o_v_e(
(not(b) => a) | Curr))
=>
(a or b)

(n: a) &
not(n: b) &
bguard(attempt_to_prove: a_t_t_e_m_p_t__t_o__p_r_o_v_e(
(a: POW(b))| Curr))
=>
bfalse

This last rule is a forward rule. If an hypothesis matching n: a has just been generated, if there is an hypothesis not(n: b) and if the prover is able to show that a: POW(b) is true, then the hypothesis bfalse is generated.

Difference

Syntax: bguard(Fast_Prove_Difference: not(a = b)

Translation: not(a = b)

Description: This mechanism may be employed to prove that two terms are not equal. If the call succeeds, then a and b are not equal.

Examples :

bguard(Fast_Prove_Difference: not(a = b)) &
blvar(Q) &
Qnot(a = b)
=>
({a}<<|{b|->c} == {b|->c})

bguard(Fast_Prove_Difference: not(a = c)) &
blvar(Q) &
Q(a = c)
=>
({a|->b}<+{c|->d} == {a|->b}/{c|->d})

Order relation

Syntax: bguard(Fast_Prove_Order: m<=n)

Translation: m<=n

Description: If the call to this mechanism is successful , then the relation m <= n is true.

Example:

bguard(Fast_Prove_Order: c<=d) &
(a = c) &
(b = d)
=>
(a..b = c..d)

Positive value

Syntax: bguard(Fast_Prove_Positif: a)

Translation: 0<=a

Description: If the call to this mechanism succeeds, then the value of the arithmetic expression a is positive or zero.

Example :

binhyp(s: POW(a..b)) &
bguard(Fast_Prove_Positif: a)
=>
(s: POW(NATURAL))

Non membership

Syntax: bguard(Fast_Prove_Distinction: not(x: s))

Translation: not(x: s)

Description: If the call to this mechanism is successful , then x does no belong to s.

Example :

Fast_Prove_Distinction(not(a: dom({c|->d})))
=>
not({a|->b} = {c|->d})

Membership to INTEGER

Syntax: bguard(Fast_Prove_Num: n)

Translation: n: INTEGER

Description: A call to this mechanism is successful entails that n is an integer.

Example :

bguard(Fast_Prove_Num:(x))
=>
(succ(x) == x+1 )

Guards

This chapter presents succinctly the different kinds of guards that are available to write mathematical rules (for further details, see Appendix C). For each guard, the following elements are presented:

syntax,
possibly its semantics,
a textual description of its behaviour.

It must be noted that certain guards have a mathematical semantics only under special circumstances (e.g. the bsearch guard).

The following guards may be employed to obtain one or several hypothesis from the stack, by processing first the most recently inserted hypothesis.

Syntax	Semantics
bgetallhyp(H)	H
bgethyp(H)	H
binhyp(H)	H

The following guard checks if s is an element of STRING.

Syntax	Semantics
bstring(s)	s : STRING

The following guard checks if P is a conjunction.

Syntax	Semantics
bpattern(P, (Q & R))	P <=> (Q & R)

The bsearch guard has a mathematic semantics when the list in which the search is performed is the argument list of an associative and commutative operator. This is the case for the operators &, or, / and /. This is also the case of the operator , (comma) for a list of quantified variables. One must thus check that the application of the rule remains within such cases.

Syntax	Semantics
bsearch(N, (P, Q), M)	(P, Q) = (M, N)
bsearch(N, (P & Q), M)	(P & Q) <=> (M & N)
bsearch(d, (a or b), c)	(a or b) <=> (c or d)
bsearch(d, (a / b), c)	a / b = c / d
bsearch(d, (a / b), c)	a / b <=> c / d

The following guard succeeds if t is true and has the form a op b.

Syntax	Semantics
btest(t)	t

The following guard checks if n is a numeric value both positive and smaller or equal to maxint.

Syntax	Semantics
n : NATURAL

The following guard succeeds if both arguments succeed.

Syntax	Semantics
band(P, Q)	Semantics of P and semantics of Q

The role of the following guards is to verify the relationship between wildcards representing variables and wildcards representing expressions.

Syntax	Semantics
bvrb(x)	x
blvar(x)	x
x P	x (if x P)
bfresh(x, P, y)	y (if y P)

Normalisation of Expressions

In order to limit the number of rules in the prover base, expressions are normalized. Every expression that the prover manipulates must have been first normalized. Thus every user rule found in a Pmm file is automatically normalized when it is loaded. However the rules that are stored in the PatchProver need to be manually normalized, otherwise they may induce an anomalous behavior of the prover.

The normal forms are the following:

Expression	Normal form
n > m – 1	m <= n
m < n	m <= n – 1
a <=> b	(a => b) & (b => a)
a <: b	a : POW(b)
a <<: b	a : POW (b) & not (a = b)
a /: b	not (a : b)
a /= b	not (a = b)
a /<: b	not (a : POW(b))
a /<<: b	a : POW(b) => a = b
a : NATURAL	a : INTEGER & 0 <= a
NATURAL1	NATURAL – {0}
NAT1	NAT – {0}
FIN1(A)	FIN(A) – {}
POW1(A)	POW(A) – {}
seq1(A)	seq(A) – {}
iseq1(A)	iseq(A) – {{}}
perm(E)	iseq(E) / (NATURAL – {0} +->> E)
<>	{}
{x, y}	{x} / {y}
P}	SET(x).P

When writing a rule, it is necessary to check that this rule is indeed normalized. Otherwise, the rule will be normalized when it is loaded and may no longer be applicable as desired.

For instance, the following rule:

btest(0<x)
=>
0<=x**2-1

is normalized into

btest(0+1<=x)
=>
0<=x**2-1

But the guard btest only accepts as argument expression of the form a op b, where a and b are integers. This rule will thus never be applicable. The following rule should be thus preferred:

btest(1<=x)
=>
0<=x**2-1

Common pitfalls

What is an infinite loop of the prover?

For instance, consider applying the rule:

a * a == a * a * a / a

on the following goal

cc(v) = vv * vv

We will obtain successively the following goals:

cc(v) = vv * vv * vv / vv
cc(v) = (vv * vv * vv / vv) * vv / vv
...

The kernel of the prover then produces the following messageskrt: sequence memory short

krt: asking for 1500000 int, waiting for system reply...
krt: OK, memory obtained, we continue.
krt: sequence memory short
krt: asking for 2249997 int, waiting for system reply...
krt: OK, memory obtained, we continue.
krt: sequence memory short
 krt: asking for 3374992 int, waiting for system reply...
krt: OK, memory obtained, we continue.
...

The messages krt: sequence memory short are generated by the kernel when it dynamically claims additional memory.

This example is simple. Infinite loops may be caused by combination of rule applications and be more difficult to detect a priori.

Guards in the theory language

This chapter presents guards (operators) that may be used to write rules. Such guards may be used to constrain the domain of application of a rule, using informations related to the goal and the hypothesis. To help writing and verifying the rules, all the guards of the theory language are documented thereafter.

A guard is a special antecedent in a rule. In fact, each guard in a rule is interpreted directly before the rule being effectively applied or not. Evaluating a guard never results in the creation of a SUCCESSor. The evalution of a guard may succeed or fail. For a rule to be effectively applicable, all the associated guard must be successful .

The following table summarizes the guard constructs:

bmatch bnot

band	conjunction of two guards
bfresh	construction of a fresh variable
bgetallhyp	obtains all the hypothesis
binhyp	tests the presence of a formula in (as ???) an hypothesis
blvar	lists the quantified variables
identity by matching
negation of a guard
bnum	numerality test
bpattern	tests formula matching
bsearch	tests presence in a list
bstring	tests if is a character string
bsubfrm	finds sub-formulas
btest	numeric comparison
bvrb	variable test

band

band(g1,g2)

Parameters

g1 : guard
g2 : guard

Nature

guard

Summary

Combines several guards.

Evaluation

The evaluation strategy differs according to the nature of the guards g1 and g2 :

if g1 is binhyp(H ), or binhyp(n,H ), or binhyp(m,n,H ), and if, in the last two cases, n is a wildcard, then the resulting guard succeeds if there exists an hypothesis h that matches H and that is such that g2 is successful
if g1 is a bsubfrm, bsearch or brule guard, then the resulting guard is successful if there exists a wildcard instantiation such that g1 successful , and such that g2 is successful .
in all other cases, the resulting guard is successful if both guards g1 and g2, evaluated in sequence are successful . If g2 fails, the evaluation does not backtrack to g1 as in the preceding cases.

Example

THEORY tentative IS
band(binhyp(aaa(x)), band(binhyp(ccc),binhyp(bbb(x))) ) &
bcall(WRITE: bwritef("x: %n",x))
=>
H;

bcall((DED~;ess):((bbb(1) => (aaa(2) & bbb(2) & ccc & aaa(1) => titi))))
=>
foobar
END

Result

x: 1

bnot

bnot(g)

Parameters

g : guard

Nature

Guard

Summary

Used to simplify expression of guards in case of failure.

Evaluation

The evaluation of bnot(g) is successful if the evaluation of g is a failure.

Example

THEORY tentative IS
bcall(WRITE: bwritef("OK n"))
=>
aaa(n);

breade("Write ?>? (substituting the ? with numbers): ",a>b) &
bnot(btest(a>b)) &
bcall(WRITE: bwritef("Hello??? n")) &
aaa(n+1)
=>
aaa(n)/*(a,b)*/;

bcall((ARI;ess)~: aaa(1))
=>
foobar
END

Result

Write ?>? (substituting the ? with numbers): 3>5
Hello???
Write ?>? (substituting the ? with numbers): 4>9
Hello???
Write ?>? (substituting the ? with numbers): 5>1
OK

bfresh

bfresh(v, f, V)

Parameters

v: variable or variable list
f: formula
V: wildcard

Nature

Guard

Summary

To create fresh variables.

Evaluation

The evaluation is always successful . The wildcard V is instantiated with as many variables as there are in v. Moreover the new variables are not free in f. If v is not free in f, then V is the same as v.

Example

THEORY tentative IS
bfresh((xx,yy,zz),aaa+xx$0-yy*zz,V) &
bcall(WRITE: bwritef("%n",V))
=>
foobar
END

Result

xx$1,yy$1,zz$1

bgethyp

bgethyp(h), bgetallhyp(h)

Parameters

h : formula

Nature

Guard

Summary

This guard gets the hypothesis in a proof.

Evaluation

The evaluation of the guard is successful when the proof contains hypothesis and that the conjunction of these hypothesis matches with formula h. These hypothesis also depend on the type of guard:

Guard bgethyp only yields the main hypothesis;
Guard bgetallhyp yields the main hypothesis as well as the hypothesis derived from these main hypothesis.

In any case, all the wildcards of h are instantiated.

Example

THEORY tentative IS
bgethyp(H) &
bgetallhyp(G) &
bcall(WRITE: bwritef("Main hypothesis: %n",H)) &
bcall(WRITE: bwritef("Main and derived hypothesis: %n",G))
=>
P;

bcall((DED;ess),fwd: (aaa & bbb => ggg))
=>
foobar
END

&

THEORY fwd IS
aaa => ccc;
ccc & bbb => ddd & eee
END

Result

Main hypothesis: aaa & bbb
Main and derived hypothesis: aaa & bbb & ccc & ddd & eee

binhyp

binhyp(h)
binhyp(n, h)
binhyp(m, n, h)

Parameters

h: formula
n: formula
m: number

Nature

Guard

Summary

To access an hypothesis.

Evaluation

The guard binhyp(h) is successful when there exists an hypothesis that matches h. When there are several hypothesis, the last one is picked. All wildcards of h are instantiated. The evaluation of the guard binhyp(n,h ) depends on the nature of n: When n is a number, the evaluation is successful when the hypothesis of rank n exists and matches hypothesis h. All wildcards of h are instantiated. When n is a wildcard, the evaluation is successful if there exists an hypothesis that matches hypothesis h. n is then instantiated with the rank of h. All wildcards of h are instantiated. In all other cases, the evaluation fails. The evaluation of the guard binhyp(m,n,h) is similar to that of the guard binhyp(n,h), but in the case where n is a wildcard, the selected hypothesis is the last that matches h and with rank smaller or equal to i m. Note the similarities between these last two forms of the binhyp guard and the guards brule and lemma.

Example

THEORY tentative IS
foo(i);

binhyp(i,n,H) &
bcall(WRITE: bwritef("hyp_%: %n",n,H)) &
foo(n-1)
=>
foo(i);

binhyp(n,H) &
bcall(WRITE: bwritef("hyp_%: %n",n,H)) &
foo(n-1)
=>
bar;

binhyp(1,H) &
bcall(WRITE: bwritef("hyp_1: %n",H)) &
bar
=>
baz;

binhyp(H+G) &
bcall(WRITE: bwritef("hyp: %n",H+G)) &
baz
=>
P;

bcall((DED;(ARI;ess)~):((aaa & bbb+ccc & ddd) => pp))
=>
foobar
END

Result

hyp: bbb+ccc
hyp_1: aaa
hyp_3: ddd
hyp_2: bbb+ccc
hyp_1: aaa

blvar

blvar(l)

Parameters

l : list of variables

Nature

Guard

Summary

To get the list of quantified variables at the current rewrite position.

Evaluation

The guard is always successful . If there is at least one quantified variable at the current rewrite position, l contains the list of quantified variables. Othewise l contains ?. For instance, if the current goal is

(aa,bb,cc).0<=aa & 0<=bb & 0<=cc => 0<=aa+bb+cc

and the rule

binhyp(x=0) &
blvar(Q) &
xQ
=>
x == 0

is applied, then Q will be (aa,bb,cc).

This guard is used within rewrite rules. It provides the guarantee that one does not mix quantified with non-quantified variables. It is often used in conjunction with the absence of freedom guard bnfree x E. ? E is always true, whatever E is.

Example

THEORY tentative IS
bnot(blvar(?))
=>
qq == pp;

!qq.(qq+1>qq)
=>
%ii.(ii: NAT | uu) = oi$5;

blvar(t$i)
=>
(t$i) == ii;

blvar(Q) &
Q!yx.(yx<yx+oo) &
bcall(WRITE: bwritef("free Q is %n",Q)) &
%(tt$0).(tt$0: NAT | uu) = oi$5
=>
!yx.(yx<yx+oo);

blvar(Q) &
Q(aa+2) &
bcall(WRITE:bwritef("aa transforms into oon"))
=>
aa == oo;

blvar(Q) &
Q(yx+2) &
bcall(WRITE:bwritef("yx transforms into zan"))
=>
yx == za;

!yx.(yx<yx+aa)
=>
!(zz$0,uu,hh$9).(zz$0+uu+hh$9>0);

blvar(Q) &
bcall(WRITE:bwritef("Q is %n",Q))
=>
vv == hh;

!(zz$0,uu,vv$9).(zz$0+uu+vv$9>0)
=>
!yy.(yy<yy+1);

blvar(Q) &
bcall(WRITE:bwritef("Q is %n",Q))
=>
xx == yy;

!xx.(xx < xx+1)
=>
foobar

END

Result

Q is xx
Q is xx
Q is xx
Q is zz$0,uu,vv$9
Q is zz$0,uu,vv$9
aa transforms into oo
free Q is ?
EXECUTION ABORTED ON GOAL: !pp.(pp+1>pp)

bmatch

bmatch(x, p, q e)

Parameters

x: variable
p: formula
q: formula
e: formula

Nature

Guard

Summary

Checks if a quantified formula may be instantiated.

Evaluation

For the guard to be successful , it is first necessary that the formula p does not contain quantifiers. Then it is required that there exists a formula f such that the substitution of x by f in p is the same as formula q. Finally, formula f must match e. All wildcards in e are instantiated.

Example

THEORY tentative IS
binhyp(!x.(H=>P)) &
bmatch(x,P,Q,E) &
bcall((SUB;WRITE):
bwritef("P: %nx: %nE: %n[x:=E]P: %nQ: %n",P,x,E,[x:=E]P,Q))
=>
Q;

( !(xx$1,yy).(qq(xx$1,yy) => pp(xx$1,ff(xx$1),yy))
=>
pp(aa,ff(aa),bb)
)
=>
ccc;

bcall((ess;DED;ess):ccc)
=>
foobar
END

Result

P: pp(xx$1,ff(xx$1),yy)
x: xx$1,yy
E: aa,bb
[x:=E]P: pp(aa,ff(aa),bb)
Q: pp(aa,ff(aa),bb)

bpattern

bpattern(f, g)

Parameters

f: formula
g: formula

Nature

Guard

Summary

Tests if a formula matches another formula.

Evaluation

The guard is successful if formula f matches formula g. All wildcards in g are instantiated.

Example

THEORY tentative IS

bnot(bpattern(p,q)) &
bcall(WRITE: bwritef("FAILURE"))
=>
baz(p,q);

bpattern(aaa+bbb,a+b) &
bcall(WRITE: bwritef("% %n",a,b)) &
baz(aaa+bbb,k+l)
=>
foobar

END

Result

aaa bbb
FAILURE

bsearch

bsearch(p, l, r)
bsearch(p, l, r, s)

Parameters

p: formula
l : non-atomic formula
r: formula
s: formula

Nature

Guard

Summary

To search, and possibly modify an element in a list.

Evaluation

The formula l has the form l1 op … op li op … op ln where n is greater than or equal to 2 and op is a binary operator.

The guard bsearch(p,l,r ) is successful when there exists a sub-formula li that matches p, and when the formula obtained by removing li from l matches formula r.

The guard bsearch(p,l,r,s ) is successful when there exists a sub-formula li that matches p, and when the formula obtained by substituting li in l with the corresponding instance matches formula r.

All wildcards in p, r and s are instantiated.

Example

THEORY tentative IS
bsearch((a-{x}),(aaa / (bbb-{xx}) / ccc / (ddd / {xx}) / eee),r,a) &
bsearch((b/{x}),r,s,b) &
bsearch((b/{x}),(aaa / (bbb-{xx}) / ccc / (ddd / {xx}) / eee),h) &
bcall(WRITE: bwritef("r: %na: %nb: %ns: %nh: %n",r,a,b,s,h))
=>
foobar
END

Result

r: aaa/bbb/ccc/(ddd/{xx})/eee
a: bbb
b: ddd
s: aaa/bbb/ccc/ddd/eee
h: aaa/bbb-{xx}/ccc/eee

bstring

bstring(f)

Parameters

f: formula

Nature

Guard

Summary

To test that a formula is a character string.

Evaluation

The evaluation of the guard is successful if f is a character string (i.e. a sequence in characters between double-quotes). A double-quote may be present inside the string if it is preceded by a backslash.

Example

THEORY tentative IS

bcall (WRITE: bwritef("test3: FAILUREn"))
=>
test3;

bstring(aa+bb);
bcall (WRITE: bwritef("test3: SUCCESSn"))
=>
test3;

bcall (WRITE: bwritef("test2: FAILUREn"))
test3
=>
test2;

bstring(aaa) &
bcall (WRITE: bwritef("test2: SUCCESSn")) &
test3
=>
test2;

bcall (WRITE: bwritef("test1: FAILUREn")) &
test2
=>
test1;

bstring("Hello "Sir"") &
bcall (WRITE: bwritef("test1: SUCCESSn")) &
test2
=>
test2;

bcall(ess: test1)
=>
foobar

END

Result

test1: SUCCESS
test2: FAILURE
test3: FAILURE

bsubfrm

bsubfrm(g, d, p, q)
bsubfrm(g, d, p, (q, v))

Parameters

g: formula
d: formula
p: formula
q: formula
v: formula

Nature

Guard

Summary

Tests the presence of a sub-formula in a formula and substitute it with another one.

Evaluation

For the evaluation of the first type of guard to be successful , it is first necessary that a formula f of p matches g (not instantiated). We then consider p obtained by substitution, in p, by the instantiated sub-formula f. Such formula p must match q (not instantiated). Most of the time, q is a simple wildcard.

In the second type of guard, the list of quantified variables on which f depends is also considered. If there is no such variable, then the list contains a single element: ?. This list must match v, not instantiated. Most of the time v is also a simple wildcard. All remaining unmatched wildcards are instantiated.

Example

THEORY tentative IS
bsubfrm(x/:s,not(x:s),#(y,z).!(xxx$1,x,bbb).(x/:s => aaa),(q,v)) &
bcall((SUB;WRITE): bwritef("q: %nv: %n",q,v))
=>
foobar
END

Result

q: #(y,z).!(xxx$1,x,bbb).(not(x: s) => aaa)
v: xxx$1,x,bbb,y,z

btest

btest(m op n)

Parameters

m: formula
n: formula
op: comparison operator

Nature

Guard

Summary

To compare two numeric values.

Evaluation

The evaluation of the guard is successful when m and n related by the specified operator. The comparison operators:

Equal: =
Different: /=
Smaller: <
Smaller or equal: <=
Greater: >
Greater or equal: >=

When the operator is equality or difference, the evaluation of the guard is also successful when m and n are both identifiers that are related by the operator

Example

THEORY tentative IS

btest(bb/=aa) &
bcall(WRITE: bwritef("test3: SUCCESSn"))
=>
test3;

bnot(btest(8=aa)) &
bcall(WRITE: bwritef("test2: FAILUREn")) &
test3
=>
test2;

btest(8=8) &
bcall(WRITE: bwritef("test1: SUCCESSn")) &
test2
=>
foobar

END

Result

test1: SUCCESS
test2: FAILURE
test3: SUCCESS

bvrb

bvrb(f)

Parameters

f : formula

Nature

Guard

Summary

To test that a formula is a variable.

Evaluation

The evaluation is successful if f is a variable. Recall that a variable is either a letter (wildcard) or an identifier that do not start with an underscore, or one of the two previous possibilities followed by a $ and a number smaller than 10000, or a list composed of distinct elements that fall into the previous cases.

Example

THEORY tentative IS

bcall(WRITE: bwritef("test5: FAILUREn"))
=>
test5;

bvrb(a+b) &
bcall(WRITE: bwritef("test5: SUCCESSn"))
=>
test5;

bcall(WRITE: bwritef("test4: FAILUREn")) &
test5
=>
test4;

bvrb(_a) &
bcall(WRITE: bwritef("test4: SUCCESSn")) &
test5
=>
test4;

bcall(WRITE: bwritef("test3: FAILUREn")) &
test4
=>
test3;

bvrb(a$10000) &
bcall(WRITE: bwritef("test3: SUCCESSn")) & test4
=>
test3;

bcall(WRITE: bwritef("test2: FAILUREn")) &
test3
=>
test2;

bvrb(a,a,bbb) &
bcall(WRITE: bwritef("test2: SUCCESSn")) &
test3
=>
test2;

bcall(WRITE: bwritef("test1: FAILUREn")) &
test2
=>
test1;

bvrb(aaaa_3,xxx,xx$2,y) &
bcall(WRITE: bwritef("test1: SUCCESSn")) &
test2
=>
test1;

bcall(ess: test1)
=>
foobar

END

Result

test1: SUCCESS
test2: FAILURE
test3: FAILURE
test4: FAILURE
test5: FAILURE

Writing Mathematical Rules

Versions history

Acknowledgements

Introduction

Bibliography

Terminology

Abbreviations

Terms

Introduction to the Theory Language

What is a wildcard?

What is a formula?

Matching Formulas

What is a rule?

Application of a rule to a formula

Deduction rule

Rewrite rule

What is a theory?

Proof

Proof of a formula

Special case of conjunctive formulas

How to Write Mathematical Rules

Order of rule applications

Restricting the application domain of a rule

Principle of equivalence

Rewrite rules

Forward rules

Lists

Tips for parenthesis

Wildcard instantiation

Ambiguities

Miscellaneous remarks

Using Automatic Prover Mechanisms

Trying a proof

Difference

Order relation

Positive value

Non membership

Membership to INTEGER

Guards

Normalisation of Expressions

Common pitfalls

What is an infinite loop of the prover?

Guards in the theory language

band

Parameters

Nature

Summary

Evaluation

Example

Result

bnot

Parameters

Nature

Summary

Evaluation

Example

Result

bfresh

Parameters

Nature

Summary

Evaluation

Example

Result

bgethyp

Parameters

Nature

Summary

Evaluation

Example

Result

binhyp

Parameters

Nature

Summary

Evaluation

Example

Result

blvar

Parameters