Stream: Coq users

Topic: Proving the existence of a coinductive term

Calvin Beck (Feb 13 2023 at 14:21):

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?

Karl Palmskog (Feb 13 2023 at 14:59):

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.

Guillaume Melquiond (Feb 13 2023 at 15:05):

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?

Pierre-Marie Pédrot (Feb 14 2023 at 07:26):

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.

Paolo Giarrusso (Feb 14 2023 at 14:05):

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: Oct 04 2023 at 19:01 UTC