The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Hi,

Sorry to ask a very old question, but I have not found a satisfactory
answer to it, on the Web.

Since I have programmed in Coq (three years), I have always wondered
why there is this duality between propositions and functions. I mean,
I don't ask here how to use them, I do it daily and sometimes change
from one form to the other. My question is epistemologic.

Here is what I understand about it.

Let us suppose we want to compare these two forms:
  * x = 0 => something
  * if x = 0 then something

In both cases, we "reach" the "something" when x is equal to 0.

In the first case, "time" is not involved: you can say:
   - when I have x = 0, I get something
   - to get something, it is sufficient to have x = 0
   - if I don't have something, x cannot be 0 (in classical logic)
   - I have x ≠ 0 or something (classic too)
   - etc.

In the second case, "time" is involved: I compare x with 0 and if they
are equal, I go to something. It is code, I can generate code, and when
I run it, I cannot go backward.

Moreover, there is a *decidability* issue: if the equality is not
decidable, I can use:
   x = 0 => something
but not:
   if x = 0 then something

But this duality is strange to me. Why two notions almost doing the
same thing?

In mathematical lessons, we learn about propositions (x = 0 => something)
but not about functions (if x = 0 then something). We learn functions only
in programming lessons.

But this duality seems to be an important thing, at least in Coq and
therefore in mathematics (I believe that Coq = Mathematics). Does that
mean that we should teach these duality in future mathematic classes?

It seems that mathematicians generally do not consider this difference
in their pen and paper proofs. They often say: "there are two cases, x
is equal to 0 or x is not equal to 0", without questionning themselves
about decidability.

Why Nature built that?

Is there something which I could read on that topic? (which is not too
theoretical please).

Thank you.

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/