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?