## Stream: Coq users

### Topic: Recursion using map

#### 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...

#### Li-yao (May 25 2021 at 15:52):

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

#### 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: Jun 25 2024 at 18:02 UTC