The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon mulhern 
<mulhern AT gmail.com>:

Hi,

 Let's symplify your example a little :

  Inductive ab : Set := z : ab | a : ab -> ab | b : ab -> ab.


Fixpoint f0 (x:ab) : ab :=
match x with z => z
            |a x  => f0 x
            | b x => f0 x
end.

Fixpoint g0 (x : ab) : ab :=
match x with z => z
            | b x => g0 x
            | y => f0 y

 end.




Fixpoint g1 (x : ab) : ab :=
match x with z => z
            | b x => g1 x
            | y => f1 y
 end
with  f1 (x:ab) : ab :=
match x with z => z
            |a x  => f1 x
            | b x => f1 x
end.


(*

EError:
Recursive definition of g1 is ill-formed.
In environment
g1 : ab -> ab
f1 : ab -> ab
x : ab
a : ab
Recursive call to f1 has principal argument equal to
"x"
instead of a
*)


In the first( non-mutually recursive) definition,
f0 is clearly well formed. Then we use f0 to define g0. OK.

In the second definition, the recursive call of f1 from g1 is
not associed with any decrease in the argument.

The syntactic procedure used to check well-formedness of recursive
definition may fail.
Perhaps a more complex test would give a postive result (at which cost?).
In the example you gave, you haven't truely mutually recursive functions,
the it's best to define them one after one.
In more complex examples, it can be necesary to give arguments for
showing that your recursion is well founded.

Pierre









> 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
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>


-- 
Pierre Casteran
(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.