# 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

```
```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

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

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
*********************************************************************
```
```
```

• References: