Module WeakSimulation

Definition of a weak simulation for a small-step semantics.

Require Import Relations.
Require Import Wellfounded.
Require Import Coqlib.
Require Import AST.
Require Import Events.
Require Import Globalenvs.
Require Import Integers.
Require Import Smallstep.

Set Implicit Arguments.

Section CLOSURES.

Variable genv: Type.
Variable state: Type.

A one-step transition relation has the following signature. It is parameterized by a global environment, which does not change during the transition. It relates the initial state of the transition with its final state.
Variable step: genv -> state -> state -> Prop.

No transitions: stuck state

Definition nostep (ge: genv) (s: state) : Prop :=
  forall s', ~(step ge s s').

Zero, one or several transitions. Also known as Kleene closure, or reflexive transitive closure.

Inductive star (ge: genv): state -> state -> Prop :=
  | star_refl: forall s,
      star ge s s
  | star_step: forall s1 s2 s3,
      step ge s1 s2 -> star ge s2 s3 ->
      star ge s1 s3.

Lemma star_one:
  forall ge s1 s2, step ge s1 s2 -> star ge s1 s2.
Proof.
  intros. eapply star_step; eauto. apply star_refl.
Qed.

Lemma star_trans:
  forall ge s1 s2, star ge s1 s2 ->
  forall s3, star ge s2 s3 -> star ge s1 s3.
Proof.
  induction 1; intros; auto.
  eapply star_step; eauto.
Qed.

Lemma star_left:
  forall ge s1 s2 s3,
  step ge s1 s2 -> star ge s2 s3 ->
  star ge s1 s3.
Proof star_step.

Lemma star_right:
  forall ge s1 s2 s3,
  star ge s1 s2 -> step ge s2 s3 ->
  star ge s1 s3.
Proof.
  intros. eapply star_trans. eauto. apply star_one. eauto.
Qed.

One or several transitions. Also known as the transitive closure.

Inductive plus (ge: genv): state -> state -> Prop :=
  | plus_left: forall s1 s2 s3,
      step ge s1 s2 -> star ge s2 s3 ->
      plus ge s1 s3.

Lemma plus_one:
  forall ge s1 s2,
  step ge s1 s2 -> plus ge s1 s2.
Proof.
  intros. econstructor; eauto. apply star_refl.
Qed.

Lemma plus_star:
  forall ge s1 s2, plus ge s1 s2 -> star ge s1 s2.
Proof.
  intros. inversion H; subst.
  eapply star_step; eauto.
Qed.

Lemma plus_right:
  forall ge s1 s2 s3,
  star ge s1 s2 -> step ge s2 s3 ->
  plus ge s1 s3.
Proof.
  intros. inversion H; subst. simpl. apply plus_one. auto.
  eapply plus_left; eauto.
  eapply star_right; eauto.
Qed.

Lemma plus_left':
  forall ge s1 s2 s3,
  step ge s1 s2 -> plus ge s2 s3 ->
  plus ge s1 s3.
Proof.
  intros. eapply plus_left; eauto. apply plus_star; auto.
Qed.

Lemma plus_right':
  forall ge s1 s2 s3,
  plus ge s1 s2 -> step ge s2 s3 ->
  plus ge s1 s3.
Proof.
  intros. eapply plus_right; eauto. apply plus_star; auto.
Qed.

Lemma plus_star_trans:
  forall ge s1 s2 s3,
  plus ge s1 s2 -> star ge s2 s3 -> plus ge s1 s3.
Proof.
  intros. inversion H; subst.
  econstructor; eauto. eapply star_trans; eauto.
Qed.

Lemma star_plus_trans:
  forall ge s1 s2 s3,
  star ge s1 s2 -> plus ge s2 s3 -> plus ge s1 s3.
Proof.
  intros. inversion H; subst.
  simpl; auto.
  econstructor. eauto. eapply star_trans. eauto.
  apply plus_star. eauto.
Qed.

Lemma plus_trans:
  forall ge s1 s2 s3,
  plus ge s1 s2 -> plus ge s2 s3 -> plus ge s1 s3.
Proof.
  intros. eapply plus_star_trans. eauto. apply plus_star. eauto.
Qed.

Lemma plus_inv:
  forall ge s1 s2,
  plus ge s1 s2 ->
  step ge s1 s2 \/ exists s', step ge s1 s' /\ plus ge s' s2.
Proof.
  intros. inversion H; subst. inversion H1; subst.
  left. auto.
  right. exists s3; split. auto.
  econstructor; eauto.
