[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Syntax and prover




Robert:

> 1.  I may be doing something wrong, but my impression was that using IFF
> expressions in proofs was less "convenient" (for lack of a better word).
>  Is that true?  If so, would it be helpful for me to take IFF
> expressions, and generate implication lemmas out of them for use in proofs?

I'm not sure what you have in mind but there's no big downside to using IFF.
The main difference between using = and IFF is that propositional commands
like flatten, split, and prop process IFF but not =.  The rewrite
commands handle both the same.  IFF could be inconvenient if you want
to keep the equality in its undecomposed form.  

> 2.  A relation I have been using is naturally expressed as a transition
> relation of roughly the following form:
> 
> Trans(program, state, ancillary-state,program1, state1, ancillary-state1)
> 
> Question:  in order to do an inductive proof, should I group the three
> state components into one entity (and then possibly provide a conversion
> to get back the original form)?

I don't think it makes a difference in terms of inductive proofs.  The
main reason for grouping them is to exploit some generic theories
that might require the pre and post states to be packaged together.
You could use conversions going back and forth for this purpose.

Cheers,
Shankar