Download Interactive Prover

Chapter 9
Frequently asked questions
9.1
Pr may mislead us
There is a fundamental difference between the mp command and the pr command.
Regardless of the prover force used, the mp command applies rules of goal and hypotheses
simplification, and some resolution mechanisms.
The pr command is built according to the same principles, but contains other mechanisms.
Especially, some simplification heuristics of the existential predicates, of the last equalities
loaded in hypotheses and processing the starting up of proof by cases that improve the
efficiency of this command.
For example, if the current goal has the following form
x∈S
and the hypothesis
x∈A∪a
does exist, then the current proof is divided in two cases:
x=a ⇒ a∈S ∧
x ∈ A ∧ not(x = a) ⇒ x ∈ S
Another example, if the dom(A ∗ B) formula appears in the current goal P , then two cases
are generated:
(B = ∅ ⇒ [dom(A ∗ B) := ∅]P ) ∧
(not(B = ∅) ⇒ [dom(A ∗ B) := A]P )
[f := g]P here means that all the f occurencies in P are replaced with g.
However, the proof by cases can be useless and require to prove a lemma as many times
as there are cases. Indeed, these proof by cases are started up according to some local
155