如何在Coq中切换当前目标？ [英] How to switch the current goal in Coq?

问题描述

是否可以切换当前目标或子目标以在Coq中进行证明？

Is it possible to switch the current goal or subgoal to prove in Coq?

例如，我有一个这样的目标（来自自我存在者）：

For example, I have a goal like this (from an eexists):

______________________________________(1/1)
?s > 0 /\ r1 * (r1 + s1) + ?s = r3 * (r3 + s2)

我想做的是分割并首先证明正确的合取。我认为这将给出存在变量？s 的值，而左合词应该只是一个简化形式。

What I want to do is to split and prove the right conjunct first. This I think will give the value of the existential variable ?s, and the left conjunct should be just a simplification away.

但是默认情况下分开设置左合词？s> 0 作为当前目标。

But split by default set the left conjunct ?s > 0 as the current goal.

______________________________________(1/2)
?s > 0
______________________________________(2/2)
r1 * (r1 + s1) + ?s = r3 * (r3 + s2)

我知道我可以在第二个子目标上使用 2：作为战术的前缀，但这很尴尬

I know I can prefix tactics with 2: to operate on the second subgoal, but it's awkward because

1）我看不到目标＃2和

1) I can't see the hypotheses for goal#2 and

2的假设，如果它在不同的环境中，目标＃ 2可能是第三个目标或第k个目标。证明不会是可移植的。

2) if it's in a different context, goal#2 might be the third or the k_th goal. The proof won't be portable.

这就是为什么我要将第二个目标设置为当前目标。

That's why I want to set the second goal as the current.

顺便说一句，我正在使用CoqIDE（8.5）。

BTW, I am using CoqIDE (8.5).

推荐答案

您可以使用焦点2 专注于第二个目标。

You can use Focus 2 to focus on the second goal.

这篇关于如何在Coq中切换当前目标？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！