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