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

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



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