尝试像集合和子集一样对待类型类和子类型 [英] Trying to Treat Type Classes and Sub-types Like Sets and Subsets

查看：52 发布时间：2021/7/23 19:15:13 types typeclass set isabelle

本文介绍了尝试像集合和子集一样对待类型类和子类型的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！

问题描述

这个问题与我之前的 SO 问题有关类型类.我问这个问题是为了设置一个关于语言环境的未来问题.我不认为类型类对我正在尝试做的事情有用，但是类型类的工作方式让我知道我想从语言环境中获得什么.

下面，当我使用大括号表示法{0,0}时，它不代表正常的HOL大括号，而0代表空集.>

如果你想要一些文件

A_i130424a.thy友好的你.
i130424a.thy - 非-ASCII 友好 THY.
i130424a_DOC.pdf - PDF 显示行号.立>
MFZ_DOC.pdf - 与此相关的主要项目.
此问题的 GitHub 文件夹和 MFZ GitHub 文件夹.

问题前谈话

我在 THY 中描述了我正在做的事情(包括在底部)，然后我基本上会问，我可以在这里做些什么来解决这个问题，以便我可以使用类型类?"

正如在上面链接的 SO 问题中一样，我试图与 Groups.thy semigroup_add.我所做的是使用 typedef 创建我的类型 sT 的子类型，然后我尝试将我的一些基本函数常量和运算符提升到新类型中，例如我的联合运算符geU，我的空集emS，我的无序对集paS，以及我的成员谓词inP.

这不起作用，因为我试图将新类型视为子集.特别是，我的新类型应该表示集合 { {0,0} }，它旨在成为平凡半群的一部分，一个只有一个元素的半群.

问题是无序对公理指出如果集合x存在，则集合(paS xx)存在，并且联合公理指出如果集合x>x 存在，则设置 (geU x) 存在.因此，当我尝试将联合运算符提升为我的新类型时，证明者神奇地知道我需要证明 (geU{0,0} = {0,0})，但事实并非如此，但是在我的新类型中只有一个元素 {0,0}，所以必须是这样.

问题

我能解决这个问题吗?在我看来，我将集合和子集与类型和子类型进行比较，我知道它们并不相同.调用我的主类型 sT 和我的子类型 subT.我需要的是所有已定义为 sT 类型的运算符，例如 sT =>sT，当 subT 被视为类型 sT 时，为 subT 类型工作.使用 subT 类型定义的新运算符和常量，例如 subT => 类型的函数；subT，这会以某种方式解决，就像事情神奇地应该与这些事情一起工作一样.

发表问题谈话

在这里，我通过 THY 中的行号指出发生了什么.行号将显示在 PDF 和 GitHub 站点上.

在第 21 行到第 71 行中有四个部分，我将相关的常数、符号和公理结合起来.

输入 sT、成员谓词 inP/PIn 和等式公理(21 到 33).
空集 emS/SEm 和空集公理(37 到 45).
无序对常数 paS/SPa 和无序对公理(49 到 58).
联合常数 geU/UGe 和联合公理(62 到 71).

从第 75 行开始，我使用 typedef 创建一个新类型，然后将其实例化为类型类 semigroup_add.

在我尝试解除我的无序对函数 {.x,y.}，第 108 行和我的联合函数 (geU x) 之前，没有任何问题，第 114 行.

在 Isar 命令下方，我显示的输出告诉我我需要证明某些集合等于 {0,0}，这是无法证明的事实.

这是 ASCII 友好的源代码，我从上面链接的 THY 中删除了一些注释和行:

