Как вычислить sqrt естественного или рационального числа в coq?

Я изучаю coq, и я пытаюсь создать свои собственные типы данных Point и Line. Я хотел бы создать функцию, которая возвращает длину строки, но я не могу найти функцию sqrt, которая вернет вычисление. Я попытался использовать Coq.Reals.R_sqrt, но, видимо, это используется только для абстрактной математики, поэтому он не будет запускать вычисления.Как вычислить sqrt естественного или рационального числа в coq?

Итак, я попробовал импортировать 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 
).

источник

2015-08-30 Albtzrly

Вы должны решить, какой тип * * Вы хотите, чтобы квадратный корень, чтобы иметь, и то, что вы хотите, чтобы это произошло, когда квадратный корень не существует. Например, какое значение и тип вы хотите 'line_length (строка (точка 0 0) (точка 1 1))' для возврата? –

Я хотел бы, чтобы тип был действительным числом, а затем ограничил квадратный корень только положительными числами - что должно произойти, если я возьму только квадратный корень из (x1 - x2)^2 + (y1 -y2)^2. Это всегда будет положительным числом. Но тогда, если возможно, приведите действительное число к рациональному числу? В противном случае, я не уверен. Может ли coq выводить значения, выраженные как квадратный корень? Так, например, расстояние между точкой (0,0) и точкой (1,1) будет выводить sqrt (2). – Albtzrly

Если вы хотите, чтобы ваш квадратный корень, чтобы вычислить, есть две вещи, которые вы можете сделать.

Использовать CoRN library. Тогда вы получите реальные функции числа, которые фактически вычисляются. Тем не менее, эти действительные числа будут просто функциями, которые вы можете запросить приближениями к определенной точности, так что, возможно, не то, что вы ищете. Кроме того, я думаю, что CoRN в настоящее время не очень хорошо поддерживается.
Используйте натуральное число квадратный корень из стандартной библиотеки, о котором вы уже упоминали, и используйте это, чтобы вычислить квадратные корни, которые вы хотите с определенной точностью. Эта функция, которую вы получите за счет импорта BinNat:
```
Coq < Require Import BinNat. 
[Loading ML file z_syntax_plugin.cmxs ... done] 

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

источник

2017-01-22 10:46:50

Как вычислить sqrt естественного или рационального числа в coq?

ответ

Смежные вопросы