Simplify untaus: remove bool and nat arguments

[Lysxia]

CC @gilhur for comments, but otherwise this is mergeable.

• Eq.UpToTaus: In the definition of untausF, split up the bool into a separate notauF clause for unalltausF, and remove the nat in favor of a strong induction principle directly on untausF (untausF_strong_ind).

  • Splitting unalltausF into untausF and notausF is a bit annoying, but I'm hoping we can use projections and hints to alleviate that.

  • I didn't manage to make the induction using ... tactic recognize it as an induction principle yet, but while trying I found that homfix_is_interp (in Fix, basically an unfolding lemma for mfix) can be rewritten as a strict bisimulation (eq_itree), with a slight reformulation of interp (called interp1, in Morphisms), which removes the current main consumer of that nat parameter.

• This got me to refactor the definition of interp and interp1 in Morphisms, which takes a small half of this PR.

[Lysxia]

Some proof in MorphismsFacts requires Coq 8.9, but we're still waiting for the version bound in coq-ext-lib to be raised so CI can grab it https://github.com/coq/opam-coq-archive/pull/564

[gilhur]

I clicked a review request button to @gmalecha by mistake.

I will review this PR today. I want to check whether the strong induction condition is sufficient though the new proof of the fixpoint lemma does not require "eutt".

[gilhur]

@Lysxia I wonder whether you changed the definition of "interp" to make the fixpoint be eq_itree instead of eutt? I previously thought that the fixpoint is not bisimulation because there were different numbers of taus, which may be wrong. Anyway, it is a better result and a simpler proof to show an eq_itree version of the fixpoint.

[Lysxia]

@gilhur The changed definition used in the homfix_is_interp lemma is interp1 https://github.com/DeepSpec/InteractionTrees/pull/49/files#diff-d1338c2acba7fe0e3594f79f907b2e23R63

Both interp and interp1 seem useful to have around, hence why I kept both.

Proving eq_itree instead of eutt for this lemma makes strong induction no longer necessary.

[gilhur]

@Lysxia I simplified and completed your proof of fixpoint. I also simplified the strong induction principle for untausF. Please have a look.

https://github.com/gilhur/InteractionTrees/commit/7a82080a745b5a2be2b5c9f4bc0422f386656fd0

[gilhur]

I also removed paco2_upto.v and some code subsumed by Paco 2.0.

https://github.com/gilhur/InteractionTrees/commit/512aa89419e34ceeba4124040c9d4bb2ad892e53

[Lysxia]

Thanks gil! I incorporated your proof improvements in this PR. Removing paco2_upto.v would be nice in another PR!

[gilhur]

I will make a PR for removing paco2_upto.v

[gilhur]

Both interp and interp1 seem useful to have around, hence why I kept both.

Would it be necessary/useful to prove the relation between interp and interp1 using eutt?

[Lysxia]

That seems definitely useful.

[Zdancewic]

There's another concept of "effect inclusion" that might be useful to have around -- it doesn't need to use bind anywhere and so should yield stronger relations (eq_itree rather than eutt). How does it relate to interp and interp1?

(* Strong homomorphisms between effects *)
Definition eff_incl (E E' : Type -> Type) : Type :=
  forall t, E t -> E' t.

Definition include_match {E F R}
           (f : eff_incl E F) (hom : itree E R -> itree F R)
           (t : itree E R) :=
  match t.(observe) with
  | RetF r => Ret r
  | VisF e k =>Vis (f _ e) (fun x => hom (k x))
  | TauF t' => Tau (hom t')
  end.

CoFixpoint include {E F R} (f:eff_incl E F) (t : itree E R) := include_match f (include f) t.

[gmalecha]

I thought we had this concept in OpenSum

[Zdancewic]

I don't think so -- we don't have a function of type: `{F -< E} -> itree F X -> itree E X (which should just map convert over each effect.