The Coq mailing list

[Christian Kjær Larsen <christianden AT gmail.com>]

Hi,

I'm currently writing my bachelors thesis, and I'm hitting some problems with pattern matching on dependent
types, and I was wondering if you guys could help. It seems a bit difficult to work with in Coq.

I'm trying to formalise a small array language using intrinsically typed
syntax, de bruijn indices for binders and Adam Chlipalas heterogeneous list implementation from his book.

The idea is that I want to implement some fusion rules (like https://wiki.haskell.org/Fusion), and prove them correct using a semantics encoded in Coq.

The syntax is like this

Inductive exp G : ty -> Type :=
| evar : forall t, member t G -> exp G t
| etrue : exp G TBool
| efalse : exp G TBool
| econst : nat -> exp G TNat
| esucc : exp G TNat -> exp G TNat
| enil : forall t, exp G (TList t)
| econs : forall t, exp G t -> exp G (TList t) -> exp G (TList t)
| emap : forall t1 t2, exp (t1 :: G) t2 -> exp G (TList t1) -> exp G (TList t2)
| efilter : forall t1, exp (t1 :: G) TBool -> exp G (TList t1) -> exp G (TList t1).

And I have tried to define a fusion rule for (map f (map g) == map (f o g)) like this

Definition map_fusion t G (e : exp G t) :=
  match e in exp _ t return exp G t with
  | emap t2 t1 g em => match em in exp _ (TList t3) return exp G t with
                       | emap t3 t2 f eb => emap (compose f g) eb
                       | _ => e
                       end
  |  _ => e
end.

This does not work, because Coq does not know that the t2's are the
same. Do you have any tips for doing this style of dependent pattern
matching in Coq. I have tried to use the Program tactic, but I hit some
kind of bug. (https://coq.inria.fr/bugs/show_bug.cgi?id=5473).

I hope that my question makes sense, and that some of you will have the time to answer.

Cheers,

Christian Kjær Larsen
Student at the University of Copenhagen, Denmark.