在 Isabelle 中引入商类型的固定表示

Question

这个问题最好用一个例子来解释。假设我想证明以下引理：

lemma int_inv: "(n::int) - (n::int) = (0::int)"

我如何非正式地证明这是沿着这些思路的：

引理：n - n = 0，对于任何整数 n 和 0 = abs_int(0,0).

证明：
对于一些固定的自然数 abs_int(a,b) = n a 和 b.
--- 这里有一些复杂而令人兴奋的论点 ---
这意味着足以证明 a+b+0 = a+b+0，这是自反性成立的。
QED.

但是，我在第一步时遇到了问题“令 abs_int(a,b) = n ”。 let 语句似乎不是为此而做的，因为它只允许左侧有一个术语，所以我不知道如何引入变量 a 和 b 在 n.

的任意表示中

如何为商类型引入固定表示，以便我可以使用其中的变量？

注意：我知道上面的陈述可以被auto证明，可以通过将引理重写为“引理int_inv：”[=62来回避问题=](a,b) - Abs_integ(a,b) = (0::int)”。但是，我正在寻找一种通过在证明中引入任意表示来证明的方法。

Answer 1

你可以用定理int.abs_induct引入一个具体的表示。但是，您几乎不想手动执行此操作。

证明商命题的一般方法是先陈述一个关于底层关系的等价定理，然后使用传递工具。如果你的例子没有被自动化自动释放，那将会有所帮助......事实上，让我们创建我们自己的小 int 类型，这样它就不会：

theory Scratch
  imports Main
begin

quotient_type int = "nat × nat" / "intrel"
  morphisms Rep_Integ Abs_Integ
proof (rule equivpI)
  show "reflp intrel" by (auto simp: reflp_def)
  show "symp intrel" by (auto simp: symp_def)
  show "transp intrel" by (auto simp: transp_def)
qed

lift_definition sub :: "int ⇒ int ⇒ int"
  is "λ(x, y) (u, v). (x + v, y + u)"
  by auto

lift_definition zero :: "int" is "(0, 0)".

现在，我们有

lemma int_inv: "sub n n = zero"
  apply transfer

proof (prove)
goal (1 subgoal):
 1. ⋀n. intrel ((case n of (x, y) ⇒ λ(u, v). (x + v, y + u)) n) (0, 0)

所以，我们要证明的版本是

lemma int_inv': "intrel ((case n of (x, y) ⇒ λ(u, v). (x + v, y + u)) n) (0, 0)"
  by (induct n) simp

现在我们可以用

转移它

lemma int_inv: "sub n n = zero"
  by transfer (fact int_inv')

请注意，transfer 证明方法是回溯 — 这意味着它将尝试许多可能的转移，直到其中一个成功。但是请注意，此回溯不适用于单独的 apply 命令。因此，您总是希望将转移证明写成 by transfer something_simple，而不是说 proof transfer.

您可以看到许多可能的版本

apply transfer
back back back back back

另请注意，如果您的定理提到了关于 int 的常数，而这些常数没有用 lift_definition 定义，您将需要单独证明它们的传递规则。有一些这样的例子 here。

一般来说，在定义一个商之后，您会希望尽快“忘记”它的底层结构，通过转移证明足够的属性，这样就可以在不窥视您的类型结构的情况下证明其余部分。

在 Isabelle 中引入商类型的固定表示

Introducing fixed representation for a quotient type in Isabelle

isabelle