The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Mon, Apr 29, 2013 at 12:08 PM, Marco Servetto <marco.servetto AT gmail.com> wrote:

I do not understand two things here:
First

>>Definition X (n : nat) : Ensemble unit
>>:= fun _ => …
>>   (*stating that the nth Turing Machine halts on any input *).

How can such function be accepted by coq? i.e. only provable
terminable functions can be defined, thus the halting problem stop  us
here.

Ensemble unit is morally equivalent to Prop, which allows you to formulate basically any mathematical statement, regardless of whether you can compute whether it's true or false.  For example, given an appropriate formalization of "Turing Machine", it will be easy to define the function TuringMachines -> States -> Inputs -> Prop which states: Turing Machine T starting at state s halts on input I (such as fun T s I => exists n:nat, TuringMachineHaltsWithin n T s I) where TuringMachineHaltsWithin obviously should be computable.

Second:
Is not a finite set (over elements with ordering) isomorph to an
ordered list with no repetition?

In principle, yes.  However, what you want you're trying to define in the original post is a function which, given that you know "somehow" that a certain abstract set is finite, terminates and returns a list of its values.  But there are a couple problems with that: first of all, for an abstract set, membership in that set might not be a computable function.  And even if it were: if the domain is infinite, just from knowing that the set is finite, you can't determine when you've examined enough elements to safely terminate the function.  (And if the domain isn't even countable, that raises more issues...)

However, if your domain is finite, and you're given some function which computes membership in the set, then it should be easy to write a function to test membership for each element of the domain and return a list of values for which it passes.

Reiterating what other people have said in this thread, it would help if we knew what you were trying to accomplish (e.g. mathematical formalization? program verification?).
--
Daniel Schepler