The Coq mailing list

["Arnaud Spiwack" <Arnaud.Spiwack AT lix.polytechnique.fr>]

(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.

By the way, another way of decomposing the problem is (using Nicolas's definitions) :

(********************************************)
Definition pi (xs : Stream) : Stream :=
  match xs with
  | cons ys => ys
  end
.

Eval compute in fun xs => pi (cons xs).
 (* = fun xs : Stream => xs *)

Definition out' xs := cons (pi xs).

Eval compute in fun xs => out' (cons xs).
  (* = fun xs : Stream => cons xs *)

(********************************************)


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".

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 ?

Additionally, I've tried analyzing the problem under the point of view of co-algebra as Anton Setzer advertised at the DTP'08 workshop, and only managed to reproduce the same issue in another tone of speech. From which I conclude that I'm lost.



Arnaud Spiwack