Ist es möglich, das aktuelle Ziel oder Unterziel zu wechseln, um in Coq zu beweisen?Wie schalte ich das aktuelle Ziel in Coq?
Zum Beispiel habe ich ein Ziel wie folgt (von einem eexists):
______________________________________(1/1)
?s > 0 /\ r1 * (r1 + s1) + ?s = r3 * (r3 + s2)
Was ich will ist split tun und das Recht conjunct zuerst beweisen. Dies wird meiner Meinung nach den Wert der existentiellen Variablen ?s ergeben, und der linke Konjunkt sollte nur eine Vereinfachung sein.
Aber split standardmäßig setzen Sie die linke Konjunktion ?s > 0 als das aktuelle Ziel.
______________________________________(1/2)
?s > 0
______________________________________(2/2)
r1 * (r1 + s1) + ?s = r3 * (r3 + s2)
Ich weiß, ich Taktik mit 2: auf dem zweiten Teilziel zu betreiben Präfix kann, aber es ist umständlich, weil
1) ich nicht die Voraussetzungen für Ziel # 2 und
2 sehen) Wenn es sich in einem anderen Kontext befindet, könnte Ziel Nr. 2 das dritte oder das k-te Ziel sein. Der Beweis wird nicht tragbar sein.
Deshalb möchte ich das zweite Ziel als die aktuelle setzen.
BTW, ich verwende CoqIDE (8.5).