Library ASCommon.FMon


From stdpp Require Import option.
Require Import Options.
Require Import Common.

Reexporting Effects. Using FMon implies using Effects
Require Export Effects.

#[export] Typeclasses Transparent Equiv.

Free monad

This is a custom implementation of a free monad, which is basically a finite itree (thus inductive, not coinductive). Therefore, it cannot represent non-termination.
It is acceptable to use this for individual instruction semantics because they always terminate

Section FMon.
  Context {Eff : eff}.
  Context {ER : Effect Eff}.
  Context {ED : EqDecision Eff}.
  Context {Wf : EffWf Eff}.
  Context {CT : EffCTrans Eff}.
  Context {CTS : EffCTransSimpl Eff}.

This implementation is not very computationally efficient in case of repeated binds, but has the advantage of being canonical, e.g. trace equivalence is Leibtniz equality (with functional extensionality)
  Inductive fMon {A : Type} :=
  | Ret (ret : A)
  | (call : Eff) (k : eff_ret call → fMon).
  Arguments fMon : clear implicits.

  #[global] Instance fMon_ret : MRet fMon := @Ret.

  #[global] Instance fMon_bind : MBind fMon :=
    λ _ _, fix bind f ma :=
      match ma with
      | Ret x ⇒ f x
      | Next oc k ⇒ Next oc (λ x, bind f (k x)) end.

  #[global] Instance fMon_join : MJoin fMon :=
    λ _ mmx, mx ← mmx; mx.

  #[global] Instance fMon_fmap : FMap fMon :=
    λ _ _, fix map f ma :=
      match ma with
      | Ret x ⇒ Ret (f x)
      | Next oc k ⇒ Next oc (λ x, map f (k x)) end.

  #[global] Instance fMon_call : MCall Eff fMon := λ out, Next out Ret.

  #[export] Instance fMon_monad : Monad fMon.
  Proof.
    split.
    - unfold mret, fMon_ret. done.
    - intros A. induction f; hauto lq:on use:functional_extensionality.
    - intros A B C. induction a; hauto lq:on use:functional_extensionality.
  Qed.

  #[export] Instance fMon_monad_fmap : MonadFMap fMon.
  Proof.
    intros A B f.
    apply functional_extensionality.
    intro x.
    induction x; hauto lq:on use:functional_extensionality.
  Qed.

Events

