Я изучаю coq и пытаюсь создать свои собственные типы данных Point и 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
).
line_length (line (point 0 0) (point 1 1))
возвращал? - person Mark Dickinson   schedule 30.08.2015