The Coq mailing list

[Jean-Francois Dufourd <dufourd AT dpt-info.u-strasbg.fr>]

Hello Hermann,

Yves Bertot knows the solution, but the bug has yet to be corrected in a 
next version of Coq.

Sincerely,

J.-F. Dufourd

Hermann Lehner a écrit :
> Hello all,
>
> Some time ago (Mon, 30 Jul 2007 18:07:18 +0200), J.-F. Dufourd came 
> across the following issue.
>
> ---snip----
>
> Function div(a b:nat){measure (fun m:nat=>m) a}:nat:=
>   if eq_nat_dec b 0 then 0
>   else if (le_lt_dec b a) then (div (a-b) b) + 1 else 0.
> Proof. intros. omega. Defined.
>
> is refused with the message:
>
> "Anomaly: Cannot create equation Lemma. Please report".
>
> ---snip----
>
> Anyone having an answer on that, as I have the same problem with a 
> much larger definition. The little example above still does not work 
> with Coq 8.1pl3.
>
> Does someone know which part of the function definition triggers this 
> anomaly, so that it can be bypassed?
>
> Thanks!
>
> Best regards
>   Hermann Lehner

begin:vcard
fn;quoted-printable:Jean-Fran=C3=A7ois Dufourd
n;quoted-printable:Dufourd;Jean-Fran=C3=A7ois
org:University of Strasbourg;LSIIT - UMR CNRS 7005
title:Professor in Computer Science
tel;work:(+33) 3 90 24 45 55
version:2.1
end:vcard