The Coq mailing list

[Iain Whiteside <Iain.Whiteside AT newcastle.ac.uk>]

Dear all,

I am investigating the ways in which different theorem provers handle 
undefinedness. In Isabelle, for example, 5/0 is represented as some number, 
but we cannot reason about it; alternatively, partial functions can be 
encoded in a monad (None | Some x).

I’d be interested to hear what is the (if any) canonical way of representing 
partiality in Coq and pCiC? For example, how could a recursive difference 
function like below (deliberately partial) be represented?

diff (i,j) = if i = y then 0 else diff(i+1,j) + 1

additionally, could a theorem such as  

forall i j. diff(i,j) = i - j \/ diff(j,i) = j - i

Many thanks in advance,

Iain