問題タブ [isar]

見せ方のルール知ってる人いますか

リアルで？

「クエリ」パネルを使用して、次のルールを見つけました。

私はどういうop意味で少し混乱していますが。

n (nat 型) の帰納法によってステートメントを証明できるようにしたいと考えています。これは、前件が n >= 2 の場合にのみ真である条件で構成されます。前件が偽である条件は、常に真です。そこで、n=0、n=1、n=2 の場合を主な誘導ステップとは別に証明したいと思います。次のような3つの基本ケースで帰納法による証明を行うことは可能ですか?

現状では、これは機能していないようです。代わりに帰納法で証明することもでき"P (n+2) --> Q"ますが、それはそれほど強力なステートメントではありません。"n=0"、"n=1"およびに分割された場合を考えており"n>=2"、帰納法によって最後の場合のみを証明しています。

次の状況で目標を並べ替える方法を知りたいです。

補題ステートメントの変更を伴わない解決策が欲しいです。prefer適用式の証明でも使えると実感しているのですが、その部分deferで使える方法があればいいなと思っています。proof (...)

編集：

Andreas Lochbihler が言うrule iffI[rotated]ように、上記の例では書き込みが機能します。しかし、次のような状況で補題の命題を変えずにゴールの順序を入れ替えることは可能でしょうか?

この例は不自然に見えるかもしれませんが、補題のステートメントを変更するのは不便である場合や、 などの規則の事前適用がない場合にゴール順序を交換する必要がある場合があると思いますiffI。