The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

Hello,

I've been working on extending DEVOID a lot recently (I'll send out info about a mailing list at some point soon, for people who want to hear more about what we've been up to). One thing I keep coming back to is supporting lifting between { l : list T & length l = n } and (vector T n), instead of just (list T) and (sigT (vector T)). Or the analogous problem for the other equivalences in the class like this that DEVOID handles.

It should be really easy to extend DEVOID to compose liftings, and some early thoughts on that are here. The second equivalence follows very trivially from the first, and with the original equivalence that DEVOID finds, you can always lifting between { l : list T & length l = n } and { s : sigT (vector T) & projT1 s = n }. Two questions follow from this.

Eliminator for { l : list T & length l = n }

I keep hearing from people that { l : list T & length l = n } is easier to use than (vector T n). I understand why this is true in theory, but I haven't found it to be true in practice. I don't find it any easier to deal with the rewrites at the term level than at the type level. Is there an eliminator that people typically use for this that lets them cleanly separate the list proofs and functions from the length proofs? If so, what is it?

"Relational UIP"

Another question follows from that. One reason { l : list T & length l = n } is a particularly easy case is that nat is an hset. So we can show that all equalities between proofs of (length l = n) are equal. Lately I've been very frustratingly trying to figure out if I can make that any easier when the index type isn't necessarily an hset, but when there's still some equivalence between { a : A & indexer a = i_b } and B i_b. It seems to me that, in theory, this class of types should be easier to deal with than indexed types in general, even when the type of i_b is not an hset. In practice, I can't figure out a way to make that true without assuming any axioms.

The simplest example I can think of looks like this:

Inductive A: Type :=

| foo : A.

Inductive B : Type -> Type :=

| bar : B nat.

Clearly, we can't show that all equalities between terms of type Type are equal to each other. But we do know that if we have a B, it's not any type. It must be nat in particular.

Is there any way we can use this information to make it easier to show equalities between terms of type B? This question is a bit more open-ended.

Talia