The Coq mailing list

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

  Dear all,

 During my work I encountered the following problem, to which I think I
found a solution just I'd like to confirm that my line of reasoning is
correct and that there is no simpler approach.

 I need to specify a partial, injective function on natural numbers
(mapping on natural numbers) and I need to be able to compute its
inversion. I _definitely_ don't want to use classical logic so I suppose
in general my task is hopeless as even if I know that the inverse exists
(function is injective) I may not be able to compute it efficiently. Is
that true?

 However in my problem the domain of mapping is always finite which
should make the task feasible. The approach I was thinking of is to
define the function as a relation with appropriate constraints and with
the number indicating the maximal natural number that belongs to the
domain or range of the function. In Coq it would be something like:

Record natFun : Type := {
  nf:      relation nat;
  lok:     forall i j j', nf i j -> nf i j' -> j = j';
  rok:     forall i i' j, nf i j -> nf i' j -> i = i';
  size:    nat;
  size_ok: forall i j, nf i j -> i <= size /\ j <= size
} 

  To compute inverse of the function I simply take the transposition of
the relation. To compute f(i) I look at nf(i, j) for all j <= size. If
none holds 'i' is not in the domain of the function. If I find nf(i, j)
to hold for some 'j' then f(i) = j and because of 'lok' I know that this
'j' is unique. Does it make sense? Is there a simpler approach that I
can take?
 
  Thanks a lot in advance!
  Kind regards,
   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 
========================================================================