coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problems with dependently typed function

From: Stefan Monnier <monnier AT iro.umontreal.ca>
To: Jean-Francois Monin <jean-francois.monin AT univ-grenoble-alpes.fr>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Problems with dependently typed function
Date: Fri, 22 Mar 2019 08:16:34 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=monnier AT iro.umontreal.ca; spf=Pass smtp.mailfrom=monnier AT iro.umontreal.ca; spf=None smtp.helo=postmaster AT mail01.iro.umontreal.ca
Ironport-phdr: 9a23:j8nrNB11A8LvSNHasmDT+DRfVm0co7zxezQtwd8ZseMWKvad9pjvdHbS+e9qxAeQG9mCs7Qb0qGN7ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVmDaxe7F/IAi5oQjftsQdnJdvJLs2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3UbJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5LpwRRT2lCkIKSI28GDPisxxkq1bpg6hpwdiyILQeY2ZKeZycr/Ycd4cWGFPXNteVzZZD428cYUBEukPPehWoYb/qVQBogexCBKwBO/z0DJEmmP60Lcm3+knDArI3BYgH9ULsHnMsdv1KLkdUe6vw6nO0D7NaPRW2TH76IjJbB8hu+yHULV1ccrWz0kvEQLFgUuKqYH+PjOVzOMNv3KG7+plUuKvjXInqxtvrTe1wscgkJXGiZgMx13C6C53zoE1JdiiR056Z96pCIZQtyebN4toW88iW3tnuDw7yr0dpJK2cjIGyJo9xxPZdveJcJCI7wr+WOufPzt0nmxpdK6wihqo70StyvfwWteo3FpXtiZIkNnBumoQ2xDO7sWLUOVx80i/1TqVyQze6v9ILEYpnqTBMZEh2KQ/lp8LvETDACD2nEL2gbeTdko+++io7/jrbqj8qp+dLY90jRvyMrkrmsy4B+Q4LhIOUHaB9uS4zrHs4Vf2TK1Ljv0wjKbZrIjXKdkVq6KnGQNZzJov5hmlAzu40NkUh2cLIE5YdB6fiojmIVDOIPT2DfelhFSslS9mx/XBPr3nBJXNL2bMkK36cLZ88U5czxA/zc1a55JTDLEBPOjzVVHru9zcFBM2Lxa7z/79CNphzoMeRX6PAqiBPazOtl+I//sjLPWIZI8IoznwMOMl5v7rjX8hg1ARZ6ip3Z0NaHC5BPtqOUuZYWC/yusGREUHtwx7YvbjjlaFUCUbQnG0XqR0sjM2AYTjA53KQIuqgafH2SC9H5t+e2ZHFBWDC3rucI+AVrIFbDqfOYlviGpXe6KmTtoayRygvQmy7r1hKOvZ4GVMsJXl0tl4/cXSjxZ06DlzCdiH3miJCWp9yDBbDwQq1bxy9BQugmyI1rJ11rkBTYQKtqF5FzwiPJuZ9NRUTtX7WwbPZNCMEQb0Q8+hRyw0SdQt2dIHZwB2Eof710yR72+RG7YQ0oezKtks6KuFjyrwPcE71nPB0rU7glAiBMBGZzX/2/xPsjPLDouMqH230qancaNGgXzI/WaHlTPIvVtfFhN1VqPZR30WYg3dpIah6w==

> More or less folklore in proof theory, usually presented
> in sequent calculus.
> But not that easy to find references on the web.
> Here is one, an expert could provide better answers.
> https://lipn.univ-paris13.fr/~mazza/teaching/ProofTheoryNotes-M1.pdf

Adam Chlipala calls it the "convoy pattern" in his book,

Stefan

[Coq-Club] Problems with dependently typed function, Christian Kjær Larsen, 03/22/2019
- Re: [Coq-Club] Problems with dependently typed function, Gaëtan Gilbert, 03/22/2019
  - Re: [Coq-Club] Problems with dependently typed function, Beta Ziliani, 03/22/2019
    - Re: [Coq-Club] Problems with dependently typed function, Jean-Francois Monin, 03/22/2019
      - Re: [Coq-Club] Problems with dependently typed function, Stefan Monnier, 03/22/2019
- Re: [Coq-Club] Problems with dependently typed function, Sylvain Boulmé, 03/22/2019