0

Isabelle に次のコードがあります。

typedecl Person
consts age :: "Person ⇒ int" 

lemma "⟦(∀p::Person. age p > 20);p ∈ Person⟧⟹ age p > 20"
apply (auto)
done

自動証明法は問題なく機能し、補題が証明されます! 補題の前提の最初の部分を以下の定義 C1 として除外したい場合:

definition C1::bool where "C1 ≡ (∀p::Person. age p > 20)"

autoメソッドは、次のコードで証明できません。

lemma "⟦C1;p ∈ Person⟧⟹ age p > 20"
apply (auto)
done

なぜこれが起こるのですか？最初の仮定を因数分解する方法で間違っている場合 --- きちんと構造化されたように見えるように仮定を整理するためにこれを行っています -- 証明方法に影響を与えないこれを行うための最良の方法は何ですか (自動)機能。

ありがとう

4

2 に答える 2

1

まず、実際に値を追加するために、ルールとしてdeclare追加する方法を示します。次に、あなたの に関するいくつかの要求されていないポインターを提供し、次に、Stackoverflow のエチケットに関するいくつかの要求されていないポインターを (私の観点から) 提供します。C1_defsimplemma

単純なルールとして定義を宣言する

アレクサンダーが指摘したように、 aはルールdefinitionとして自動的に追加されません。simp

simp次のようなルールとして宣言できます。

declare C1_def [simp add]

auto自動証明メソッド、simp、などで単純なルールを使用すると、不適切fastforceなループが発生したり、数式を展開したくない方法で数式を展開したりする可能性があるため、追加した後、次のsimpようにルールとして削除できます。

declare C1_def [simp del]

あなたの補題についてのコメント

あなたの補題の式はまさにあなたが望むものである可能性がありますが、私の意見では、あなたの表記法は混乱の潜在的な原因です. 特に、Person型の名前とセット変数の両方として使用していること。私は明確化を求めずにこれらのコメントをします。

私自身の質問は、「集合があるのに、集合ではないのにp ∈ Person、なぜエラーが発生しないのですか。PersonPersontypedecl Person

より多くの情報を得る 1 つの方法は、 を使用することdeclare [[show_types, show_consts]]です。

私の質問に答えるために、私は次のことを行いました (ブラウザーの移植性のためにシンボルを変換します)。出力パネルに表示されたものの一部を示します。

declare [[show_types, show_consts]]
lemma "[|(!p::Person. age p > 20); p ∈ Person|] ==> (age p > 20)"
oops
(*OUTPUT:
  variables:
    Person :: Person set
    p :: Person *)

Personが自由変数であることを示しています。に関してはp、それは の束縛変数ですが(!p::Person. age p > 20)、補題の残りの部分では自由なので、仮説にはすべてpの型Personがすべての型のセットにあるという式が含まれていますPerson set。

それはあなたが望むものかもしれませんが、この場合、補題は基本的に の形式であるため、違いはありませんA and B implies A。

回答済みの SO 質問への回答を受け入れる必要があります

約2時間で姿を消す前に、isabelleタッグのために、SOエチケットポリスとしての念願の任務を再び遂行する。

3 つの質問をしました。特に、これがあります：

それは率直な質問であり、率直な答えが与えられています。あなたはそれを答えとして受け入れる必要があります。さもないと、

  • 「isabelle」タグの「未回答」タブをクリックすると、未回答として表示される場合があり、未回答の場合、
  • 与えられた答えに対して、適切な感謝の気持ちを示していません。

私がリンクした質問の場合、(私とは異なり) Isbelle/HOL の専門家の 1 人から回答を得ました。人がそのような回答を入力するには、かなりの時間がかかります。極端に長くはありませんが、ワンライナーでもありません。

于 2014-11-07T14:59:23.693 に答える
1

この構成definitionは、実装の詳細を抽象化する方法として機能します。その使用の 1 つは、関連付けられた用語のいくつかのプロパティを証明し、用語宣言自体の代わりにプロパティに依存することです。したがって、定義された用語の簡略化規則は に自動的に追加されませんsimpset。ルールは、サフィックス付きの用語の名前で引き続き使用でき、_def明示的に使用できます。

lemma "⟦C1; p ∈ Person⟧ ⟹ age p > 20"
  apply (auto simp add: C1_def)
done
于 2014-11-07T06:04:19.350 に答える