The Coq mailing list

[Xavier Leroy <xavier.leroy AT college-de-france.fr>]

On Mon, Jun 29, 2020 at 5:39 PM Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> wrote:

You may convert is_valid to an inductive type, that way it only has constructors for the cases you want and you can destruct it directly.
see attached file for an example

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

Gaëtan Gilbert

On 29/06/2020 16:46, Blaudeau Clément wrote:
> Hi Everyone,
> I'm currently working to prove results on a fonction that uses several levels of nested pattern matching and it generates *a lot* of trivial subgoals, to the point that every proof takes several minutes to go through.
>
> ##### High level view of the problem
>
> I have an inductive type with ~ 50 constructors, and nested pattern matching on lists of that type. The nested pattern matching is translated into several levels of normal pattern matching with one case that is interesting and 49 useless cases. To build proofs on my function, I would like to be able to extract easily the interesting cases, and quickly drop all useless cases. Is there automated ways of doing that ? Just destruct the match expressions and using `congruence` is too slow.
>
> ##### More details
>
> I have a function  `is_valid : A -> bool`, and I want to prove results of the form `is_valid a = true -> P`, where `A` is an inductive type of the form
> ```Coq
> Inductive A := | N : B -> (list A) -> A . % N is the only constructor
> ```
> And `B` is also an inductive type **with around 50 constructors**.
> The problem is that, in the `is_valid` function, I have nested pattern matching (on the list) like
> ```Coq
> | N b1 (N b2 [])::(N b3 [])::_ => (f b1 b2 b3) % some property computed using b1 b2 b3
> ```
> generates huge patterns, because the internal translation of nested patterns is to create several levels of patterns. As my type `B` has 50 constructors, each level of pattern matching generates **a lot** of subgoals and slows down the proofs.
>
> Is there a simple way to say that if `is_valid a = true` then all the possible cases are only the ones of the main pattern matching, without having to break all sub-levels of matching using `congruence` everywhere ? Just doing an `unfold` of the `is_valid` function takes ~2 min on my computer. The dream would be that `is_valid a = true -> P` could be split into the few subgoals of the form `.. /\ (f b1 b2 b3) -> P /\ ...`
>
> Thank you for your help !
> Clément
>
> PS: I could write a big theorem saying that for any property P, but I'm looking for an automated way of doing it
>