The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

When you write "propositions" you probably mean "relations". As it happens, for every function, there is a relation called its graph (in Coq-ish notation):

Gr f := fun x y => x = f y

Obviously, Gr f is such that for every x, there is a unique y such that x and y are related through Gr f. Such a relation is called a functional relation. As it happens, in ordinary mathematics, Gr as a function from functions to functional relations is invertible. So that functions and functional relations can be identified (as a matter of fact, functional relations are a common definition of functions). This property, by the way, is (somewhat clumsily) called unique choice.

It is important to realise that the failure of unique choice in Coq is not due to the fact that Coq is constructive. In fact, ordinary (pen&paper) constructive mathematics typically assume unique choice. In Coq, functions and functional relations are distinct, but they are not very different. There are theoretical reasons for the distinction in Coq (something to do with strong sums from an impredicative sort being inconsistent, to use a lot of jargon), but from a practical point of view, I like to argue that this distinction is useful because it allows to have computationally inefficient proofs without them spilling into functions which we want to keep efficient. I touch these issues in the first chapter of my thesis [ http://assert-false.net/callcc/Arnaud/thesis ].

In the perspective where functions and functional relations are identified, we could see function constructions as operations on relations which happen to preserve the existence and uniqueness of the image. However, the relation between if and logical implication is tenuous. Indeed, if p is a property such that p∨¬p, we can define if p then u else v in two equivalent manners:

(p ⇒ u)∧(¬p ⇒ v)

or

(p∧u)∨(¬p∧v)

Which I will leave as an exercise.

On 23 January 2014 15:39, Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr> wrote:

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/