Library OracleLanguages.Oracles.UniversalOracle

Require Import Common.
Require Import ProgrammingLanguage.
Require Import OracleLanguage.

Parameters L₁ L₂ : language.

Definition _state : Type := state L₁ × state L₂.
Definition _genv : Type := genv_type L₁ × genv_type L₂.

Definition _step (genv : _genv) (S : _state) : option _state :=
  let '(S₁, S₂) := S in
  match step L₁ (fst genv) S₁, step L₂ (snd genv) S₂ with
  | None, None ⇒ None
  | Some S₁', Some S₂' ⇒ Some (S₁', S₂')
  | Some S₁', None ⇒ Some (S₁', S₂)
  | None, Some S₂' ⇒ Some (S₁, S₂')
  end.

Lemma _prediction_soundness:
  ∀ genv os os',
    True →
    _step genv os = Some os' →
    ∃ n₁ n₂,
      opt_state_eq (nsteps (fst genv) n₁ (fst os))
                     (Some (fst os'))
      ∧ opt_state_eq (nsteps (snd genv) n₂ (snd os))
                     (Some (snd os'))
      ∧ n₁ + n₂ > 0.

Lemma _prediction_completeness:
  ∀ genv os,
    True →
    _step genv os = None →
    step L₁ (fst genv) (fst os) = None
    ∧ step L₂ (snd genv) (snd os) = None.

Definition universal_oracle : oracle_language L₁ L₂ :=
  {|
    oracle_state := _state;
    oracle_genv := _genv;
    oracle_step := _step;
    left_state := fst;
    right_state := snd;
    left_genv := fst;
    right_genv := snd;
    invariant := λ _ _, True;
    invariant_1 := λ genv os os' _ _, I;
    prediction_soundness := _prediction_soundness;
    prediction_completeness := _prediction_completeness
  |}.