伊莎贝尔:公理化和快速检查与自动 solve_direct
Isabelle: Axiomatization and Quickcheck vs auto solve_direct
又是一个意外结果的小例子。
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.
是不是我乱用了==?
或者我需要为我的公理设置一些其他类型的限制吗?
跟进:
显然我不应该玩 equals :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) 如何从这里开始
到目前为止,我认为这不会取代引理中的子项,这有点等价。
你的公理意味着例如aa = plus aa aa
,这是错误的,因为数据类型的构造函数总是不同,在构造上。 (比照thm test.distinct
)
事实上,如果您使用 axiomatization
,您应该真正知道自己在做什么——这样很容易引入不一致。 (显然)
如果你想要一个具有某些属性的类型,你必须构造它。例如,您可以定义您的类型的表示类型(例如作为数据类型),然后在其上定义一些相等关系(即哪些值应该等于其他值)然后将“真实”类型定义为商类型您的表示类型对该关系的影响。
又是一个意外结果的小例子。
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.
是不是我乱用了==? 或者我需要为我的公理设置一些其他类型的限制吗?
跟进:
显然我不应该玩 equals :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) 如何从这里开始 到目前为止,我认为这不会取代引理中的子项,这有点等价。
你的公理意味着例如aa = plus aa aa
,这是错误的,因为数据类型的构造函数总是不同,在构造上。 (比照thm test.distinct
)
事实上,如果您使用 axiomatization
,您应该真正知道自己在做什么——这样很容易引入不一致。 (显然)
如果你想要一个具有某些属性的类型,你必须构造它。例如,您可以定义您的类型的表示类型(例如作为数据类型),然后在其上定义一些相等关系(即哪些值应该等于其他值)然后将“真实”类型定义为商类型您的表示类型对该关系的影响。