coq - 在Coq中，有没有办法摆脱假设中的“无用”前提？

有时由于remember和induction策略的结合，我最终得到了一个看起来像这样的假设：

Heqa: a = Foo b
IH1: a = Foo b -> bla_bla_bla
IH2: a = Foo b -> ble_ble_ble

有没有一种快速的方法来消除a = Foo b和IH1中那些无用的IH2前提条件？我能想到的唯一方法是非常冗长和重复：

assert (IH1': a = Foo b). { apply Heqa. }
apply IH1 in IH1'. clear IH1. rename IH1' into IH1.

assert (IH2': a = Foo b). { apply Heqa. }
apply IH2 in IH2'. clear IH2. rename IH2' into IH2.

最佳答案

您可以使用specialize策略：

specialize (IH1 Heqa).
specialize (IH2 Heqa).

会得到你

Heqa: a = Foo b
IH1: bla_bla_bla
IH2: ble_ble_ble

这似乎是您想要的。

specialize将某些参数应用于假设并重写。

顺便说一句，使用稍微相似的战术pose proof，我们可以保持原始假设不变。可以在here中找到更多详细信息。