Dependent pattern matching with indexed types

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 *)

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

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?

A quick and short answer: the Equations plugin solves exactly these kind of issues.

From Equations Require Import Equations.

Derive NoConfusion for type.
Derive Signature for expr.

Equations reduce {E:type} (e:E) : E :=
reduce (identity[x]) := x;
reduce (compose[f][g][x]) := g[f[x]];
reduce e := e.

Print reduce.

The resulting term is understandable but still quite large.

1 Like

This looks amazing! I did a quick test, but I’m getting an error

In environment
e0 : type
e : type
e1 : type
e3 : type
compose : e3 --> e1 --> e --> e0
f : e3
g : e1
x : e
The term "g" has type "expr e1" while it is expected to have type "expr (?X --> ?Y)".

If it works for you, then I’m suspecting that it is a problem of my version of coq, coq.8.9.0 and coq-equations.1.2~beta+8.9

Confirmed, updated to coq-8.10.2 and coq-equations-1.2.1+8.10 and it works!

Looks like a great plugin that will simplify my program a lot!