The Coq mailing list

["Koprowski, A." <A.Koprowski AT tue.nl>]

   Hello everybody,

 

 While working on my development in Coq I encountered the following problem: I need to define an injective, partial function. I also want to be able to have the inverse of this function. At first I thought I can just represent the function as a relation with appropriate constraints as follows:

 

Record partialFun : Type := build_partialFun {

      pf: relation nat;

      f_Lok: forall i j j’, pf i j -> pf i j’ -> j = j’;

      f_Rok: forall i i’ j, pf i j -> pf i’ j -> i = i’

}.

 

  What I liked about this definition is that it is symmetrical (and in fact this function is to serve as representation for some mapping). Also computing inversion poses no problem (transposition of relation does the job). But now I’d like to decide whether for given i, exists j, such that f i j, so basically I’d like the following result:

 

Fact partialFun_dec: forall f i,

      {exists j, pf f i j} + {forall j, ~pf f i j}.

 

  And I do no need a way to get that with my current definition (I’d prefer not to use classical logic). Or maybe is there a better way to achieve that?

 

  Thanks in advance!

   Adam Koprowski

 

--

========================================================================

 Adam Koprowski, (A.Koprowski AT tue.nl, http://www.win.tue.nl/~akoprows)

 Department of Mathematics and Computer Science

 Eindhoven University of Technology (TU/e)

 The difference between impossible and possible lies in determination

      Tommy Lasorda

========================================================================