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...
Did you mean to apply f
somewhere in the definition of map
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: Oct 13 2024 at 01:02 UTC