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

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