Library OracleLanguages.Imp.SmallStep

Small-step semantics and change-indexed presentation of small-step semantics of the Imp imperative language.

Require Import Common.
Require Import Imp.Syntax.
Require Import List.
Import ListNotations.

Module Imp (Var_as_DT : UsualDecidableTypeOrig).
  Module Syntax := Imp.Syntax.Imp Var_as_DT.
  Export Syntax.

  Definition cont := list cmd.
  Definition state := prod cont store.

  Definition state_eq (S₁ S₂ : state) : Prop :=
    let '(k₁, s₁) := S₁ in
    let '(k₂, s₂) := S₂ in
    k₁ = k₂ M.Equal s₁ s₂.

  Lemma state_eq_dec:
     S₁ S₂, {state_eq S₁ S₂} + {¬ state_eq S₁ S₂}.

  Definition beq_state (S₁ S₂ : state) :=
    if state_eq_dec S₁ S₂ then true else false.

  Lemma state_eq_sym:
     S₁ S₂,
    state_eq S₁ S₂ state_eq S₂ S₁.

  Lemma state_eq_refl:
    state_eq S S.

  Lemma state_eq_trans:
     S₁ S₂ S₃,
    state_eq S₁ S₂
    state_eq S₂ S₃
    state_eq S₁ S₃.

  Definition state_final (S : state) :=
    match S with
      | ([], _)Some tt
      | _None

  Lemma state_final_eq:
     S S',
      state_eq S S'
      state_final S = state_final S'.

  Definition step (_ : unit) (S : state) : option state :=
    let '(k, s) := S in
    match k with
    | []None
    | Skip::k'ret (k', s)
    | (Seq c₁ c₂)::k'ret (c₁::c₂::k', s)
    | (Assign x e)::k'eval_exp s e >>= λ v,
      ret (k', M.add x v s)
    | (ITE b c₁ c₂)::k'eval_bexp s b >>= λ v,
      ret ((if v then c₁ else c₂)::k', s)
    | (While b c')::k'eval_bexp s b >>= λ v,
      ret (if v then (c'::(While b c')::k', s) else (k', s))
    | (Assert b)::k'
      eval_bexp s b >>= λ v,
      if v then ret (k', s)
      else None

  Lemma step_app:
     k k' k₂ s s', step tt (k, s) = Some (k', s')
    step tt (k ++ k₂, s) = Some (k' ++ k₂, s').

  Lemma step_eq:
     genv₁ genv₂ S₁ S₂ S₁' S₂',
      genv₁ = genv₂
      state_eq S₁ S₂
      step genv₁ S₁ = Some S₁'
      step genv₂ S₂ = Some S₂'
      state_eq S₁' S₂'.

  Lemma step_eq':
     genv₁ genv₂ S₁ S₂,
      genv₁ = genv₂
      state_eq S₁ S₂
      step genv₁ S₁ = None step genv₂ S₂ = None.

  Inductive finite_small_step_exec s : state Prop :=
    | Halted : finite_small_step_exec s ([], s)
    | Step : S S',
      step tt S = Some S'
      finite_small_step_exec s S'
      finite_small_step_exec s S.

  Hint Constructors finite_small_step_exec.

  CoInductive infinite_small_step_exec : state Prop :=
    | InfStep : S S',
      step tt S = Some S'
      infinite_small_step_exec S'
      infinite_small_step_exec S.
End Imp.