CODEWITHSUNDEEP
coqsquare-rootsqrt
Albtzrly
Albtzrly

Reputation: 944

How do I the calculate the sqrt of a natural or rational number in coq?

I'm learning coq and I'm trying to make my own Point and Line data types. I'd like to make a function that returns the length of a line, but I can't seem to find the sqrt function that will return a calculation. I tried used Coq.Reals.R_sqrt, but apparently that's only used for abstract math, so it won't run the calculation.

So then I tried importing Coq.Numbers.Natural.Abstract.NSqrt and Coq.Numbers.NatInt.NZSqrt. but neither put sqrt function into the environment.

This is what I have so far...

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
).

Upvotes: 1

Views: 454

Answers (1)

Freek Wiedijk
Freek Wiedijk

Reputation: 511

If you want your square root to compute, there are two things you can do.

  • Use the CoRN library. Then you will get real number functions that actually compute. However, those real numbers will just be functions that you can ask for approximations to a certain precision, so might not be what you are looking for. Also, I think CoRN is not terribly well maintained nowadays.

  • Use the natural number square root from the standard library that you already mentioned, and use that to calculate the square roots that you want to a certain precision yourself. This function you get by importingBinNat:

    Coq < Require Import BinNat.
[Loading ML file z_syntax_plugin.cmxs ... done]

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

Upvotes: 2

Related Questions