One limitation of `cofix`

is that one can't use it to build anything other than coinductive types. So let's say I need to prove the existence of some term using `cofix`

(i.e., I want to define a function whose result lives in `Prop`

). Is the only option to define a coinductive predicate that mirrors `ex`

, and has somebody done this before maybe?

Can you give an example?

Suppose `midpoint`

is a coinductive predicate.

```
Lemma ex_midpoint : forall (s1 s2: stmt) (st: state) (tr: trace)
(h: redm (Sseq s1 s2) st tr), exists tr, midpoint h tr.
Proof.
Fail cofix COINDHYP.
```

output:

```
The command has indeed failed with message:
All methods must construct elements in coinductive types.
```

do I need to define:

```
CoInductive exc (A:Type) (P:A -> Prop) : Prop :=
exc_intro : forall x:A, P x -> exc (A:=A) P.
```

or has somebody done this? What are the consequences?

How would the recursive call be used? you can't project out of it during the cofixpoint.

there is a coinductive case in the `midpoint`

predicate. I don't see how I can handle that case without coinduction, i.e., `cofix`

.

Try to write your proof with `exc`

and see what happens

are traces finite or infinite? If it is infinite, can you actually provide it in one go?

I ask because, in general, the intuition I have from Agda codata is that coinduction creates infinite but productive computations, which can be run “step-wise”

so, make sure that your lemma can be proved that way.

For instance, if you were proving that finite reduction sequences can be extended into infinite ones (wild guess), that statement couldn’t do it I think, even with exc — you’d have to provide the trace steps one at a time

traces are possibly-infinite

_is_ the actual witness tr meant to be finite?

it could be infinite from my understanding, but doesn't have to be

I was wondering about the witness in the proof you have in mind, if you have one. If that’s, I’d maybe use an inductive version of midpoint, and try to prove that inductive midpoint implies the coinductive one (can you)? But I’m just brainstorming (per my usual), and lack experience with Coq coinduction

I have struggled with the same thing. My best answer so far was to create a corecursive function that makes the witness, prove that it's a valid witness and then wrap the two in a single proof of the existential

I looked much deeper into this. The "create a corecursive witness function" approach works if your witness function doesn't much need to look at (do inversion on) stuff in `Prop`

to do its job, i.e., it just builds something in `Set`

with only plain `destruct`

/`match`

on things in `Set`

.

However, the guardedness condition becomes a world of hurt when you need to do serious inversion on Props and thus return something like `exists t : trace, P t`

, where `P`

is a coinductive predicate on traces. Basically, to build the required trace coinductively, one usually:

- needs to do the corecursive call to obtain the "rest" of the trace (say, subtrace
`t'`

) to construct the required`t`

- applies the constructor to build the
`exists t`

, and then apply the coinductive predicate constructor to prove`P t`

using the proof of`P t'`

obtained before

This is in the **wrong** order for the guardedness checker.

In contrast, if you just want return a plain`trace`

without `exists`

, you can instead apply a coinductive constructor directly and then do the corecursive call, since you don't need further information (properties) on what the corecursive call returns at the "top level". This satisfies the guardedness condition.

In the end I resorted to `constructive_indefinite_description`

to make my plain non-`Prop`

witness function be able to do inversion on things in `Prop`

and just return a plain `trace`

. Before this, I also tried things like the recent coinduction plugin, but to no avail.

Here is the current sad state of non-constructiveness. Better ideas would be welcome.

I constructed a "minimal" example and wrote up the thing for the Disourse: https://coq.discourse.group/t/proving-existence-statements-about-coinductive-predicates-constructively/994

What if you put `ex_midpoint`

and `follows`

in `Set`

instead of `Prop`

. Then `exists tr, ...`

becomes `{ tr | ... }`

and you don't need to use choice on it anymore

I feel like if you stay in Prop, whatever you construct could be used to prove skolemization on natural numbers

good observation, yes, everything works fine if you put `follows`

in `Set`

. But then you can't use impredicativity anymore, which seems like a bad tradeoff to me. Maybe some meta-theoretical argument like one on skolemization can indeed establish that impredicativity for these kinds of relations needs to be "bought" at the cost of constructive epsilon...

I should probably augment the Discourse post with that alternative though (even though I focus on `Prop`

in the title).

Where do you use impredicativity in your code?

it's used in the larger development at https://github.com/palmskog/coind-sem-while - see p. 14 footnote in https://arxiv.org/pdf/1412.6579.pdf

I don't have high stakes riding on this, but would be nice to say definitively if certain constructive `Prop`

coinductive proofs can't be done, like we know "finite or infinite" can't be proven constructively (reduce to halting problem and so on).

That's a really cool looking project! I'll have to look closer

I was faced with a similar problem a while ago. I was proving the existence of refinement mapping in temporal logic. It boiled down, at every state of an infinite trace that there exists a suitable abstract state corresponding to the concrete state. That's where I concluded that there was no constructive solution to show that there exists a suitable abstract trace.

With your case, I'm not sure if you need to show an infinite number of existentials for your traces or just one mid-point

sounds similar, but I'll have to think some more.

along the same lines as the repo I just mentioned, this is a library with more generic traces/properties I extracted out: https://github.com/palmskog/coind-traces

Last updated: Feb 04 2023 at 22:29 UTC