在Coq中,有一种方法可以摆脱“无用的”垃圾邮件。假设的前提条件? [英] In Coq, is there a way to get rid of "useless" preconditions in a hypothesis?
问题描述
有时由于记住
和归纳
策略的结合,我最终得到了一个看起来像像这样:
Sometimes due to a combination of the remember
and induction
tactics, I end up with hypothesis that look like a bit like this:
Heqa: a = Foo b
IH1: a = Foo b -> bla_bla_bla
IH2: a = Foo b -> ble_ble_ble
有没有一种快速的方法来使那些无用的 a = Foo b
IH1 和 IH2
中的前提条件?我能想到的唯一方法是非常冗长和重复:
Is there a quick way to get those useless a = Foo b
preconditions in IH1
and IH2
out of the way? The only way to do that that I can think of is very verbose and repetitive:
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 (IH1 Heqa).
specialize (IH2 Heqa).
会让你
Heqa: a = Foo b
IH1: bla_bla_bla
IH2: ble_ble_ble
这似乎就是您想要的。
specialize
对假设应用某些参数并将其重写
specialize
applies some arguments to a hypothesis and rewrites it.
顺便说一句,使用稍微相似的战术姿势证明
,我们可以保持原始假设不变。可以在此处找到。
By the way, using a somewhat similar tactic pose proof
we can keep the original hypothesis intact. More details can be found here.
这篇关于在Coq中,有一种方法可以摆脱“无用的”垃圾邮件。假设的前提条件?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!