伊莎贝尔:公理化和快速检查与自动解决直接

Question

又是一个小例子，结果出乎意料。

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) 如何从这里继续 到目前为止，我认为这不会取代引理中的子项，这有点等价。

Answer 1

你的公理意味着例如aa = plus aa aa，这是错误的，因为数据类型的构造函数在构造上总是不同。 (参见thm test.distinct)

事实上，如果您使用公理化，您应该真正知道自己在做什么 - 这样很容易引入不一致。 (显然)

如果你想要一个具有某些属性的类型，你必须构造它。例如，您可以定义您的类型的表示类型(例如作为数据类型)，然后在其上定义一些相等关系(即哪些值应该等于其他值)，然后将“实数”类型定义为商类型您对该关系的表示类型。