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

Re: [PVS-Help] problem proving Maybe DATATYPE in PVS



Hi Cesar:

Thanks for your response. 

It seems that the PVS type inference mechanism is more robust on parameterized theories than on parameterized functions within a theory. So when I define a Maybe theory (see below), grind does indeed discharge the proof.

Regards,

Jonathan

%-----------------------
Maybe[T:TYPE] : THEORY
BEGIN
Maybe: DATATYPE 
  BEGIN
    None : none?
    Some(val:T): some?
  END Maybe
END Maybe

%-----------------------
test_maybe: THEORY
BEGIN
IMPORTING Maybe
safedivision(x,y:real): Maybe[real] =
  COND
    y=0 -> None
    ,ELSE -> Some(x/y)
  ENDCOND

test1: CONJECTURE
  safedivision(6,3) = Some(2) AND safedivision(6,0)=None

%|- test1 : PROOF
%|- (grind)
%|- QED

% (eval-formula) also works

END test_maybe
> On Nov 1, 2016, at 8:08 PM, Munoz, Cesar (LARC-D320) <cesar.a.munoz@xxxxxxxx> wrote:
> 
> Hi John,
> 
> Interestingly, this type is defined in the NASA PVS Library (structures@Maybe) and when safedivision is defined using this type, grind works without any issue:
> 
> 
>  IMPORTING structures@Maybe
> 
>  safedivision(x,y:real): Maybe[real] =
>  COND
>    y=0 -> None
>    ,ELSE -> Some(x/y)
>  ENDCOND
> 
>  test1: CONJECTURE
>    safedivision(6,3) = Some(2) AND safedivision(6,0)=None
> 
> test1 :  
> 
>  |-------
> {1}   safedivision(6, 3) = Some(2) AND safedivision(6, 0) = None
> 
> Rule? (grind)
> safedivision rewrites safedivision(6, 0)
>  to None
> safedivision rewrites safedivision(6, 3)
>  to Some(2)
> Trying repeated skolemization, instantiation, and if-lifting,
> Q.E.D.
> 
> Unrelated to your question, but since that statement only involves ground expressions, it can be proven with eval-formula:
> 
>  |-------
> {1}   safedivision(6, 3) = ok(2) AND safedivision(6, 0) = none
> 
> Rule? (eval-formula)
> Evaluating formula 1 in the current sequent,
> Q.E.D.
> 
> 
> 
> Cesar
> 
> 
> ________________________________________
> From: pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx [pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx] on behalf of Jonathan Ostroff [jonathan@xxxxxxxx]
> Sent: Tuesday, November 01, 2016 5:27 PM
> To: pvs-help@xxxxxxxxxxx
> Subject: [PVS-Help] problem proving Maybe DATATYPE in PVS
> 
> Here is the PVS equivalent of Haskell’s Maybe datatype:
> 
> ----------------------------------------------------------------------
> Maybe[T:TYPE]: DATATYPE
>  BEGIN
>    none   : none?
>    ok(t:T): ok?
>  END Maybe
> 
> safedivision(x,y:real): Maybe[real] =
>  COND
>    y=0 -> none
>    ,ELSE -> ok(x/y)
>  ENDCOND
> 
> test1: CONJECTURE
>  safedivision(6,3) = ok(2) AND safedivision(6,0)=none
> ----------------------------------------------------------------------
> 
> The right conjunct proves with grind but not the left conjunct. (grind) will get it to
> 
>        ok(2) = ok(2)
> 
> but reflexivity of equality doe not get invoked, perhaps due to type inference problems.
> 
> The following proof will work:
> 
> %|- test1 : PROOF
> %|- (spread (split)
> %|-  ((then (expand "safedivision") (name-replace "x" "ok(2)"))
> %|-   (then (expand "safedivision") (propax))))
> %|- QED
> 
> So the name-replace trick gets equality to work.
> 
> Just wondering if type inference with genericity can be improved?
> 
> Thanks,
> 
> Jonathan
> 
> 
> 
>