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

Reply: [PVS-Help] How can we extract properties from singleton_elt[nat]?




Xiwen Chen
 
Hello.
 
   I think the definition of get_index is not sound because we can not find i, j  such that "FORALL (k: nat): k /= j AND k < 3 IMPLIES k <= i"  holds when len =0 or  len = 1.
   "get_index_3" should be  proved by iintroding the lemma epsion_ax. but the proof may be complex because Your definition about get_index invokes the COVERSION mechanism in the PVS prelude file.
    Do you think so?

 
Cheers
Qingguo XU
------------------  
2012-11-08
 
 
发件人: Xiwen Chen
发送时间: 2012-11-08 07:34:31
收件人: pvs-help
抄送:
主题: [PVS-Help] How can we extract properties from singleton_elt[nat]?
Hi All,
I got so confused when proving something in PVS like:
{-1}  j = get_index(3)
   |-------
{1}   j = 1
and when I expanded "get_index", it showed me 
"singleton_elt[nat](.....)" as follows:
{-1}  j =
        singleton_elt[nat]
            ({i: nat |
                EXISTS (j: nat):
                  j < 3 AND
                   i < 3 AND
                    i < j AND
                     (FORALL (k: nat): k /= j AND k < 3 IMPLIES k <= i)})
   |-------
[1]   j = 1
(Basically, "get_index(n)" returns n-2)
To prove this, is there any way to somehow "extract" the properties 
shown in fnum[-1] as some antecedent? Thus, we can do "skolem" and 
"case" analysis to prove it.
By the way, I tried so many PVS prover command to deal with this 
singleton but failed. When I tried to expand "singleton_elt", it showed:
{-1}  j =
        the! (x: nat):
          EXISTS (j: nat):
            j < 3 AND
             x < 3 AND
              x < j AND (FORALL (k: nat): k /= j AND k < 3 IMPLIES k <= x)
   |-------
[1]   j = 1
What can we do using PVS prove command with "the!(x:nat)" ?
Really appreciate!
Thank you!
Xiwen
*********************************************************************
The whole theory is shown below if needed:
(Intuitively, "get_index(n)" returns n-2)
TEST: THEORY
BEGIN
   get_index(length:nat): nat = {i:nat| EXISTS (j:nat): j<length AND
                 i<length AND i<j AND
         (FORALL (k:nat): k/=j AND k<length
    IMPLIES  k<=i
 )
   }
   get_index_3: LEMMA FORALL (j:nat): j=get_index(3) IMPLIES j=1
END TEST
*********************************************************************