coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Prove the existence of pairwise matched stream

From: Igor Jirkov <igorjirkov AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Prove the existence of pairwise matched stream
Date: Fri, 12 Jul 2019 13:13:31 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=igorjirkov AT gmail.com; spf=Pass smtp.mailfrom=igorjirkov AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f54.google.com
Ironport-phdr: 9a23:n5Xp5Bby+JH/oYn+TwoRAgD/LSx+4OfEezUN459isYplN5qZocW/bnLW6fgltlLVR4KTs6sC17OM9f24Ejdcqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5sIBmsrQjdqsYajIVtJ60s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlSEKPCM7/m7KkMx9lK1UrhKvqRJ83oDafp2aOeFkca/BZ94XX3ZNUtpTWiFHH4iyb5EPD+0EPetArIf9qFwOrQGjDgeoBePv0DxIhnjo3aYn1OkhEA7G3As6H9IMsXTUttb1NKAMUe2uw6nIyC/Mb/JS2Tvn9IfIdRUhrOiKULltcsTR0VEiGx3ZgliUs4DoPDOY2v4Tv2SF8uZsT+KihmEhpgpsuDag3N0shZPMho8NylDL6yF5wIEtKN29UkF7YNqkHIJetiGAKod6W80iTmFntSogxb0Gvpm7fCcOyJs53RLQd/uHc42Q7hLiUuaePyt4iWp7dL6jgxu+60utx+3mWsWqzlpGszBJn9nDu3wV0hzc8MmHSv9z/ke73jaP0hje6uBLIUAzj6rbKZ8hwqQzlpoUr0TOBSD2mEDsg6+XckUo4PSn6+PiYrn+vJ+TK5d0ih3iMqQpgsGwHeM4MhEXU2eH/eS8yabs8FbiQLRKi/02irPWvIrbJcQdvK65AhVa3pwt6xalXH+a14ETmmBCJ1ZYcjqGiZLoMhfAOqPWF/C61nWjly0j5fHcPbr/SsHMIX/Zkrb7frFjw0FZwQs3i9tY4sQHWfk6PPvvVxqp55TjBRgjPlnsmre1OJBGzoobHFm3LOqcOaLWv0WP47t2ceaJbY4R/j36Lqp8vqO8vToCgVYYOJKR894XZXS/RKk0JkyYZT/zmI5EHzpW+AU5S+PuhRuJVjsBPy/uDZJ53SkyDcedNamGXpqk2eXT0yKyH5kQbWdDWAiB

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?

Igor Zhirkov

[Coq-Club] Prove the existence of pairwise matched stream, Igor Jirkov, 07/12/2019
- Re: [Coq-Club] Prove the existence of pairwise matched stream, Jannis Limperg, 07/12/2019
- Re: [Coq-Club] Prove the existence of pairwise matched stream, Xavier Leroy, 07/12/2019
  - Re: [Coq-Club] Prove the existence of pairwise matched stream, Christian Doczkal, 07/13/2019
- Re: [Coq-Club] Prove the existence of pairwise matched stream, Maximilian Wuttke, 07/12/2019