The Coq mailing list

[Jianzhou Zhao <jianzhou AT seas.upenn.edu>]

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