Require Import Bool.
Require Import EqNat.
Require Import List.

Require Import util.

Module Type ORACLE.
  Parameter t : Set.
  Parameter empty : t.
  Definition key := nat.
  Definition value := nat.

  Parameter length : t -> nat.

  Parameter keys : t -> list key.
  Parameter values : t -> list value.

  Parameter values_size: forall o l,
    length o = l -> List.length (values o) = l.

  Parameter nth_key : nat -> t -> (*default value*)key -> key.
  Parameter nth_key' : nat -> t -> option key.
  Parameter nth_value : nat -> t -> (*default value*)value -> value.
  Parameter nth_value' : nat -> t -> option value.
  Parameter nth_record : nat -> t -> option (key * value).

  Parameter In_nth_key' : forall k o,
    In k (keys o) ->
    exists i, i < length o /\ nth_key' i o = Some k.
  Parameter nth_nth_value : forall i o,
    nth i (values o) O = nth_value i o O.

  (* look for an element in the keys; O if not found, 1 o.w. *)
  Parameter find_key : key -> t -> nat. 
  Parameter find_value : value -> t -> nat.

  Parameter find_key_length_O : forall o,
    length o = O -> forall k, find_key k o = O.
  Parameter find_value_length_O : forall o,
    length o = O -> forall v, find_value v o = O.
  Parameter not_In_find_key_zero : forall k o,
    ~ In k (keys o) -> find_key k o = O.
  Parameter find_value_In_values: forall o v,
    (find_value v o > 0)%nat -> In v (values o).
  Parameter find_value_not_In_values: forall o v,
    find_value v o = O -> ~ In v (values o).

  Parameter insert : key -> value -> t -> t.

  Parameter In_value_insert' : forall v vs o,
    In v (keys (insert v vs o)).
  Parameter insert_new_len : forall o k v, 
    find_key k o = O -> length (insert k v o) = S (length o).
  Parameter insert_len_le : forall o k v, 
    length (insert k v o) >= length o.
  Parameter nth_key'_insert : forall o l,
    length o = l ->
    forall k, find_key k o = O ->
      forall v, nth_key' l (insert k v o) = Some k.
  Parameter nth_value_insert : forall i k v o def,
    find_key k o = O ->
    length o = i ->
    nth_value i (insert k v o) def = v.
  Parameter nth_key'_insert' : forall i o k k' v,
    nth_key' i o = Some k ->
    nth_key' i (insert k' v o) = Some k.
  Parameter nth_value_values : forall o i def,
    nth_value i o def = nth i (values o) def.
  Parameter nth_value_insert' : forall i k v o def,
    length o > i ->
    nth_value i (insert k v o) def = nth_value i o def.
  Parameter find_key_insert: forall t v x y, 
    find_key v (insert x y t) = O ->
    find_key v t = O.
End ORACLE.

Module Oracle : ORACLE.
  Axiom t : Set.
  Axiom empty : t.
  Definition key := nat.
  Definition value := nat.

  Axiom length : t -> nat.

  Axiom keys : t -> list key.
  Axiom values : t -> list value.

  Axiom values_size: forall o l,
    length o = l -> List.length (values o) = l.

  Axiom nth_key : nat -> t -> (*default value*)key -> key.
  Axiom nth_key' : nat -> t -> option key.
  Axiom nth_value : nat -> t -> (*default value*)value -> value.
  Axiom nth_value' : nat -> t -> option value.
  Axiom nth_record : nat -> t -> option (key * value).

  Axiom In_nth_key' : forall k o,
    In k (keys o) ->
    exists i, i < length o /\ nth_key' i o = Some k.
  Axiom nth_nth_value : forall i o,
    nth i (values o) O = nth_value i o O.

  (* look for an element in the keys; O if not found, 1 o.w. *)
  Axiom find_key : key -> t -> nat. 
  Axiom find_value : value -> t -> nat.

  Axiom find_key_length_O : forall o,
    length o = O -> forall k, find_key k o = O.
  Axiom find_value_length_O : forall o,
    length o = O -> forall v, find_value v o = O.
  Axiom not_In_find_key_zero : forall k o,
    ~ In k (keys o) -> find_key k o = O.
  Axiom find_value_In_values: forall o v,
    find_value v o > 0 -> In v (values o).
  Axiom find_value_not_In_values: forall o v,
    find_value v o = O -> ~ In v (values o).

  Axiom insert : key -> value -> t -> t.

  Axiom In_value_insert' : forall v vs o,
    In v (keys (insert v vs o)).
  Axiom insert_new_len : forall o k v, 
    find_key k o = O -> length (insert k v o) = S (length o).
  Axiom insert_len_le : forall o k v, 
    length (insert k v o) >= length o.
  Axiom nth_key'_insert : forall o l,
    length o = l ->
    forall k, find_key k o = O ->
      forall v, nth_key' l (insert k v o) = Some k.
  Axiom nth_value_insert : forall i k v o def,
    find_key k o = O ->
    length o = i ->
    nth_value i (insert k v o) def = v.
  Axiom nth_key'_insert' : forall i o k k' v,
    nth_key' i o = Some k ->
    nth_key' i (insert k' v o) = Some k.
  Axiom nth_value_values : forall o i def,
    nth_value i o def = nth i (values o) def.
  Axiom nth_value_insert' : forall i k v o def,
    length o > i ->
    nth_value i (insert k v o) def = nth_value i o def.
  Axiom find_key_insert: forall t v x y, 
    find_key v (insert x y t) = O ->
    find_key v t = O.
End Oracle.