Re: [PVS-Help] [PVS HELP] problem with lemma

[Sam Owre <owre@xxxxxxxxxxx>]

Hi Михаил,

The problem is that you're trying to instantiate a nested forall in one
shot

  fp1: AXIOM
    (FORALL (alloc: alloc_table):
    (FORALL (i: int):
    (i >= 0 IMPLIES
    (FORALL (m: int):
    (0 < m AND m < 32 IMPLIES
    (FORALL (p: pointer[global]):
    (valid[global](alloc, p) AND valid_range[global](alloc, p, i, m) IMPLIES
    fp(p, i, m) >= 0)))))))

You can bring in fp1 with alloc instantiated:

Rule? (lemma "fp1" (alloc "alloc!1"))
Applying fp1 where 
  alloc gets alloc!1,
this simplifies to: 
min_impl_po_1.1 :  

{-1}  FORALL (i: int):
        (i >= 0 IMPLIES
          (FORALL (m: int):
             (0 < m AND m < 32 IMPLIES
               (FORALL (p: pointer[global]):
                  (valid[global](alloc!1, p) AND
                    valid_range[global](alloc!1, p, i, m)
                    IMPLIES fp(p, i, m) >= 0)))))
...

But after that you need to use inst to instantiate the rest (plus some
simplification, i.e., assert to get the quantifier to the top).

Hope this helps,
Sam

Гильмендинов Михаил <mix_-@mail.ru> wrote:

> Hi,
> 
> proof of lemma reduced to
> 
> <...>
> -----
> {1} fp(t!1, 0, n!1)
> 
> it can be prooved with fp1 axiom.
> 
> 
> Rule? (lemma "fp1" (alloc "alloc!1" i "0" m"n!1" p "t!1"))
> 
> PVS returns:
> 
> Found 0 resolutions etc.
> 
> when i wrote:
> 
> Rule? (lemma "fp1[global]" (alloc "alloc!1" i "0" m"n!1" p "t!1"))
> 
> there is another error:
> 
> Couldn't find a definition or lemma named fp1[global]
> Expecting a formula or constant
> No resolution for fp1[global]
> 
>  Check the actual parameters; the following instances are visible,
>  but don't match the given actuals:
>    y_spec_why.fp1
> 
> No change on: (lemma "fp1[global]"
>                (alloc "alloc!1" i "0" m "n!1" p "t!1"))
> 
> How can I use fp1 axiom?
> 
> example in attachment.
> 
> I use Caduceus  1.20, Why 2.20 and PVS 4.2