# 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
%|-  ((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

```