proposition: Corollary compile_com_correct_diverging: forall s c, cexecinf s c -> forall C pc σ, code_at C pc (compile_com c) -> infseq (transition C) (pc, σ, s).
proof: Proof. intros. set (X := fun (pcss: config) => let '(pc, σ, s) := pcss in exists c, cexecinf s c /\ code_at C pc (compile_com c)). apply infseq_coinduction_principle with X. - intros [[pc1 σ1] s1] (c1 & EXEC & CODEAT). edestruct (compile_com_productive _ _ EXEC) as (c' & pc' & s' & PLUS & EXEC' & CODEAT'); eauto. exists (pc', σ1, s'); split. exact PLUS. exists c'; auto. - exists c; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)