Library OracleLanguages.ProgrammingLanguage

Basic definitions about deterministic programming languages.
We specify a record signature whose inhabitants define a deterministic programming language.
This signature requires a type state for the dynamically changing part of the configuration while genv_type is the static part of the configuration (typically containing the source code and runtime constants and primitives).
This signature also requires that the semantics of the programming language is described by a small-step reduction function step. This reduction function is a partial function that may rewrite a dynamic state into a new dynamic state.
For practical reasons, the dynamic state must be equipped with a decidable equality.

Require Import Common.

Record language : Type :=
    return_type : Type;
    state : Type;
    genv_type : Type;

    step : genv_type state option state;
    state_final : state option return_type;
    state_final_no_step : genv s v, state_final s = Some v step genv s = None;

    prog : Type;
    initial_state : prog genv_type × state;

    genv_eq : genv_type genv_type Prop;
    genv_eq_refl : genv, genv_eq genv genv;
    genv_eq_sym : genv₁ genv₂, genv_eq genv₁ genv₂ genv_eq genv₂ genv₁;
    genv_eq_trans : genv₁ genv₂ genv₃,
        genv_eq genv₁ genv₂
        genv_eq genv₂ genv₃
        genv_eq genv₁ genv₃;
    genv_eq_dec : genv genv',
        {genv_eq genv genv'} + {¬ genv_eq genv genv'};

    state_eq : state state Prop;
    state_eq_refl : S, state_eq S S;
    state_eq_sym : S S', state_eq S S' state_eq S' S;
    state_eq_trans : S₁ S₂ S₃,
        state_eq S₁ S₂ state_eq S₂ S₃ state_eq S₁ S₃;
    state_eq_dec : S S',
        {state_eq S S'} + {¬ state_eq S S'};

    state_final_eq : S S',
        state_eq S S'
        state_final S = state_final S';
    step_eq : genv₁ genv₂ S₁ S₂ S₁' S₂',
        genv_eq genv₁ genv₂
        state_eq S₁ S₂
        step genv₁ S₁ = Some S₁'
        step genv₂ S₂ = Some S₂'
        state_eq S₁' S₂';
    step_eq' : genv₁ genv₂ S₁ S₂,
        genv_eq genv₁ genv₂
        state_eq S₁ S₂
        step genv₁ S₁ = None step genv₂ S₂ = None

We call a configuration the pair of the static global environment and the dynamic state of a program.

Definition configuration (L : language) : Type := genv_type L × state L.

Definition initial_configuration {L : language} (p : prog L) :=
  initial_state L p.

Definition configuration_eq {L : language} (c₁ c₂ : configuration L) :=
  genv_eq L (fst c₁) (fst c₂) state_eq L (snd c₁) (snd c₂).

Definition opt_state_eq {L : language} (oS₁ oS₂ : option (state L)) : Prop :=
  (oS₁ = None oS₂ = None)
   S₁ S₂, oS₁ = Some S₁ oS₂ = Some S₂ state_eq L S₁ S₂.

Lemma opt_state_eq_dec:
   {L : language} (oS₁ oS₂ : option (state L)),
    { opt_state_eq oS₁ oS₂ } + { ¬ opt_state_eq oS₁ oS₂ }.

Lemma state_eq__opt_state_eq:
   {L} (S₁ S₂ : state L),
    state_eq L S₁ S₂ opt_state_eq (Some S₁) (Some S₂).

Lemma opt_state_eq_Some_r__state_eq:
   {L} (S : state L) (oS : option (state L)),
    opt_state_eq oS (Some S)
     S', oS = Some S' state_eq L S' S.

Lemma opt_state_eq_refl:
   {L} (oS : option (state L)),
    opt_state_eq oS oS.

Lemma opt_state_eq_sym:
   {L} (oS₁ oS₂ : option (state L)),
    opt_state_eq oS₁ oS₂ opt_state_eq oS₂ oS₁.

Lemma opt_state_eq_trans:
   {L} (oS₁ oS₂ oS₃ : option (state L)),
    opt_state_eq oS₁ oS₂ opt_state_eq oS₂ oS₃ opt_state_eq oS₁ oS₃.

We use nsteps to repeatedly call the reduction function step. As step is a partial function, so is nsteps.
We also define a total function nsteps' that always return a state together with the number of reduction steps it could not perform.
Hence, if nsteps' n state = (state', 0), the reduction function has been applied n times successfully (nsteps_nsteps'_0_iff). On the other hand, if nsteps' n state = (state', S n'), state' is guaranteed to be a stuck state and was obtained by rewriting state n - S n' times.

Definition nsteps {lang : language} (genv : genv_type lang)
           (n : nat) (S : state lang) : option (state lang) :=
  napply (step lang genv) n S.

Definition nsteps' {lang : language} (genv : genv_type lang)
           (n : nat) (S : state lang) : state lang × nat :=
  napply' (step lang genv) n S.

Lemma nsteps_eq:
   {L : language} (genv₁ genv₂ : genv_type L) (S₁ S₂ : state L) (n : nat),
    genv_eq L genv₁ genv₂
    state_eq L S₁ S₂
    opt_state_eq (nsteps genv₁ n S₁) (nsteps genv₂ n S₂).

Lemma nsteps_plus_0:
   {L : language} (genv : genv_type L) {n₁ n₂ : nat} (S₁ : state L),
    nsteps genv (n₁ + n₂) S₁ = nsteps genv n₁ S₁ >>= λ S₂, nsteps genv n₂ S₂.

Lemma nsteps_plus_1:
   {L : language} (genv : genv_type L) {n₁ n₂ : nat} (S₁ S₂ : state L),
    nsteps genv n₁ S₁ = Some S₂ nsteps genv (n₁ + n₂) S₁ = nsteps genv n₂ S₂.

Lemma nsteps_plus_1':
   {L : language} (genv : genv_type L) {n₁ n₂ : nat} (S₁ S₂ : state L),
    opt_state_eq (nsteps genv n₁ S₁) (Some S₂)
    opt_state_eq (nsteps genv (n₁ + n₂) S₁) (nsteps genv n₂ S₂).

Lemma nsteps_plus_2:
   {L} {genv : genv_type L} n n' S S',
    nsteps genv (n + n') S = Some S'
      nsteps genv n S = Some S₁.

Definition terminates {L} genv S :=
   n S', nsteps genv n S = Some S' step L genv S' = None.

Require Import Omega.

Lemma nsteps_split_helper:
   {L} genv n n' S S' oS',
    nsteps genv n S = Some S'
    step L genv S' = None
    opt_state_eq (nsteps genv n' S) oS'
    (n' = n)
     ( S', n > n' nsteps genv n' S = Some S')
     (n' > n nsteps genv n' S = None).