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;
|}.