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'。在這種情況下得到的證明將使用一些額外的公理。使用'打印假設'。得到它們。 –