The Coq mailing list

[Pablo Argon <pargon AT cadence.com>]

Hello all,
        I have two questions about recursive definitions:

A) First I want to define a mutual dependent recursive definition.

In ML I write;

let rec sum f n = 
  if n=0 
  then (f 0)
  else (sum f (n-1)) + (f n)
and
  kmcm n =
  if n=0
  then 1
  else (sum kmcm (n-1))
;;

So, in Coq I coded it:

Fixpoint Sum [ n: nat] : nat :=
 Cases n of
 O => (KMCM O)
|(S m)=>(plus  (KMCM n) (Sum m))
end 
with
        KMCM [n:nat] : nat :=
Cases n of
     O => (S O)
|(S m) => (Sum m )
end.

This definition produces an error that I don't understand,
Error: Recursive call applied to an illegal term
 The 1-th recursive definition KMCM :=
 [n:nat]Cases n of
          O => (KMCM O)
        | (S m) => (plus (KMCM n) (Sum m))
        end is not well-formed


B) Using Refine, I made the following function definition;
(here is the whole executable code)

(*----------------------------------------------*)
Require Lt.
Require ProgBool.
Require Refine.

Variable dummy : bool.
Variable h : nat -> (nat -> bool) -> (nat -> bool).


Theorem foo : (n:nat)(Acc nat lt n)-> (nat -> bool).
Fix 2.
Intro n.
Intro H.
Refine (h n
         [j:nat]
          Cases (lt_ge_dec j n) of
            (left eqxy) => (foo j ? j)
          | (right diseq) => dummy
          end).
Inversion H.
Apply H0.
Assumption.
Qed.

(*----------------------------------------------*)

It seems to me that the proof is sound, but for some reason it
doesn't save... I guess a Transparent/Opaque problem but I can't
fix it.

Thank you all by advance, Pablo