Suppose we have two predicates on streams `P Q : stream -> Prop`

, and suppose we have a goal like the following:

```
forall (s : stream), P s -> exists (u: stream), Q u
```

My intuition is that I want to coinductively consume the hypothesis `P s`

in order to produce the proof of `Q u`

. However, the (inductive) existential requires us to produce `u`

upfront. This means we want to use `P s`

to corecursively produce `u`

, instantiate the existential, and then coinductively prove `Q u`

. However, this requires us to eliminate the `Prop`

(`P s`

) in `Type`

(`u`

)... Coq does not allow this elimination, but I think in this case it might be innocent because we only want to build a `Type`

by eliminating a `Prop`

in order to construct the propositional existential. In some sense this elimination seems to be "guarded".

Is there a way to get around all of these constraints and do our proof? The only thing that I can think to do is provide an elimination axiom for `P s`

in `Type`

, but that seems a bit risky. Is there a more principled way?

did you look at https://coq.inria.fr/library/Coq.Logic.ClassicalEpsilon.html#constructive_indefinite_description ? Sounds like this can't be proven constructively, and that axiom is likely the most direct way.

The usual way of doing that (irrespective of coinductive types) is to instantiate `u`

by looking only at `s`

, and then to look at `P s`

only for the proof of `Q u`

. Do you really need to look at `P s`

to build `u`

?

The necessary details are lacking, but description axioms are probably too strong for this kind of statement. It does look like a for of choice, though. Indeed, it's not because you return a Prop that you can eliminate over quantified Props (e.g. as a stream). For instance, the following statement

```
forall (A : Type) (P : nat -> A -> Prop),
(forall n : nat, exists x : A, P n x) -> exists (f : nat -> A), forall n : nat, P n (f n).
```

is not provable in Coq and corresponds to countable choice.

what seems unfortunate is that such statements are easy to realize even when erasing Prop, since the `u`

is also erased — strengthening `Prop`

's proof theory seems hard, but it feels like some _irrelevance modality_ might support this scenario better?

Last updated: Jun 17 2024 at 22:01 UTC