2

导入 Reals 库

Require Import Reals.

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

4

1 回答 1

3

您可以像这样定义常量：

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

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

您可以将标准库中的实数视为AST，由标记为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在类似情况下为 s 完成）：

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.

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

于 2017-02-09T13:16:39.367 回答