coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Mutual Fixpoints into mutual inductive types

From: Merlin Göttlinger <megoettlinger AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Mutual Fixpoints into mutual inductive types
Date: Fri, 05 Jan 2018 18:55:04 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=megoettlinger AT gmail.com; spf=Pass smtp.mailfrom=megoettlinger AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f53.google.com
Ironport-phdr: 9a23:QNzI1RE0qhAWxWiQvXCaUp1GYnF86YWxBRYc798ds5kLTJ7zp82wAkXT6L1XgUPTWs2DsrQY07OQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmCexbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KODE38G7VisJ+gqFVrg+/qRNj2IPbep2ZOeBkc6/BYd8XR2xMVdtRWSxbBYO8apMCAe0fMuZCq4n9pl0OogO/CxGqGOPv1jtIhn7w3a01zeshCxzN0QslH90Qv3TUq8v6NLsOUeCxzanIyzrDYO1M2Trm54jIdwouofCIXb5qbcXRzkwvGhrDg16Np4LlODaV2f4Ms2id9+dgV+WvhHQ7pAFxozivw94ghZLTho0Ly1DE6SN5z5gvJdGiVUF0f8aoEJRRtyGGN4t2X9gtT3t0tyY9z70Lv4OwcisSyJk/2RLTd/iKf5KL7x/jTuqdPyp0iX1/dL+/iRu/91WrxPfmWcmuyllKqzJIktnSuXAJ0Bze8s2HReF8/kelwDqP1hzT5v1dLUA6lafWJYQtwrE3lpoUvkTDGjH5lF/qg6+Rc0Uo4umo6+L5bbX6vpKQKZN4hwXkPqktmsGzG/o0PhUBUmSB+emx2qXv/UjjT7VLiv02nLPZsJffJckDo662HQBV0oE95BajEzem1NUYnX8ILF1bYhKKlIfpO1TUL/D5CfezmUijkDBux/zeJL3uHo3NLmTfkLfmZbty90lcyBMqwd9D45JUF6oOLenoWk7xsdzYFgU2Pxa1w+bhEtV915kRVXiBAq+DY+vutgqD4ftqKO2RbqcUviz8Ir4r/a3Al3g8zHoQZ62o26w49mykGvVgLEiDKS7pj9gGHHsWugs4Q+HwoFKHWD9XIX21WvRvtXkAFIu6ANKbFciWi7ub0XLjEw==

Hi,

that sounds promising. I would be interrested to hear how this trick works because it certainly isn't obvious to me from looking a tthe code.

So if you find the time later on to explain this I would be greatfull, but in any case thank you both for your help.

Cheers,

Merlin

Joachim Breitner <mail AT joachim-breitner.de> schrieb am Fr., 5. Jan. 2018 um 19:14 Uhr:

Hi,

Am Freitag, den 05.01.2018, 11:54 +0000 schrieb Merlin Göttlinger:
> VectorUtils.traverse depends on a bunch of stuff I implemented and is
> the usual operation known from e.g. Haskell with signature G A -> (A
> -> F B) -> F (G B) where G is (fun T => Vector.t T n) and F is list
> in my case.

Coq’s termination checker cannot look through type class instances.

There is a trick, however, if you get to choose the type class. See
https://github.com/antalsz/hs-to-coq/blob/master/base/GHC/Base.v#L41-L54
and let me know if you want more explanation (I am on the run right
now).

Joachim

--
Joachim Breitner
mail AT joachim-breitner.de
http://www.joachim-breitner.de/

[Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/05/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Pierre Courtieu, 01/05/2018
  - Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/05/2018
    - Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Pierre Courtieu, 01/05/2018
    - Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Joachim Breitner, 01/05/2018
      - Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/05/2018
        
        Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Joachim Breitner, 01/05/2018
        
        Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/07/2018
        
        Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Joachim Breitner, 01/07/2018
        Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/08/2018
        Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Joachim Breitner, 01/08/2018
        Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/08/2018
        Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Joachim Breitner, 01/08/2018
        Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/08/2018
        Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Joachim Breitner, 01/08/2018