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.

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