Coq 实数 - 词法分析和解析 3.14

Question

导入了 Reals 库

Require Import Reals.

如何定义 3.14 或 10.1 等常量并将它们用于函数定义或计算？

Answer 1

您可以像这样定义常量：

Definition a := 10 + /10.
Definition b := 3 + 14/100.

但是请注意，标准库定义实数 公理化。您可以找到主要定义 here。请注意，定义为 Parameters，它是 Axiom 的同义词。例如，R0 和 R1 代表实数 0 和 1，Rplus 和 Rmult 代表加法和乘法，但这些定义不是归纳数据类型和函数，因为它们缺乏定义。为了能够处理实数，我们需要公理，控制它们之间的相互作用（给定 here）。

您可以将标准库中的实数视为 ASTs，由标记为 R0、R1、Rplus 等的节点组成。你会得到一些规则（公理），这些规则（公理）指定了你可以对这些 AST 执行的（唯一的）转换。

让我们看看 Coq 是如何表示实数的：

Require Import Coq.Reals.Reals.
Local Open Scope R_scope.
Unset Printing Notations.
Check 5+/2  (* 5½ *).

(*
Rplus (Rplus R1
             (Rmult (Rplus R1 R1)
                    (Rplus R1 R1)))
      (Rinv (Rplus R1 R1)).
i.e. (1 + (1 + 1) * (1 + 1)) + (1 + 1)⁻¹ 
*)

在这种公理化方法的后果中，有一个事实是以下目标不能再由 reflexivity 证明（因为在类似情况下可以为 nat 证明）：

Set Printing Notations.
Goal a = 9 + 1 + /10.
  Fail reflexivity.

这失败了，因为等式两边的 AST（术语）不同，Coq 没有将它们转换为一些规范值以在最后比较它们。这次我们需要证明两个AST是可以相互转换的。

  enough (9 + 1 = 10).
  - now rewrite H.

现在我们需要证明9 + 1 = 10:

  - rewrite Rplus_comm, <-Rplus_assoc.
    rewrite <-(Rmult_1_r 2) at 1.
    rewrite <-Rmult_plus_distr_l.
    reflexivity.

幸运的是，有一种策略可以为我们完成这项繁琐的工作：

    Restart.
    unfold a; field.
Qed.

然而，标准库方法并不是唯一可能的方法。 by @gallais 可以帮助您探索其他选择。

Coq 实数 - 词法分析和解析 3.14

Coq Real numbers -lexing and parsing 3.14

coq

real-number