3

次の簡単な証明があります。

lemma
    fixes a b n :: nat
    assumes a: "a > n" "b > n"
    shows "a*b > n*n"
proof -
    from assms show "a*b > n*n" by(simp_all add: field_simps)  ERROR
qed

証明状態で、イザベルは次のように述べています。

エクスポートされたルールによってゴールを解決しようとして成功しました: n * n < a * b

しかしその後：

初期証明方法の適用に失敗しました⌂: これを使用: n < a n < b ゴール (1 サブゴール): 1. n * n < a * b

何が問題ですか？。実際、プロフを行うための実際の単一ステップに興味があるので、isabelle がその方法を教えてくれると思いました。

4

1 に答える 1

4

field_simps用語の並べ替えには適していますが、この種の推論にはあまり適していません。このようなことを証明したい場合、通常は適切なルールが必要です。この場合、(厳密な) 不等式と乗算に関する何かです。

些細なことに見えるが、それを正確に証明する方法がわからない、および/または関連する事実がIsabelleで何と呼ばれているのかわからない場合は、次のsledgehammerことが役立ちます。

from assms show "a*b > n*n"
  sledgehammer

  > Sledgehammering... 
  > Proof found... 
  > "cvc4": Try this:
  >   by (metis (no_types, lifting) dual_order.strict_trans gr_implies_not_zero 
  >         linorder_neqE_nat mult.commute nat_0_less_mult_iff 
  >         nat_mult_less_cancel1) (796 ms)

によって発見された証明の問題点は、おわかりのsledgehammerように、それらがしばしば長く、遅く、あまり明るくないということです。物事のメンテナンス面では、それらはバックグラウンド理論の変更に関してはやや壊れやすいものでもあります。それでも、始めるには良い場所であり、多くの場合、大ハンマー証明 (たとえば、nat_mult_less_cancel1ここ) から証明に関連する事実を読むことができます。

関連する事実を見つけるもう 1 つの方法はfind_theorems、Isabelle/jEdit IDE のコマンドまたは同等のクエリ パネルです。もしあなたがそうするなら

find_theorems "_ * _ > _ * _"

または、同等に_ * _ > _ * _、Query パネルに入ると、読み通すために多くの出力が得られますが、いくつかの関連する事実はその出力の最後に隠されていますmult_strict_mono'。

thm mult_strict_mono'
> ?a < ?b ⟹ ?c < ?d ⟹ 0 ≤ ?a ⟹ 0 ≤ ?c ⟹ ?a * ?c < ?b * ?d

証明は次のようになります。

from assms show "a*b > n*n"
  by (rule mult_strict_mono') simp_all

残りのsimp_all立証義務を免除するだけn ≥ 0です。

ああ、ちなみに: が表示された後にエラー メッセージが表示されるという事実は、インタラクティブなIsabelleSuccessful attempt to solve goalの非線形の性質の結果です:byその後、あたかも証明が成功したかのように進みます。これは、並列化を可能にし、一部の証明が壊れていてもユーザーがドキュメントの作業を続行できるようにするためです。

メッセージはのSuccessful attempt後に呼び出される Isabelle の部分から来ておりshow、その部分は の成功した (ただしまだ保留中の) 証明を確認しa*b > n*nます。ただし、すぐにby (simp_all …)、証明方法が失敗したというエラー メッセージが表示されます。バッチ処理モードでは、このような失敗はより劇的です (そしてより明白になります)。

于 2016-11-16T07:08:57.230 に答える