如何在Coq中實例化一個假設的變量？

Question

我有兩個假設

IHl: forall (lr : list nat) (d x : nat), d = x \/ In x l' -> (something else) 
Head : d = x 

，而我想apply IHl上頭，因爲它符合國際人道法的d = x \/ In x l。但apply with戰術將失敗，簡單提示Error: Unable to unify。

我應該使用哪種策略來實例化假設中的變量？

Answer 1

您的假設IHl需要4個參數：lr : list nat,d : nat，x : nat和_ : d = x \/ In x l'。

您的假設Head : d = x沒有正確的類型作爲第四個參數傳遞。你需要把它從一個平等證明變成一個脫節證明。幸運的是，你可以使用：

or_introl 
    : forall A B : Prop, A -> A \/ B 

這是or類型的兩個構造之一。

現在，您可能必須明確通過B支柱，除非它可以通過統一在上下文中找到。

這裏有事情，應該工作：

(* To keep IHl but use its result, given lr : list nat *) 
pose proof (IHl lr _ _ (or_introl Head)). 

(* To transform IHl into its result, given lr : list nat *) 
specialize (IHl lr _ _ (or_introl Head)). 

有可能是一個apply就可以使用，但根據什麼是隱含/推斷爲你，這是我很難告訴你這是哪一個。