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