Can I use a "decreasing" proof witness in order to prove termination of a function? I'm inclined to believe this isn't possible because of terms in Prop
not being computationally accessible, but (intuitively speaking) it feels weird to me that I can't manipulate proof objects in a "termination proof."
The trick is that there ARE some Prop
s that can be eliminated in Type
, the most notable one being Acc
. https://github.com/coq/coq/wiki/The-Logic-of-Coq#do-false-eq-and-acc-have-a-special-status
Thanks for the reference! Does that mean that it's therefore impossible to recurse on, say, the data inside an ex
?
Acc is in Prop, so if you manage to prove that a recursion is performed a well-founded order in Prop you're fine. In particular, anything in Prop goes, so you can pry open exists proofs when doing that.
In particular, you can turn a Prop
-existential over an enumerable type into an actual value.
see for instance Coq.Logic.ConstructiveEpsilon for an example of this feature.
(This is, by the way, the utmost advantage of Coq over, say, Agda, since with this you can prove the strong normalization of System F. What is the purpose of all the debauchery of induction-recursion if you can't prove the good old SN theorem for F?)
Just to make sure I understand @Pierre-Marie Pédrot: Is the solution to use constructive_indefinite_ground_description
to extract the value in question? Or is ConstructiveEpsilon
just an example of a more general technique?
It is more like the latter. It is the archetypal example that a proof witness can be used to define a terminating function in Coq. You can use your decreasing argument to provide a custom Acc
relation and then define a Fixpoint
over this Acc
.
I'm new enough at this that, unfortunately, I don't think I completely understand: What would the type of my custom relation (for use in Acc
) be? I assume not (for example) R : (exists n : nat, P n) -> (exists n : nat, P n) -> Prop
(because then I run into Prop
-inaccessibility errors), so would it just be R : nat -> nat -> Prop
?
Wait a second... is the below a valid (and/or useful) ordering in Prop
?
Inductive foo_order (P : nat -> Prop) : (exists n : nat, P n) -> (exists n : nat, P n) -> Prop :=
| foo_lt : forall (n1 n2 : nat) (H1 : P n1) (H2 : P n2),
n1 < n2 ->
foo_order _ (ex_intro _ _ H1) (ex_intro _ _ H2).
Because if so, I think I'm actually good to go then, lol
You said you had a decreasing witness. Then, R
is the corresponding order. Having R : (exists n : nat, P n) -> (exists n : nat, P n) -> Prop
does not make sense to me, because there is no way you can guarantee that a given proof term was built with a smaller witness than another proof term.
Consider the algorithm that tests all the values by increasing order until it finds one that satisfies some predicate P
. What is "decreasing" is the currently tested value. And here, "decreasing" means getting closer to a value satisfying P
. So, the relation looks like R y x := y > x /\ forall z, P z -> y <= z
. (In the case of nat
, you can replace y > x
by y = S x
, since you know you are not skipping any value.) Then one just needs to prove that the initial value is accessible (0
for nat
), assuming there is a value satisfying P
, i.e., (exists x, P x) -> Acc R 0
, which should be straightforward if I did not mess the definition of R
.
Update: I tried to implement a custom Acc
relation for my specific case, and as part of that process, I realized that I can (probably) recast my proposition into one of the form exists n : nat, P n
... furthermore, I'm fairly certain my P
is decidable, so I'll just use constructive_ground_epsilon_nat
directly! Thank you both for the help—I'll definitely be referencing this conversation in the future if I end up in a situation like this again :-)
Last updated: Oct 13 2024 at 01:02 UTC