ドロップのは私が目標</p> <pre><code>1. A ⟹ B ⟹ C ⟹ D </code></pre> <p>を取得するには、次の補題</p> <pre><code>lemma "⟦ A; B; C ⟧ ⟹ D" </code></pre> <p>を表示したいとしましょうスタイル

Question

を適用における目標で前提しかし、私はBを必要としません。私は

1. A ⟹ C ⟹ D 

のようなものに私の目標を転送することができますどのようにしてスタイルを適用するには、元の文lemma、ちょうど現在の目標を変更する必要はありません。

Answer 1

希望するものはapply (thin_tac B)です。しかし、私が最後にこのことをしたとき、Peter Lammichは "Oh god、なぜあなたはこれをしているのですか"と叫んだ。嫌になり、thin_tacを取り除くために私の証明を書き直した。だから、この戦術を使うことは、もはやまさに奨励されるようには見えません。

Answer 2

通常、後で削除するのではなく、ゴール状態で望ましくないものを避ける方がよいでしょう。あなたが証明問題を定式化する方法は、あなたがそれを解決する方法に影響します。

これは、構造化された証明のために特に重要である：あなたの代わりに否定それらのいくつかを抑制する、積極証明の次のステップに参加すべきであるそれらの事実にをアピール。

など。

校正に関連する事実を知ることは、既に読みやすさの出発点です。

そのスタイルに続いて、あなたの最初の問題は次のようになります。減少した冗長性と

lemma 
    assumes A and B and C 
    shows D 
proof - 
    from `A` and `C` show D sorry 
qed 

かのように、ABCDが大命題であれば：

​​