Stream: Coq users

Topic: Well-founded recursion on proof?


view this post on Zulip Joshua Grosso (Mar 23 2021 at 21:10):

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

view this post on Zulip Li-yao (Mar 23 2021 at 21:38):

The trick is that there ARE some Props 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Guillaume Melquiond (Mar 23 2021 at 21:47):

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

view this post on Zulip Pierre-Marie Pédrot (Mar 23 2021 at 21:49):

see for instance Coq.Logic.ConstructiveEpsilon for an example of this feature.

view this post on Zulip 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?)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Joshua Grosso (Mar 24 2021 at 01:03):

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

view this post on Zulip 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.

view this post on Zulip 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 :-)


Last updated: Jan 31 2023 at 13:02 UTC