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.