The Coq mailing list

[Stefan Karrmann <sk AT mathematik.uni-ulm.de>]

Dear all,

here are my 2 Cent thoughts about Prop, Set and extraction.

The distinction into the two sorts Prop and Set in Coq complicates
libraries IMHO. It forces library writer to multiplicate constructions. In
the standard theories there are some examples:

(a) and, prod, prodT
(b) or, sum, sumbool, sumor
(c) ex, sig, sigS, sigT
(d) Prop(True, False), bool(true, false)
(e) identity, eq
(f) not, notT

The development of C-Corn is a nice example of the problems. First,
everything was in Prop. Second, everything was in Set. Eventually, it
contains a well chosen mixture of Prop and Set. Some standard constructions
are doubled in another sort. C.f. [1].


The sorts Prop, Set and Type(i) are given early in the definition of
(co-)inductive types. Is it possible to provide the information if a value
is non-informative later or automatically?


Suppose you have a function f:A->B with Hoare style pre- and post-conditions
P and Q, respectively. In Coq you can declare:

   Variable f : forall (x:A), P x -> { y:B | Q x y }.


1. Non-informative by attribute
===============================

Suppose that we drop Prop and only keep Set (:= Type(0)). This alone would
make extracts to ML ineffective or difficult. So assume a prefix operator
`^' which marks the type as non-informative. (^ is mnemonic for throw it
out and away in extracts to ML.) Then the function f can be declared as:

   f : forall (x:A), ^ P x -> { y:B & ^ Q x y }

You can still declare types non-informative, e.g.:

Definition P' (x:A) := ^ P x.


2. Automatic non-informative
===============================

Suppose again that we drop Prop. If 'P x' is really a pre-condition there
is no match on it in the definition of f. Thus, Coq can infer that it is in
'^ P x'. If no caller of f does a match on 'Q x y' Coq can infer that the
second part of the result is in '^ Q x y', too.

Of course, Coq must know *every* caller in its analysis. (Even indirect
callers. For 'P x' it must check called functions, too.)
This reminds me of dead code analysis.


Is something like this possible?

Any remarks are welcomed.

Related articles:
=================
[1] http://www.pps.jussieu.fr/~letouzey/download/these_letouzey_English.ps.gz
[2] http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2003/berghofer.pdfo
[3] http://c-corn.cs.kun.nl/

Regards,
-- 
Stefan Karrmann