Library OracleLanguages.Oracles.Identity

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

Parameter L : language.

Definition _state := state L.

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

Lemma _prediction_completeness:
  ∀ genv os,
    True →
    step L genv os = None →
    step L genv os = None
    ∧ step L genv os = None.

Definition identity_oracle : oracle_language L L :=
  {|
    oracle_state := _state;
    oracle_genv := genv_type L;
    oracle_step := step L;
    left_state := id;
    right_state := id;
    left_genv := id;
    right_genv := id;
    invariant := λ _ _, True;
    invariant_1 := λ genv os os' _ _, I;
    prediction_soundness := _prediction_soundness;
    prediction_completeness := _prediction_completeness;
  |}.