理论 A_i130424a进口 Complex_Main开始--AXIOM(sT 类型、inP 谓词和等式公理)"typedecl sT ("sT")consts PIn :: "sT => sT => bool"符号PIn ("in'_P") 和PIn(中缀inP"51)和PIn(中缀inP"51)公理化其中Ax_x:(！x.x inP r <-> x inP s)<->(r = s)"- [结尾]"--"AXIOM (emS 和空集公理)"consts SEm :: "sT" ("emS")符号(输入)SEM(emS")公理化其中Ax_em [simp]: "(x niP emS)"- [结尾]"--"AXIOM (paS 和无序对公理)"consts SPa :: "sT => sT => sT"符号SPA(paS")和SPA ("({.(_),(_).})")公理化其中Ax_pa [simp]: "(x inP {.r,s.}) <-> (x = r | x = s)"- [结尾]"--AXIOM(geU 和联合公理)"consts UGe :: "sT => sT"符号UGe(geU")和UGe(geU")公理化其中Ax_un: "x inP geU r = (? u.x inP u & u inP r)"- [结尾]"--"EXAMPLE (一个 typedef 类型不能被视为一组类型 sT)"typedef tdLift = "{x::sT.x = {.emS,emS.}}"通过(简单)setup_lifting type_definition_tdLift实例化 tdLift :: semigroup_add开始Lift_definition plus_tdLift::tdLift => tdLift => tdLift"是 "% x y. {.emS,emS.}" by(simp)实例证明修复 n m q :: tdLift显示(n + m) + q = n + (m + q)"通过(转移，简单)qed结尾定理"((n::tdLift) + m) + q = n + (m + q)"通过(转移，简单)类 tdClass =修复 emSc :: "'a" ("emSk")修正 inPc :: "'a => 'a => bool" (中缀 "∈k" 51)修复 paSc :: "'a => 'a => 'a" ("({.(_),(_).}k)")修复 geUc :: "'a => 'a" ("⋃k")实例化 tdLift :: tdClass开始Lift_definition inPc_tdLift::"tdLift => tdLift => bool"是% x y.x inP y"通过(简单)Lift_definition paSc_tdLift::tdLift => tdLift => tdLift"是% x y.{.x,y.}"--"输出: 1. (!! (sT1 sT2). ([|(sT1 = emS); (sT2 = emS)|] ==> ({.sT1,sT2.} = emS)))"应用(自动)--"输出:1. ({.emS.} = emS)"哎呀Lift_definition geUc_tdLift::tdLift => tdLift"是% x.geU x"--"输出:1. (!! sT. ((sT = {.emS,emS.}) ==> ((geU sT) = {.emS,emS.})))"应用(自动)--"输出:1. ((geU {.emS,emS.}) = {.emS,emS.})"哎呀Lift_definition emSc_tdLift::"tdLift"是emS"- 输出:异常 THM 1 引发(drule.ML 的第 333 行):RSN:没有统一者(?t = ?t) [名称 HOL.refl]((emS = {.emS,emS.}) ==> (Lifting.invariant (% x. (x = {.emS,emS.})) emS emS))"哎呀实例 ..结尾- [结尾]"结尾

解决方案

我部分回答了我的问题，部分原因是在我提出有关 Isar 子类型的问题时参考这个.从表面上看，我在这里的问题和答案与子类型有关.

至于我是否可以解决我描述的类型类的问题，我不知道.

(更新:我使用类型类的可能解决方案将是多种想法的组合，解决方案的一部分是类型强制，如对我的 SO 问题的回答中所述:什么是 Isabelle/HOL 子类型?哪些 Isar 命令会产生子类型?

如果使用 Groups.thy 中的语言环境对我来说是一种方法，那么这些语言环境的相应类型类也可能会起作用.我可以实例化一个类，例如 semigroup_add，使用 lift_definition 来定义 plus 运算符，甚至取消返回 bool 的运算符 进入类型.无论如何，不能被提升到新类型的运算符在新类型的上下文中有点荒谬，其中类型强制可以发挥作用，使它们对集合的并集之类的事情有意义.魔鬼在细节中.)

根据我所说的我想要的类型和子类型，我发现我确实使用 typedef 获得了一种形式，该形式是函数 Rep 和 Abs，我一直在使用它.

如 isar-ref 中所述.pdf 页.242,

<块引用>

对于 typedef t = A，新引入的类型 t 伴随着一对态射，将其与旧类型的表示集相关联.默认情况下，从类型到集合的注入称为 Rep t 及其逆 Abs t...

下面，我在一个小例子中使用 Rep 和 Abs 来证明我可以将我的主要类型 sT 与新的类型我用 typedef 定义，也就是类型 tsA.

我不认为类型类是最重要的.我正在探索两件主要的事情，

我是否可以绑定到 Groups.thy 的语言环境，
更普遍的是使用类型来限制我的半群、群等的二元运算符的域和共域.

例如，在 Groups.thy 中，有

locale semigroup =修正 f :: "'a => 'a => 'a" (infixl "*" 70)假设 assoc [ac_simps]:a * b * c = a * (b * c)"

如果我不使用子类型，我想我将不得不做这样的事情，其中 inP 是我的 \<in>(我是刚从语言环境开始):

