1
我有以下设置（对不起，如果这是一个有点长的MCVE），我试图证明的定理，但我被卡住，因为它不能统一的类型因为它们依赖理论上不同的对象类型，即使对象类型是相同的。平等
是否有一个通用的策略来分解具有相关类型的构造函数？ injection和inversion产生什么似乎是无用的结果与ob_fn（我可以很容易地证明等效定理），而不是morph_fn。
Inductive Cat := cons_cat (O : Type) (M : O -> O -> Type).
Definition ob (c : Cat) :=
match c with cons_cat o _ => o end.
Definition morph (c : Cat) : ob c -> ob c -> Type :=
match c with cons_cat _ m => m end.
Inductive Functor
(A B : Cat)
: Type :=
cons_functor
(ob_fn : ob A -> ob B)
(morph_fn : forall {c d : ob A}, morph A c d -> morph B (ob_fn c) (ob_fn d)).
Definition ob_fn {A B : Cat} (f : Functor A B) : ob A -> ob B :=
match f with cons_functor f' _ => f' end.
Definition morph_fn {A B : Cat} {c d : ob A} (f : Functor A B)
: morph A c d -> morph B (ob_fn f c) (ob_fn f d) :=
match f with cons_functor _ f' => f' c d end.
Theorem functor_decompose {A B : Cat} {o fm gm} : cons_functor A B o fm = cons_functor A B o gm -> fm = gm.
intros H.
assert (forall c d, @morph_fn A B c d (cons_functor A B o fm) = @morph_fn A B c d (cons_functor A B o gm)).
intros.
rewrite H.
你正面临着相关类型的典型问题，你的目标不能因为它不会很好，当它是广义上的第一个参数类型重写。如果你想引入公理，你可以使用'eq_dec'或'JM_eq'来避免这个问题，（或者你可以使一些基类型为可判定的）。如果不是这样，除了用复杂模式证明注入性之外，你将没有别的选择匹配。 – ejgallego
如果我假设我的基类型是可确定的（在本例中假设您的意思是O），那么是否有通向解决方案的直接路径？ –
是的，有。请参阅James Wilcox的[无公理的Coq案例分析]（https://homes.cs.washington.edu/~jrw12/dep-destruct.html）。链接文章的摘录：“如果索引的类型具有可判定的相等性，则不需要'JMeq'来获得依赖性案例分析”。或者，您可以'要求导入Coq.Program.Equality.'并对构造函数相等性执行'dependent destruction'。在这种情况下得到的证明将使用一些额外的公理。使用'打印假设'。得到它们。 –