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: Jan 31 2023 at 13:02 UTC