Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • 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? 

BR 
Igor Zhirkov



Archive powered by MHonArc 2.6.18.

Top of Page