## Stream: Coq users

### Topic: Well-founded recursion on proof?

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

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

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

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

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

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

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

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

Last updated: Sep 30 2023 at 05:01 UTC