Qed.

Lemma star_inv:
  forall ge s1 s2,
  star ge s1 s2 ->
  s2 = s1 \/ plus ge s1 s2.
Proof.
  intros. inv H. left; auto. right; econstructor; eauto.
Qed.

Counted sequences of transitions

Inductive starN (ge: genv): nat -> state -> state -> Prop :=
  | starN_refl: forall s,
      starN ge O s s
  | starN_step: forall n s s' s'',
      step ge s s' -> starN ge n s' s'' ->
      starN ge (S n) s s''.

Remark starN_star:
  forall ge n s s', starN ge n s s' -> star ge s s'.
Proof.
  induction 1; econstructor; eauto.
Qed.

Remark star_starN:
  forall ge s s', star ge s s' -> exists n, starN ge n s s'.
Proof.
  induction 1.
  exists O; constructor.
  destruct IHstar as [n P]. exists (S n); econstructor; eauto.
Qed.

Infinitely many transitions

CoInductive forever (ge: genv): state -> Prop :=
  | forever_intro: forall s1 s2,
      step ge s1 s2 -> forever ge s2 ->
      forever ge s1.

Lemma star_forever:
  forall ge s1 s2, star ge s1 s2 ->
    forever ge s2 ->
    forever ge s1.
Proof.
  induction 1; intros. simpl. auto.
  econstructor; eauto.
Qed.

An alternate, equivalent definition of forever that is useful for coinductive reasoning.

Variable A: Type.

Infinitely many silent transitions

CoInductive forever_silent (ge: genv): state -> Prop :=
  | forever_silent_intro: forall s1 s2,
      step ge s1 s2 -> forever_silent ge s2 ->
      forever_silent ge s1.

End CLOSURES.


Section TYPE.


Variable T : Type.
Variable Teq : T -> T -> Prop.

Hypothesis Teq_refl: forall t', Teq t' t'.

Our semantics has no order (related to well-founded recursion) associated to each state.
Record T_semantics : Type := Semantics {
  state: Type;
  funtype: Type;
  vartype: Type;
  step : Genv.t funtype vartype -> state -> state -> Prop;
  initial_state: state -> Prop;
  final_state: state -> T -> Prop;
  globalenv: Genv.t funtype vartype
}.

Notation semantics := T_semantics.

Handy notations.

Notation " 'Step' L " := (step L (globalenv L)) (at level 1) : smallstep_scope.
Notation " 'Star' L " := (star (step L) (globalenv L)) (at level 1) : smallstep_scope.
Notation " 'Plus' L " := (plus (step L) (globalenv L)) (at level 1) : smallstep_scope.
Notation " 'Forever_silent' L " := (forever_silent (step L) (globalenv L)) (at level 1) : smallstep_scope.
Notation " 'Nostep' L " := (nostep (step L) (globalenv L)) (at level 1) : smallstep_scope.

Open Scope smallstep_scope.

Forward simulations between two transition semantics.


The general form of a forward simulation.

Weak simulations do not preserve diverging behaviors, due to the lack of ordering relation between states.
Record forward_simulation (L1 L2: semantics) : Type :=
  Forward_simulation {
    fsim_match_states :> state L1 -> state L2 -> Prop;
    fsim_match_initial_states:
      forall s1, initial_state L1 s1 ->
        exists s2, initial_state L2 s2 /\ fsim_match_states s1 s2;
    fsim_match_final_states:
      forall s1 s2 t'1 t'2,
      fsim_match_states s1 s2 -> Teq t'1 t'2 -> final_state L1 s1 t'1 -> final_state L2 s2 t'2;
    fsim_simulation:
      forall s1 s1', Step L1 s1 s1' ->
      forall s2, fsim_match_states s1 s2 ->
        exists s2',
          Star L2 s2 s2'
      /\ fsim_match_states s1' s2';
    fsim_symbols_preserved:
      forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id
  }.

Implicit Arguments forward_simulation [].

Forward simulation diagrams.


Various simulation diagrams that imply forward simulation

Section FORWARD_SIMU_DIAGRAMS.

Variable L1: semantics.
Variable L2: semantics.

Hypothesis symbols_preserved:
  forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id.

Variable match_states: state L1 -> state L2 -> Prop.

Hypothesis match_initial_states:
  forall s1, initial_state L1 s1 ->
  exists s2, initial_state L2 s2 /\ match_states s1 s2.

