defined the Eff_eq by iterating over naturals.

[aa755]

Thus, coinductive proofs about Eff_eq can be done by induction on natural numbers, instead of paco or cofix. In my experience formalizing Nuprl metatheory, these proofs by natural induction exactly mimic the cofix proof (and there is no need to worry about productivity check failing at Qed). However, when using Paco, non-trivial work is needed in strengthening the coinduction hypothesis.

[gmalecha]

This looks really interesting and like it could improve things a lot.

Can you factor out the technique into a separate file (Fn, RTopN, and the theorem about how this is equivalent to the "standard co-inductive definition"). That should give a great view of how the definitions fit together.

[gmalecha]

I dug into this a bit more for my own understanding. Here's what I came up with:

Section with_generating_function.
  Context {A : Type}.
  Variable step : A -> A.

  Section Fn.
    Variable f0 : A.

    Fixpoint Fn (n:nat) :=
      match n with
      | O => f0
      | S n => step (Fn n)
      end.
  End Fn.

End with_generating_function.

Section rel_3.
  Variable T0 : Type.
  Variable T1 : T0 -> Type.
  Variable T2 : forall x, T1 x -> Type.

  Definition rel3 : Type :=
    forall a b, T2 a b -> Prop.

  Definition rel3_impl (r1 r2 : rel3) : Prop :=
    forall a b c, r1 a b c -> r2 a b c.

  Definition rel3_iff (r1 r2 : rel3) : Prop :=
    forall a b c, r1 a b c <-> r2 a b c.

  Definition top3 : rel3 :=
    fun _ _ _ => True.

  (* TODO: generalize for hetero relations *)
  Definition RTopN (Rs: rel3 -> rel3) (n:nat) : rel3 :=
    Fn Rs top3 n.

  (* greatest fixpoint if F is continuous *)
  Definition GFPC (Rs: rel3 -> rel3) : rel3 :=
   fun t0 t1 t2 => forall n, RTopN Rs n t0 t1 t2.

  Lemma GFPC_unfold : forall rs, rel3_iff (GFPC rs) (rs (GFPC rs)).
  Proof. (* This doesn't seem provable... *) Admitted.

I thought it would be nice to prove this isomorphic to the basic co-inductive definition but you can't phrase that because of strict positivity. But maybe we can prove it equivalent to the paco3 definition. That is, some proof that says (probably under an assumption about rs being monotone).

Theorem GFPC_paco_iso : forall rs,
      rel_iff3 (paco3 rs (fun _ _ _ => False)) (GFPC rs).

[aa755]

That is a nice generalization.

Monotonicity is not sufficient for the paco3 and the GFPC definitions to be equivalent. A notion of continuity should suffice; I had defined it somewhere in Nuprl; will look at the Nuprl repo.

It should be possible to get rid of the UIP requirement in the proof I committed yesterday by defining something equivalent to Eff_eqF using Fixpoint instead of indexed induction.

[gmalecha]

Does the definition of Eff_eqF_inj_interact solve the axiom problem? It actually turns out that paco uses axioms as well which is sad (it would be worth fixing if we go that way in my opinion).

I'd be really interested in seeing the definition of continuous.