add some meta theory on finite step-indexed simulations

theories/examples/keyideas/simulations.v

@@ -91,7 +91,7 @@ Section simulations.
    Qed.
 
   Lemma sim_execute_tgt t s t':
-    rtc tgt_step t t' → satisfiable (sim t s) 
+    rtc tgt_step t t' → satisfiable (sim t s)
     → ∃ s', rtc src_step s s' ∧ satisfiable (sim t' s').
   Proof.
     induction 1 in s.
@@ -127,3 +127,126 @@ Section simulations.
   Qed.
 End simulations.
 
+
+
+From Coq.Logic Require Import Classical_Prop.
+
+Section finite_stepindex_simulation.
+  Context {SI} {Σ: gFunctors SI} `{!FiniteIndex SI}.
+
+  (* Some generic properties about reduction relations *)
+
+  Lemma ex_loop_sn {X: Type} (R: relation X) (x: X):
+    ex_loop R x ↔ ¬ sn R x.
+  Proof.
+    split.
+    - intros Hloop Hsn. by eapply acc_not_ex_loop.
+    - intros Hsn. revert x Hsn. cofix IH.
+      intros x Hsn. enough (∃ x', R x x' ∧ ¬ sn R x') as [x' [Hstep Hsn']].
+      { econstructor; eauto. }
+      destruct (classic (∃ x' : X, R x x' ∧ ¬ sn R x')); first done.
+      exfalso. eapply Hsn. constructor. intros x' Hstep.
+      destruct (classic (sn R x')); first done.
+      exfalso. eapply H. eauto.
+  Qed.
+
+  Lemma sn_finite_nondet_bounded {X: Type} (R: relation X) (x: X):
+    (∀ x, ∃ X: list X, (∀ x', R x x' ↔ x' ∈ X)) →
+    sn R x →
+    ∃ n, ∀ x' m, nsteps R m x x' → m < n.
+  Proof.
+    intros Hbounded. induction 1.
+    destruct (Hbounded x) as [xs Hbounded'].
+    assert (∀ y, y ∈ xs → ∃ n : nat, ∀ (x' : X) (m : nat), nsteps R m y x' → m < n) as Hx.
+    { intros ??. eapply H0. simpl. eapply Hbounded'. eauto. }
+    assert (∃ n : nat, ∀ y, y ∈ xs → ∀ (x' : X) (m : nat), nsteps R m y x' → m < n) as Hx'.
+    - clear Hbounded'. induction xs as [|y xs IH]; first by exists 0; set_solver.
+      destruct (Hx y) as [n1 Hx'']; first set_solver.
+      destruct (IH) as [n2 Hxs]; first set_solver. exists (n1 `max` n2).
+      intros z. rewrite elem_of_cons. intros [->|?].
+      + intros ?? Hsteps. eapply Hx'' in Hsteps. lia.
+      + intros x' m. intros ?. eapply Hxs in H1; last done. lia.
+    - destruct Hx' as [n Hx']. exists (1 + n). intros x' m Hsteps.
+      inversion Hsteps; subst; first lia. eapply Hbounded' in H1.
+      eapply Hx' in H1; last done. lia.
+  Qed.
+
+
+  Lemma finite_nondet_ex_loop_diverge {X: Type} (R: relation X) (x: X):
+    (∀ x, ∃ X: list X, ∀ x', R x x' ↔ x' ∈ X) →
+    (∀ n, ∃ m, n ≤ m ∧ ∃ x', nsteps R m x x') →
+    ex_loop R x.
+  Proof.
+    intros Hb Hsteps. eapply ex_loop_sn. destruct (classic (sn R x)) as [Hsn|]; last done.
+    eapply sn_finite_nondet_bounded in Hsn; last done.
+    destruct Hsn as [n Hsn]. destruct (Hsteps n) as [m [Hle [x' Hsteps']]].
+    eapply Hsn in Hsteps'. lia.
+  Qed.
+
+  Lemma ex_loop_extract_finite_execution {X: Type} (R: relation X) (x: X) n:
+    ex_loop R x →
+    ∃ x', nsteps R n x x'.
+  Proof.
+    intros Hloop. induction n as [|n IH] in x, Hloop |-*.
+    - exists x. constructor.
+    - destruct Hloop as [x x' Hstep Hloop]. eapply IH in Hloop.
+      destruct Hloop as [x'' Hsteps]. exists x''. econstructor; eauto.
+  Qed.
+
+
+
+  (* We assume a source and a target language *)
+  Variable (S T: Type) (src_step: S → S → Prop) (tgt_step: T → T → Prop).
+  Variable (V: Type) (val_to_src: V → S) (val_to_tgt: V → T).
+  Variable (val_irred: ∀ v, ¬ ∃ t', tgt_step (val_to_tgt v) t') (val_inj: Inj eq eq val_to_tgt).
+
+  Definition sim_finite_ref (t: T) (s: S) :=
+    ∀ n t', nsteps tgt_step n t t' →
+    ∃ m s', nsteps src_step m s s' ∧ n ≤ m ∧
+      (∀ v, val_to_tgt v = t' → val_to_src v = s').
+
+  Notation sim := (sim (Σ := Σ) S T src_step tgt_step V val_to_src val_to_tgt).
+  Notation tpr := (tpr S T src_step tgt_step V val_to_src val_to_tgt).
+
+  Lemma satisfiable_laterN n (P: iProp Σ): satisfiable (▷^n P)%I → satisfiable P.
+  Proof. induction n; eauto using satisfiable_later. Qed.
+
+  Lemma sim_to_sim_finite_ref t s: (⊢ sim t s) → sim_finite_ref t s.
+  Proof.
+    intros Hsim n t' Hsteps.
+    eapply sim_valid_satisfiable in Hsim.
+    eapply satisfiable_pure, (satisfiable_laterN n), satisfiable_mono; eauto.
+    iIntros "Hsim". clear Hsim. iInduction Hsteps as [] "IH" forall (s).
+    - rewrite sim_unfold. iDestruct "Hsim" as "[H|[H _]]".
+      + iDestruct "H" as (v')  "[<- <-]". iPureIntro.
+        eexists _, _. split; first constructor. split; first lia.
+        intros v <-%val_inj. done.
+      + iDestruct "H" as (t') "%". iPureIntro.
+        eexists _, _. split; first constructor. split; first lia.
+        intros ??. exfalso. naive_solver.
+    - rewrite sim_unfold. iDestruct "Hsim" as "[H|[H X]]".
+      + iDestruct "H" as (v')  "[<- <-]". exfalso. naive_solver.
+      + iDestruct "H" as (t') "_". iDestruct ("X" with "[//]") as "X".
+        iDestruct "X" as (s' Hstep) "Hsim". simpl. iNext. simpl.
+        iDestruct ("IH" with "Hsim") as "Hn". iNext. simpl.
+        iDestruct "Hn" as (m s'') "%". iPureIntro. destruct H0 as (?&?).
+        eexists _, s''. split; first eauto using nsteps_l. split; first lia.
+        naive_solver.
+  Qed.
+
+  Lemma sim_finite_ref_tpr t s:
+    (∀ s, ∃ ss: list S, ∀ s', src_step s s' ↔ s' ∈ ss) →
+    sim_finite_ref t s →
+    tpr t s.
+  Proof.
+    intros Hb Href. split.
+    - intros v Hsteps. eapply rtc_nsteps in Hsteps as [n Hsteps].
+      eapply Href in Hsteps as (m & s'&?&?& Hv); eauto.
+      specialize (Hv v eq_refl). subst. by eapply nsteps_rtc.
+    - intros Hloop. eapply finite_nondet_ex_loop_diverge; first done.
+      intros n. eapply (ex_loop_extract_finite_execution _ _ n) in Hloop as [x' Hsteps].
+      eapply Href in Hsteps as (m & s'&?&?&?); eauto.
+  Qed.
+
+End finite_stepindex_simulation.
+