时间戳

首页 > 解决方案 > 要求澄清伊莎贝尔理论中涉及自然数的理论中明显的实强制的出现

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

问题描述

我正在 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 ∈ ℚ&quot;
  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。

我追查了该理论文件中的参考资料，并查看了高阶逻辑证明助手中的第8.4.5 节，我发现自然数类型nat是线性有序半环，类型int是有序环，类型real是有序场地。属性可能不适用于特定的类，例如，没有涉及减法的抽象属性适用于类型nat（因为，当然，最终可能是负数，而不是自然数）。相反，提供了特定的定理来解决类型的减法nat。更重要的是，“所有涉及除法的抽象属性都需要一个域。”（高阶逻辑的证明助手。）

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

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

标签： isabelletype-coercion

解决方案

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

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

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

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

推荐阅读