Well-founded recursion on proof? · Coq users

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

Li-yao (Mar 23 2021 at 21:38):

Joshua Grosso (Mar 23 2021 at 21:41):

Thanks for the reference! Does that mean that it's therefore impossible to recurse on, say, the data inside an ex?

Pierre-Marie Pédrot (Mar 23 2021 at 21:45):

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.

Guillaume Melquiond (Mar 23 2021 at 21:47):

In particular, you can turn a Prop-existential over an enumerable type into an actual value.

Pierre-Marie Pédrot (Mar 23 2021 at 21:49):

Pierre-Marie Pédrot (Mar 23 2021 at 21:51):

(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?)

Joshua Grosso (Mar 23 2021 at 22:28):

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?

Guillaume Melquiond (Mar 23 2021 at 22:33):

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.

Joshua Grosso (Mar 24 2021 at 00:08):

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?

Joshua Grosso (Mar 24 2021 at 01:03):

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

Guillaume Melquiond (Mar 24 2021 at 05:05):

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.

Joshua Grosso (Apr 02 2021 at 03:32):

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

Stream: Coq users

Topic: Well-founded recursion on proof?

Joshua Grosso (Mar 23 2021 at 21:10):