代码之家 › 专栏 › 技术社区 › tinlyx

如何陈述《伊莎贝尔》中关于等价物的引理

isabelle

0

tinlyx · 技术社区 · 5 年前

我正试图从它的文档中学习Isabelle符号和语法。特别是,我试图用等价符号来陈述一个引理( equiv 在伊莎贝尔2020的main.pdf中)。

equiv  :: 'a set â ('a Ã 'a) set â bool

引理不一定有用,但我希望语法正确。我试图用以下内容来填补空白,希望说明平等是一种等价关系:

lemma "equiv nat (=)"

尝试未成功,并生成以下错误:

Type unification failed: Clash of types "_ â _" and "_ set"

Type error in application: incompatible operand type

Operator:  equiv :: ??'a set â (??'a Ã ??'a) set â bool
Operand:   nat :: int â nat

我的问题是:

如何正确表述平等的等价性?

更一般地说,如何找到使用基本符号或语法(如Main中的符号或语法)的正确方法?

(我只对这里的符号感兴趣,不一定证明任何东西)

0 回复 | 直到 5 年前

1

Mathias Fleury 5 年前

尝试符号时的第一件关键事情是查看类型或类型错误消息:

Operator:  equiv :: ??'a set â (??'a Ã ??'a) set â bool
Operand:   nat :: int â nat

这表明 nat 具有类型 int â nat ,而 equiv 期望第一个参数具有类型 ?'a set 因此,你希望得到一组自然数,而不是将整数转换为自然数的函数。

如何解决这个问题?要么你已经知道了 UNIV 存在用于此目的,或者您在上搜索示例 Find facts ,基于对名字的一些直觉。

一旦你改变了这一点,你会看到一个类似的平等打字问题,你可以很容易地解决。