6

次の補題を示したいとしましょう

lemma "⟦ A; B; C ⟧ ⟹ D"

私は目標を達成します

1. A ⟹ B ⟹ C ⟹ D

ただし、必要ありませんB。どうすれば私の目標を次のようなものに移すことができますか

1. A ⟹ C ⟹ D

元のステートメントを変更したくはありませんlemma。適用スタイルの現在の目標だけを変更します。

4

2 に答える 2

6

あなたが欲しいのはですapply (thin_tac B)。しかし、私が最後にこれをしたとき、ピーター・ラミッチは「なんてことだ、なぜあなたはこれをしているのか！」と叫んだ。嫌悪感を持って、thin_tacを取り除くために私の証明を書き直しました。したがって、この戦術を使用することは、もはや正確には奨励されていないようです。

于 2013-03-09T14:54:54.927 に答える
5

通常、後で削除するのではなく、目標状態で不要なものを回避することをお勧めします。証明問題を定式化する方法は、それを解決する方法に影響します。

これは、構造化された証明にとって特に重要です。いくつかの事実を否定的に抑制するのではなく、証明の次のステップに参加する必要がある事実に積極的に訴えます。

例：このように：

from `A` and `C` have D ...

どの事実が証明に関連しているかを伝えることは、すでに読みやすさの始まりです。

そのスタイルに従うと、最初の問題は次のようになります。

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

または、ABCDが大きな命題である場合は、冗長性を減らしてこのようにします。

lemma
  assumes a: A and b: B and c: C 
  shows D
proof -
  from a c show ?thesis sorry
qed
于 2013-03-09T15:28:10.883 に答える