Можно ли переключить текущую цель или подзадачу на подтверждение в Coq?
Например, у меня есть такая цель (из существующего):
______________________________________(1/1)
?s > 0 /\ r1 * (r1 + s1) + ?s = r3 * (r3 + s2)
Что я хочу сделать, так это split и сначала доказать правильное соединение. Я думаю, это даст значение экзистенциальной переменной ?s, а левый конъюнкт должен быть просто упрощением.
Но split по умолчанию устанавливает левое соединение ?s > 0 как текущую цель.
______________________________________(1/2)
?s > 0
______________________________________(2/2)
r1 * (r1 + s1) + ?s = r3 * (r3 + s2)
Я знаю, что могу префикс тактики с 2: для работы над второй подцелью, но это неудобно, потому что
1) Я не вижу гипотез для цели №2 и
2) если это в другом контексте, цель №2 может быть третьей или k_й целью. Доказательство непереносимо.
Вот почему я хочу поставить вторую цель как текущую.
Кстати, я использую CoqIDE (8.5).
