在Coq中,有没有办法摆脱假设中的"无用"前提条件？

Question

有时由于战术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.

Answer 1

你可以使用这个specialize策略:

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

会得到你

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

这似乎是你想要的.

specialize 将一些参数应用于假设并重写它.

顺便说一下,使用一种类似的策略,pose proof我们可以保持原始假设的完整性.更多细节可以在这里找到.