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

[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