From ShiftReset Require Import Basics ShiftFree.

Reduction rules

Lemma red_normal : forall f,
shift_free f ->
entails (rs f) f.

Proof.

  introv Hsf.
  unfold entails. intros.
  inverts H as H; destr H.
  { (* this case cannot be as f is shift-free *)
    apply Hsf in H.
    false. }
  { assumption. }
Qed.

Lemma red_skip : forall f1 f2,
shift_free f1 ->
entails (rs (f1;; f2)) (f1;; rs f2).

Proof.

  introv Hsf.
  unfold entails. intros.
  inverts H as H; destr H.
  { (* if either f1 or f2 produce a shift *)
    inverts H as H. destr H.
    { (* f2 produces a shift *)
      eapply s_seq.
      exact H.
      eapply s_rs_sh.
      exact H8. eassumption. }
    { (* f1 cannot produce a shift as it is shift-free *)
      apply Hsf in H.
      false. } }
  { (* if f1 returns *)
    inverts H as H. destr H.
    eapply s_seq.
    exact H.
    apply s_rs_val.
    assumption. }
Qed.

Lemma red_skip_conv : forall f1 f2,
shift_free f1 ->
entails (f1;; rs f2) (rs (f1;; f2)).

Proof.

  introv Hsf. unfold entails. intros.

  inverts H as H. 2: { apply Hsf in H. false. }
  inverts H7 as H7.

  { eapply s_rs_sh.
    apply* s_seq.
    eassumption. }
  { apply s_rs_val.
    apply* s_seq. }
Qed.

Lemma red_skip2 : forall f1 f2,
shift_free f1 ->
bientails (rs (f1;; f2)) (f1;; rs f2).

Proof.

  introv Hsf.
  unfold bientails. iff H.
  { apply* red_skip. }

  inverts H as H. 2: { apply Hsf in H. false. }
  inverts H7 as H7.

  { eapply s_rs_sh.
    apply* s_seq.
    eassumption. }
  { apply s_rs_val.
    apply* s_seq. }
Qed.

Module ReductionOld

Reduction rules