The Coq mailing list

[Robin Green <greenrd AT greenrd.org>]

On Mon, 08 Sep 2008 11:00:40 +0200
Cody Roux 
<Cody.Roux AT loria.fr>
 wrote:

> - It is not clear to me that all theorems for free are not provable in
> the calculus of (inductive) constructions

I understand you to mean: "I do not see why it should be the case that
_no_ theorems for free could ever be provable inside C(I)C".

You would have to introduce some axioms. You could try to prove
theorems for free based on axioms about what closed terms can
be constructed in Coq. That is, a reflection based approach, where you
reflect on the entirety of the CIC within itself. I fear this would run
into foundational issues however, as you would not be able to represent
type universes consistently (is this something to do with Godel's
Incompleteness Theorem?).

I have tried to prove theorems for free based on introducing
other theorems for free as axioms (i.e. to see if some are consequences
of others), but I have not had much success even with this approach. I
don't see how you could do it without introducing any axioms.

If, instead, you actually meant "I do not see why there exists a theorem
for free that holds for simpler languages but that does _not_ hold for
C(I)C" I will quote you something from my MSc thesis (which has been
submitted but not yet accepted):

---
>From the point of view of proving free theorems, the basic idea of
parametricity is that “a polymorphic term that gives outputs in the
same type for all input types, must be constant.” (Term here means
function.) In System F augmented with the latter axiom (called System
Fc), the following theorem holds:

** Genericity Theorem ** “If two second-order terms coincide on an input
type, then they are, in fact, the same function.”[longo_genericity_1993]

** Theorem 9.1 ** The Genericity Theorem does not hold for Coq's
Calculus of Inductive Constructions.

** Proof ** This proof consists in exhibiting a counterexample. A sized
list type is a well-known dependent type which is parameterised by its
length and its element type (in that order). Suppose this is converted
into an indexed type -- that is, the length is represented as a
type-level natural number, instead of an ordinary natural number. Take
the two terms in question to be the polymorphic identity on sized
lists, and the function of the same type which ignores its arguments
and yields an empty sized list. These terms coincide on an input type
of Zero, but are not the same function. \square

The key difference compared to System Fc is that in Coq, indexed types
can be constructed -- and not all constructors of an indexed type are
necessarily available for all type arguments. In the counterexample
above, only the empty list constructor is available when the length
type argument is Zero.
---

-- 
Robin Green