要求澄清伊莎贝尔理论中涉及自然数的理论中明显的实强制的出现

Posted 2023-02-23

【中文标题】要求澄清伊莎贝尔理论中涉及自然数的理论中明显的实强制的出现

【英文标题】：request clarification on appearance of apparent real coercion in theory involving natural numbers in Isabelle theory

【发布时间】：2021-04-26 10:41:29

【问题描述】：

我正在 Isabelle2020 /jEdit 中研究以下理论：

theory Sqrt
imports Complex_Main "HOL-Computational_Algebra.Primes"
begin

theorem
  assumes "prime (p::nat)"
  shows "sqrt p ∉ ℚ"
proof
  from ‹prime p› have p: "1 < p" by (simp add: prime_nat_iff)
  assume "sqrt p ∈ ℚ"
  then obtain m n :: nat where
      n: "n ≠ 0" and sqrt_rat: "¦sqrt p¦ = m / n"
    and "coprime m n" by (rule Rats_abs_nat_div_natE)

[we omit the remainder of the proof]

输出窗格显示证明状态：

have (⋀m n. n ≠ 0 ⟹ ¦sqrt (real p)¦ = real m / real n ⟹ coprime m n ⟹ ?thesis) ⟹ ?thesis 
proof (state)
this:
    n ≠ 0
    ¦sqrt (real p)¦ = real m / real n
    coprime m n

goal (1 subgoal):
 1. sqrt (real p) ∈ ℚ ⟹ False

我的问题是：这些“真实”的外观是类型强制吗？我已经阅读了第 8 章，讨论了 Isabelle 分布附带的所谓教程中的类型（标题为 A Proof Assistant for Higher-Order Logic）。我阅读了 Florian Haftman 的文档标题 Isabelle/HOL 类型类层次结构（也是 Isabelle 发行版的一部分）。上述理论陈述中使用的规则Rats_abs_nat_div_natE 是Real.thy 理论中的一个引理。

我追查了该理论文件中的参考资料，并查看了 A Proof 中的 §8.4.5 高阶逻辑助手，我发现自然 数字类型nat 是线性有序半环，类型int 是有序环， 并且类型 real 是一个有序字段。属性可能不适用于特定的类，例如，对于类型 nat，不存在涉及减法的抽象属性（因为当然，最终可能会得到一个负数，这不是自然数）。取而代之的是，提供了针对 nat 类型的减法的特定定理。更重要的是，“所有涉及除法的抽象属性都需要一个字段。”（A Proof Assistant for Higher-Order Logic.）

所以，我们是否在这里看到了一种商类型，用于将自然或整数类型的除法提升为抽象实类型以满足该字段 要求（参见 §11.9 Isabelle/Isar 参考手册）？商类型 real 是根据 Real.thy 文件中的等价关系定义 realrel 创建的。

我很惊讶在证明中看到实数取决于素数、正整数和有理数，并想确保我至少已经接近解释为什么会在 Isabelle 证明中发生这种情况。

【参考方案1】：

函数sqrt 仅在实数上定义。因此，您需要将其参数p 从nat 转换为real。有一种强制为您自动执行此操作；因此你可以使用real 函数。

之后，输入m/n 的唯一方法是real m / real n。

一般来说，重载的语法对于证明助手来说是个问题。例如，纸上的2/3 可以是 Isabelle 中的有理数 Fract 2 3、实数 2/3，或者是 F_5 中 3 的倒数乘以 2，或其他。

在 Isabelle 中，这是通过（在一定程度上）避免重载和使用不同的符号来解决的。

【讨论】：

我将您的答案纳入了针对新 Isabelle 用户的教程（并引用了您的论文 hal.inria.fr/hal-02276530，我很喜欢）。对于那些感兴趣的人，带有屏幕截图的 LaTex 排版教程位于github.com/AncientZygote/izzie/blob/main/IsabelleTutorial.pdf