bla_bla_bla IH2: -6ren">
gpt4 book ai didi

coq - 在 Coq 中,有没有办法摆脱假设中的 "useless"前提条件?

转载 作者:行者123 更新时间:2023-12-04 22:57:19 25 4
gpt4 key购买 nike

有时由于 remember 的组合和 induction战术,我最终得到的假设看起来有点像这样:

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

有没有快速的方法来获得那些无用的 a = Foo b前提条件 IH1IH2挡道?我能想到的唯一方法是非常冗长和重复:
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 .

关于coq - 在 Coq 中,有没有办法摆脱假设中的 "useless"前提条件?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/39904991/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com