The Coq mailing list

[Wilayat Khan <wilayatk AT gmail.com>]

Hello Courtieu 

 I just ran destruct on the same functions using both Coq8.8 and Coq8.3 and there wasn't so much difference in time (i did not record the actual numbers, though). Anyway, enclosed are the results of few experiments on Coq8.8 using destruct in three different ways.The three values in row 'Proof time', are for the Coq8.8 it takes to close proof when destruct is used with

 a)  all variables in destruct, such as destruct a, b, c....;simpl;auto

 b)  group of 8 variables, such as

   try (destruct a,b,c,d,e,f,g,h; simpl; auto);

       (destruct i,j,k,l,m,n,o,p; simpl; auto);

       (destruct p,q,r,s,t; simpl; auto). 

 c)  tactic DestructMatchArg,  respectively.   

************Experiments result (time is in seconds)***************

Equation:   a*b*c*d*e*f*g*h*i = a*b*c*d*e*f*g*h*i

Proof time: 0.799   0.637   0.339   

Equation:   a*b*c*d*e*f*g*h*i*j*k*l*m*n = a*b*c*d*e*f*g*h*i*j*k*l*m*n

Proof time: 40.234   0.715   0.361   

Equation:   a*b*c*d*e*f*g*h*i*j*k*l*m*n+x+x*y = a*b*c*d*e*f*g*h*i*j*k*l*m*n+x

Proof time: 658.995   739.105   0.435   

Equation:   x+x*y = x

Proof time: 0.3   0.299   0.291   

Equation:   ¬a*¬b*¬c*¬d*¬e*¬f*¬g*¬h*¬i*¬j*¬k*¬l*¬m*¬n*¬o+¬a*¬b*¬c*¬d*¬e*f*g*h*i*j*¬k*l*¬m*¬n*¬o*¬p+a*b*¬c*¬d*¬e*¬f*g*h*¬i*j*¬k*l*¬m*¬n*¬o*¬p = 

            ¬a*¬b*¬c*¬d*¬e*¬f*¬g*¬h*¬i*¬j*¬k*¬l*¬m*¬n*¬o+¬a*¬b*¬c*¬d*¬e*f*g*h*i*j*¬k*l*¬m*¬n*¬o*¬p+a*b*¬c*¬d*¬e*¬f*g*h*¬i*j*¬k*l*¬m*¬n*¬o*¬p

Proof time: 795.225   1.326   0.407   

Equation:   ¬a*¬b*¬c*¬d*¬e*¬f*¬g*¬h*¬i*¬j*¬k+x+x*y = ¬a*¬b*¬c*¬d*¬e*¬f*¬g*¬h*¬i*¬j*¬k+x

Proof time: 13.853   14.976   0.384   

Equation:   x+y = x+y

Proof time: 0.315   0.308   0.309   

Best, 

Wilayat

On Fri, May 11, 2018 at 11:04 AM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

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
>