2

再び、予期しない結果を伴う小さな例です。

theory Scratch
imports Main
begin

datatype test = aa | bb | plus test test

axiomatization where
   testIdemo : "x == plus x x"

lemma test1 : "y == plus y y"

今、私は次のメッセージを受け取ります：

Auto solve_direct: The current goal can be solved directly with
  Scratch.testIdemo: ?x ≡ test.plus ?x ?x 
Auto Quickcheck found a counterexample:
  y = aa
Evaluated terms:
  test.plus y y = test.plus aa aa

そして、スレッジハンマーを実行しようとすると、次のようになります。

"remote_vampire": Try this: using testIdemo by auto (0.0 ms). 
"spass": The prover derived "False" from "test.distinct(5)" and "testIdemo". 
This could be due to inconsistent axioms (including "sorry"s) or to a bug in Sledgehammer. 
If the problem persists, please contact the Isabelle developers.

これは私が==をいじったせいですか？または、私の公理に他の種類の制限を設定する必要がありますか?

ファローアップ：

どうやら私は等号で遊ぶべきではありません:Pだから私は自分の関係を定義する必要があります。

axiomatization
testEQ ::  "test ⇒ test ⇒ bool" (infixl "=" 1)
  where
reflexive [intro]: "x = x" and
substitution [elim]: "x = y ⟹ B x = B y" and
symmetric : "x = y ⟹ y = x"

したがって、基本的なプロパティを定義する必要があると思います。再帰性、置換、対称性は、最初はいいように思えます。'a => 'a => bool でジェネリックにすることができます

ここで、私は自分の関係をさらに定義します。例にとどまる：

axiomatization
  plus :: "test⇒ test⇒ test" (infixl "+" 35)
where
  commutative:  "x + y         = y + x"  and
  idemo:  "x + x           = x"

a) これは今のところ正しいですか b) ここからどのように進めるか これまでのところ、これが等価点のような補題の下位項に取って代わるとは思いません。

4

1 に答える 1

3

データ型のコンストラクターは常に構造によって異なるため、公理は eg を意味aa = plus aa aaしますが、これは falseです。（参照）thm test.distinct

実際、 を使用する場合はaxiomatization、自分が何をしているのかを本当に理解している必要があります。そのようにして矛盾を導入するのは非常に簡単です。（明らかに）

特定のプロパティを持つタイプが必要な場合は、それを構築する必要があります。たとえば、型の表現型を (たとえばデータ型として) 定義し、それに何らかの等価関係を定義し (つまり、どの値が他のどの値と等しくなければならないか)、「実数」型を商型として定義できます。その関係に対するあなたの表現型の。

于 2016-01-10T21:59:20.577 に答える