The Coq mailing list

[Anders Lundstedt <anders AT anderslundstedt.se>]

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.