The Coq mailing list

[Hermann Lehner <hermann.lehner AT inf.ethz.ch>]

Dear Club,

I'm trying to define a mutual recursion between a 'Fixpoint' and a  
well-founded 'Function'. As I don't see how this is done by defining  
them at the same time by using 'with', i tried to pass the Fixpoint to  
the Function as argument it.

After some simplification, and exchanging the Function by another  
Fixpoint (It triggers the same message), I get an error that I simply  
don't understand in the following (ok, stupid) definition:

------

Inductive Data : Type :=
  | D1 (d : Data)
  | D2 (d : Data).

(* No real fixpoint, just to show the problem *)
Fixpoint Fix1 (f : Data -> Data) (d : Data) {struct d} : Data :=
  match d with
  | D1 d' => f d'
  | D2 d' => d'
  end.

(* The same as above, this time using 'Definition' *)
Definition Dev1 (f : Data -> Data) (d : Data) : Data :=
  match d with
  | D1 d' => f d'
  | D2 d' => d'
  end.

(* This works fine *)
Fixpoint FixOK (d : Data) : Data :=
  match d with
  | D1 d' => Dev1 FixOK d'
  | D2 d' => Dev1 FixOK d'
  end.

(* This fails *)
Fixpoint FixFAIL (d : Data) : Data :=
  match d with
  | D1 d' => Fix1 FixFAIL d'
  | D2 d' => Fix1 FixFAIL d'
  end.

------

The last Fixpoint declaration fails with:
Error:
Recursive definition of FixFAIL is ill-formed.
In environment
FixFAIL : Data -> Data
d : Data
d' : Data
Recursive call to FixFAIL has not enough arguments.
Recursive definition is:
"fun d : Data =>
 match d with
 | D1 d' => Fix1 FixFAIL d'
 | D2 d' => Fix1 FixFAIL d'
 end".



So it seems to work when using 'Definitions', but not with 'Fixpoint'  
and also not with 'Function' ... any clue why?

I guess it's related to http://www.nabble.com/Program-Fixpoint's-binding-behavior-td17478094.html 
 , but I can't see a solution for this. I'm working with the SVN  
Version of Coq.

Thanks!

Best Regards
 Hermann

--
http://www.hermann-lehner.com