Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] is matching bool slower than sum?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] is matching bool slower than sum?


chronological Thread 
  • From: Bruno Barras <bruno.barras AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] is matching bool slower than sum?
  • Date: Tue, 20 Jul 2010 13:42:35 +0200

On 07/18/2010 06:57 PM, Jianzhou Zhao wrote:
Hi,

For some reason I have a definition 'insnEq' that compares two 'insn's
and returns bool. The 'insn' defines instructions in a language.  What
'insnEq' does is just matching the two instructions and checking if
their sub-components are equal with corresponding 'comparison'
functions (which are defined in the similar fashion). Then I defined
others 'Fixpoint's :

Fixpoint InInsns (i:insn) (li:list insn) {struct li} : bool :=
match li with
| nil =>  false
| i' :: li' =>  insnEq i i' || InInsns i li'
end.

Definition block := list insn.

Fixpoint foo(i:insn) (lb:list block) {struct lb} : option block :=
match lb with
| nil =>  None
| b::lb' =>
   match (InInsns i b) with
   | true =>  Some b
   | false =>  foo i lb'
   end
end.

The compilation of foo is very slow, it takes around 2-3 mins. But, if
I proved this decidability lemma first,

Lemma InInsns_dec : forall i b,
   {InInsns i b = true} + {InInsns  i b = false}.
Proof.
   intros. destruct (InInsns i b); auto.
Qed.

and then let foo match InInsns_dec,

Fixpoint foo2(i:insn) (lb:list block)) {struct lb} : option block :=
match lb with
| nil =>  None
| b::lb' =>
   match (InInsns_dec i b) with
   | left =>  Some b
   | right =>  foo2 i lb'
   end
end.

Coq compiles this foo2 immediately. Why is the first 'foo' slow?

Hello,

As suggested by Ryan, InInsns is transparent while InInsns_dec is opaque, and this is the problem. You probably wonder why does Coq need to unfold InInsns ? The reason is: to check the termination of your fixpoint. When a match appears inside a fixpoint Coq tries to determine if the eliminated object is a subterm of the recursive argument in order to propagate size information on the pattern variables... which is stupid here since you do a match on a boolean so there is no pattern variables.

This source of inefficiency has been spotted recently, so your v8.2 has the problem. It has been fixed since revision 13022 of the svn repository of Coq. Either you try to compile from the sources, or you wait until v8.3 is released (which should be soon).

Regards,

Bruno Barras.



Archive powered by MhonArc 2.6.16.

Top of Page