The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi,

I tried your exemple, but I had to add some context to fil the holes
(variables for insn, insnEq, and so). Using my version of Coq,
everything works fine. (Version 8.3 r 13244)

Could you check your version of Coq and report this version ? BTW, I
assumed that by 'compile' you meant type-check (making the blue line
going on your definition in CoqIDE), if it is not the case please let
me know.

thomas



On Sun, Jul 18, 2010 at 6:57 PM, Jianzhou Zhao 
<jianzhou AT seas.upenn.edu>
 wrote:
>
> 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.