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

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



Hi Qingguo,

I really appreciate for your suggestions and solutions! So the key point is to use (lemma "singleton_elt_lem[nat]") to somehow get the properties of "j". Therefore, we can then use those properties to prove the goal.

That lemma is quite useful. One thing that I want to double check is the way to instancing the set and the nat variable. Did you try to instance the set "a" and number "x" as
a={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)}

x=j


Another solution is to re-formalize the function in a way such that we can directly get such properties:

****THEORY*************
get_index_v2(i,length:nat): bool = 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_v2: LEMMA FORALL (j:nat): get_index(j,3) IMPLIES j=1
*************************

By using this way the proof will be much more simplified than the version which regards the "get_index" as a function to return a number.

Thank you so much,
Xiwen


-----------------------------------------------------------------------------------
Xiwen Chen

Hello.
    I had some time last evening and have proved "get_index_3".    After using  (lemma "singleton_elt_lem[nat]")  and then instancing the set and the nat variable,  you can complete the rest proof via "assert" command and others frequently-used proving command.  

Cheers
Qingguo XU 
------------------  
2012-11-14


发件人: 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
*********************************************************************