A event of an effect type is a combination of an effect call and its result
  Record fEvent := FEvent {fcall : Eff; fret : eff_ret fcall}.
  Infix "&→" := FEvent (at level 45, no associativity).

  Lemma fEvent_call_eq `{Effect Eff} (call call' : Eff) ret ret' :
    call &→ ret = call' &→ ret' → call = call'.
  Proof. cdestruct call |- ***. Qed.

  Lemma fEvent_ret_JMeq `{Effect Eff} (call call' : Eff) ret ret' :
    call &→ ret = call' &→ ret' → ret =ⱼ ret'.
  Proof. cdestruct call |- ***. Qed.

  Lemma fEvent_eq_spec_JMeq `{Effect Eff} (call call' : Eff) ret ret' :
    call &→ ret = call' &→ ret' ↔ call = call' ∧ ret =ⱼ ret'.
  Proof. cdestruct call |- *** #CDestrSplitGoal. Qed.

Decide if a call matches an event ev and return the return value with the correct type if it matches
  Definition event_extract (ev : fEvent) (call : Eff) : option (eff_ret call) :=
    match decide (ev.(fcall) = call) with
    | left e ⇒ Some (ctrans e ev.(fret))
    | right _ ⇒ None
    end.

  Lemma event_extract_Some ev (call : Eff) ret :
    event_extract ev call = Some ret ↔ ev = (call &→ ret).
  Proof using CTS.
    unfold event_extract.
    destruct ev. cbn in ×.
    case_decide.
    - subst. simp ctrans. naive_solver.
    - naive_solver.
  Qed.
  Hint Rewrite @event_extract_Some : fmon.

  Lemma event_extract_None ev (call : Eff) :
    event_extract ev call = None ↔ fcall ev ≠ call.
  Proof using CTS.
    rewrite eq_None_not_Some.
    apply not_iff_compat.
    unfold is_Some.
    setoid_rewrite event_extract_Some.
    destruct ev. naive_solver.
  Qed.
  Hint Rewrite @event_extract_None : fmon.

Event as transitions

One can see a free monad (or an itree) as a state transtion system where the free monad value itself is the state and events are transitions.
fsteps describe the result of a list of transitions, labelled by events in the list, allowed by the monad. For a single transition, there is an fstep notation that uses that on a singleton list, instead of a separate predicate.
fsteps f evs f' iff free monad value f can do a sequence of transitions, labelled by the events of the list evs, to free monad value f'.
In the rhs of the body of FMCons, the monadic value Next call k can do a transition with label call &→ ret, with the same call and an arbitrary return value ret, and then the rest of the events tl, to reach monadic value f', reached by applying the continuation k to that return value ret.

  Inductive fsteps {A : Type} : fMon A → list fEvent → fMon A → Prop :=
  | FMNil f : fsteps f [] f
  | FMCons call k ret tl f' :
    fsteps (k ret) tl f' → fsteps (Next call k) ((call &→ ret) :: tl) f'.
  Notation fstep f ev f' := (fsteps f [ev] f').
  Hint Constructors fsteps : fmon.

  Lemma fsteps_nil {A} (f f' : fMon A) :
    fsteps f [] f' ↔ f = f'.
  Proof. sauto. Qed.
  Hint Rewrite @fsteps_nil : fmon.

  Lemma fsteps_app {A} l l' (f f' : fMon A) :
    fsteps f (l ++ l') f' ↔ ∃ f'', fsteps f l f'' ∧ fsteps f'' l' f'.
  Proof.
    split.
    - generalize dependent f.
      induction l; cbn.
      + sauto lq:on.
      + intros f H. dependent destruction H.
        sauto lq:on.
    - intros (f'' & H & H').
      induction H; hauto.
  Qed.

  Definition fsteps_cons {A} ev tl (f f' : fMon A) :
    fsteps f (ev :: tl) f' ↔ ∃ f'', fstep f ev f'' ∧ fsteps f'' tl f'
  := fsteps_app [ev] tl f f'.
  Lemma fsteps_Next_cons {A} call k ret tl (f : fMon A) :
      fsteps (Next call k) ((call &→ ret) :: tl) f ↔ fsteps (k ret) tl f.
    Proof.
      split; intro H.
      - by dependent destruction H.
      - by constructor.
  Qed.
  Hint Rewrite @fsteps_Next_cons : fmon.

  Lemma fsteps_Ret_cons {A} ret l (f : fMon A) :
    fsteps (Ret ret) l f ↔ l = [] ∧ f = Ret ret.
  Proof.
    split; intro H.
    - by dependent destruction H.
    - hauto ctrs:fsteps.
  Qed.

Replay function

freplay is a computational version of fsteps. It takes a free monad and a list of events and tries to replay it. It might fail of course
  Equations freplay {A} (f : fMon A) (l : list fEvent) : option (fMon A) :=
    freplay f [] := Some f;
    freplay (Next call k) (ev :: tl) with event_extract ev call := {
      | Some ret ⇒ freplay (k ret) tl
      | None ⇒ None
      } ;
    freplay _ _ := None.

  Lemma freplay_ind A
    (P : fMon A → list fEvent → option (fMon A) → Prop)
    (Pempty: ∀ f : fMon A, P f [] (Some f))
    (PRetNone: ∀ ret ev tl, P (Ret ret) (ev :: tl) None)
    (Pcallmatch: ∀ call k ret tl o,
       freplay (k ret) tl = o →
       P (k ret) tl o → P (Next call k) (call &→ ret :: tl) o)
    (Pcallnomatch: ∀ call k call' ret' tl ,
       call ≠ call' → P (Next call k) (call' &→ ret' :: tl) None) f l :
    P f l (freplay f l).
    funelim (freplay _ _); sauto db:fmon lq:on.
  Qed.
  Remove Hints FunctionalElimination_freplay : typeclass_instances.
  #[global] Instance FunctionalElimination_freplay' A :
    FunctionalElimination (@freplay A) _ 5 := @freplay_ind A.

  Lemma freplay_Some l {A} (f f' : fMon A) :
    freplay f l = Some f' ↔ fsteps f l f'.
  Proof using CTS. funelim (freplay _ _); sauto db:fmon lq:on dep:on. Qed.

  Lemma freplay_None l {A} (f f' : fMon A) :
    freplay f l = None ↔ ∀ f', ¬ fsteps f l f'.
  Proof using CTS.
    setoid_rewrite <- freplay_Some.
    destruct (freplay _ _); naive_solver.
  Qed.

Free monad traces

The type of finite traces over fMon. These traces are partial and can stop anywhere, including having or not an incomplete next event.
Rationale: we define traces as a pair of a list of events and a trace end, rather than defining a new list type with the trace ends in place of Nil, as otherwise we need to redefine all the standard list utilities.

Trace ends

A trace end is either return value, a effect call without a result, or just a stop marker
  Inductive fTraceEnd {A : Type} :=
  | FTERet (a : A)
  | FTEOpenCall (call : Eff)
  | FTEStopped.
  Arguments fTraceEnd : clear implicits.

  #[export] Instance fTraceEnd_eqdec `{EqDecision A} : EqDecision (fTraceEnd A).
  Proof using ED. solve_decision. Defined.

Definition of trance end matching a value of the monad
  Definition fmatch_end {A} (f : fMon A) (tre : fTraceEnd A) :=
    match tre with
    | FTERet r ⇒ if f is Ret r' then r = r' else False
    | FTEOpenCall call ⇒ if f is Next call' _ then call = call' else False
    | FTEStopped ⇒ True
    end.

  #[export] Instance fmatch_end_dec `{EqDecision A}
    (f : fMon A) tre : Decision (fmatch_end f tre).
  Proof using ED. unfold fmatch_end. tc_solve. Defined.

  Lemma fmatch_end_ret `(r : A) : fmatch_end (Ret r) (FTERet r).
  Proof. done. Qed.
  Hint Resolve fmatch_end_ret : fmon.

  Lemma fmatch_end_open {A} (call : Eff) k :
    fmatch_end (A := A) (Next call k) (FTEOpenCall call).
  Proof. done. Qed.
  Hint Resolve fmatch_end_open : fmon.

Traces

A trace is a list of events and an end.
  Definition fTrace A : Type := list fEvent × fTraceEnd A.

  #[global] Typeclasses Transparent fTrace.
  Notation FTRet a := ([], FTERet a).
  Notation FTOpenCall call := ([], FTEOpenCall call).
  Notation FTStopped := ([], FTEStopped).
  Definition FTCons ev `(itrc : fTrace A) : fTrace A :=
    (ev :: itrc.1, itrc.2).

We keep the defintion of a trace matching a monad value as an inductive for convenience
  Inductive fmatch {A : Type} : fMon A → fTrace A → Prop :=
  | FTMStopped f : fmatch f FTStopped
  | FTMRet a : fmatch (Ret a) (FTRet a)
  | FTMOpenCall call k : fmatch (Next call k) (FTOpenCall call)
  | FTMNext call k ret tl tre :
    fmatch (k ret) (tl, tre) → fmatch (Next call k) ((call &→ ret) :: tl, tre).

Matching a whole trace is the same as running all the transitions and then matching the end of the trace
  Lemma fmatch_fsteps {A} (f : fMon A) tr :
    fmatch f tr ↔ ∃ f', fsteps f tr.1 f' ∧ fmatch_end f' tr.2.
  Proof.
    split.
    - induction 1; hauto l:on db:fmon.
    - destruct tr. cbn. intros [f' [FS FME]].
      induction FS; sauto.
  Qed.

fmatch is decidable which is very important for the rest of this project
  Equations fmatch_dec `{EqDecision A}
    (f : fMon A) tr : Decision (fmatch f tr) :=
    fmatch_dec f (l, tre)
      with inspect (freplay f l) := {
      | Some f' eq: _ ⇒
          dec_if (decide (fmatch_end f' tre))
      | None eq: _ ⇒ right _
      }.
  Solve All Obligations with
    intros; cbn in *;
    rewrite fmatch_fsteps;
    setoid_rewrite <- freplay_Some;
    naive_solver.

  Lemma fmatch_next A (call : Eff) (k : eff_ret call → fMon A) (ret : eff_ret call) tl tre:
    fmatch (Next call k) (call &→ ret :: tl, tre)
      ↔ fmatch (k ret) (tl, tre).
  Proof using.
    repeat rewrite fmatch_fsteps.
    by setoid_rewrite fsteps_Next_cons.
  Qed.

Full traces

TP: deprecated notion Full trace are traces that only stop on a non returning effect
  Definition ftfull {A} (ft : fTrace A) :=
    match ft.2 with
    | FTERet _ ⇒ True
    | FTEOpenCall call ⇒ eff_ret call → False
    | FTEStopped ⇒ False
    end.
  Lemma ftfull_FTRet {A} (a : A) : ftfull (FTRet a).
  Proof using. naive_solver. Qed.
  Hint Resolve ftfull_FTRet : fmon.
  Lemma ftfull_FTOpenCall {A} (call : Eff) :
    (eff_ret call → False) → ftfull (A := A) (FTOpenCall call).
  Proof using. naive_solver. Qed.
  Hint Resolve ftfull_FTOpenCall : fmon.
  Lemma ftfull_FTOpenCall_spec {A} (call : Eff) :
    ftfull (A := A) (FTOpenCall call) ↔ (eff_ret call → False).
  Proof using. split; [sfirstorder | apply ftfull_FTOpenCall]. Qed.
  Hint Rewrite @ftfull_FTOpenCall_spec : fmon.

  Equations ftfull_dec {A} `{!EffWf Eff} (ft : fTrace A) : Decision (ftfull ft) :=
    ftfull_dec (_, FTEOpenCall call) with decideT (eff_ret call) := {
      | inleft _ ⇒ right _
      | inright _ ⇒ left _
      };
    ftfull_dec (_, FTEStopped) := right _;
    ftfull_dec (_, FTERet) := left _.
  Solve All Obligations with unfold ftfull; sfirstorder.

A full trace always exists for any free monad value
  Lemma ftrace_ftfull_exists {A} (m : fMon A) : ∃ t, fmatch m t ∧ ftfull t.
  Proof using Wf.
    setoid_rewrite fmatch_fsteps.
    unfold fTrace. apply exists_pair.
    induction m as [|?? IH].
    - repeat (eexists || split || auto with fmon || cbn).
    - destruct (decideT (eff_ret call)) as [e | ?].
      + specialize (IH e). sauto q:on dep:on db:pair.
      + repeat (eexists || split || auto with fmon || cbn).
  Qed.

Two values of the free monad that generate the same sets of full traces are equal
  Theorem fmon_eq_via_ftrace_ftfull A m1 m2:
    (∀ trc : fTrace A, ftfull trc → fmatch m1 trc ↔ fmatch m2 trc) → m1 = m2.
  Proof using Wf.
    generalize dependent m2.
    induction m1 as [ret| call k IH]; intros m2 Ht.
    - specialize (Ht ([], FTERet ret)). hauto l:on inv:fmatch db:fmon.
    - destruct m2 as [ret2 | call2 k2].
      + clear IH. specialize (Ht ([], FTERet ret2)).
        hauto l:on inv:fmatch db:fmon.
      + destruct (ftrace_ftfull_exists (Next call k)) as [tr [Htr Hfull]].
        pose proof Htr as Htr2.
        apply Ht in Htr2. 2: done.
        dependent destruction Htr; dependent destruction Htr2;
          cbn in *; first done.
        all: f_equal.
        all: apply functional_extensionality.
        all: intro ret'.
        × done.
        × apply IH.
          intros [tl' tre'].
          specialize Ht with (call &→ ret' :: tl', tre').
          by setoid_rewrite fmatch_next in Ht.
  Qed.

  Corollary fmon_eq_via_ftrace A m1 m2:
    (∀ trc : fTrace A, fmatch m1 trc ↔ fmatch m2 trc) → m1 = m2.
  Proof using Wf. intro. apply fmon_eq_via_ftrace_ftfull. naive_solver. Qed.

Free monad effect handling

A handler is a function that describes how to interpret all effects of Eff in a monad M
  Definition fHandler (M : Type → Type) := ∀ call : Eff, M (eff_ret call).

If the target monad already supports the effect, then there is a trivial handler
  Definition mcall_fHandler `{MC : !MCall Eff M} : fHandler M := mcallM M.
  #[export] Typeclasses Transparent mcall_fHandler.
  #[global] Arguments mcall_fHandler {_ _} _ /.

Free monad interpret: Interprets a free monad over Eff in an arbitrary monad, using a handler
  Fixpoint finterp `{MR: MRet M, MB: MBind M} (handler : fHandler M)
    [A] (mon : fMon A) : M A :=
    match mon with
    | Ret a ⇒ (mret a : M A)
    | Next call k ⇒ ret ←@{M} handler call; finterp handler (k ret)
    end.

Interpreting inside the free monad itself is the identity
  Lemma finterp_mcall A (f : fMon A) : finterp mcall_fHandler f = f.
  Proof using. induction f; hauto l:on use:functional_extensionality.
  Qed.
  Hint Rewrite finterp_mcall : fmon.
End FMon.

Arguments fMon _ {_}.
Arguments fEvent _ {_}.
Arguments fTraceEnd :clear implicits.
Arguments fTrace _ {_}.
Arguments fHandler _ {_}.

Infix "&→" := FEvent (at level 45, no associativity).
Infix "&→@{ Eff }" := (@FEvent Eff _)
                        (at level 45, only parsing, no associativity).

Notation fstep f ev f' := (fsteps f [ev] f').
Notation FTRet a := ([], FTERet a).
Notation FTOpenCall call := ([], FTEOpenCall call).
Notation FTStopped := ([], FTEStopped).

Helper for the following Hint Extern. The goal is that in case of an fEvent equality, where the return values happen to be of the same type, then call &→ ret = call' &→ ret' can be simplified to call = call' ∧ ret = ret'
Lemma fEvent_eq_helper `{Effect Eff} (call call' : Eff) ret ret' P :
  ret =ⱼ ret' ↔ P →
  call &→ ret = call' &→ ret' ↔ call = call' ∧ P.
Proof. intros <-. apply fEvent_eq_spec_JMeq. Qed.

Perform the CDestruct simplification described above
#[export]
Hint Extern 2
  (CDestrSimpl _
     (@FEvent ?Eff ?ER ?call ?ret = @FEvent ?Eff ?ER ?call' ?ret') ?Q) ⇒
       eunify Q (call = call' ∧ ret = ret');
       constructor;
       refine (@fEvent_eq_helper Eff ER call call' ret ret' _ _);
       exact (JMeq_simpl _ ret ret') : typeclass_instances.

Create a handler for a sum of effects from handler for each individual effects
Definition fHandler_plus `{Effect Effl, Effect Effr, MRet M, MBind M}
    (fl : fHandler Effl M) (fr : fHandler Effr M) : fHandler (Effl + Effr) M :=
  λ call, match call with
          | inl l ⇒ fl l
          | inr r ⇒ fr r
          end.
Infix "+ₕ" := fHandler_plus (at level 50, left associativity).

Choice monad: Non deterministic free monad

Notation Nextl e := (Next (inl e)).
Notation Nextr e := (Next (inr e)).

Section CMon.
  Context {Eff : eff}.
  Context {ER : Effect Eff}.
  Context {ED : EqDecision Eff}.
  Context {Wf : EffWf Eff}.
  Context {CT : EffCTrans Eff}.
  Context {CTS : EffCTransSimpl Eff}.

A choice monad is just a free monad with additional choice effects. The only difference is the theory around it (equivalence, trace matching, etc.)
  Definition cMon := fMon (Eff + MChoice).
  #[export] Typeclasses Transparent cMon.

Interprets the effect in a monad supporting non-determinism
  Definition cinterp `{MR: MRet M, MB: MBind M, MCh: MChoose M}
      (f : fHandler Eff M) [A] (c : cMon A) : M A :=
    finterp (f +ₕ mcall_fHandler) c.

Matching a choice monad with a trace that does not contain choice

points
  Inductive cmatch {A : Type} : cMon A → fTrace Eff A → Prop :=
  | CTMNothing f : cmatch f FTStopped
  | CTMRet a : cmatch (Ret a) (FTRet a)
  | CTMStop (call : Eff) k : cmatch (Nextl call k) (FTOpenCall call)
  | CTMNext (call : Eff) k ret tl tre :
    cmatch (k ret) (tl, tre) → cmatch (Nextl call k) (call &→ ret :: tl, tre)
  | CTMChoose n i k tr : cmatch (k i) tr →
    cmatch (Nextr (ChooseFin n) k) tr.

  Lemma cmatch_Nextl A (call : Eff) (k : eff_ret call → cMon A)
    (ret : eff_ret call) tl tre:
    cmatch (Nextl call k) (call &→ ret :: tl, tre)
      ↔ cmatch (k ret) (tl, tre).
  Proof using.
    split.
    - intro H. by dependent destruction H.
    - by constructor.
  Qed.

Decide a cmatch: This is a bit dumb, it will try every possible non-deterministic choice until one match succeeded or all failed. However in practice, if concrete value of cMon avoid doing choice before doing very long identical sequences of calls in all branches, this shouldn't be that bad.
  Equations cmatch_dec `{EqDecision A} (f : cMon A) tr
    : Decision (cmatch f tr) :=
    cmatch_dec _ FTStopped := left _;
    cmatch_dec (Ret r) (FTRet r') := dec_if (decide (r = r'));
    cmatch_dec (Nextl call k) (FTOpenCall call') :=
      dec_if (decide (call = call'));
    cmatch_dec (Nextl call k) (ev :: tl, tre)
      with inspect (event_extract ev call) := {
      | Some ret eq: _ ⇒
          dec_if (cmatch_dec (k ret) (tl, tre))
      | None eq: _ ⇒ right _
      } ;
    cmatch_dec (Nextr (ChooseFin n) k) tr :=
      dec_if (@decide (∃x : fin n, cmatch (k x) tr)
                (@exists_dec _ _ _ _ (λ x, cmatch_dec (k x) tr)));
    cmatch_dec _ _ := right _.
  Solve All Obligations with
    cbn;
    intros;
    try match goal with | H : ∃ _, _ |- _ ⇒ destruct H end;
    try rewrite event_extract_Some in *;
    try rewrite event_extract_None in *;
    subst;
    try (intro H; dependent destruction H);
    try econstructor;
    naive_solver.
  #[export] Existing Instance cmatch_dec.

Choice monad equivalence

A choice monad is not a canonical representation, so there is a non-equality equivalence relation
Definition of strong equivalence. I haven't found a way to define it in a more useable manner. In particular one can't do (yet) an induction on it
  Definition cequiv {A} : Equiv (cMon A) :=
    λ c1 c2, ∀ tr, cmatch c1 tr ↔ cmatch c2 tr.

  #[local] Instance local_cequiv_params : Params (@cequiv) 1 := {}.

  #[global] Instance cequiv_sym A : Symmetric (@cequiv A).
  Proof using. unfold Symmetric, cequiv in ×. naive_solver. Qed.
  #[global] Instance cequiv_refl A : Reflexive (@cequiv A).
  Proof using. unfold Reflexive, cequiv in ×. naive_solver. Qed.
  #[global] Instance cequiv_trans A : Transitive (@cequiv A).
  Proof using. unfold Transitive, cequiv in ×. naive_solver. Qed.
  #[global] Instance cequiv_equiv A : Equivalence (@cequiv A).
  Proof using. constructor; tc_solve. Qed.

  #[global] Instance cmatch_cequiv_Proper A :
    Proper (cequiv ==> eq ==> iff) (@cmatch A).
  Proof using.
    intros m1 m2 H ? t →.
    by unfold cequiv in H.
  Qed.

  Lemma cequiv_Ret A (a : A) : cequiv (Ret a) (Ret a).
  Proof using. reflexivity. Qed.

  Lemma cequiv_Next A call k k':
    pointwise_relation (eff_ret call) cequiv k k' →
    @cequiv A (Next call k) (Next call k').
  Proof using.
    intros H trc.
    unfold pointwise_relation in H.
    destruct call;
      split;
      intro Hc;
      dependent destruction Hc;
      econstructor;
      by rewrite H in ×.
  Qed.

  #[global] Instance Next_cequiv_Proper A call:
    Proper (pointwise_relation (eff_ret call) cequiv ==> @cequiv A) (Next call).
  Proof using. intros k k'. apply cequiv_Next. Qed.

  Definition fMon_to_cMon {A} (f : fMon Eff A) : cMon A :=
    finterp mcall_fHandler f.

  Lemma fMon_to_cMon_sound {A} (f : fMon Eff A) (t : fTrace Eff A) :
    fmatch f t ↔ cmatch (fMon_to_cMon f) t.
  Proof.
    unfold fMon_to_cMon.
    induction f in t |- × .
    - split; inversion_clear 1; constructor.
    - split; sinv 1; cdestruct t |- ***; hauto lq:on ctrs:cmatch,fmatch.
  Qed.

  Definition determinize_fHandler :
      fHandler MChoice cMon :=
    λ '(ChooseFin n),
      if n is 0%nat then mdiscard else mret 0%fin.

  Definition determinize_cMon {A} (f : cMon A) : cMon A :=
    finterp (mcall_fHandler +ₕ determinize_fHandler) f.

  Lemma determinize_trace_subset {A} (f : cMon A) (t : fTrace Eff A) :
    cmatch (determinize_cMon f) t → cmatch f t.
  Proof.
    unfold determinize_cMon.
    induction f in t |- ×.
    - inversion_clear 1; constructor.
    - destruct call as [|[[]]].
      all: sinv 1.
      all: cdestruct t |- ***.
      all: hauto lq:on ctrs:cmatch.
  Qed.
End CMon.
Arguments cMon _ {_}.

#[global] Instance cequiv_params : Params (@cequiv) 2 := {}.