10

私は次のイザベルの目標を持っています：

lemma "⟦ if foo then a ≠ a else b ≠ b ⟧ ⟹ False"

非常に単純であるにもかかわらず、戦術、、、、、などのいずれも目標を達成することはできませsimpん。fastclarsimpblastfastforce

なぜIsabelleはif、「a≠a」と「b≠b」の両方がになるように構成の本体を単純化してFalse、目標を解決しないのですか？

4

4 に答える 4

7

合同if_weak_congルール

デフォルトでは、Isabelleには、簡略化が行われる場所に影響を与える一連の「合同ルール」が含まれています。特に、デフォルトの合同ルールはif_weak_cong次のとおりです。

b = c ⟹ (if b then x else y) = (if c then x else y)

ifこの合同規則は、ステートメント（ ）の条件を単純化するように単純化器に指示しますが、ステートメントb = cの本体を単純化しようとはしませんif。

次のいずれかを使用して、合同ルールを無効にすることができます。

apply (simp cong del: if_weak_cong)

または、代替の（より強力な）合同ルールでオーバーライドします。

apply (simp cong: if_cong)

これらの両方が上記の補題を解決します。

if_weak_congデフォルトのcongセットにあるのはなぜですか

もう1つの合理的な質問はif_weak_cong、「上記のような問題が発生した場合、なぜデフォルトの合同セットに含まれるのでしょうか？」です。

1つの動機は、次の場合のように、単純化子が再帰関数を無限に展開しないようにすることです。

fun fact where
    "fact (n :: nat) = (if n = 0 then 1 else (n * fact (n - 1)))"

この場合、

lemma "fact 3 = 6"
  by simp

目標を解決しながら、

lemma "fact 3 = 6"
  by (simp cong del: if_weak_cong)

定義の右側がfact継続的に展開されるため、単純化子をループに送信します。

この2番目のシナリオは、デフォルトになる動機となる元の質問のシナリオよりも頻繁に発生する傾向がif_weak_congあります。

于 2013-03-26T01:14:41.123 に答える
5

分割ルール

ケース分析と合同ルールに加えて、単純化器を使用してこの目標を解決する3番目の方法があります。それはスプリッターです。スプリッターを使用すると、シンプリファイアはそれ自体で限定された形式のケース分析を実行できます。用語をそれ自体でこれ以上単純化できない場合にのみ実行されます（ケースを分割すると、簡単に目標が爆発する可能性があります）。

見出語は、次の仮定でsplit_if_asm分割するようにスプリッターに指示します。if

lemma "⟦ if foo then a ≠ a else b ≠ b ⟧ ⟹ False"
  by (simp split: split_if_asm)

splitシングルステップ分割は、次の方法で実行できます。

lemma "⟦ if foo then a ≠ a else b ≠ b ⟧ ⟹ False"
  apply (split split_if_asm)
  apply simp_all
  done

if結論（）でを分割するルールsplit_ifは、デフォルト設定の一部であることに注意してください。

ところで、データ型ごとtに、データ型パッケージは分割ルールt.splitを提供し、型を含む式のt.split_asmケース分析を提供します。caset

于 2013-03-29T07:57:53.790 に答える
4

含む証明を進歩させるもう1つの自然な方法はif _ then _ else _、条件に関するケース分析です。

lemma "(if foo then a ~= a else b ~= b) ==> False"
  by (cases foo) simp_all

または、fooが自由変数ではないが、最も外側のメタレベル全称記号によってバインドされている場合（apply-scriptsでよくあることです）：

lemma "!!foo. (if foo then a ~= a else b ~= b) ==> False"
  apply (case_tac foo)
  apply simp_all
done

残念ながら、iffooが別の種類の数量詞にバインドされている場合、たとえば

lemma "ALL foo. (if foo then a ~= a else b ~= b) ==> False"

または、ネストされた仮定のメタレベル全称記号によって、たとえば

lemma "True ==> (!!foo. (if foo then a ~= a else b ~= b)) ==> False"

どちらcasesもcase_tac適用されません。

注：との（わずかな）違いについては、こちらも参照しcasesてくださいcase_tac。

于 2013-03-26T02:23:06.380 に答える
4

合同ルール

他の回答ですでに述べたように、if_weak_cong合同規則は、単純化器がifステートメントの分岐を単純化することを防ぎます。この回答では、単純化器による合同規則の使用について少し詳しく説明したいと思います。

詳細については、Isabelle / IsarリファレンスマニュアルのSimplifierに関する章（特にセクション9.3.2）も参照してください。

合同規則は、単純化子がどのように用語に降格するかを制御します。これらは、書き換えを制限し、追加の仮定を提供するために使用できます。デフォルトでは、単純化子が関数適用に遭遇した場合、結果の項を書き直そうとする前に、関数アプリケーションs tに下降し、それらをとに書き換えsます。ts't's' t'

定数（または変数）cごとに、単一の合同規則を登録できます。ルールif_weak_congはデフォルトで定数If（if ... then ... else ...構文の基礎となる）に登録されます。

?b = ?c ⟹ (if ?b then ?x else ?y) = (if ?c then ?x else ?y)

if ?b then ?x else ?yこれは次のようになります。「用語に遭遇し、?bに簡略化できる場合は?c、に書き直しif ?b then ?x else ?yてif ?c then ?x else ?yください」。合同ルールがデフォルトの戦略に取って代わるため?x、これはとの書き換えを禁止します?y。

代わりにif_weak_cong、強い合同規則がありif_congます。

⟦ ?b = ?c; (?c ⟹ ?x = ?u); (¬ ?c ⟹ ?y = ?v) ⟧
    ⟹ (if ?b then ?x else ?y) = (if ?c then ?u else ?v)

2つの仮定(?c ⟹ ?x = ?u)に注意してください(¬ ?c ⟹ ?y = ?v)。これらは、ifの左（または右）ブランチを単純化するときに条件が成立する（または成立しない）と仮定する可能性があることを単純化子に伝えます。

例として、ゴールでの単純化の振る舞いを考えてみましょう

if foo ∨ False then ¬foo ∨ False else foo ⟹ False

について何も知らないと仮定しfooます。それで、

  • apply simp：ルールを使用if_weak_congすると、これはに簡略化され if foo then ¬ foo ∨ False else foo ⟹ False、条件のみが書き換えられます
  • apply (simp cong del: if_weak_cong)：合同規則がない場合 if foo then ¬ foo else foo ⟹ False、条件と分岐が書き換えられるため、これはに簡略化されます

  • apply (simp cong: if_cong del: if_cancel)：ルールを使用するif_congと、この目標は if foo then False else False ⟹ False次のように簡略化されます。：条件foo ∨ Falseはに書き換えられfooます。2つのブランチの場合、シンプリファイアはとを書き換えます foo ⟹ ¬foo ∨ Falseが¬foo ⟹ foo ∨ False、どちらも明らかにFalseに書き換えられます。

    （私は削除if_cancelしました。これは通常、残りの目標を完全に解決します）

于 2013-03-29T07:36:36.257 に答える