Library mcertikos.objects.dev.LOracle

Require Import Coqlib.
Require Import List.
Require Import Bool.
Require Export Oracle.

Module LOracle (E: Event) : Oracle
  with Definition Time := nat
  with Definition Entry:= E.T.

  Definition Time := nat.
  Definition Entry:= E.T.
  Definition Tape := list Entry.

  Open Scope nat_scope.

  Definition span := 100 %nat.

  Definition tlt (x y: Time): Prop := lt x y.

  Definition tle (x y: Time): Prop := le x y.

  Definition empty: Tape := nil.

  Definition default := E.d.

  Fixpoint get (t: Time)(l: Tape): option Entry :=
    match t, l with
      | O, x :: l´ ⇒ Some x
      | _, nil ⇒ None
      | S t´, x :: l´ ⇒ get t´ l´
    end.

  Definition valid (l: Tape): Prop :=
   span ≤ length l.

  Theorem empty_def: ∀ t:Time,
      get t empty = None.
  Proof.
    unfold get, empty. destruct t; trivial.
  Qed.

  Theorem order: ∀ a b: Time,
      {tlt a b} + {a = b} + {¬tle a b}.
  Proof.
    unfold Time, tlt, tle.
    intros a b.
    case (lt_dec a b).
    - intros. left. left. trivial.
    - intros. case (le_dec a b).
      + apply not_lt in n. intros.
        left. right. omega.
      + right. exact n0.
  Qed.

  Lemma valid_range_list: ∀ (t: Time) (l: Tape),
      tlt t (length l) →
      ∃ e,
        get t l = Some e.
  Proof.
    unfold tlt. induction t.
    - intros. destruct l.
      + inversion H.
      + simpl. ∃ e. reflexivity.
    - destruct l.
      + inversion 1.
      + simpl. intros. apply IHt. omega.
  Qed.

  Theorem valid_range: ∀ (t: Time) (l: Tape),
      valid l →
      tlt t span →
      ∃ e,
        get t l = Some e.
  Proof.
    unfold valid, tlt.
    intros.
    assert (Htran: t < length l) by omega.
    apply valid_range_list.
    unfold tlt. assumption.
  Qed.

End LOracle.