locale sgA =修复 G :: sT修正 f :: "sT => sT => sT" (infixl "*" 70)假设关闭:"(a inPG) & (b inPG) --> (a * b) inPG"假设关联:(a inPG) & (b inPG) & (c inPG) --> (a * b) * c = a * (b * c)"

能够使用 Groups.semigroup 的部分答案可能是使用 Rep 和 Abs；我使用 tsA => 类型的运算符tsA＝＞tsA 在 tsA 类型上，但是当 tsA 类型的元素需要被视为 sT 类型的元素时，那么我使用Rep 将它们映射到类型 sT.

我还没有考虑所有这些，也没有进行足够的实验来知道什么最有效，但我给出了这个部分答案是为了尝试解释更多我的想法.可能会有其他人提供一些好的信息要添加.

子类型方法可能并不完全有利，如下面示例代码中的最后两个 theorem 命令所示.左边的含义是必要的，因为我没有利用类型的力量，类似于上面 locale sgAclosed 和 assoc>.然而，尽管如此，我的 simp 规则没有问题，而使用 Rep 和 Abs 的定理需要 metis 用于证明，它可能需要大量丑陋的开销才能使事情更顺畅.

下面我包含文件 A_iSemigroup_xp.thy.这是 iSemigroup_xp.thy.这些需要导入 MFZ.thy，这 3 个文件位于此 GitHub 文件夹中.

理论 A_iSemigroup_xp进口MFZ开始- [结尾]"--示例(平凡半群的可能子类型)"typedef tsA = "{x::sT.x = emS}"通过(简单)定理(Rep_tsA x) inP {.Rep_tsA x.}"通过(梅蒂斯SSi_exists)定理！x::tsA.x = (Abs_tsA emS)"by(metis(提升，full_types)Abs_tsA_casesmem_Collect_eq)定理！x.x inP {.emS.} --> x = emS"通过(简单)定理！x.x inP {.z inP {.emS.} | z = emS.} --> x = emS"通过(简单)- [结尾]"——《ISAR(理论终结)》结尾

This question is related to my previous SO question about type classes. I ask this question to set up a future question about locales. I don't think type classes will work for what I'm trying to do, but how type classes work have given me ideas about what I want out of locales.

Below, when I use the braces notation {0,0}, it doesn't represent the normal HOL braces, and 0 represents the empty set.

Some files if you want them

A_i130424a.thy - ASCII friendly THY.
i130424a.thy - non-ASCII friendly THY.
i130424a_DOC.pdf - PDF showing line numbers.
MFZ_DOC.pdf - Main project this is related to.
GitHub folder for this question and MFZ GitHub folder.

Pre-question talk

I describe what I'm doing in the THY (which I include at the bottom), and then I basically ask, "Is there something I can do here to fix this so that I can use type classes?"

As in the SO question linked to above, I'm trying to tie into Groups.thy semigroup_add. What I do is create a subtype of my type sT using typedef, and I then try to lift some of my essential function constants and operators into the new type, such as my union operator geU, my empty set emS, my unordered pair sets paS, and my membership predicate inP.

This doesn't work because I'm trying to treat the new type like a subset. In particular, my new type is supposed to represent the set { {0,0} }, which is intended to be part of the trivial semigroup, a semigroup with only one element.

The problem is that the unordered pair axiom states that if set x exists, then set (paS x x) exists, and the union axiom states that if set x exists, then set (geU x) exists. So, when I try to lift my union operator into my new type, the prover magically knows I need to prove (geU{0,0} = {0,0}), which is not true, but there's only one element {0,0} in my new type, so it would have to be that way.

Question

Can I fix this? In my mind, I'm comparing sets and subsets with types and sub-types, where I know they're not the same. Call my main type sT and my subtype subT. What I need is for all my operators that have been defined with type sT, types such as sT => sT, to work for type subT when subT is being treated as type sT. The new operators and constants that have been defined using type subT, such as a function of type subT => subT, that would somehow work out like things are magically supposed to work with these things.

Post question talk

Here, I point out what's happening by line number in the THY. The line numbers will show up in the PDF and on the GitHub site.

In lines 21 to 71 there are four sections where I combined related constants, notation, and an axiom.

Type sT, membership predicate inP/PIn, and equality axiom (21 to 33).
Empty set emS/SEm and empty set axiom (37 to 45).
Unordered pair constant paS/SPa and unordered pair axiom (49 to 58).
Union constant geU/UGe and union axiom (62 to 71).

