## Stream: Coq users

### Topic: Coinductive existence

#### Karl Palmskog (Jul 09 2020 at 11:07):

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?

#### Gaëtan Gilbert (Jul 09 2020 at 11:24):

Can you give an example?

#### Karl Palmskog (Jul 09 2020 at 11:35):

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

#### Karl Palmskog (Jul 09 2020 at 11:36):

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?

#### Gaëtan Gilbert (Jul 09 2020 at 11:38):

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

#### Karl Palmskog (Jul 09 2020 at 11:39):

there is a coinductive case in the `midpoint` predicate. I don't see how I can handle that case without coinduction, i.e., `cofix`.

#### Gaëtan Gilbert (Jul 09 2020 at 11:54):

Try to write your proof with `exc` and see what happens

#### Paolo Giarrusso (Jul 09 2020 at 11:54):

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

#### Paolo Giarrusso (Jul 09 2020 at 11:55):

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”

#### Paolo Giarrusso (Jul 09 2020 at 11:56):

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

#### Paolo Giarrusso (Jul 09 2020 at 11:57):

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

#### Karl Palmskog (Jul 09 2020 at 11:58):

traces are possibly-infinite

#### Paolo Giarrusso (Jul 09 2020 at 11:59):

_is_ the actual witness tr meant to be finite?

#### Karl Palmskog (Jul 09 2020 at 12:01):

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

#### Paolo Giarrusso (Jul 09 2020 at 12:02):

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

#### Simon Hudon (Jul 09 2020 at 12:40):

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

#### Karl Palmskog (Jul 12 2020 at 11:22):

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:

1. needs to do the corecursive call to obtain the "rest" of the trace (say, subtrace `t'`) to construct the required `t`
2. 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.

#### Karl Palmskog (Aug 04 2020 at 12:22):

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

#### Simon Hudon (Aug 04 2020 at 15:01):

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

#### Simon Hudon (Aug 04 2020 at 15:04):

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

#### Karl Palmskog (Aug 04 2020 at 15:19):

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

#### Karl Palmskog (Aug 04 2020 at 15:19):

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

#### Simon Hudon (Aug 04 2020 at 16:37):

Where do you use impredicativity in your code?

#### Karl Palmskog (Aug 04 2020 at 16:51):

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

#### Karl Palmskog (Aug 04 2020 at 16:53):

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

#### Simon Hudon (Aug 04 2020 at 17:02):

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

#### Simon Hudon (Aug 04 2020 at 17:05):

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.

#### Simon Hudon (Aug 04 2020 at 17:05):

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

#### Karl Palmskog (Aug 04 2020 at 17:14):

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

#### Karl Palmskog (Aug 04 2020 at 17:16):

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: Sep 23 2023 at 15:01 UTC