The Coq mailing list

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

Please understand what you are doing: THE 3 TACTICS DO NOT PERFORM THE SAME
NUMBER OF CASE ANALYSIS AT ALL. So you are not measuring the speed of
destruct, you are measuring the level of smartness of the three different
proofs you build. See below an explanation of what each tactic does on the
first example.

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

> 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

This generate ~16000 different subgoals and calls "simpl;auto." on each.
You are building a (stupid) proof with 16000 different cases.

>    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).

This builds a proof with 256 cases only, no surprise that it is performed
faster. More precisely: the first "destruct a,b,c,d,e,f,g,h; simpl; auto"
generate 2^8=256 goals and calls simpl;auto on each, WHICH SOLVES ALL
SUBGOALS. The remaining tactics: "(destruct i,j,k,l,m,n,o,p; simpl; auto);
(destruct p,q,r,s,t; simpl; auto)." IS NEVER EXECUTED because there are no
remaining subgoals.

You can check this:

Variables a b c d e f g h i j k l m n x y:bool.
Require Import List.
Notation "x + y" := (andb x y) (at level 50, left associativity)
:bool_scope.
Notation "x * y" := (orb x y) (at level 40, left associativity) :bool_scope.
Open Scope bool_scope.

Lemma foo1:   a*b*c*d*e*f*g*h*i = a*b*c*d*e*f*g*h*i.
    try(destruct a,b,c,d,e,f,g,h; simpl; auto).
(* No more subgoals *)


>    c)  tactic DestructMatchArg,  respectively.

For this one I need to see your script, but if there is a call to
reflexivity somewhere THEN IT SOLVES THE GOAL IMMEDIATELY and probably
almost no case analysis is perfomed at all.

Pierre