The Coq mailing list

[Claude Marche <Claude.Marche AT lri.fr>]

>>>>> "mulhern" == mulhern  
>>>>>Â <mulhern AT gmail.com>
>>>>>  writes:

    mulhern> What I really want to have is two mutually dependent Fixpoint
    mulhern> definitions which decrease in different arguments. If there is a
    mulhern> reason why that is impossible could someone let me know?

I think this question is a good candidate for the FAQ. 

The solution is not to use mutual fixpoints, but to define the second
function as a local function of the first one. Example :




Inductive tree : Set :=  Empty : tree | Node : nat -> forest -> tree
with forest : Set := Nil : forest | Cons : tree -> forest -> forest.

Fixpoint sumtree (t:tree) { struct t }: nat :=
  let sumforest := fix sumforest (f:forest) { struct f } :=
    match f with
    | Nil => 0
    | Cons t f' => sumtree t + sumforest f' 
    end
  in 
  match t with
  | Empty => 0
  | Node n f => n + sumforest f
 end.





-- 
| Claude Marché           | 
mailto:Claude.Marche AT lri.fr
 |
| LRI - Bât. 490          | http://www.lri.fr/~marche/  ;|
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85  |
| F-91405 ORSAY Cedex     | faxto: +33 1 69 15 65 86    |