 # Defining mathematical function implicitly

In Coq, how do I define a function implicitly, not using Fixedpoint?

For example, define the square root function by f(x)^2 = x.

I looked at the definition of sqrt in std, but it’s a parameter of a module. Do I need a module to define it? I tried:

``````Module Type Foo.
Parameter Inline bubba : nat -> nat.
Axiom bubba_spec: forall a, bubba(a) * bubba(a) = a.
End Foo.
``````

But I can neither `Import` nor `Export Foo`.

(I get that this definition doesn’t work for the natural numbers, I’m curious what the error message is, also I can fix it up once I get the basic syntax working.)

Do you want to define a function, or assume a function?

If you want to define a function, there is essentially no way around fixpoints.

If you want to assume the existence of such a function and the prove things based on this assumption, you can do that as follows:

``````Require Import Lia Arith.

Section assm_sqrt.

Variable sqrt : nat -> nat.

Hypothesis sqrt_spec : forall n : nat, sqrt n * sqrt n = n.

Goal sqrt 9 = 3.
Proof.
enough (Nat.pow (sqrt 9) 2 = Nat.pow 3 2).
- eapply Nat.pow_inj_l with (c := 2); now lia.
- cbn. rewrite Nat.mul_1_r. eapply sqrt_spec.
Qed.

End assm_sqrt.
``````

A frequently used pattern is to assume functions, assume a specification, prove lemmas about them, and then instantiate the lemmas to functions explicitly defined via `Fixpoint` fulfilling the specification.

Does that help?

Thanks, yes this helps a lot.

When you say " instantiate the lemmas to functions explicitly defined via `Fixpoint` fulfilling the specification," does this mean I need to come up with a separate Fixedpoint definition? Would this amount to a way to compute the function, in my case the sqrt?

So there’s no equivalent of defining a binary relation `R x y` through a property it satisfies, proving `forall x, exists y, R x y` and that y is unique, and then being on your way? You need to also provide a `Fixedpoint` definition if you don’t want to rely on assumptions?

Under the hood, proving `forall x, exists y, R x y` is the same as defining a way to compute the function (modulo noncomputational axioms).

Good point. Thanks!