The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Elias,

This is a classic but however subtle aspect of the guard-checker:

Require Import List.

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

Fixpoint map1 {X Y} (f : X -> Y) l :=
  match l with
  | nil => nil
  | x::l => f x :: map1 f l
  end.

Fail Fixpoint op1 (x: foo) :=
  match x with
  | Foo => Foo
  | Bar l => Bar (map1 op1 l)
  end.

Definition map2 {X Y} (f : X -> Y) :=
  fix loop l :=
    match l with
    | nil => nil
    | x::l => f x :: loop l
    end.

Fixpoint op2 (x: foo) :=
  match x with
  | Foo => Foo
  | Bar l => Bar (map2 op2 l)
  end.

Why does op1 fail (with map1) while op2 succeeds (with map2) ?

Let us unfold the definition of map2 inside of op2. Thus we get

Fixpoint op2 (x: foo) :=
  match x with
  | Foo => Foo
  | Bar m => Bar ((fix loop l := match l with 
                     | nil  => nil
                     | x::l => op2 x :: loop l
                   end) m)
  end.

after reduction of map2, ie substitution of f
with op2. This is possible because map2 is a
*Definition*. Giving a legit *nested* recursion scheme.

However, the unfolding with map1 fails
because Fixpoint map1 can only be unfolded when
its structural argument has a head constructor,
hence f does not get substituted with op1 and
then the guardchecker fails to detect structural
decrease.

The situation might change with 8.20+ however
as I recall a discussion on Zulip Coq.

Concerning 

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.

It gives the following *scary* warning

(* Not a fully mutually defined fixpoint
(op4 depends on myMap but not conversely).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints,default]
op4 is defined
myMap is defined
op4, myMap are recursively defined (guarded respectively on 1st, 2nd 
arguments)

*)

which means it accepts this mutual definition
even though it should not because foo and (list foo)
are not mutually defined inductive types. Maybe
the "non-full-mutual" option allows for this.
I wouldn't trust a code that produces such a warning.

For a legit mutually dependent fixpoint, you can try

Inductive foo :=
| Foo : foo
| Bar : lfoo -> foo
with lfoo :=
| Nil : lfoo
| Cons : foo -> lfoo -> lfoo.

Fixpoint op4 (x: foo) :=
  match x with
  | Foo => Foo
  | Bar l => Bar (myMap l)
  end
with myMap (l: lfoo) :=
  match l with
  | Nil => Nil
  | Cons x xs => Cons (op4 x) (myMap xs)
  end.


Best

Dominique




----- Mail original -----
> De: "Elias Castegren" <elias.castegren AT it.uu.se>
> À: "coq-club" <coq-club AT inria.fr>
> Envoyé: Mercredi 6 Novembre 2024 16:56:32
> Objet: [Coq-Club] Termination checker rejecting equivalent functions

> 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