如何证明 Isabelle/HOL 中反函数的存在？

编程问答 2022-05-11

问题描述

我正在尝试证明以下关于双射函数反函数存在的基本定理（与 Isabelle/HOL 一起学习定理证明）：

对于任何集合 S 和它的恒等映射 1_S，α:S→T 是双射的，当条件是 存在一个映射 β：T→S，使得 βα=1_S 和 αβ=1_S。

以下是我在尝试定义相关事物（包括 functions 和 their inverses）后到目前为止的结果。但由于我对 Isabelle 和/或 Isar 缺乏了解，我陷入了困境，无法取得太大进展。

theory Test
  imports  Main 
    "HOL.Relation"
begin

    lemma bij_iff_ex_identity : "bij_betw f A B ⟷ (∃ g. g∘f = restrict id B ∧ f∘g = restrict id A)" 
      unfolding bij_betw_def inj_on_def restrict_def iffI 
    proof
      let ?g = "restrict (λ y. (if f x = y then x else undefined)) B"
      assume "(∀x∈A. ∀y∈A. f x = f y ⟶ x = y)"
      have "?g∘f = restrict id B"
      proof
      (* cannot prove this *)

end

在上面，我试图给出一个明确的存在证明（即原始函数 g 的反函数 f）。我有几个关于证明的问题。

  1. 概念是否在 Isabelle 术语中定义正确（函数、反函数等）。

  2. 如何展开相关的定义，然后用功能应用来简化。我遵循了一些 Isabelle (2021) 示例/教程，其中包括应用式 simp 和结构式 Isar 证明，但无法流畅地使用 Isar 证明。一旦我启动了 proof 命令，我不知道如何简化或进一步移动。

  3. Isar 有新的 assumes ... shows ... 方法来陈述定理。是否有类似的支持来证明 iff (⟷) 就像上面的例子一样？没有它，就无法访​​问 assms 等，并且在证明过程中是否需要assume 除结论外的所有内容。

谁能帮忙解释一下上面关于反函数的存在证明是如何完成的？

解决方法

lemma bij_iff_ex_identity : "bij_betw f A B ⟷ (∃ g. g∘f = restrict id B ∧ f∘g = restrict id A)"

我认为这不是您想要的，我怀疑这是真的。 g∘f = restrict id B 并不意味着 g∘f 和 id 在 B 上相等。这意味着总函数g∘f（并且HOL中只有总函数）等于总函数restrict id B。后者在 id x 上返回 x∈B，否则返回 undefined。因此，要使此等式成立，只要 g 的输入不在 undefined 中，f 需要输出 B。但是g怎么会知道！

如果你想使用restrict，你可以写restrict (g∘f) B = restrict id B。但就我个人而言，我宁愿选择更简单的 (∀x∈B. (g∘f) x = x)。

所以修正后的定理是：

lemma bij_iff_ex_identity : "bij_betw f A B ⟷ (∃ g. (∀x∈A. (g∘f) x = x) ∧ (∀y∈B. (f∘g) y = y))"

（顺便说一下，这仍然是错误的，正如在 Isabelle/jEdit 中 quickcheck 告诉我的那样，查看输出窗口。如果 A 有一个元素并且 B 为空，f不能是双射。所以你正在尝试的定理实际上在数学上是不正确的。我不会试图修复它，而只是回答剩下的几行。

unfolding bij_betw_def inj_on_def restrict_def iffI

此处的 iffI 无效。展开只能应用 A = B 形式的定理（无条件重写规则）。 iffI 不是那种形式。 （使用 thm iffI 查看。）

proof

就我个人而言，我不使用裸形式 proof，而是始终使用 proof - 或 proof (some method)。因为 proof 只是应用了一些默认的方法（在这种情况下，相当于 (rule iffI)，所以我认为最好让它显式。proof - 只是开始证明而不应用额外的方法。

let ?g = "restrict (λ y. (if f x = y then x else undefined)) B"

这里有一个未绑定的变量 x。 （注意 IDE 中的背景颜色。）这很可能不是您想要的。形式上，它是允许的，但 x 将被视为某个任意常数。

一般来说，我认为没有任何方法可以以简单的方式定义 g（即，仅使用量词和函数应用程序以及 if-then-else）。我认为定义逆（即使您知道它存在）的唯一方法是使用 THE 运算符，因为您需要说 g y 之类的东西是“该”x使得 f x = y。 （然后在后面的证明中，您将遇到一个证明义务，即它确实存在并且它是唯一的。）参见 inv_into 中 Hilbert_Choice.thy 的定义（除了它使用 SOME not THE）。也许对于初学者来说，尝试仅使用现有的 inv_into 常量进行证明。

assume "(∀x∈A. ∀y∈A. f x = f y ⟶ x = y)"

所有 assume 命令必须具有与证明目标中完全相同的假设。您可以通过临时编写命令 show A for A 来测试您是否写对了（这是一个无法证明的目标，但是会完成证明，因此它会欺骗 Isabelle 检查它是否正确）。如果此命令没有给出错误，则您的 assume 是正确的。在您的情况下，您没有，它应该是 (∀x∈A. ∀y∈A. f x = f y ⟶ x = y) ∧ f ' A = B。 （' 是这里的反引号符号。标记不允许我写它。）

我的建议：首先尝试使用 bij 而不是 bij_betw 的证明。 （如果你想作弊，一个方向是 BNF_Fixpoint_Base.o_bij。） 完成后，您可以尝试概括。

,

