The Coq mailing list

[julien.forest AT ensiie.fr]

Hi,

Short answer : the problem comes from the use of -> construction.
Long answer : Can you please fill a bug report at
https://coq.inria.fr/bugs/ so that I can treat the problem as soon as I
come back. I won't be at work next week.

Best regard,

Julien

On Fri, 21 Feb 2014 20:38:57 +0100
Anders Lundstedt 
<anders AT anderslundstedt.se>
 wrote:

> I need to define a recursive function that is not structurally
> recursive. With the Function command I get:
>
> "failure in proveterminate
>
> Error: Found a product. Can not treat such a term"
>
> A somewhat minimal example (pastebin: http://pastebin.com/MYdaRG9x):
>
>
> Require Import Recdef.
>
> Inductive formula :=
> | atom  : formula
> | conn  : formula -> formula -> formula.
>
> Fixpoint complexity P : nat := match P with
> | atom     => 0
> | conn P Q => Peano.max (complexity P) (complexity Q) + 1
> end.
>
> (* the following definition is OK: *)
> Function truth P {measure complexity P} : Prop := match P with
> | atom     => True
> | conn P Q => truth P /\ truth Q
> end.
> Admitted.
>
> (* the following definition gives the following output:
>
> failure in proveterminate
>
> Error: Found a product. Can not treat such a term
> *)
> Function truth' P {measure complexity P} : Prop := match P with
> | atom     => True
> | conn P Q => truth' P -> truth' Q
> end.