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. :slight_smile: Thanks!