Stream: Coq users

Topic: Recursion using map


view this post on Zulip Matthis Kruse (May 25 2021 at 15:44):

Suppose you have an inductive and define a map function over it:

Inductive e := fail_c | nat_c : nat -> e | true_c | false_c
       | op_c : e -> e -> e | cmp_c : e -> e -> e | var_c : nat -> e | let_c : nat -> e -> e -> e
       | if_c : e -> e -> e -> e
.
Fixpoint map (f : e -> e) exp :=
  match e with
  | (fail_c | nat_c _ | true_c | false_c | var_c _) => exp
  | op_c e1 e2 => op_c (map f e1) (map f e2)
  | cmp_c e1 e2 => cmp_c (map f e1) (map f e2)
  | let_c n e1 e2 => let_c n (map f e1) (map f e2)
  | if_c c e1 e2 => if_c (map f c) (map f e1) (map f e2)
  end
.

Having such a map is quite useful, since we can omit uninteresting details when implementing e.g. transformations on the inductive.
Take a simple substitution as an example, instead of spelling out each and every alternative, I'd like to just do:

(* substitute what (x) for (p) in (e) *)
Fixpoint esubst x p e :=
  match e with
  | var_c y => if Nat.eqb x y then p else var_c y
  | let_c y e1 e2 => if Nat.eqb x y then let_c y (esubst x p e1) e2 else let_c y (esubst x p e1) (esubst x p e2)
  | e'' => map (fun e' => esubst x p e') e''
  end
.

Unfortunately, the termination checker has trouble guessing the decreasing argument. Is this scheme somehow possible in coq? I know that Program Fixpoint exists, but having to prove 11 obligations with respect to the termination behavior is more laborious than just "inlining" the map call all the time...

view this post on Zulip Li-yao (May 25 2021 at 15:52):

Did you mean to apply f somewhere in the definition of map

view this post on Zulip Li-yao (May 25 2021 at 15:55):

I think you mean this, which works:

Inductive e := fail_c | nat_c : nat -> e | true_c | false_c
       | op_c : e -> e -> e | cmp_c : e -> e -> e | var_c : nat -> e | let_c : nat -> e -> e -> e
       | if_c : e -> e -> e -> e
.

Definition map (f : e -> e) exp :=
  match exp with
  | (fail_c | nat_c _ | true_c | false_c | var_c _) => exp
  | op_c e1 e2 => op_c (f e1) (f e2)
  | cmp_c e1 e2 => cmp_c (f e1) (f e2)
  | let_c n e1 e2 => let_c n (f e1) (f e2)
  | if_c c e1 e2 => if_c (f c) (f e1) (f e2)
  end
.

(* substitute what (x) for (p) in (e) *)
Fixpoint esubst x p e :=
  match e with
  | var_c y => if Nat.eqb x y then p else var_c y
  | let_c y e1 e2 => if Nat.eqb x y then let_c y (esubst x p e1) e2 else let_c y (esubst x p e1) (esubst x p e2)
  | e'' => map (fun e' => esubst x p e') e''
  end
.

It's a pretty neat idea.


Last updated: Jan 27 2023 at 01:03 UTC