## Stream: Coq users

### Topic: Local fix and cbn

#### Yannick Zakowski (Feb 17 2021 at 15:30):

Hey all. Would anyone know how to get the best of both worlds in the following situation described on a minimal example that looks silly by any chance?

``````(* Here's a good old implementation of map *)
Fixpoint map {A B} (f: A -> B) (l : list A) : list B :=
match l with
| [] => []
| x :: l => f x :: map f l
end.

(* And a datatype of trees *)
Inductive Foo : Set := | Leaf | Node : list Foo -> Foo.

(* Problem: if I do a (non-trivial) recursive call via map, it fails because "map" passes `traverse_Foo` as argument. *)
Fail Fixpoint traverse_Foo (x : Foo) : bool :=
match x with
| Leaf => true
| Node Fs => match map traverse_Foo Fs with | cons _ _ =>  true | _ => false end
end.

(* This alternate definition of "map" hacks its way around: by defining the local fix, `f` is completely inlined after just an unfolding of `map'` *)
Definition map' {A B} (f: A -> B) (l : list A) : list B :=
let fix loop l :=
match l with
| [] => []
| x :: l => f x :: loop l
end
in loop l.

(* Hence the fixpoint goes through because Coq does this unfolding and hence can see it's safe *)
Fixpoint traverse_Foo (x : Foo) : bool :=
match x with
| Leaf => true
| Node Fs => match map' traverse_Foo Fs with | cons _ _ =>  true | _ => false end
end.

(* However this alternate definition has a shitty behavior w.r.t. `cbn`! *)
Goal forall A B f x xs, @map A B f (x::xs) = map' f (x::xs).
intros.
cbn.
Abort.
``````

Would anyone have a trick define the fixpoint with a definition that still reduces like we would expect with `cbn` by any chance?
(Note: frustratingly enough, `simpl` reduces the way I'd like, but I am tied to `cbn`)

#### Gaëtan Gilbert (Feb 17 2021 at 15:42):

``````Definition map' {A B} (f: A -> B) : list A -> list B :=
fix map' l :=
match l with
| [] => []
| x :: l => f x :: map' l
end
.
``````

has nice cbn for me

#### Gaëtan Gilbert (Feb 17 2021 at 15:44):

that's what

``````Section S.
Context {A B} (f:A -> B).
Fixpoint map'  l :=
match l with
| [] => []
| x :: l => f x :: map' l
end.
End S.
``````

produces btw

#### Yannick Zakowski (Feb 17 2021 at 15:48):

Oh excellent indeed it does works perfectly. Thanks!!

Last updated: Jun 23 2024 at 01:02 UTC