Starting at line 75 is where I create a new type with typedef and then instantiate it as type class semigroup_add.

There are no problems until I try to lift my unordered pair function {.x,y.}, line 108, and my union function (geU x), line 114.

Below the Isar commands, I show the output that's telling me I need to prove that certain sets are equal to {0,0}, a fact that cannot be proved.

Here is the ASCII friendly source, where I've deleted some comments and lines from the THY linked to above:

theory A_i130424a
imports Complex_Main 
begin  

--"AXIOM (sT type, inP predicate, and the equality axiom)"
typedecl sT ("sT")

consts PIn :: "sT => sT => bool"

notation
  PIn  ("in'_P") and
  PIn  (infix "inP" 51) and
  PIn  (infix "inP" 51)

axiomatization where
  Ax_x: "(! x. x inP r <-> x inP s) <-> (r = s)"
--"[END]"



--"AXIOM (emS and the empty set axiom)"
consts SEm :: "sT" ("emS")

notation (input)
  SEm ("emS")

axiomatization where
  Ax_em [simp]: "(x niP emS)"
--"[END]"



--"AXIOM (paS and the axiom of unordered pairs)"
consts SPa :: "sT => sT => sT"

notation
  SPa ("paS") and
  SPa ("({.(_),(_).})")

axiomatization  where
  Ax_pa [simp]: "(x inP {.r,s.}) <-> (x = r | x = s)"
--"[END]"



--"AXIOM (geU and the axiom of unions)"
consts UGe :: "sT => sT"

notation
  UGe ("geU") and
  UGe ("geU")

axiomatization where
  Ax_un: "x inP geU r = (? u. x inP u & u inP r)"
--"[END]"



--"EXAMPLE (A typedef type cannot be treated as a set of type sT)"
typedef tdLift = "{x::sT. x = {.emS,emS.}}"
  by(simp)

setup_lifting type_definition_tdLift

instantiation tdLift :: semigroup_add
begin
  lift_definition plus_tdLift:: "tdLift => tdLift => tdLift"
    is "% x y. {.emS,emS.}" by(simp)
  instance
  proof
    fix n m q :: tdLift
    show "(n + m) + q = n + (m + q)"
    by(transfer,simp)
  qed
end

theorem
  "((n::tdLift) + m) + q = n + (m + q)"
  by(transfer,simp)

class tdClass =
  fixes emSc :: "'a"                 ("emSk")
  fixes inPc :: "'a => 'a => bool"   (infix "∈k" 51)
  fixes paSc :: "'a => 'a => 'a"     ("({.(_),(_).}k)")
  fixes geUc :: "'a => 'a"           ("⋃k")

instantiation tdLift :: tdClass
begin
  lift_definition inPc_tdLift:: "tdLift => tdLift => bool"
    is "% x y. x inP y" 
    by(simp)
  lift_definition paSc_tdLift:: "tdLift => tdLift => tdLift"
    is "% x y. {.x,y.}"
    --"OUTPUT: 1. (!! (sT1 sT2). ([|(sT1 = emS); (sT2 = emS)|] ==> ({.sT1,sT2.} = emS)))"
    apply(auto)
    --"OUTPUT: 1. ({.emS.} = emS)"
    oops
  lift_definition geUc_tdLift:: "tdLift => tdLift"
    is "% x. geU x"
    --"OUTPUT: 1. (!! sT. ((sT = {.emS,emS.}) ==> ((geU  sT) = {.emS,emS.})))"
    apply(auto)
    --"OUTPUT: 1. ((geU  {.emS,emS.}) = {.emS,emS.})"
    oops  
  lift_definition emSc_tdLift:: "tdLift"
    is "emS" 
    --"OUTPUT: 
       exception THM 1 raised (line 333 of drule.ML):
       RSN: no unifiers
       (?t = ?t) [name HOL.refl]
       ((emS = {.emS,emS.}) ==> (Lifting.invariant (% x. (x = {.emS,emS.})) emS emS))"
    oops
  instance ..
end
--"[END]"


end

解决方案

I partially answer my question, and part of the reason is to refer to this when I ask a question about Isar subtypes. By all appearances, my question and answer here is related to subtypes.

As to whether I can fix the problem with type classes that I described, I don't know about that.

