I represent typed expressions with the following inductive types

```
Inductive type : Type :=
| base_type : nat -> type
| arrow_type : type -> type -> type.
Notation "A --> B" := (arrow_type A B) (at level 30, right associativity).
Inductive expr : type -> Type :=
| var : forall (X : type) (n : nat), expr X
| app : forall {X Y : type} (f : expr (X --> Y)) (x : expr X), expr Y
| identity : forall {X : type}, expr (X --> X)
| compose : forall {X Y Z : type}, expr ((X --> Y) --> (Y --> Z) --> (X --> Z)).
Coercion expr : type >-> Sortclass.
Notation "f [ x ]" := (app f x) (at level 8).
```

You can create a basic type indexed with an integer with `base_type`

and a function type with `arrow_type`

. Similarly, you can create a variable indexed with an integer with `var`

and apply a function with `app`

.

There are two special expressions `identity`

and `compose`

with their obvious meaning. I want to write a function which preforms the basic expected reductions:

```
identity[x] -> x
compose[g][f][x] -> f[g[x]]
```

A naive(and human readable) implementation would look like:

```
Definition reduce {E : type} (expression : E) : E :=
match expression with
| identity [ x ] => x
| compose[ g ][ f ][ x ] => f[g[x]]
| e => e (* do nothing otherwise *)
end.
```

(It is intended that the above function does reduction only on the top most level of an expression)

The above function does not type check, I should do some magic with dependent pattern matching but I’m not sure how to do it in this case. Is there a simple way to do it? Is it going to scale to more complicated patterns?

Example of a more complicated reduction(after I add more combinators like `curry`

, `uncurry`

, etc.):

```
compose [curry [compose [compose [diag] [pair_fmap [snd] [fst]]] [uncurry [identity]]]] [compose [compose [pair] [compose]]] -> curry
```

I can implement the function using tactics, but it can get quickly out of hand, become unreadable and hardly maintainable. Example of reduction only for `identity`

:

```
Definition reduce_identity (E : type) (expression : E) : E.
destruct expression as [X n | X Y f x | X | X Y Z].
- apply (var X n).
- {
inversion f as [X' n' | X' Y' f' x' | X' | X' Y' Z'].
(* identity case *)
3: {
rewrite <- H0.
apply x.
}
apply (f[x]).
apply (f[x]).
rewrite H0; apply (f[x]).
}
- apply identity.
- apply compose.
Defined.
```

I thought that I might learn something from the generated proof term:

```
Print reduce_identity.
```

But the result is barely readable to me.

Is there an easy, readable and extensible way to write the `reduce`

function?