coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proving decidable equality of a huge but simple inductive

From: Alan Schmitt <alan.schmitt AT polytechnique.org>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] proving decidable equality of a huge but simple inductive
Date: Thu, 18 Jun 2020 09:56:40 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=Pass smtp.pra=alan.schmitt AT polytechnique.org; spf=Pass smtp.mailfrom=SRS0=hNS1=77=polytechnique.org=alan.schmitt AT bounces.m4x.org; spf=Pass smtp.helo=postmaster AT mx1.polytechnique.org
Ironport-phdr: 9a23:9TbFYB3VEJfRfTMGsmDT+DRfVm0co7zxezQtwd8ZseMVI/ad9pjvdHbS+e9qxAeQG9mCtrQd1LGd6vm7EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe9bL9oMRm7rwvcusYLjYd/JKs61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzoBOjUk8m/Yl9Zwgbpbrhy/uhJwwYDUbo+WOvVxYqzQZtwaSXZbU8tLSyBNHp+wYo0SBOQBJ+ZYqIz9qkMSoBu6HwasAv7kxCJUiX/22K060vghER3b1wEnBd0OtG7brNPvOKcJTe+1zKzIzTTfb/NKwjr98I/IchQhoPGQQ71/bcrRyU8uFwPck1Wft5bpPzSP1uQCqmWW6fdrWu2zhWA9sQ5xviSvydk2ionPno8YyUzI+DlnzIg1O9G1TE12b9CkHpZRtiyXNot4T8c+T2xouys3yL4LtJq4cSUUyJoqxAPSZ+KEfoWK7R/uSuWcLDFlj3xmYLKynwu+/Vakx+HmS8W4zFlHojBLn9XQrHwA2RPe5tCFR/Z+5EutxzmC2x7J5u1ZLk04j7fXJpE9zrM2i5Edq17MHjXsl0XzlKKWdlsr+uyv6+n/Z7XnqYKQO5VsigH5NqQvmtC/DvokPQgOWWib+P281KD98kHjR7VKlPI2nrHYsJDcO8sbura0DxJL3osn8RqzEiuq3dsCkXQJMF5JYhyKgofxN1HLOv/4DPO/g1q2kDdswvDLJqDvDInQIHTfiLrhfa5z5VNBxAcrz91S5YpZCqkGIPL3Wk7xqMLXAQM5MwyywubnEch92Z0EVWKIGK+ZP7vfvkWM5u01JemAfpQVtyr9K/gg5v7ukWM5lEQGcqmuwJsXbmy3Eep9I0mDZHrhjdgAHX0NvgokQ+zmkEeCXiJLZ3auQ6I84Sk2B56hDYfaX4yinLiB3DqgEZBNfWBHClWMEW/yeImeWvcMbjiSIs57nTAeW7ihUdxp6Rb7vwjjjrFjM+CcriYfrNfo0MV/z+zVjxA7szJuWZezyWaIGkhwl2VAfDQ22aFjvQQpw1OK1+5jiPxdFMBPz+tOVhYmOJXcye1jFt20XRjOKITaAG26S8mrVGliBuk6xMUDNh4kR4eSyyvb1i/vOIc70qSRDcVloLrb22ntKs19zXffyaRniEMpEJIWaD+Ww5Vn/g2WPLbn1kWUk6HwLvYZzHeL7GCH3HaDt0FeURdtXOPCR39NPxKH/+S83VvLSvqVMZpiNwJAzcCYLa4TNY/jikhAT/r4ftGCcyS2gWjiXBs=

Thank you for all the replies, I learned a lot looking at the different
solutions. A form of reflection seems to be the most efficient way to
tackle the issue.

Regarding the huge inductive itself, it's automatically generated from a
description that is big itself. I'm going to see how we can factorize
things, but I'm not very confident we can do something generic about it.
Samuel's approach based on the spec types might be something we could do
automatically (but it's slower than Jason's suggestion).

Thanks again!

Best,

Alan

Attachment: signature.asc
Description: PGP signature

Re: [Coq-Club] proving decidable equality of a huge but simple inductive, (continued)
- Re: [Coq-Club] proving decidable equality of a huge but simple inductive, Benoît Montagu, 06/17/2020
  - Re: [Coq-Club] proving decidable equality of a huge but simple inductive, magaud, 06/17/2020
- Re: [Coq-Club] proving decidable equality of a huge but simple inductive, jonikelee AT gmail.com, 06/17/2020
- Re: [Coq-Club] proving decidable equality of a huge but simple inductive, Samuel Gruetter, 06/17/2020
  - Re: [Coq-Club] proving decidable equality of a huge but simple inductive, Jim Fehrle, 06/17/2020
- Re: [Coq-Club] proving decidable equality of a huge but simple inductive, Frédéric Besson, 06/17/2020
- Re: [Coq-Club] proving decidable equality of a huge but simple inductive, Raphaël Cauderlier, 06/17/2020
  - Re: [Coq-Club] proving decidable equality of a huge but simple inductive, Dominique Larchey-Wendling, 06/17/2020
- Re: [Coq-Club] proving decidable equality of a huge but simple inductive, Jason Gross, 06/17/2020
  - Re: [Coq-Club] proving decidable equality of a huge but simple inductive, Alan Schmitt, 06/18/2020
    - Re: [Coq-Club] proving decidable equality of a huge but simple inductive, Jean-Francois Monin, 06/18/2020