(UPDATE: The likely solution for my use of type classes will be a combination of ideas, part of the solution being type coercion, as explained in the answer to my SO question: What is an Isabelle/HOL subtype? What Isar commands produce subtypes?

If using the locales in Groups.thy is the way to go for me, then the corresponding type classes to those locales will probably also work. I can instantiate a class such as semigroup_add, use lift_definition to define the plus operator, and even lift my operators that return a bool into the type. The operators that can't be lifted into the new type are somewhat nonsensical in the context of the new type anyway, wherein type coercion can come into play to make sense of them for things like unions of sets. The devil is in the details.)

With what I said I want out of types and subtypes, I figured out I do get a form of that with typedef, the form being the functions Rep and Abs, which I have been working with a little.

As described in isar-ref.pdf pg. 242,

For typedef t = A the newly introduced type t is accompanied by a pair of morphisms to relate it to the representing set over the old type. By default, the injection from type to set is called Rep t and its inverse Abs t...

Below, I use Rep and Abs in a small example to demonstrate that I can relate my main type, sT, with the new type I define with typedef, which is type tsA.

I don't think type classes are of ultimate importance. There are two main things I'm exploring,

whether I can tie into the locales of Groups.thy,
where that is more generally about using types to restrict the domain and co-domain of the binary operators of my semigroups, groups, etc.

For example, in Groups.thy, there is

locale semigroup =
  fixes f :: "'a => 'a => 'a" (infixl "*" 70)
  assumes assoc [ac_simps]: "a * b * c = a * (b * c)"

If I don't use subtypes, I think I'll have to do something like this, where inP is my \<in> (I'm just starting with locales):

locale sgA =
  fixes G :: sT
  fixes f :: "sT => sT => sT" (infixl "*" 70)
  assumes closed:
    "(a inP G) & (b inP G) --> (a * b) inP G"
  assumes assoc:
    "(a inP G) & (b inP G) & (c inP G) --> (a * b) * c = a * (b * c)"

Part of the answer in being able to use Groups.semigroup could be the use of Rep and Abs; I use the operator of type tsA => tsA => tsA on type tsA, but when the elements of type tsA need to be treated as elements of type sT, then I use Rep on them to map them to type sT.

I haven't thought all this out or experimented enough to know what will work best, but I gave this partial answer to try and explain more of what I have in my mind. There might be someone else out there with some good information to add.

The subtypes approach may not be all upside, as shown below by the last two theorem commands in the example code. The left-hand side of the implications are necessary because I'm not exploiting the power of types, similar to closed and assoc above in locale sgA. However, in spite of that, it's no problem for my simp rules, whereas, the theorems that are using Rep and Abs are requiring metis for the proofs, and it might require a lot of ugly overhead to get things working smoother.

Below I include the file A_iSemigroup_xp.thy. This is an ASCII version of iSemigroup_xp.thy. These require the import of MFZ.thy, where these 3 files are in this GitHub folder.

theory A_iSemigroup_xp
imports MFZ
begin
--"[END]"

--"EXAMPLE (Possible subtype for a trivial semigroup)"
typedef tsA = "{x::sT. x = emS}"
  by(simp)

theorem "(Rep_tsA x) inP {.Rep_tsA x.}"
  by(metis 
    SSi_exists)

theorem "! x::tsA. x = (Abs_tsA emS)"
  by(metis (lifting, full_types) 
    Abs_tsA_cases 
    mem_Collect_eq)

theorem "! x. x inP {.emS.} --> x = emS"
  by(simp)

theorem "! x. x inP {.z inP {.emS.} ¦ z = emS.} --> x = emS"
  by(simp)
--"[END]"

--"ISAR (Theory end)"
end

这篇关于尝试像集合和子集一样对待类型类和子类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！

查看全文

尝试像集合和子集一样对待类型类和子类型 [英] Trying to Treat Type Classes and Sub-types Like Sets and Subsets

问题描述

如果你想要一些文件

问题前谈话

问题

发表问题谈话

Some files if you want them

Pre-question talk

Question

Post question talk

相关文章

其他开发最新文章

热门教程

热门工具

登录关闭

尝试像集合和子集一样对待类型类和子类型 [英] Trying to Treat Type Classes and Sub-types Like Sets and Subsets

问题描述

如果你想要一些文件

问题前谈话

问题

发表问题谈话

Some files if you want them

Pre-question talk

Question

Post question talk

相关文章

其他开发最新文章

热门教程

热门工具

登录 关闭

登录关闭