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

Re: [PVS-Help] how to prove such a simple lemma?

K.Wei wrote:
> Hello all,
> I just met a so simple lemma, but don't know how to prove it. Who could help me?
> P,Q: VAR [size:{a:nat| a>=3}, [below[size] ->set[nat]]]
> test: LEMMA   P`1=Q`1+1 AND FORALL (i:below(P`1)),(j:below(Q`1)): P`2(i)=Q`2(j) 
>                           IMPLIES EXISTS (i,j:below(P`1)): P`2(i)=P`2(j)
> since the size of Q is 1 less than the size of P, so this lemma should hold. I think I should use epsilons, but don't know how to apply this command.
> many thanks!
> Kun


The epsilon function is not required in this case.
You can instantiate i and j in the EXISTS ...
with two constants. For example, i=0, j=0 should work

For this to work, you need to fix the formula above
(otherwise PVS will parse it into something not provable).

Assuming it's rewritten as

test: LEMMA
P`1=Q`1+1 AND (FORALL (i:below(P`1)),(j:below(Q`1)):P`2(i)=Q`2(j))
IMPLIES EXISTS (i,j:below(P`1)): P`2(i)=Q`2(j)

Then (skosimp)(inst + "0" "0")(reduce) should work,