Hypothesis match_final_states:
  forall s1 s2 t'1 t'2,
  match_states s1 s2 ->
  Teq t'1 t'2 ->
  final_state L1 s1 t'1 ->
  final_state L2 s2 t'2.

Simulation when one transition in the first program corresponds to zero, one or several transitions in the second program. However, there is no stuttering: infinitely many transitions in the source program must correspond to infinitely many transitions in the second program.

Section SIMULATION_STAR_WF.

Hypothesis simulation:
  forall s1 s1', Step L1 s1 s1' ->
  forall s2, match_states s1 s2 ->
  exists s2',
    Star L2 s2 s2'
  /\ match_states s1' s2'.

Lemma forward_simulation_star_wf: forward_simulation L1 L2.
Proof.
  apply Forward_simulation with
    (fsim_match_states := fun s1 s2 => match_states s1 s2);
  auto.
Qed.

End SIMULATION_STAR_WF.

End FORWARD_SIMU_DIAGRAMS.

Forward simulation of transition sequences


Section SIMULATION_SEQUENCES.

Variable bs : list positive.
Variable L1: semantics.
Variable L2: semantics.
Variable S: forward_simulation L1 L2.

Lemma simulation_star:
  forall s1 s1', Star L1 s1 s1' ->
    forall s2, S s1 s2 ->
      exists s2', Star L2 s2 s2' /\ S s1' s2'.
