並べ替えゴール（イザベル）

Question

は、私は次のような状況での目標を並べ替える方法を知りたい：

lemma "P=Q" 
    proof (rule iffI, (*here I would like to swap goal order*), rule ccontr) 
oops 

私は補題ステートメントを変更伴わない溶液をしたいと思います。私はpreferとdeferが適用スタイルプルーフに使用できることを認識していますが、proof (...)の部分で使用できる方法がありたいと思います。

編集：アンドレアスLochbihlerとして

は、上記の例ではrule iffI[rotated]作品を書いて、と言います。しかし、次のような状況で、補助定理のステートメントを変更することなく、ゴールオーダーを入れ替えることは可能ですか？

lemma "P==>Q" "Q==>P" 
    proof ((*here I would like to swap goal order*), rule ccontr) 
oops 

この例は不自然に見えるかもしれませんが、私は補題のステートメントを変更することは不便である状況があるかもしれないことを感じ、またはルールの以前のアプリケーションが存在しない場合、目標順位を入れ替えることが必要です例えば、iffI。

Answer 1

サブゴールの順番は、適用する規則の前提条件の順序によって決まります。それは、一般的に

proof(rule iffI[rotated], rule ccontr) 

は、目標の順序を変更する証明方法が存在しないように属性[rotated]を使用して、例えば、iffIルールの前提を交換すればよいです。 autoのような洗練された証明自動化でこれを使うことを考えているなら、私はこの種のことをしないように強く勧めます。多くの自動化された証明スクリプトは、目標の順序とは独立して機能するはずです。そうしないと、プルーフオートメーション設定の内容が変更されたときにプルーフが簡単に破損します。

しかし、いくつかの低レベルの証明戦法では、明示的な目標アドレッシング（主に_tacで終わるもの）を使用することができます。たとえば、

proof(rule iffI, rule_tac [2] ccontr) 

は、最初のサブゴールではなく2番目のサブゴールに適用されます。