Re: [Spark] Splitting 'and' conditions into multiple conditions

[Peter Amey <peter.amey@praxis-cs.co.uk>]

Lutz Donnerhacke wrote:
> The simplifier is often unable to prove easy conclusions, because conditions
> given als assert, precondition, and postcondition occur as a single
> conclusion.
> 
> Example:
> C1: res__1 >= buf__first and res__1 <= buf__last and (res__1 >= 0 and res__1
> 	  <= 0) -> res__1 >= buf__first and res__1 <= buf__last .
> 
> Or do I misinterpret this line containing an implication?
> Should the simplifier not able to handle this by transfering the frist part
> to the hypothis?

Lutz,

We are always interested in collecting examples where the Simplifier can 
be improved.  You should note, however, that the Simplifier is just 
that, it is not intended to be a heavyweight proof engine like PVS.  The 
idea is to limit what the Simplifier gets up to so as to maintain clear 
traceability between what goes into it and what comes out and to avoid 
the possibility of multiple substitutions leaving the formulae in a 
worse state than they started.  The unsimplified VCs that are left can 
always be tacked with the interactive Prof Checker tool.

Peter