我正在学习coq,并且正在尝试制作自己的Point and Line数据类型。我想制作一个返回行长的函数,但是我似乎找不到能返回计算结果的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
).
如果要计算平方根,可以做两件事。
使用CoRN库。然后,您将获得实际计算的实数函数。但是,这些实数仅是您可以要求近似精确度的函数,因此可能不是您想要的。另外,我认为CoRN如今维护得不好。
使用您已经提到的标准库中的自然数平方根,然后使用该自然数来自己计算要达到一定精度的平方根。您可以通过导入获得此功能BinNat
:
Coq < Require Import BinNat.
[Loading ML file z_syntax_plugin.cmxs ... done]
Coq < Eval compute in N.sqrt 1000.
= 31%N
: N
本文收集自互联网,转载请注明来源。
如有侵权,请联系 [email protected] 删除。
我来说两句