Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Recursive Notation in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Recursive Notation in Coq


Chronological Thread 
    < Chronological >      < Thread >
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Recursive Notation in Coq
  • Date: Tue, 28 Jul 2020 08:44:54 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
  • Ironport-phdr: 9a23:Gaa3BBbegsoN8rjkT3XkPHv/LSx+4OfEezUN459isYplN5qZrsu+bnLW6fgltlLVR4KTs6sC17OI9f66EjFaqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5zIRmsrAjdqMYajIt8Jq0s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlTwKPCAl/m7JlsNwjbpboBO/qBx5347Ue5yeOP5ncq/AYd8WWW9NU8BMXCJDH4y8dZMCAfcfM+ZWr4fzpFUAohWxCgauGOzi0SVHimPs0KAgz+gsHwPL0Qo9FNwOqnTUq9D1Ob8OXO+o1qbIyCjIYu1W2Tf56YjIagouofWWUrltdsfe01QgGBnAjlqMsoHqIyiV2f4Ms2if9eZgUOOvi3I9pw5vvzev294hh4/UjY0a1l7K7z92wJopJdKmUk57Z8apHZlTuiyEKYd7Xt0uTWF0tSs51LALuJC1cSoUxZk6yBDRa/6KfoeV7h/jW+ufITh1iXZ4db6hhhu/80eux+3zW8SyzV1ErTJFn8HRunwT1BHf8MaKRudn8ku/wzqDyR3f5v1cLUwqiabWK4QtzqAsmpYOq0jPAyv7lF/4gaOIcEgv5/Km5P79Yrr8o5+RL490hR/6MqQpgsG/Bvk4MhQBX2ic+OS80rLj8VTiQLVWlPI2jrPWvIrGKsQAvKG5AgtV3pwm6xa+EzeqysoXkmQaLF5deRKHiZbmO03WLfzlE/uygE6gnTl3y/zcILHtGIvBImXfnLv5eLZy8U9cyA49zdBF4JJUD6kML+juVUDrsdzXEgQ0PBCvw+n9CdV90pkSWWeOAq+FKq/dr0KH5v83L+mWeIAVoCr9K+Qi5/P2kXA5nkYdcbC10psTdXC3Be9rI16ZYHrpmtcOC30Gvgs4TOzwiV2NSyRfZ3ioX6gk/DE0FJqmDZvfRoCqmLGB2D20HodKaWBGFF+NEWzldoSFW/cJcy2SONVuniYFVbinUY8h1AuhuBX0y7p9faLo/Xg0spfi0tls+uCbsRgo/jx5HoGi3meBS2BykStcSzgz3aZ+uFFwjFOKy6N4ju0dCtFV6/dIVAgSMZnGzuU8BcqkCSzbedLcYVqvR52NATUwVts1ypdaakp0Ht6KhQvK3i7sBr4J0bGHGcpnoernw3HtKpMlmD793647ggxjG5MXbDD0tutE7wHWQrXxvQCZmqKtLvxO2zPR+2CCy2XLp11RTAc2Wr7MXHRZY0rK69n1+xGaFu78OfEcKgJEjPW6BO5PY9ztg09BQa6+at/FamO13WKxGVCFyq7eNdO2KVVY5z3UDQ0/qy5W5WyPbFVsDTyoomaYCT1yU1/jfhG0/A==
My guess is that (1) you may need to add some kind of brackets around the notation, and (2) you may need to build a Gallina list of the different elements and then apply a Gallina function that checks relatedness of adjacent elements.  There is indeed a built-in notation facility for variable-length forms, but I don't think it allows constructing subterms out of adjacent parts of the original argument list, and it doesn't allow referencing the same notation recursively in the expansion.

On 7/28/20 8:39 AM, Dominique Larchey-Wendling wrote:
Dear all,

If a notations wizard could help me at defining
the following recursive notation in Coq, I would
be very grateful.

x ⪯ y ⪯ .. ⪯ z := red x y /\ y ⪯ .. ⪯ z

where red : _ -> _ -> Prop

ie

a ⪯ b ⪯ c ⪯ d would be (red a b) /\ (red b c /\ red c d).

Sequences must have length >=2 (otherwise they would be meaningless)

Thank you very much for some insights,

Dominique



Archive powered by MHonArc 2.6.19+.

Top of Page