Introduction to mathematical rules

There are 3 kinds of rules:
  • Backforward: a predicate is transformed into zero, one or more (simpler) predicates
  • Forward: 1 or more new hypotheses are generated
  • Rewriting: a predicate or expression is rewritten

Common concepts

Rules are generic. Wildcards (1-letter identifiers) are used to denote any identifier.
For example, the predicate aa+bb+cc <= dd + ee matches with the following formulas:
  • x <= y where x = aa+bb+cc and y = dd+ee
  • x+y <= z where x = aa+bb, y=cc and z=dd+ee
Rules container is THEORY

Backward rules

Their general form is
  • either A => B (the => symbol is a separator between sequents, not the logical implication)
  • or B
B is the predicate that should match with the goal.
A (optional) is a list of conditions C (guards) and sub-goals G.
The proof of B is then replaced by the proof of G if C is true, namely C & G => B
The rule is applied without condition:
The rule is applied if the guards hold (binhyp(H)is successful if H is an hypothesis):

Forward rules

Their general form is A & B => C
A is an hypothesis that has been generated
B is made of guards (D) and sub-goals (G)
C is a (list of) hypothesis to generate
If D is true and G proved then C is added to hypotheses

Rewriting rules

Their general form is C & G => A == B
A is the predicate or expression to rewrite in B
C are conditions
G are sub-goals
If C is true and G proved the A is rewritten in B