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

Re: [PVS-Help] problem when proving false in forall clause

Hi Chen.

One of the things to keep in mind when proving with sequents is that you
can either drive a consequent (below the line) to TRUE or an antecedent
(above the line) to FALSE.  In this case, you can make it FALSE by
supplying a nat less than 20, e.g.,

Rule? (inst - "0")

The reason the grind gets it for the = TRUE case is that it skolemizes
FORALLs in the consequent, and when skolemized, it reduces to TRUE.
FORALLs in the antecedent (and EXISTS in the consequent) require
instantiation.  Grind attempts to instantiate based on patterns and
terms it finds in the sequent.  In this case the only nat available is
20, but this doesn't satisfy the subtype constraint.  So grind leaves it
for you to instantiate.

Hope this helps,

CHEN Chunqing <chenchun@comp.nus.edu.sg> wrote:

> Dear all,
> Currently I am using PVS (version 3.1) in my research. I encounter an
> interesting problem when proving the following lemma:
> False_n_emp: LEMMA (forall (y : {z : nat | z < 20}): FALSE) = FALSE;
> After I tried the command "grind", the result is:
> {-1} (forall (y: {z : nat | z < 20}): FALSE)
>   |---------------------------
> Rule?
> that is to say, there is no consequent, and I have no idea what to do
> next. So could you kindly enlighten me how to solve the problem and what
> causes the problem?
> Actually, it is strange when I modified the above lemma to:
> False_n_emp: LEMMA (forall (y: {z : nat | z < 20}): TRUE) = TRUE;
> This time, PVS can prove it by single command "grind".
> Does anyone meet the similar problem before, and could you please share
> your experience?
> Thank you in advance and looking forward to your reply.
> Regards
> Chunqing