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

Question

我试图证明以下关于双射函数的反函数存在的基本定理（用 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

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

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

2. 如何扩展相关定义，然后用函数应用对其进行简化。我遵循了一些关于应用样式 simp 和结构化样式 Isar 证明的 Isabelle (2021) 示例/教程，但无法流利地使用 Isar 证明。一旦我开始证明命令，我不知道如何简化或进一步移动。

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

有人可以帮忙解释一下上述关于反函数的存在性证明是如何完成的吗？

Answer 1

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。后者在x∈B 上返回id x，否则在undefined 上返回。所以为了使这个相等成立，g 需要在f 的输入不在B 中时输出undefined。但是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))"

（顺便说一句，这仍然是错误的，正如 quickcheck 在 Isabelle/jEdit 中告诉我的那样，请参阅输出窗口。如果 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 是“the”x 这样f x = y。 （然后在稍后的证明中，您将遇到证明它确实存在并且它是唯一的证明义务。）参见Hilbert_Choice.thy 中inv_into 的定义（除了它使用SOME 而不是THE）。也许对于初学者来说，尝试仅使用现有的inv_into 常量进行证明。

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

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

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

Answer 2

我同意 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] 的文章From Types to Sets by Local Type Definition in Higher-Order Logic。该框架还存在一个大规模应用示例[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） 关于 apply 风格的 simp 和结构化的示例/教程 风格 Isar 证明，但不能流利地使用 Isar 证明。有一次，我 启动了证明命令，我不知道如何简化或移动任何 进一步。

我相信，学习您正在尝试学习的内容的最佳方法是遵循 Tobias Nipkow 和 Gerwin Klein [5] 所著的具体语义一书中的练习。此外，我还会查看 Tobias Nipkow 等人 [6] 的 A Proof Assistant for Higher-Order Logic（它有点过时了，但我发现它特别适合学习 apply-样式脚本/直接规则应用程序）。顺便说一句，我主要是从这些书中自学 Isabelle，而没有任何正式方法方面的经验。

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

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

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

参考文献

1. Avigad J、Lewis RY 和 van Doorn F. 逻辑与证明。
2. Jech T. 集合论。第三版。海德堡：斯普林格； 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 的具体语义。海德堡：施普林格出版社； 2017. (http://concrete-semantics.org/)
6. Nipkow T、Paulson LC、Wenzel M. 高阶逻辑证明助手。海德堡：施普林格出版社； 2017 年。