The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

On 11/05/2011 02:31 PM, Adam Chlipala wrote:
> It's not obvious to me that your lemma is provable, even given the full
> set of axioms commonly assumed in Coq developments. You must
> fundamentally do inversion on [eqfun] with a particular function type as
> a parameter, which seems to call for a proof step going from [(D1 -> R1)
> = (D2 -> R2)] to [D1 = D2] and [R1 = R2], but I don't think such a rule
> is provable in CIC, and I don't think any of the common axioms imply the
> soundness of this step. It may be validated by the usual Boolean model
> in ZF, so perhaps it would be consistent to assert this as an axiom.

In fact, the intuitive set-theoretical model disproves it: when D1 = D2 
= empty, then D1->R1 = D2->R2 holds for all R1 and R2. Dually, when 
R1=R2=empty, we cannot deduce D1=D2.

Even when both sets are non-empty, we're not out of trouble: there is a 
set-theoretical model of Coq which disproves (D1->R1=D2->R2) -> D1=D2 in 
that case. It uses Aczel's encoding of functions (*), in which 
D1->{empty} = D2->{empty} (= {empty}) holds for all D1 and D2. 
(Remember: {empty}=True, and (D1->True) <-> True.)

However, David's problem can be solved without such principle, but just 
assuming functional extensionality (as Hugo just showed), which is 
supported by the IZF model.

In Coq, it is most of the time awkward to put arbitrary types as index 
(when other indexes are constrained by them). You'd better write a 
"code" for your types and use it as index. David seems to consider only 
a subset of simple types, so a list of types would do (with the obvious 
decoding function). You could then make a definition of [eqfun] (by 
induction on the list) which entails [cnuf] definitionally (no axiom 
needed).

Bruno.

(*)
Peter Aczel's encoding for a (meta-)function f with domain D is
{ (x,y) | x in D and y in f(x) }. Compare this to the standard encoding:
{ (x,y) | x in D and y = f(x) }.

--
Bruno Barras                    Typical team - INRIA Saclay
LIX - Ecole Polytechnique       91128 Palaiseau Cedex - France
Tel: +33 1 69 33 40 57          Fax: +33 1 69 33 30 14