PVS theorem prover

General

• -: antecedent
• +: consequent
• PVS specifications are packaged as theories.

Emacs

Recovering from errors

(restart) may be helpful.

• fail
• undo
• postpone
• skip

Logic of PVS

PVS uses sequent calculus.

Inference rules are of the form:

 Γ₁ ⊢ Δ₁     ...    Γₙ ⊢ Δₙ
----------------------------
            Γ ⊢ Δ

Given a leaf node of a proof tree with Γ ⊢ Δ, this rule allows adding n children to that node (making it a non-leaf node).

Structural rules:

    A,A,Γ ⊢ Δ                    Γ ⊢ A,A,Δ
---------------- c⊢          ----------------- ⊢c              
     A,Γ ⊢ Δ                      Γ ⊢ A,Δ



  Γ₁,A,B,Γ₂ ⊢ Δ                Γ ⊢ Δ₁,A,B,Δ₂
---------------- x⊢          ----------------- ⊢x              
  Γ₁,B,A,Γ₂ ⊢ Δ                Γ ⊢ Δ₁,B,A,Δ₂



Propositional rules:

    A,B,Γ ⊢ Δ                  Γ ⊢ A,Δ     Γ ⊢ B,Δ
---------------- ∧⊢          ----------------------- ⊢∧              
  A ∧ B,Γ  ⊢ Δ                     Γ ⊢ A ∧ B,Δ     



  A,Γ ⊢ Δ   B,Γ ⊢ Δ           Γ ⊢ A,Δ     Γ ⊢ B,Δ
--------------------- ∨⊢     ----------------------- ⊢∨              
    A ∨ B,Γ ⊢ Δ                   Γ ⊢ A ∧ B,Δ     

More stuff

• Primitive proof rules
• Proof strategies: In Coq, similar purpose is served by user-defined rules with Ltac.

Keywords for symbols

And WHEN is same as IMPLIES with the order of operands reversed.

These symbols are simply textual replacements.

So λn:n is not same as λ n: n. Former would give error as they expand like:

And pvs would flag the LAMBDAn part as a syntax error.

Strategy application stuff

a strategy invoked with a $ suffix means that the strategy will be executed with the expanded internal steps still visible. Useful for debugging.

• * suffix: repeatedly apply strategy
• ! suffix: use generated names
• !! suffix:
• + suffix:
• no suffix: use specified names

Naming convention

From prover-guide section 4.13:

Deprecated form:

• "name": lazy
• ("name"): eager
• (("name")): macro

New form:

• "name": lazy
• "name!": eager
• "name!!": macro

Both forms still work, but can't be mixed.

A proof with TCCs

Sum of first n natural numbers

sumn: THEORY
BEGIN
  n: VAR nat
  sum(n): RECURSIVE nat =
    (IF n = 0 THEN
       0
     ELSE
       n + sum(n-1)
     ENDIF)
    MEASURE (LAMBDA n: n)

  nnatsum: THEOREM
    sum(n) = (n * (n+1)) / 2
END sumn

Proof?:

(induct "n")
(expand "sum")
(skolem!)
(flatten)
(expand "sum" +)
(assert)

Rules and strategies

User guides the proof construction process via rules and strategies.

Some rules:

• skolem introduces Skolem constants for universal strength quantifiers.
• inst instantiates a Skolem constant for existential strength quantifiers.

If we got a sequent like ⊢ (a → b), flatten can make it a ⊢ b.

Import system is there (IMPORTING), but not going into that.