The Coq mailing list

[mulhern <mulhern AT gmail.com>]

Hi!

Suppose I have the following two Fixpoint definitions:

Fixpoint lookup_sub (tcs_var:tcs) (name:String.string) {struct
tcs_var} : Sool.ty := match tcs_var with
          List.nil => Sool.TyId(name)
        | List.cons (Sool.IdType(name'),(ty, ct)) tl =>
                if (String.equals name name')
                        then match ct with
                                  Constraint.Equality => ty
                                | Constraint.SubtypeBound => Sool.TyId(name)
                        end
                        else lookup_sub tl name
end.

Fixpoint lookup (tcs_var:tcs) (ty:Sool.ty) {struct ty} : Sool.ty :=
match ty with
    Sool.TyConstant _ => ty
  | Sool.TyId name => lookup_sub tcs_var name
  | Sool.TyReference ty => Sool.TyReference (lookup tcs_var ty)
end.

In that case, Coq considers them well formed. However, suppose I
change them to two mutually recursive Fixpoints by introducing a with,
thus:

Fixpoint lookup_sub (tcs_var:tcs) (name:String.string) {struct
tcs_var} : Sool.ty := match tcs_var with
          List.nil => Sool.TyId(name)
        | List.cons (Sool.IdType(name'),(ty, ct)) tl =>
                if (String.equals name name')
                        then match ct with
                                  Constraint.Equality => ty
                                | Constraint.SubtypeBound => Sool.TyId(name)
                        end
                        else lookup_sub tl name
end
with
 lookup (tcs_var:tcs) (ty:Sool.ty) {struct ty} : Sool.ty := match ty with
    Sool.TyConstant _ => ty
  | Sool.TyId name => lookup_sub tcs_var name
  | Sool.TyReference ty => Sool.TyReference (lookup tcs_var ty)
end.

Then Coq gives me the following error message.

Error while reading /Users/mulhern/mulhern/cs/translator/coq/load.v :
File "/Users/mulhern/mulhern/cs/translator/coq/sooltypechecker/tcs.v",
line 9, characters 0-601
Error:
Recursive definition of lookup is ill-formed.
In environment
lookup_sub : tcs -> String.string -> Sool.ty
lookup : tcs -> Sool.ty -> Sool.ty
tcs_var : tcs
ty : Sool.ty
name : String.string
Recursive call to lookup_sub has principal argument equal to
"tcs_var"
instead of a subterm of ty

Could someone tell me why, in the one case, I don't receive any error
and in the other case I do?

In the example you see, lookup_sub doesn't have a call to lookup. I've
omitted the call I want to have to make my example clearer.

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

Thanks,

-mulhern