The Coq mailing list

[Nicolas Oury <Nicolas.Oury AT laposte.net>]

Greetings,


Le 6 juin 08 à 19:29, Arnaud Spiwack a écrit :
> 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.


I am not sure of that. Actually, we looked to this with Nils Anders  
Danielsson on Friday and it seems impossible to prove forall xs, out  
xs = xs with Anton Setzer notation.
Only forall xs, bisim (out xs) xs sems to be provable. But, maybe, I  
am wrong.

It seems to me that the main problem with coinductive in Coq currently  
is the fact that dependent case analysis is possible on coinductive  
values.
This dependent case analysis implies this elimination principle:
el :
 forall P : Stream -> Type, (forall xs, P (cons xs)) -> forall ys, P  
ys.

This states that every  Stream is a cons of a Stream. This is  
perfectly sensible from the observational point of view:
We know that every stream behaves exactly like a cons and, at runtime,  
we know that a Stream will be a cons and that, if we run the program,  
our screen will be
full of 'cons'es...
Anyway, this eliminator is a lie at compile time (or during type  
checking) as any closed value is not always convertible to a cons of a  
Stream.
For example, ones is not convertible to a cons: this explains why ones  
= 1 : ones is not provable by reflexivity.

The problem is that dependent case analysis on coinudctive values is a  
lie during type checking, even if the principle is perfectly  
consistent with the observational behavior of the Stream.

I can see two ways out, there are probably many better:

1. Remove the lie. We can try to remove dependent pattern matching.
What can we use to replace it?

Let's denote ~ the bisimulation of Streams defined by ~-cons : forall  
xs, ys, tail xs ~ tail ys -> xs ~ ys

I think it is possible to prove forall xs, xs ~ cons (tail xs) without  
dependent case analysis.
The idea would be to apply ~-cons and allow the non-dependent case  
analysis to reduce in the goal.
Then a proof of (tail xs) ~ (tail xs) is easy to build.
(I am afraid I have no working version of Coq on my laptop and cannot  
typecheck what I am writing before tomorrow.)

With a proof of forall xs ~ cons (tail xs), we have two possibilities:
a. Prove that P respects ~ and work modulo ~. This should be possible  
often as ~ represents being the same at runtime.
b. Admit an extensionnality axiom : forall xs, ys ->  xs ~ ys -> xs =  
ys. With this axiom, it is possible to prove the dependent elimination  
principle.
  Anyway, now, 1 : ones = ones will not compute to refl_equal but to  
a proof using this axiom. This proof would still be valid.

A variation of the last possibility is to admit directly the dependent  
elimination principle, as an axiom, without any computation rule.

I wonder if this would break a lot of contributions. Does anyone know?

2. Make the lie true.
This means tweaking the conversion rule so that  v and  cons (tail v)  
are convertible for any non neutral v.
(I think haveing this only for values is not sufficient:
Coninductive pack (v:Stream) =   cons v.
out (pack v) = cons v
and pack v = cons v is not provable by refl.)

I think it is a difficult thing to do.
The idea would be:
- to compare intentionaly two cofixpoints
- to unfold a cofixpoint when it s compared to a non cofixpoint.

For this to terminate, we have to restrict unfolding only on one side.  
If there is already an unfolding on one side of the equality test,  
then never unfold on
the other side.

The problem with this test is that it is not transitive:
ones = cons  ones
ones' = cons ones

Then by transitivity ones should be convertible with ones'. This is  
not the case. And we have the initial problem again.
If you're not convince by the ones' example, thinking a useless  
cofixpoint should be reduced to its content, you can think of:

n_cons 0 xs       = xs
n_cons (S n) xs = cons (n_cons n xs)

CoInductive loop i = cons (n_cons i (loop 0))

then loop 0 == cons (cons (loop 0)) and loop 1 == cons (cons (loop 0))
but it is going to be difficult to find any good reason to unfold loop  
when testing loop 0 == loop 1.

One way to solve the problem would be to use Hash Consing during  
equality test. I think it might be too complicated for a kernel.

All the best,

Nicolas.