Dependent type list concatenation in Coq

Question

I have a graph with objects and arrows and from this I have defined the notion of a path of arrows. I want to define concatenation of these paths. The following code is my naive attempt. But I get an error when p' is emptyPath in the match clause: 'The term "p" has type "path A B" while it is expected to have type "path A C".' Conceptually there should be no problem since in this case B equals C. How can I get this to work?

Parameter Object : Set.
Parameter Arrow : Object -> Object -> Set.

Inductive path : Object -> Object -> Set :=
  emptyPath : forall X, path X X
| cons : forall {A B C} (p : path A B) (f : Arrow B C), path A C.

Fixpoint concat {A B C : Object} (p : path A B) (p' : path B C) :  path A C :=
  match p' return path A C with
    | emptyPath _ => p
    | cons _ _ _ p0 f => cons (concat p p0) f
  end. 

Answer 1

Whenever you have "varying indices" like in your definition, you need to apply the so-called "convoy pattern" to get your definition to work. The basic idea is to reabstract some of your arguments so that dependent pattern matching can "change" their types.

Parameter Object : Set.
Parameter Arrow : Object -> Object -> Set.

Inductive path : Object -> Object -> Set :=
  emptyPath : forall X, path X X
| cons : forall {A B C} (p : path A B) (f : Arrow B C), path A C.

Fixpoint concat {A B C : Object} (p : path A B) (p' : path B C) :  path A C :=
  match p' in path B C return path A B -> path A C with
    | emptyPath _ => fun p => p
    | cons _ _ _ p0 f => fun p => cons (concat p p0) f
  end p.

You can learn more about the convoy pattern in Adam Chlipala's CPDT book.

Answer 2

(* You could use Program *)

Parameter Object : Set.
Parameter Arrow : Object -> Object -> Set.

Inductive path : Object -> Object -> Set :=
  emptyPath : forall X, path X X
| full : forall {A B C} (p : path A B) (f : Arrow B C), path A C.

Require Import Coq.Program.Program.

Program Fixpoint concat {A B C : Object} (p : path A B) (p' : path B C) :  path A C :=
  match p' with
    | emptyPath _ => p
    | full _ _ _ p0 f => full (concat p p0) f
  end. 

(* Unfortunately, I don't think Program produces an easy way to unfold
or simpl the definitions it produces, so programs about them are
difficult. *)

(* You could also switch to an unyped representation. I find this
method much easier to reason about. *)

Definition sArrow := prod Object Object.

Definition spath := list sArrow.

Fixpoint bound (xs:spath) a b :=
  match xs with
    | nil => a = b
    | cons y ys =>
      a = fst y /\
      bound ys (snd y) b
  end.

Lemma concatBound : forall xs a b c ys (top:bound xs a b), bound ys b c -> bound (xs ++ ys)%list a c.
induction xs; intros.
{
  unfold app; unfold bound in *; subst; assumption.
}
{
  simpl in *.
  destruct top; split; subst; auto.
  eapply IHxs; solve [eauto].
}
Qed.