在 Coq 中,有没有办法摆脱假设中的 "useless" 前提条件?
In Coq, is there a way to get rid of "useless" preconditions in a hypothesis?
有时,由于 remember
和 induction
策略的结合,我最终会得出类似这样的假设:
Heqa: a = Foo b
IH1: a = Foo b -> bla_bla_bla
IH2: a = Foo b -> ble_ble_ble
有没有一种快速的方法来消除 IH1
和 IH2
中那些无用的 a = Foo b
前提条件?我能想到的唯一方法是非常冗长和重复:
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.
有时,由于 remember
和 induction
策略的结合,我最终会得出类似这样的假设:
Heqa: a = Foo b
IH1: a = Foo b -> bla_bla_bla
IH2: a = Foo b -> ble_ble_ble
有没有一种快速的方法来消除 IH1
和 IH2
中那些无用的 a = Foo b
前提条件?我能想到的唯一方法是非常冗长和重复:
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.