我同意 Dominique Unruh 提供的富有洞察力的评论。但是，我想提一下，Isabelle/HOL 主库的源代码中已经存在一个定理，该定理捕获了您试图证明的定理背后的思想。事实上，它至少以两种不同的格式存在：让我将它们命名为传统的 Isabelle/HOL 格式和规范的 FuncSet 格式。对于前一个，请参见定理 bij_betw_iff_bijections：

"bij_betw f A B ⟷ (∃g. (∀x ∈ A. f x ∈ B ∧ g(f x) = x) ∧ (∀y ∈ B. g y ∈ A ∧ f(g y) = y))"

FuncSet 的情况稍微复杂一些。似乎不存在一个单一的定理来捕捉这个想法。然而，定理 bij_betwI、bij_betw_imp_funcset 和 inv_into_funcset 一起几乎等同于您试图陈述的定理。让我提供一个草图，说明如何以一种在 FuncSet 意义上被认为是合理规范的方式表达这个定理（尝试自己证明）：

lemma bij_betw_iff:
  shows "bij_betw f A B ⟷
    (
      ∃g.
        (∀x. x∈A ⟶ g (f x) = x) ∧
        (∀y. y∈B ⟶ f (g y) = y) ∧
        f ∈ A → B ∧
        g ∈ B → A
    )"
sorry

我还想重复 Dominique Unruh 给出的建议并提供一些补充说明：

我的建议：首先尝试使用 bij 而不是 bij_betw 的证明。

确实，这是一个非常好的主意。一般来说，通过尝试将问题限制在明确定义的集合 A 和 B，而不是直接处理类型，您触及了一个称为 相对化 的主题逻辑。例如，对于一个温和的外行人的介绍，请参见 https://leanprover.github.io/logic_and_proof/first_order_logic.html [1]，对于在集合论的上下文中稍微更彻底的介绍，请参见 [2，第 12 章]。正如您现在可能已经注意到的那样，在 Isabelle/HOL 中相对化定理并不容易，并且需要额外的证明工作。 然而，存在 Isabelle/HOL 的扩展，允许定理相对化过程的自动化。有关此扩展的更多信息，请参阅 Ondřej Kunčar 和 Andrei Popescu [3] 的文章从高阶逻辑中的本地类型定义到集合。还存在该框架的大规模应用实例[4]。独立地，我正在努力使这个扩展更加用户友好，并且非常缓慢地接近我努力的最后阶段：见 https://gitlab.com/user9716869/tts_extension。因此，原则上，如果你知道如何使用 Types-To-Sets 并接受它的公理，那么用 bij 证明定理就足够了，例如，

"bij f ⟷ (∃g. (∀x. g (f x) = x) ∧ (∀y. f (g y) = y))",

那么，定理如 bij_betw_iff_bijections 和 bij_betw_iff 可以通过点击一个按钮（几乎......）自动自动合成。

最后，为了完整起见，让我就您的疑问提供我自己的建议（尽管正如我所提到的，我同意 Dominique Unruh 所说的一切）

如何展开相关定义，然后用 功能应用。我关注了一些伊莎贝尔 (2021) 有关应用式 simp 和结构化的示例/教程 样式 Isar 证明但不能流畅地使用 Isar 证明。有一次，我 启动了证明命令，我不知道如何简化或移动任何 进一步。

我相信，学习您正在尝试学习的内容的最佳方法是通过 Tobias Nipkow 和 Gerwin Klein [5] 所著的具体语义一书中的练习进行练习。此外，我还会阅读 Tobias Nipkow 等人的高阶逻辑证明助手 [6]（它有点过时，但我发现它特别适用于学习{{1} } 样式的脚本/直接规则应用程序）。顺便说一下，我大部分时间都是从这些书中自学的 Isabelle，没有任何形式方法方面的经验。

Isar 有一种新的假设方式......显示......来陈述定理。 是否有类似的支持证明 iff 的 (⟷) 像上面的例子一样？ 没有它，就无法访​​问 assms 等，是否有必要 在证明过程中假设除结论外的所有内容。

我会让 Dominique Unruh 给出的建议更加明确：为此使用 apply 或 rule iffI。

编辑。当您使用 intro iffI（或类似的）开始您的结构化 Isar 证明时，您需要为每个子目标明确陈述您的假设（使用 rule iffI 范式）。但是，有一种工具可以自动生成此类样板 Isar 代码。它被称为 Sketch-and-Explore，您可以在 Isabelle/HOL 主库的目录 assume ... show ... 中找到它。在这种情况下，您只需输入 HOL/ex，就会为每个子目标自动生成 sketch(rule iffI)/assume 范式。

参考资料

  1. Avigad J、Lewis RY 和 van Doorn F. 逻辑与证明。
  2. Jech T. 集合论。第 3 版。海德堡：斯普林格； 2006.（纯数学和应用数学，系列专着和教科书）。
  3. Kunčar O、Popescu A. 从高阶逻辑中的局部类型定义从类型到集合。自动推理杂志。 2019;62(2):237–60。
  4. Immler F、Zhan B。Isabelle/HOL 中线性代数集的平滑流形和类型。在：第 8 届 ACM SIGPLAN 国际认证程序和证明会议。纽约：ACM； 2019 年。 65-77。 （CPP 2019）。
  5. Nipkow T、Klein G. 与 Isabelle/HOL 的具体语义。海德堡：Springer-Verlag； 2017. (http://concrete-semantics.org/)
  6. Nipkow T、Paulson LC、Wenzel M。高阶逻辑的证明助手。海德堡：Springer-Verlag； 2017.