The Coq mailing list

[Xavier Leroy <xavier.leroy AT college-de-france.fr>]

On Fri, Jul 12, 2019 at 1:49 PM Igor Jirkov <igorjirkov AT gmail.com> wrote:

Hello,

I have troubles proving an existence of an infinite stream that is a "transformed" version of an existing one.

However, the stream is not actually transformed by mapping its elements with a computable function ; 

its elements are related by a relation 'R' to the elements of the original stream.

MWE follows:

Parameter T: Type.
Parameter R: T -> T -> Prop.

Hypothesis exists_all :forall a, exists a', R a a'.

CoInductive stream : Type :=
| sintro: forall a: T, stream -> stream.

CoInductive smatch : stream -> stream -> Prop :=
| smatch_intro:
    forall a1 a2 s1' s2',
    R a1 a2 ->
    smatch s1' s2'  ->
    smatch (sintro a1 s1') (sintro a2 s2')
.

Theorem stream_ex:
  forall s, exists s', smatch s s'.
Proof.
Abort.

I can't prove this theorem using 'cofix' (The error message is "All methods must construct elements in coinductive types").

However,I could have proved stream_ex, if I had a computable function that related s and s' 

How are such problems approached? Are there some fundamental restrictions of Coq theory that emerge here? 

I'm pretty sure there is no constructive proof of your theorem.  However, if you strengthen the hypothesis to

Hypothesis exists_all' : forall a, { a' | R a a' }.

you should be able to prove the theorem, taking s' = map (fun a => proj1_sig (exists_all' a)) s.

 

Then, you can use a classical axiom (constructive_indefinite_description in Coq's standard library) to derive exists_all' from exists_all.

Hope this helps,

- Xavier Leroy

BR 

Igor Zhirkov