如何计算 coq 中自然数或有理数的 sqrt？答案

【问题标题】：How do I the calculate the sqrt of a natural or rational number in coq?如何计算 coq 中自然数或有理数的 sqrt？
【发布时间】：2015-08-30 17:48:54
【问题描述】：

我正在学习 coq，并且正在尝试创建自己的点和线数据类型。我想做一个返回行长的函数，但我似乎找不到返回计算的 sqrt 函数。我试过用Coq.Reals.R_sqrt，但显然它只用于抽象数学，所以它不会运行计算。

然后我尝试导入 Coq.Numbers.Natural.Abstract.NSqrt 和 Coq.Numbers.NatInt.NZSqrt. 但都没有将 sqrt 函数放入环境中。

这就是我目前所拥有的......

Require Import Coq.QArith.QArith_base.
Require Import Coq.Numbers.NatInt.NZSqrt.
Require Import Coq.Numbers.Natural.Abstract.NSqrt.
Require Import Coq.ZArith.BinInt.

Inductive Point : Type :=
  point : Q -> Q -> Point.

Inductive Line : Type :=
  line : Point -> Point -> Line.

Definition line_fst (l:Line) :=
  match l with
  | line x y => x
  end.

Definition line_snd (l:Line) :=
  match l with
  | line x y => y
  end.

Definition point_fst (p:Point) :=
  match p with
  | point x y => x
  end.

Definition point_snd (p:Point) :=
  match p with
  | point x y => y
  end.

(* The reference sqrt was not found in the current environment. *)
Definition line_length (l:Line) :=
  sqrt(
    (minus (point_snd(line_fst l)) (point_fst(line_fst l)))^2 
    +
    (minus (point_snd(line_snd l)) (point_fst(line_snd l)))^2
  ).

Example line_example : (
  line_length (line (point 0 0) (point 0 2)) = 2
).

【问题讨论】：

您需要确定您希望平方根具有什么类型，以及当平方根不存在时您希望发生什么。例如，您希望line_length (line (point 0 0) (point 1 1)) 返回什么值和类型？
我希望类型为实数，然后将平方根限制为仅正数 - 如果我只取 (x1 - x2)^2 + ( y1 -y2)^2。这保证总是一个正数。但是如果可能的话，将实数转换为有理数？否则，我不确定。 coq 输出值可以表示为平方根吗？因此，例如 point(0,0) 和 point(1,1) 之间的距离将输出 sqrt(2)。

标签： coq square-root sqrt

【解决方案1】：

如果您想要计算平方根，您可以做两件事。

使用CoRN library。然后您将获得实际计算的实数函数。但是，这些实数只是您可以要求以某种精度进行近似的函数，因此可能不是您要寻找的。另外，我认为现在的 CoRN 维护得不是很好。
使用您已经提到的标准库中的自然数平方根，并使用它来计算您自己想要达到一定精度的平方根。这个函数通过importBinNat得到：
```
Coq < Require Import BinNat.
[Loading ML file z_syntax_plugin.cmxs ... done]

Coq < Eval compute in N.sqrt 1000.  
      = 31%N
      : N
```

【讨论】：