The Coq mailing list

[Wilayat Khan <wilayatk AT gmail.com>]

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