Конкатенация зависимого типа в Coq

Question

У меня есть график с объектами и стрелками, и из этого я определил понятие пути стрелок. Я хочу определить конкатенацию этих путей. Следующий код - моя наивная попытка. Но я получаю сообщение об ошибке, когда p' равно emptyPath в предложении match: «Термин« p »имеет тип« путь A B », в то время как ожидается, что он будет иметь тип « путь A C ». ' Концептуально не должно быть проблем, так как в этом случае B равно C. Как я могу заставить это работать?

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

Всякий раз, когда у вас есть «различные показатели», как в вашем определении, вам необходимо применить так называемый «конвой шаблон», чтобы получить ваше определение работать. Основная идея состоит в том, чтобы повторно описать некоторые из ваших аргументов, чтобы зависимое сопоставление шаблонов могло «изменять» их типы.

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. 

Вы можете узнать больше о картине конвоя в CPDT книге Адама Chlipala в.

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.