# Existentially quantified coinductive predicates

How does one prove theorems where the conclusion is an existentially quantified coinductive proposition?

I am attempting to adapt Xavier Leroy’s compiler correctness tutorial; this involves adding traces of events to the source and target languages. For the coinductive `infseq` predicate, I have done this as follows:

``````(* the type of states *)
Variable A: Type.
Variable event: Type.

Variable R: A -> event -> A -> Prop.

Definition trace := list event.
Definition inftrace := Stream event.

Inductive star: A -> trace -> A -> Prop :=
| star_refl: forall a,
star a [] a
| star_step_ev: forall a b c e t,
R a e b -> star b t c -> star a (e :: t) c.

Definition all_seq_inf (a: A) : Prop :=
forall t b, star a t b -> exists e c, R b e c.

CoInductive infseq: A -> inftrace -> Prop :=
| infseq_step_ev: forall a e b t,
R a e b -> infseq b t -> infseq a (Cons e t).
``````

I need to prove the following lemma:

``````Lemma infseq_if_all_seq_inf:
forall a, all_seq_inf a -> exists t, infseq a t.
``````

However, I am unable to use `cofix` on this goal–I get the error `All methods must construct elements in coinductive types.` When traces are not involved, the equivalent lemma is fairly easy to prove (see here).

I would be really grateful for any suggestions on how to prove this.

That proposition is not provable without an axiom, and that is arguably the reason why the tutorial defines `infseq` just on states. The tutorial mentions the trouble with `nat -> A`—which is isomorphic to `stream A`, so it suffers from the same issue:

as a function f: nat → A such that
(…)
This is a correct characterization of the existence of an infinite sequence of reductions. However, it is very inconvenient to work with this definition in Coq’s constructive logic: in most use cases, the function f is not computable and therefore cannot be defined in Coq.

`cofix` is only allowed when the result type (the thing on the right of the `forall` and arrows) is coinductive. Here the result type is `ex`, not `infseq`, so `cofix` is not allowed. The only constructive way to prove such an existential is to actually construct the trace all at once, presumably using `cofix` on `inftrace`. And then you will need a second `cofix` to prove the `infseq` proposition.

The problem now is that `all_seq_inf` does not give you access to the successor of a finite trace, unless you use an axiom to turn an `exists` proposition (`exists e c, R b e c`) into a sigma type `{ '(e, c) | R b e c }`. One such axiom is the constructive indefinite description.

``````Axiom constructive_indefinite_description :
forall (A : Type) (P : A->Prop),
(exists x, P x) -> { x : A | P x }.
``````
1 Like

Thank you very much for the response—this is really helpful. In my setting I believe it may actually be possible to write a `CoFixpoint` that constructs an `inftrace` starting from a particular state (under certain assumptions). I have managed to make this approach work in a stylized example, and I will try to extend it to this setting. If this fails to work I will use the `constructive_indefinite_description` axiom you mention.

I really appreciate your guidance on this issue!