Proof.
  induction 1; intros.
  exists s2; split; auto. apply star_refl.
  exploit fsim_simulation; eauto. intros [s2' [A B]].
  exploit IHstar; eauto. intros [s2'' [C D]].
  exists s2''; split; auto. eapply star_trans; eauto.
Qed.

End SIMULATION_SEQUENCES.



Inductive function_behavior: Type :=
  | Terminates: T -> function_behavior
  | Diverges: function_behavior
  | Goes_wrong: function_behavior.

Definition not_wrong (beh: function_behavior) : Prop :=
  match beh with
  | Terminates _ => True
  | Diverges => True
  | Goes_wrong => False
  end.

Definition behavior_improves (beh1 beh2: function_behavior) : Prop :=
  beh1 = beh2 \/ beh1 = Goes_wrong.

Lemma behavior_improves_refl:
  forall beh, behavior_improves beh beh.
Proof.
  intros; red; auto.
Qed.

Lemma behavior_improves_trans:
  forall beh1 beh2 beh3,
  behavior_improves beh1 beh2 -> behavior_improves beh2 beh3 ->
  behavior_improves beh1 beh3.
Proof.
  intros. red. destruct H; destruct H0; subst; auto.
Qed.

Lemma behavior_improves_bot:
  forall beh, behavior_improves (Goes_wrong) beh.
Proof.
  intros. right. auto.
Qed.

Section PROGRAM_BEHAVIORS.

Variable L: semantics.

Inductive state_behaves (s: state L): function_behavior -> Prop :=
  | state_terminates: forall s' t',
      Star L s s' ->
      final_state L s' t' ->
      state_behaves s (Terminates t')
  | state_diverges: forall s',
      Star L s s' -> Forever_silent L s' ->
      state_behaves s (Diverges)
  | state_goes_wrong: forall s',
      Star L s s' ->
      Nostep L s' ->
      (forall r, ~final_state L s' r) ->
      state_behaves s (Goes_wrong).

Inductive function_behaves: function_behavior -> Prop :=
  | function_runs: forall s beh,
      initial_state L s -> state_behaves s beh ->
      function_behaves beh
  | function_goes_initially_wrong:
      (forall s, ~initial_state L s) ->
      function_behaves (Goes_wrong).

Lemma state_behaves_star:
  forall s1 s2 beh,
  Star L s1 s2 -> state_behaves s2 beh -> state_behaves s1 beh.
Proof.
  intros. inv H0.
  apply state_terminates with (s' := s'); auto; eapply star_trans; eauto.
  apply state_diverges with (s' := s'); auto; eapply star_trans; eauto.
  apply state_goes_wrong with (s' := s'); auto; eapply star_trans; eauto.
Qed.

Require Import Classical.
Require Import ClassicalEpsilon.

Lemma diverges_forever_silent:
  forall s0,
  (forall s1, Star L s0 s1 -> exists s2, Step L s1 s2) ->
  Forever_silent L s0.
Proof.
  cofix COINDHYP; intros.
  destruct (H s0) as [s1 ST]. constructor.
  econstructor. eexact ST. apply COINDHYP.
  intros. eapply H. eapply star_left; eauto.
Qed.

Lemma state_behaves_exists:
  forall s, exists beh, state_behaves s beh.
Proof.
  intros s0.
  destruct (classic (forall s1, Star L s0 s1 -> exists s2, Step L s1 s2)).
  destruct (classic (exists s1, Star L s0 s1 /\
                       (forall s2, Star L s1 s2 ->
                        exists s3, Step L s2 s3))).
  destruct H0 as [s1 [A B]].
  exists (Diverges); econstructor; eauto.
  apply diverges_forever_silent; auto.
  generalize (not_ex_all_not _ _ H0 s0). intro A; clear H0.
  destruct (not_and_or _ _ A).
  elim H0. apply star_refl.
  destruct (not_all_ex_not _ _ H0) as [s2 C]; clear H0.
  destruct (not_all_ex_not _ _ C) as [D E]; clear C.
  apply H in D. inv D.
  destruct (not_ex_all_not _ _ E) with (n := x); auto.
  destruct (not_all_ex_not _ _ H) as [s1 A]; clear H.
  destruct (not_all_ex_not _ _ A) as [B C]; clear A.
  destruct (classic (exists r, final_state L s1 r)) as [[r FINAL] | NOTFINAL].
  exists (Terminates r); econstructor; eauto.
  exists (Goes_wrong); econstructor; eauto. red. intros.
  intro.
  apply C. exists s'. auto.
Qed.

Theorem function_behaves_exists:
  exists beh, function_behaves beh.
Proof.
  destruct (classic (exists s, initial_state L s)) as [[s0 INIT] | NOTINIT].
  destruct (state_behaves_exists s0) as [beh SB].
  exists beh; econstructor; eauto.
  exists (Goes_wrong). apply function_goes_initially_wrong.
  intros. eapply not_ex_all_not; eauto.
Qed.

End PROGRAM_BEHAVIORS.

Section FORWARD_SIMULATIONS.

Variable L1: semantics.
Variable L2: semantics.
Variable S: forward_simulation L1 L2.

Lemma forward_simulation_state_terminates:
  forall s1 s2 t',
    S s1 s2 -> state_behaves L1 s1 (Terminates t') ->
    state_behaves L2 s2 (Terminates t').
Proof.
  intros. inv H0.
  exploit simulation_star; eauto. intros [s2' [A B]].
  econstructor; eauto. eapply fsim_match_final_states; eauto.
Qed.

Theorem forward_simulation_behavior_terminates:
  forall t',
    function_behaves L1 (Terminates t') ->
    function_behaves L2 (Terminates t').
Proof.
  intros. inv H.
  exploit (fsim_match_initial_states S); eauto. intros [s' [INIT MATCH]].
  exploit forward_simulation_state_terminates; eauto.
  intros. econstructor; eauto.
Qed.

End FORWARD_SIMULATIONS.

Record sem_deterministic (L: semantics) := mk_deterministic {
  det_step: forall s0 s1 s2,
    Step L s0 s1 -> Step L s0 s2 -> s1 = s2;
  det_initial_state: forall s1 s2,
    initial_state L s1 -> initial_state L s2 -> s1 = s2;
  det_final_state: forall s r1 r2,
    final_state L s r1 -> final_state L s r2 -> r1 = r2;
  det_final_nostep: forall s r,
    final_state L s r -> Nostep L s
}.

Section DETERM_SEM.

Variable L: semantics.
Hypothesis DET: sem_deterministic L.

Ltac use_step_deterministic :=
  match goal with
  | [ S1: Step L _ _, S2: Step L _ _ |- _ ] =>
    generalize (@det_step L DET _ _ _ S1 S2); intros EQ; subst
  end.

Determinism for finite transition sequences.

Lemma star_step_diamond:
  forall s0 s1, Star L s0 s1 ->
  forall s2, Star L s0 s2 ->
     (Star L s1 s2)
  \/ (Star L s2 s1).
Proof.
  induction 1; intros; auto.
  inv H1. right.
  econstructor; eauto.
  use_step_deterministic.
  exploit IHstar. eexact H3. intros A.
  destruct A. left; intuition. right; intuition.
Qed.

Ltac use_star_step_diamond :=
  match goal with
  | [ S1: Star L _ _, S2: Star L _ _ |- _ ] =>
    let P := fresh "P" in
    destruct (star_step_diamond S1 S2)
    as [ P | P ]; subst
 end.

Ltac use_nostep :=
  match goal with
  | [ S: Step L ?s _, NO: Nostep L ?s |- _ ] => elim (NO _ S)
  end.

Lemma star_step_triangle:
  forall s0 s1 s2,
  Star L s0 s1 ->
  Star L s0 s2 ->
  Nostep L s2 ->
  Star L s1 s2.
Proof.
  intros.
  use_star_step_diamond.
  auto.
  inv P. constructor.
  use_nostep.
Qed.

Ltac use_star_step_triangle :=
  match goal with
  | [ S1: Star L _ _, S2: Star L _ ?s2, NO: Nostep L ?s2 |- _ ] =>
    let P := fresh "P" in
    generalize (star_step_triangle S1 S2 NO); intros P
  end.

Lemma steps_deterministic:
  forall s0 s1 s2,
  Star L s0 s1 -> Star L s0 s2 ->
  Nostep L s1 -> Nostep L s2 ->
  s1 = s2.
Proof.
  intros. use_star_step_triangle. inv P.
  auto. use_nostep.
Qed.

Lemma terminates_not_goes_wrong:
  forall s s1 r s2,
  Star L s s1 -> final_state L s1 r ->
  Star L s s2 -> Nostep L s2 ->
  (forall r, ~final_state L s2 r) -> False.
Proof.
  intros.
  assert (s1 = s2).
    eapply steps_deterministic; eauto. eapply det_final_nostep; eauto.
  destruct H4; subst. elim (H3 _ H0).
Qed.

Determinism for infinite transition sequences.

Lemma star_final_not_forever_silent:
  forall s s', Star L s s' ->
  Nostep L s' ->
  Forever_silent L s -> False.
Proof.
  induction 1; intros.
  inv H0. use_nostep.
  inv H2. use_step_deterministic. eauto.
Qed.

Lemma star2_final_not_forever_silent:
  forall s s1 s2,
  Star L s s1 -> Nostep L s1 ->
  Star L s s2 -> Forever_silent L s2 ->
  False.
Proof.
  intros. use_star_step_triangle.
  eapply star_final_not_forever_silent. eexact P. eauto. auto.
Qed.

Lemma star_forever_silent_inv:
  forall s s', Star L s s' ->
  Forever_silent L s ->
  Forever_silent L s'.
Proof.
  induction 1; intros.
  auto.
  subst. inv H1. use_step_deterministic. eauto.
Qed.

Determinism for program executions

Lemma state_behaves_deterministic:
  forall s beh1 beh2,
  state_behaves L s beh1 -> state_behaves L s beh2 -> beh1 = beh2.
Proof.
  generalize (det_final_nostep DET); intro dfns.
  intros until beh2; intros BEH1 BEH2.
  inv BEH1; inv BEH2.
  assert (s' = s'0). eapply steps_deterministic; eauto.
  destruct H3. f_equal; auto. subst. eapply det_final_state; eauto.
  byContradiction. eapply star2_final_not_forever_silent with (s1 := s') (s2 := s'0); eauto.
  byContradiction. eapply terminates_not_goes_wrong with (s1 := s') (s2 := s'0); eauto.
  byContradiction. eapply star2_final_not_forever_silent with (s2 := s') (s1 := s'0); eauto.
  f_equal. use_star_step_diamond.
  exploit star_forever_silent_inv. eexact P. eauto.
  intros [A B]. subst; traceEq.
  exploit star_forever_silent_inv. eexact P. eauto.
  intros [A B]. subst; traceEq.
  byContradiction. eapply star2_final_not_forever_silent with (s1 := s'0) (s2 := s'); eauto.
  byContradiction. eapply terminates_not_goes_wrong with (s1 := s'0) (s2 := s'); eauto.
  byContradiction. eapply star2_final_not_forever_silent with (s1 := s') (s2 := s'0); eauto.
  assert (s' = s'0). eapply steps_deterministic; eauto.
  destruct H5. congruence.
Qed.

Theorem function_behaves_deterministic:
  forall beh1 beh2,
  function_behaves L beh1 -> function_behaves L beh2 ->
  beh1 = beh2.
Proof.
  intros until beh2; intros BEH1 BEH2. inv BEH1; inv BEH2.
  assert (s = s0) by (eapply det_initial_state; eauto). subst s0.
  eapply state_behaves_deterministic; eauto.
  elim (H1 _ H).
  elim (H _ H0).
  auto.
Qed.

End DETERM_SEM.

End TYPE.
Generated by coq2html