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`

)

```
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

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

Oh excellent indeed it does works perfectly. Thanks!!

Last updated: Jun 23 2024 at 01:02 UTC