Library OracleLanguages.Imp.Oracles.Renaming

Require Import Common.
Require Import Imp.Lang.
Require Import ProgrammingLanguage.
Require Import OracleLanguage.

Module Make
       (Var_as_DT : UsualDecidableTypeOrig)
       (Import Lang : ImpProgrammingLanguage Var_as_DT).

  Definition bijective {A B : Type} (f : A → B) : Prop :=
    ∃ f', ∀ x y, f x = y ↔ f' y = x.

  Definition bijection (A B : Type) :=
    { f : A → B | bijective f }.

  Definition _genv := bijection varid varid.

  Inductive _state : Type :=
  | State : state → state → _state.

  Definition _step (_ : _genv) (S : _state) : option _state :=
    let '(State S₁ S₂) := S in
    match step tt S₁, step tt S₂ with
    | Some S₁', Some S₂' ⇒
      Some (State S₁' S₂')
    | _, _ ⇒
      None
    end.

  Definition _left_state (S : _state) : ProgrammingLanguage.state imp_language :=
    match S with
    | State S₁ _ ⇒ S₁
    end.

  Definition _right_state (S : _state) : ProgrammingLanguage.state imp_language :=
    match S with
    | State _ S₂ ⇒ S₂
    end.

  Fixpoint rename_exp (f : varid → varid) e :=
    match e with
    | Int n ⇒ Int n
    | Var x ⇒ Var (f x)
    | Sum e₁ e₂ ⇒ Sum (rename_exp f e₁) (rename_exp f e₂)
    | Sub e₁ e₂ ⇒ Sub (rename_exp f e₁) (rename_exp f e₂)
    | Mult e₁ e₂ ⇒ Mult (rename_exp f e₁) (rename_exp f e₂)
    | Div e₁ e₂ ⇒ Div (rename_exp f e₁) (rename_exp f e₂)
    | Modulo e₁ e₂ ⇒ Modulo (rename_exp f e₁) (rename_exp f e₂)
    end.

  Fixpoint rename_bexp (f : varid → varid) b :=
    match b with
    | True | False ⇒ b
    | EQ e₁ e₂ ⇒ EQ (rename_exp f e₁) (rename_exp f e₂)
    | LT e₁ e₂ ⇒ LT (rename_exp f e₁) (rename_exp f e₂)
    | LE e₁ e₂ ⇒ LE (rename_exp f e₁) (rename_exp f e₂)
    | EQB b₁ b₂ ⇒ EQB (rename_bexp f b₁) (rename_bexp f b₂)
    | AND b₁ b₂ ⇒ AND (rename_bexp f b₁) (rename_bexp f b₂)
    | OR b₁ b₂ ⇒ OR (rename_bexp f b₁) (rename_bexp f b₂)
    | NOT b ⇒ NOT (rename_bexp f b)
    end.

  Fixpoint rename_cmd (f : varid → varid) c :=
    match c with
    | Skip ⇒ Skip
    | Assign x e ⇒ Assign (f x) (rename_exp f e)
    | Seq c₁ c₂ ⇒ Seq (rename_cmd f c₁) (rename_cmd f c₂)
    | ITE b c₁ c₂ ⇒ ITE (rename_bexp f b) (rename_cmd f c₁) (rename_cmd f c₂)
    | While b c' ⇒ While (rename_bexp f b) (rename_cmd f c')
    | Assert b ⇒ Assert (rename_bexp f b)
    end.

  Definition rename_cont (f : varid → varid) k := List.map (rename_cmd f) k.
  Definition rename_store_helper (f : varid → varid) x v (s : store) := M.add (f x) v s.
  Definition rename_store (f : varid → varid) s :=
    M.fold (rename_store_helper f) s (M.empty _).

  Definition _invariant (m : _genv) (S : _state) : Prop :=
    let '(State (k₁, s₁) (k₂, s₂)) := S in
    let f := proj1_sig m in
    rename_cont f k₁ = k₂ ∧ M.Equal (rename_store f s₁) s₂.

  Lemma rename_store_preserves_values:
    ∀ f, bijective f →
    ∀ x s, M.find (f x) (rename_store f s) = M.find x s.

  Lemma rename_eval_exp:
    ∀ f, bijective f →
    ∀ s₁ s₂, M.Equal (rename_store f s₁) s₂ →
    ∀ e, eval_exp s₁ e = eval_exp s₂ (rename_exp f e).

  Lemma rename_eval_bexp:
    ∀ f, bijective f →
    ∀ s₁ s₂, M.Equal (rename_store f s₁) s₂ →
    ∀ b, eval_bexp s₁ b = eval_bexp s₂ (rename_bexp f b).

  Lemma rename_Equal:
    ∀ f, bijective f →
    ∀ s x, M.find x s = M.find (f x) (rename_store f s).

  Lemma rename_store_comm_add:
    ∀ f, bijective f →
    ∀ s x v,
    M.Equal (rename_store f (M.add x v s)) (M.add (f x) v (rename_store f s)).

  Lemma _invariant_1:
    ∀ genv os os',
      _invariant genv os →
      _step genv os = Some os' →
      _invariant genv os'.

  Lemma _prediction_soundness :
    ∀ genv os os',
      _invariant genv os →
      _step genv os = Some os' →
      ∃ n₁ n₂,
        opt_state_eq (nsteps υ n₁ (_left_state os))
                       (Some (_left_state os'))
        ∧ opt_state_eq (nsteps υ n₂ (_right_state os))
                       (Some (_right_state os'))
        ∧ n₁ + n₂ > 0.

  Lemma _prediction_completeness :
    ∀ genv os,
      _invariant genv os →
      _step genv os = None →
      step tt (_left_state os) = None
      ∧ step tt (_right_state os) = None.

  Definition renaming_oracle : oracle_language imp_language imp_language :=
    {|
      oracle_state := _state;
      oracle_genv := _genv;
      oracle_step := _step;
      left_state := _left_state;
      right_state := _right_state;
      left_genv := λ _, υ;
      right_genv := λ _, υ;
      invariant := _invariant;
      invariant_1 := _invariant_1;
      prediction_soundness := _prediction_soundness;
      prediction_completeness := _prediction_completeness
    |}.
End Make.