The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

Hi Arnaud

On 6 Jun 2008, at 19:29, Arnaud Spiwack wrote:

> (out (cons xs)) should not compute to (cons xs)
> except en passant, in an outer case analysis
> demanding to strip the cons.
>
> This is very troubling actually, because no cofixpoint is even  
> involved here.

I think it's match that's the problem, somehow,
or rather (see Russell's message) that match
can see further than the definitional equality.

[..]

> It seems very natural that "pi (cons xs)"  reduces to "xs", as it  
> is supposed to be its very definition. Then I guess it means that  
> "A convertible to B" should not imply "cons A convertible to cons B".

I'm not sure it's that bad. I'd expect

  A = B <-> cons A = cons B

but that uses of match only compute when they're
blocking the production of a value of positive
type. At least, that's the "match gets lazier"
approach to the problem, which is annoyingly
weak, but correspondingly less frightening than
the "equality tries harder" approach.

> It might make sense in the purely negative view of cons, like if it  
> was a lambda under which no conversion would be allowed. However,  
> proof assistant have made a history of reducing partial terms (same  
> as reducing under lambdas). So, what would make "cons" essentially  
> *more negative* (whatever this means) than lambdas ?

This is a good question. After some sleep, I
can perhaps suggest something. Lambda
abstraction allows you to name and consider
a hypothetical input, cons doesn't allow you
to consider arbitrary positions---it forces
a case analysis. In the functional translation
from Stream to nat -> unit

  ones = cons ones

becomes

  ones 0     = void
  ones (S n) = ones n

and nothing corresponds intensionally to

  fun n => void

Correspondingly, in the world of open terms,
we can perhaps make more "abstract
observations" of functions than we can of
streams.

Thinking about it in this way suggests another
aspect of the problem. The dependent case
analysis principle says something rather
extensional: "every value is given by cons".
As things stand, it is not true that every
closed stream is definitionally equal to a
cons. This now makes me wonder whether making
computation even weaker can really fix the
problem.

Hmmmm

Conor