PVS‎ > ‎

inference

This is an inference summary: most, if not all, useful PVS proof commands are included.

 Current Sequent Applicable Proof Command[s] and Resulting Sequent[s]
 Universal consequent





...

|-

(FORALL (a: A, b: B): alpha),

...

Applicable Proof CommandsResulting 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 CommandsResulting 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 CommandsResulting 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 CommandsResulting 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 CommandResulting 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 CommandResulting Sequents




(split)

... |- alpha, ...

... |- beta, ...

alpha, ... |- ...

beta, ... |- ...

... |- alpha, ...

beta, ... |-  ...

alpha, ... |- beta, ...

beta, ... |- alpha, ...

e, ... |- a, ...

... |- e, b, ...

several sequents





... |- ...

Applicable Proof CommandResulting Sequents
Use a lemma on the fly.

(case "alpha")

alpha, ... |- ...

... |- alpha, ...


 Toward  propositional calculus

Boolean equality
... |- ..., alpha = beta, ...

provided alpha, beta: bool

Applicable Proof CommandResulting Sequent

(iff)

... |- ..., 
alpha IFF beta

Embedded test
... |- p(IF e THEN a ELSE b ENDIF), ...

Embedded cases
... |- p(CASES e OF ... ENDCASES), ...


Applicable Proof CommandResulting 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 CommandResulting Sequents

(prop)

some sequents or none

linear arithmetic sequent
=, <=, >, >=

Applicable Proof CommandResulting Sequents

(assert)

simplified sequent (or nomore sequent)


propositional + linear arithmetic sequent

Applicable Proof CommandResulting Sequents

(ground)

some sequents or none


Using  function definitions


sequent containing f (...)
typically with f non recursive

Applicable Proof CommandResulting Sequent

(expand "f")
(expand "f" +)
(expand "f" -)

sequent with some f(...)
function calls unfolded


sequent containing f(...)
typically with f recursive

Applicable Proof CommandResulting Sequent

(expand "f" :if-simplifies t)

f(...) calls are unfolded
provided some simplification occurs


... f(e1) ... f(e2) ... |- ... f(e3) ...

Applicable Proof CommandResulting Sequent

(expand "f" * 2)
(expand "f" - 2)

... f(e1) ... fe2_unfolded ... |- ... f(e3) ...




sequent containing
f(...)
Applicable Proof CommandResulting 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 CommandResulting 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 CommandResulting Sequent[s]

(apply-extensionality :hide? t)

... |- f(x!1) = g(x!1), ...


Using an equality
a = b, ... |- ...

Applicable Proof CommandResulting 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 CommandResulting 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 CommandResulting 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 CommandResulting Sequent

(comment "Bla bla bla.")

... |- ...
sequent is left unchanged


... |- ...

Applicable Proof CommandResulting 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 CommandResulting 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 CommandResulting 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

More on PVS inference

The slides below have been obtained by conversion from “ppt” to “Google slides” format: the translation is not perfect! Please wait for fixes; check the “ppt” or “pdf” versions in the mean time (bottom of the page).

PVS inference - Slides



ą
Paul Y Gloess,
18 sept. 2013 à 10:04
Ċ
Paul Y Gloess,
13 sept. 2013 à 07:07
ć
Paul Y Gloess,
13 sept. 2013 à 07:07
Comments