The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Wilayat,

 

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

 

Since the number of cases obviously rises exponentially with the number of variables destructed in parallel, it is obvious that the compute time rises exponentially as well. Destructing increasing numbers of variables in Coq is not a really fruitful approach. You should try to take some shortcuts, e.g. see that after destructing 2 variables you see that the others need only be destructed in one case. With 14 variables you end up with 16.384 cases – 14s is not bad for this – less than 1ms per case.

 

What helps me in many cases is a tactic I wrote which destructs the argument of the first match in the goal. This usually helps to destruct only those variables which need to be destructed in order to make progress and keep the number of cases reasonably small.

 

Best regards,

 

Michael

 

P.S.: The tactic I am using looks something like below. It is a bit cut down – my version contains some additional boiler plate code to avoid backwards rewriting with destruct equations.

 

(* In nested matches, get the argument of the inner most match *)

 

Local Ltac GetInnerMatch term :=

  match term with

  | context [match ?inner with _ => _ end] => GetInnerMatch inner

  | _ => term

  end.

 

(**  Destruct the argument of a match in the goal or hypothesis *)

 

Ltac DestructMatchArg :=

  match goal with

  | |- context [match ?term with _ => _ end] =>

    let EQ:=fresh "EQ_DestructMatchArg" in

    let inner:=GetInnerMatch term in

    destruct inner eqn:EQ;

  | H: context [match ?term with _ => _ end] |- _ =>

    let EQ:=fresh "EQ_DestructMatchArgInHyp" in

    let inner:=GetInnerMatch term in

    destruct inner eqn:EQ;

  end.

 

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928