The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 02/05/2017 14:45, Christian Kjær Larsen wrote:

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

First of all, writing the term for map_fusion by hand is incredibly
difficult. It might be better to switch to interactive mode and create
the term piecewise using tactics:

Definition map_fusion t G (e : exp G t) : exp G t.

Second, you will encounter various issues. The most obvious one is that
you are matching on "e" yet you are returning "e" in some branches.
Unfortunately, "e" still has its original type, which does not match the
type expected by the branches. So your outer term has to look like:

Definition map_fusion t G (e : exp G t) :=
  match e in exp _ t' return exp G t' -> exp G t' with
  | emap t2 t1 g em => ...
  |  _ => fun e => e
  end e. (* notice "e" here! *)

Now for the "..." part. The "em" binder is of type "exp G (TList t2)".
But if you match on it, you necessarily lose the "TList t2" part. For
instance, in the "etrue" case, this part is "TBool". This is obviously
contradictory and thus "em" cannot be "etrue", but this is not readily
apparent to Coq's type system. So you have to preserve the information
manually.

To do so, you need to change "em" so that it is of type "exp G lt2" for
some arbitrary lt2 while keeping the identity "TList t2 = lt2" in your
context. So the "..." part becomes

(fun lt2 (em' : exp G lt2) =>
  match em' in exp _ lt2 return (TList t2 = lt2 -> _) with
  | emap t3 t2' f eb => fun Heq _ => emap (compose f ...) eb
  | _ => fun _ e => e
  end) (TList t2) em eq_refl

Now you are back to your initial problem, since you have to fill "..."
of type "exp (t2' :: G) t1" with "g" of type "exp (t2 :: G) t1". The
good news is that, since "lt2" was substituted with "TList t2'", "Heq"
has type "TList t2 = TList t2'". So using injectivity and rewriting, you
can convince Coq that "g" has the expected type.

Note that is only one way of building the term. There exist other ways
and some might even be more concise, for instance by using "match" in a
"return" clause to avoid having to deal with injectivity and rewriting.

Best regards,

Guillaume