coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Simplify proofs with nested pattern matching (cases explosion)

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Simplify proofs with nested pattern matching (cases explosion)
Date: Wed, 1 Jul 2020 08:59:33 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f176.google.com
Ironport-phdr: 9a23:0r+gRxZuxPH540zpY/9G3UT/LSx+4OfEezUN459isYplN5qZrsm9bnLW6fgltlLVR4KTs6sC17OI9fi5EjVZvd7B6ClELMUREUddyI0/pE8JOIa9E0r1LfrnPWQRPf9pcxtbxUy9KlVfA83kZlff8TWY5D8WHQjjZ0IufrymUoHdgN6q2O+s5pbdfxtHhCanYbN1MR66sRjdutMZjId/K6s90AfFrmZHd+hL2G9lKk+YkxLg6sut5pJu/DlctvI7+8JcTan2erkzQKBFAjghL207/tDguwPZTQuI6HscU2EWnQRNDgPY8hz0XYr/vzXjuOZl1yaUIcP5TbYvWTS/9KhrUwPniD0GNzEi7m7ajNF7gb9BrxKgoxx/xJPUYJ2QOfFjcK7RYc8WSGxcVctKSSdPHp2zYJcOD+oZPOZXsY/9p0cVrRCjAQWgHf7jxiNUinPz26AxzuYvHhzc3AE4EN0OvnbbotX7OqkRTO670rXHwzrYYvNKwDfw8pTEfgw9rfyOW797bMrfyVMoFwPAllies43lMC2P1uQXrWeQ8vRtVeWyi249twFxoyagxtoxgYTOnoIVy07L9T9jwIkrP9G3VEl7YcO+EJtMtiGVKZZ2T9gtQ2Ftoik6y7kGtYSncygNzZQq3hjSYOGIfIaU+BzsTvqRIStmi3J/frKynwi//VWvx+DzS8S50VlHoyRbn9TQqHwAywDf58aaRvZ+8Ums2jaB2x3T5O1aIU06larWJpohz7MuiJYfr1jOEzPwlU7rgqGWcUAk9fKp6+Therjmp5mcN5V1ig7kKKgulNa/DOIlOQYNR2iW4fqw2KHn8EHjQ7hHjuc6nrTYvZ3bP8gXu6y0Dg5T340+8RiwFS2m384dnXQfLFJKZhaHj4/xNlHLOv/4DPO/j02tkDdv2vzKJ7PhDojPI3XCirvhcrF960lTyAo3099T/Y5bCrYEIP7rW0/xssLXDgMhPgCq3+rqDM9x24AeVG6VH6OUMaLfvUWV6u8tIuSAfIoVtyz8K/gh6f7ul3g5mVoFcKmx3JsYdmq4Hu54LEmDfXXshcoBEX0Wvgo/UuPqlUaPUTFWZ3moXqI84is3B56hDYfGXoytmqCO3D+nHp1KYWBLEkyDEXDxd4mdR/gMbD+SLdR6nzwfVbmhTpch2gu0uA/7zbpnNOvU9TcCuZLtztgmr9HUwDo17HRfC9mXmzWGSHgxlWcVTRc32rp+qApz0AHQ/7J/hqlgFNFJ/f4BeQAnL4LdwvEyX8jzVxjbc5GCT0u8XtSrHBk+S9swx5kFZEMrSIbqtQzKwyf/W+xdrLeMHpFht/uEhyGgdfY48G7P0ewat3djR8JOMWO8gasmrlrcAofIlwOSkKP4LP1Ajh6Iz3+KyC+1hG8dSBR5CPyXUnUWZ0+QptP8tBubEu2eTI8/Ow4E8vasb6tHbtqz0wdDTfbnfdXaOie/wjjuQxmPwbyIYczhfGBPhCg=

Hi,
Can you give a url where we can see the code please?

Best regards,
P.

Le mer. 1 juil. 2020 à 07:26, Blaudeau Clément
<clement.blaudeau AT kes.eleves.polytechnique.fr> a écrit :
>
> Thank you for your answer !
>
> I’ve tried to use Function, but Coq cannot create the inductive predicate
> R_is_valid as soon as I add the non-trivial cases :
>
> is_valid is defined
> is_valid is recursively defined (decreasing on 1st argument)
> Warning: Cannot define graph(s) for is_valid
> [funind-cannot-define-graph,funind]
> Warning: Cannot build inversion information
> [funind-cannot-build-inversion,funind
>
> However, to me, my function looks like a valid pattern matching tree
> without dependent type (the two issues mentioned in the documentation). The
> cases that are not accepted by Coq are of the following form :
>
> | N b1 (((N b2 _ ) as d2)::((N b3 _) as d3)::nil) => (* sequence of boolean
> tests *) && (is_valid d2) && (is_valid d3)
>
> Am I missing something ?
>
> Thank you again,
>
> Best,
>
> Clément
>
> Le 29/06/2020 à 20:29, Julien Forest a écrit :
>
> On Mon, 29 Jun 2020 18:08:34 +0200
> Xavier Leroy <xavier.leroy AT college-de-france.fr> wrote:
>
> On Mon, Jun 29, 2020 at 5:39 PM Gaëtan Gilbert <
> [...]
>
> [...]
>
> That's a very good trick, and it can be automated using Function
> instead of Definition, see ttps://
> coq.inria.fr/distrib/current/refman/language/gallina-extensions.html#coq:cmd.function
>
> Function is_valid b :=
> match b with
> | x00 | xff => true
> | _ => false (* 254 cases hidden in this _ *)
> end.
>
> will generate the inductive predicate R_is_valid and the proofs of
> equivalence with the is_valid function.
>
> Hope this helps,
>
> - Xavier Leroy
>
> Just to illustrate both Gaëtan and Xavier ideas using Function.
>
> Cheers,
>
> Julien Forest
>
> [...]
> [...]
> [...]
> [...]
> [...]
> [...]
> [...]
> [...]
> [...]
> [...]
> [...]
> [...]
> [...]
> [...]
> [...]
> [...]
> [...]
> [...]
> [...]
>
>

Re: [Coq-Club] Simplify proofs with nested pattern matching (cases explosion), Blaudeau Clément, 06/30/2020
- Re: [Coq-Club] Simplify proofs with nested pattern matching (cases explosion), Blaudeau Clément, 07/01/2020
  - Re: [Coq-Club] Simplify proofs with nested pattern matching (cases explosion), Pierre Courtieu, 07/01/2020
  - Re: [Coq-Club] Simplify proofs with nested pattern matching (cases explosion), Yves Bertot, 07/02/2020