The Coq mailing list

[Ryan Wisnesky <ryan AT cs.harvard.edu>]

Hello,

InInsns_dec is declared opaque (Qed) - maybe this is stopping reduction 
much earlier than with your other boolean functions?

-Ryan

On 7/18/2010 9:57 AM, 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?
>
> Thanks.