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

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



Yes, I agree with "x=1"!  Thank you so much!

Cheers,
Xiwen


于 12-11-14 2:00 AM, 许庆国 写道:
Xiwen Chen

    you are right.  I think it will be more efficient instance "x" as 1 rather than "j".  thank you!
   BTW, your improved version is quite nature in the logic view.

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

发件人: Xiwen Chen
发送时间: 2012-11-14 14:46:01
收件人: 许庆国
抄送: pvs-help
主题: Re: Reply: [PVS-Help] 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
*********************************************************************