Stream: Coq users

Topic: Local fix and cbn


view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Yannick Zakowski (Feb 17 2021 at 15:48):

Oh excellent indeed it does works perfectly. Thanks!!


Last updated: Jan 27 2023 at 00:03 UTC