Require Import Relations Transitive_Closure.

Section Preliminaries.

  Context {X : Type} (step : X -> X -> Prop).

  Definition stuck s := forall t, ~ step s t.

  Definition terminates s := exists t, clos_refl_trans X step s t /\ stuck t.

  Fact terminates_extend {s t} : clos_refl_trans X step s t -> terminates t -> terminates s.
  Proof.
    intros ? [u [??]]. exists u. eauto using clos_refl_trans.
  Qed.

  Lemma clos_trans_clos_refl_trans s t : clos_trans _ step s t -> clos_refl_trans _ step s t.
  Proof.
    intros H. now induction H; eauto using clos_refl_trans.
  Qed.

End Preliminaries.

Section Deterministic_simulation.

  Context {X Y : Type}.

  Context {step1 : X -> X -> Prop} {step2 : Y -> Y -> Prop}.

  Context {sync : X -> Y -> Prop}.

  Context (step2_det : forall s' t1' t2', step2 s' t1' -> step2 s' t2' -> t1' = t2').
  Arguments step2_det {s' t1' t2'}.

  Context (fstep : forall s t s', step1 s t -> sync s s' ->
                     exists t', clos_trans Y step2 s' t' /\ sync t t').
  Arguments fstep {s t s'}.

  Context (fstop : forall s s', stuck step1 s -> sync s s' -> terminates step2 s').
  Arguments fstop {s s'}.

  Context (step1_intro : forall s, (exists t, step1 s t) \/ stuck step1 s).

  Lemma clos_refl_trans_transport {s s' t} :
    sync s s' -> clos_refl_trans _ step1 s t ->
    exists t', sync t t' /\ clos_refl_trans _ step2 s' t'.
  Proof using fstep.
    intros Hss' Hst. apply clos_rt_rt1n in Hst.
    revert s' Hss'. induction Hst as [|??? Hxy Hyz IH].
    - intros s' ?. exists s'. now split; [|apply rt_refl].
    - intros s' Hxs'. destruct (fstep Hxy Hxs') as [y' [Hs'y' Hyy']].
      destruct (IH _ Hyy') as [t' [? Hy't']].
      exists t'. split; [|eapply rt_trans; [apply clos_trans_clos_refl_trans|]]; eassumption.
  Qed.

  Lemma terminates_transport {s s'} :
    sync s s' -> terminates step1 s -> terminates step2 s'.
  Proof using fstop fstep.
    intros Hss' [t [Hst Ht]].
    destruct (clos_refl_trans_transport Hss' Hst) as [t' [Htt' Hs't']].
    apply (terminates_extend _ Hs't').
    eapply fstop; eassumption.
  Qed.

  Lemma terminating_Acc {s} : terminates step2 s -> Acc (fun y x => step2 x y) s.
  Proof using step2_det.
    intros [t [Hst%clos_rt_rt1n Ht]].
    induction Hst as [|??? Hxy Hyz IH]; constructor.
    - now intros y ?%Ht.
    - intros y' Hxy'. rewrite <- (step2_det Hxy Hxy'). now apply IH.
  Qed.

  Lemma terminates_reflection {s s'} : sync s s' -> terminates step2 s' -> terminates step1 s.
  Proof using step2_det step1_intro fstep.
    intros Hss' Hs'%terminating_Acc%(Acc_clos_trans Y).
    revert s Hss'. induction Hs' as [s' _ IH].
    intros s. destruct (step1_intro s) as [[t Hst] | Hs].
    - intros [t' [Hs't' Htt']]%(fstep Hst).
      apply (terminates_extend _ (t := t)); [now apply rt_step|].
      eapply (IH t'); [|now apply Htt'].
      now eapply clos_trans_transp_permute.
    - intros _. exists s. eauto using clos_refl_trans.
  Qed.

End Deterministic_simulation.