| Current Sequent | Applicable Proof Command[s] and Resulting Sequent[s] |
Universal consequent
...
|-
(FORALL (a: A, b: B): alpha),
... | | Applicable Proof Commands | Resulting Sequent[s] | Skolemization is straightforward. (skolem * ("aa" "bb"))
(skolem + ("aa" "bb")) |
... |- alpha[a/aa; b/bb], ... | Partial skolemization
(skolem * ("_" "bb"))
(skolem + ("_" "bb")) | ...
|-
(FORALL (a: A): alpha[b/bb],
... | | Well founded induction often requires human insight.
(induct "a")
(induct "b") |
several sequents
corresponding to inductive cases |
|
Existential antecedent (EXISTS (a: A, b: B): alpha),
... |- ... | | Applicable Proof Commands | Resulting Sequent | Skolemization is straightforward.
(skolem * ("aa" "bb"))
(skolem - ("aa" "bb")) |
alpha[a/aa; b/bb],
...
|-
... |
|
Universal consequent
...
|-
(FORALL (a: (a?)): p(a)),
... | | Applicable Proof Commands | Resulting Sequent | Explicit subtype information
(skolem * "aa" :skolem-typepreds? t)
(apply (then (skolem * "aa") (typepred "aa"))
see proof management below |
a?(aa), ...
|-
p(aa), ... |
|
Specific consequent ... |- p(eA), ...
assuming eA: A | | Applicable Proof Commands | Resulting Sequent | Generalization is the inverse of skolemization: requires human insight and often precedes well founded induction.
(generalize "eA" "a") |
... |- (FORALL (a: A): p(a)), ... |
|
| Instantiation | often requires human insight: "eA" and "eB" templates may be complex expressions. |
Existential consequent ... |- (EXISTS (a: A, b: B): alpha), ... | | Applicable Proof Commands | Resulting Sequent
|
(inst * "eA" "eB")
(inst + "eA" "eB")
(inst?) |
... |- alpha[a/eA; b/eB]
... |- eA: A, ...
... |- eB: B, ... |
|
Universal antecedent
(FORALL (a: A, b: B): alpha), ...
|-
... | | Applicable Proof Commands | Resulting Sequent |
(inst * "eA" "eB")
(inst - "eA" "eB")
(inst?) | alpha[a/eA; b/eB], ... |- ...
... |- eA: A, ...
... |- eB: B, ... |
(inst-cp * "eA" "eB")
(inst-cp - "eA" "eB") | alpha[a/eA; b/eB], (FORALL (a: A, b: B): alpha), ... |- ... ... |- eA: A, ... ... |- eB: B, ... same as above, except for preserving FORALL |
|
| Flattening | usually simplifies sequent by removing some logical connectors |
| | ... |- alpha IMPLIES beta, ... | ... |- alpha OR beta, ... | alpha AND beta, ... |- ... |
| | Applicable Proof Command | Resulting Sequent |
(flatten) | alpha, ... |- beta, ... | ... |- alpha, beta, ... | alpha, beta, ... |- ... |
|
|
| Case splitting | may complexify proof but is sometimes necessary |
| | ... |- alpha AND beta, ... | alpha OR beta, ... |- ... | alpha IMPLIES beta, ... |- ... | .. |- alpha IFF beta, ... | ... |- IF e THEN a ELSE b ENDIF, ... | ... |- CASES e OF ... ENDCASES, ... |
| | Applicable Proof Command | Resulting Sequents |
(split) | ... |- alpha, ...
... |- beta, ... | alpha, ... |- ...
beta, ... |- ... | ... |- alpha, ...
beta, ... |- ... | alpha, ... |- beta, ...
beta, ... |- alpha, ... | e, ... |- a, ...
... |- e, b, ... | several sequents |
|
|
... |- ... | | Applicable Proof Command | Resulting Sequents | Use a lemma on the fly. (case "alpha") | alpha, ... |- ...
... |- alpha, ... |
|
| Toward | propositional calculus |
|
Boolean equality
... |- ..., alpha = beta, ... provided alpha, beta: bool | | Applicable Proof Command | Resulting Sequent |
(iff) |
... |- ..., alpha IFF beta |
|
|
Embedded test
... |- p(IF e THEN a ELSE b ENDIF), ... | Embedded cases
... |- p(CASES e OF ... ENDCASES), ... |
| | Applicable Proof Command | Resulting Sequent |
(lift-if) | |
... |- IF p(e) THEN p(a) ELSE p(b) ENDIF, ... | |
... |- CASES e OF ... ENDCASES, ...
where p applies to each clause result |
|
|
| Decision | procedures for propositional calculus and linear arithmetics |
|
propositional sequent
NOT, AND, OR, IMPLIES, IFF
IF, CASES | | Applicable Proof Command | Resulting Sequents |
(prop) |
some sequents or none |
|
|
linear arithmetic sequent
=, <=, >, >= | | Applicable Proof Command | Resulting Sequents |
(assert) |
simplified sequent (or nomore sequent) |
|
|
propositional + linear arithmetic sequent
| | Applicable Proof Command | Resulting Sequents | |
(ground) |
some sequents or none |
|
| Using | function definitions |
|
sequent containing f (...)
typically with f non recursive | | Applicable Proof Command | Resulting Sequent | |
(expand "f")
(expand "f" +)
(expand "f" -) |
sequent with some f(...)
function calls unfolded |
|
|
sequent containing f(...)
typically with f recursive | | Applicable Proof Command | Resulting Sequent | |
(expand "f" :if-simplifies t) |
f(...) calls are unfolded
provided some simplification occurs |
|
|
... f(e1) ... f(e2) ... |- ... f(e3) ... | | Applicable Proof Command | Resulting Sequent | |
(expand "f" * 2)
(expand "f" - 2) |
... f(e1) ... fe2_unfolded ... |- ... f(e3) ... |
|
sequent containing f(...) | | Applicable Proof Command | Resulting Sequent | |
(auto-rewrite "f") |
sequent unchanged
subsequent (ground) will automatically trigger (expand "f" :if-simplifies t) |
|
| Using | lemmas, theorems, corollaries or the like |
|
antecedents |- consequents | | Applicable Proof Command | Resulting Sequent[s] | |
(lemma "foo") |
fooLemmaFormula, antecedents |- consequents | |
(use "foo") |
fooLemmaFormulaInstance, antecedents |- consequents
combines (lemma "foo") and (inst?) | |
(rewrite "foo") |
sequent with some term rewritten
according to lemma main equality
lemma hypotheses may trigger subgoals | |
(rewrite "foo" :subst ("a" ... "b" ...)) |
same as above but specifies
instantiation in part or whole | |
(rewrite "foo" :dir RL) |
same as (rewrite "foo") except that
main equality is applied from right to left | |
(rewrite "foo" :fnums +
:target-fnums +) |
same as (rewrite "foo") except that
rewriting only occurs within consequents | |
(auto-rewrite "foo")
Useful if "foo" lemma is
a good rewrite lemma |
sequent unchanged
subseqent (ground) will trigger rewriting
according to "foo" lemma if a match occurs
and all lemma hypotheses can be proved |
|
| Dealing with equality: | prefer (assert) whenever applicable |
|
proving function equality
... |- f = g, ... assuming f, g: [T -> U] | | Applicable Proof Command | Resulting Sequent[s] | |
(apply-extensionality :hide? t) |
... |- f(x!1) = g(x!1), ... |
|
|
Using an equality
a = b, ... |- ... | | Applicable Proof Command | Resulting Sequent | |
(replace -1 :hide? t) |
...[a/b] |- ...[a/b] | |
(replace -1 :hide? t :dir RL) |
...[b/a] |- ...[b/a] |
|
| Improve | readability |
|
hiding alpha1, alpha2, alpha3 |- beta1 beta2 | | Applicable Proof Command | Resulting Sequent | |
(hide -2 -3 1)
may hinder proof robustness |
alpha1
|-
beta2 |
|
|-
beta1 |
|
|
renaming constants
..., p(X!1, X!2), ...
|-
..., q(X!2, Y!3), ... | | Applicable Proof Command | Resulting Sequent | |
(name-replace "b" "X!2")
|
.., p(X!1, b), ...
|-
..., q(b, Y!3), ... | |
(name-replace*
("a" "X!1" "b" "X!2" "c" "X!3")) |
..., p(a, b), ...
|-
..., q(b, c), ... |
|
|
... |- ... | | Applicable Proof Command | Resulting Sequent | |
(comment "Bla bla bla.") |
... |- ...
sequent is left unchanged |
|
|
... |- ... | | Applicable Proof Command | Resulting Sequent | |
(apply (then c1 c2 c3)) |
sequent resulting from sequential application
of commands c1, c2, c3 | |
(undo) |
go back one proof step to parent sequent | |
(postpone) |
switch to next sequent,
therefore postponing current sequent proof | |
(quit)
quit |
quit PVS prover, saving current partial proof |
|
| Recover from | PVS crash |
|
LISP error!!!
(PVS bug) | | Applicable Proof Command | Resulting Sequent | |
(restore) |
goes back to previous coherent state of the proof, just before the proof command responsible for PVS crash |
|
| Believe in | miracles! |
|
... |- ... | | Applicable Proof Command | Resulting Sequent[s] | | (grind) | either some clumsy often unprovable sequents
or finishes proof of sequent
most powerful PVS proof command: OK to try,
but undo if does not complete the proof |
|
