The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Don’t miss the point here: there are much less case analysis done with Michael’s solution than with yours.

P

Le ven. 11 mai 2018 à 05:55, Wilayat Khan <wilayatk AT gmail.com> a écrit :

Hello  Maxime

 I performed the same testing on Coq 8.8 and the numbers are almost the same. The time of case analysis using destruct, though, reduces dramatically with

Michael Soegtrop's tactic DestructMatchArg.

Best, 

Wilayat

On Tue, May 8, 2018 at 11:48 AM, Maxime Dénès <mail AT maximedenes.fr> wrote:

Hello,

Could you try the same experiments with Coq 8.8? 8.3 is fairly old and
Coq's performance has improved in many areas since then.

If the numbers are still not good, I suggest you open an issue at
https://github.com/coq/coq/issues

Thank you!

Maxime.

On 05/08/2018 06:30 AM, Wilayat Khan wrote:
> Hello
>
>   Am using tactic *destruct* over inductive variables of type bool with
> just two constructors. I observed, it takes too long (over 14 seconds)
> for the destruct to return when used for 14 variables at a time (e.g.,
> destruct a, b, c, d, e, f, g, h, i, j, k, l , m, n; simpl;auto) or used
> for individual variable, combined with ; (e.g., destruct a; destruct b;
> destruct c;...;simpl;auto). The time of execution increases with
> variables and terms.  Coq's performance is best at using destruct over 8
> variables at  a time. I am using Coq 8.3 on my 64bit Intel Core i5, 8GB
> RAM with 2.6GHz machine 
>
> I am wondering, if there is any systemic study/analysis assessing the
> performance of Coq over *destruct* tactic (in particular case analysis
> on inductive type bool) and comparing Coq (or interactive theorem
> provers in general) with automatic solvers.  
>
> Best, 
>
> Wilayat
>