在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屋！