Download Interactive Prover

120
Interactive Prover - User Manual
7.3
User rules application
Here are some hints for the application of a user rule:
• do not forget to normalize the rules:
– The rules of Pmm files are normalized by the prover when they are loaded,
– the rules of PatchProver files have to be normalized by the user.
– a < b is normalized by the prover in a + 1 ≤ b. Thus the guard btest(a < b)
will be rewrited btest(a + 1 ≤ b) and will never succeed.
• in the case of complex expressions, do not hesitate to overparenthesise your rule
terms.
• check that you use only jokers (one letter identifiers).
The rule:
binhyp(xx = 0)
⇒
xx mod 2 = 0
will be applied only if the goal is strictly xx mod 2 = 0,but not if it is yy mod 2 = 0.
• check that you do not introduce never instanciated jokers in your rule. In practice,
all the jokers appearing in a Backward rule consequent are instanciated. Make sure
that, in the case of a goal replacement by an equivalent one, the generated goal is
fully instanciated.
For example, the rule:
binhyp(H) ∧
(h ⇒ B)
⇒
B
will produce, for the goal
xx = 0
the derived incoherent goal
h ⇒ xx = 0
Other example, the rule:
binhyp(b)
⇒
B
is false because the mathematical associated lemma