The Coq mailing list

[Elias Castegren <elias.castegren AT it.uu.se>]

Hi all

I ran into an issue I don’t understand yesterday, minimised below:

I have a datatype where one constructor holds a list of recursive values:


Inductive foo :=
| Foo : foo
| Bar : list foo -> foo.


Sometimes I want to apply operations to values of this type, and then I
can use Coq’s standard map function to handle the Bar constructor:


Fixpoint op1 (x: foo) :=
  match x with
  | Foo => Foo
  | Bar l => Bar (List.map op1 l)
  end.
(* Compiles OK! *)


However, I am really using the TLC library and if I use the corresponding
map function the termination checker complains (the two functions have
the same type according to Check):


Fixpoint op2 (x: foo) :=
  match x with
  | Foo => Foo
  | Bar l => Bar (LibList.map op2 l)
  end.
(* Recursive call to op2 has principal argument equal to "x0"
instead of one of the following variables: "l" "l0".

Recursive definition is:
"fun x : foo =>
 match x with
 | Foo => Foo
 | Bar l => Bar (map op2 l)
 end".
*)


If I write a dedicated map function that is mutually recursive I get
the same error:


Fixpoint op3 (x: foo) :=
  match x with
  | Foo => Foo
  | Bar l => Bar (myMap l)
  end
with
  myMap (l: list foo) :=
    match l with
    | nil => nil
    | x :: xs => op3 x :: myMap xs
    end.
(* Recursive call to op3 has principal argument equal to
"x" instead of "xs".
Recursive definition is:
"fun l : list foo =>
 match l with
 | nil => nil
 | x :: xs => op3 x :: myMap xs
 end".
*)


However, if I write a slightly less dedicated map function as a
mutually recursive function it works:


Fixpoint op4 (x: foo) :=
  match x with
  | Foo => Foo
  | Bar l => Bar (myMap op4 l)
  end
with myMap (f: foo -> foo) (l: list foo) :=
  match l with
  | nil => nil
  | x :: xs => f x :: myMap f xs
  end.
(* Compiles OK! *)


Strangely, even though this is not a true mutually recursive
definition, if I separate the two I get an error about the number
of arguments which doesn’t make sense to me:


Fixpoint myMap2 (f: foo -> foo) (l: list foo) :=
  match l with
  | nil => nil
  | x :: xs => f x :: myMap2 f xs
  end.

Fixpoint op5 (x: foo) :=
  match x with
  | Foo => Foo
  | Bar l => Bar (myMap2 op5 l)
  end.
(* Recursive call to op5 has not enough arguments.
Recursive definition is:
"fun x : foo =>
 match x with
 | Foo => Foo
 | Bar l => Bar (myMap op5 l)
 end".
*)


Any ideas of what is going on is greatly appreciated!

/Elias








När du har kontakt med oss på Uppsala universitet med e-post så innebär det 
att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan 
du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. 
For more information on how this is performed, please read here: 
http://www.uu.se/en/about-uu/data-protection-policy