Library OracleLanguages.Common

Require Export Utf8.
Require Export List.
Export ListNotations.
Require Export Equalities.
Require Export Bool.

Definition ret {A : Type} (x : A) := Some x.
Definition bind {A B : Type} (a : option A) (f : A → option B) :=
    match a with
    | None ⇒ None
    | Some x ⇒ f x
    end.

Notation "a >>= f" := (bind a f) (at level 40, left associativity).

CoInductive coplist (A : Type) : Type :=
| CSingle : A → coplist A
| CCons : A → coplist A → coplist A.

Definition coplist_id_force (A : Type) (l : coplist A)
  : coplist A :=
  match l with
  | CCons _ c l' ⇒ CCons _ c l'
  | CSingle _ c ⇒ CSingle _ c
  end.

Lemma coplist_id_force_eq:
  ∀ A l, coplist_id_force A l = l.

Definition first {A : Type} (l : coplist A) : A :=
match l with
| CSingle _ x ⇒ x
| CCons _ x _ ⇒ x
end.

Definition next {A : Type} (l : coplist A) : option (coplist A) :=
match l with
| CSingle _ _ ⇒ None
| CCons _ _ xs ⇒ Some xs
end.

Fixpoint skipn {A : Type} (n : nat) (l : coplist A) :=
  match n with
  | 0 ⇒ Some l
  | S n' ⇒ next l >>= λ l',
            skipn n' l'
  end.

CoInductive coplist_in {A : Type} : A → coplist A → Prop :=
| CoplistInHead : ∀ x l, coplist_in x (CCons _ x l)
| CoplistInSingle : ∀ x, coplist_in x (CSingle _ x)
| CoplistInTail : ∀ x y l, coplist_in x l → coplist_in x (CCons _ y l).

Fixpoint take {A} (n : nat) (l : coplist A) : list A × option (coplist A) :=
  match n with
    | O ⇒ (nil, Some l)
    | S k ⇒
      match next l with
      | None ⇒
        (first l :: nil, None)
      | Some l ⇒
        let r := take k l in
        (first l :: fst r, snd r)
      end
  end.

CoFixpoint map {A B : Type} f (s : coplist A) : coplist B :=
  match s with
    | CSingle _ x ⇒ CSingle _ (f x)
    | CCons _ x xs ⇒ CCons _ (f x) (map f xs)
  end.

Fixpoint napply {A : Type} (f : A → option A) (n : nat) (a : A) : option A :=
  match n with
  | 0 ⇒
    Some a
  | S n' ⇒
    f a >>= λ a',
    napply f n' a'
  end.

Fixpoint napply' {A : Type} (f : A → option A) (n : nat) (a : A) :
  A × nat :=
  match n with
  | 0 ⇒
    (a, 0)
  | S n' ⇒
    match f a with
    | Some a' ⇒
      napply' f n' a'
    | None ⇒
      (a, n)
    end
  end.

Property napply'_1:
  ∀ {A : Type} (f : A → option A) n a a' n',
    napply' f n a = (a', n') → n' ≤ n.

Property napply_napply'_Sn_iff:
  ∀ {A : Type} (f : A → option A) n a,
    napply f n a = None ↔
    ∃ n' a',
      napply' f n a = (a', S n') ∧ f a' = None.

Property napply'_prefix:
  ∀ {A : Type} (f : A → option A) n n' a a',
    napply' f n a = (a', n') →
    napply' f (n - n') a = (a', 0).

Property napply_napply'_0_iff:
  ∀ {A : Type} (f : A → option A) n a a',
    napply f n a = Some a' ↔ napply' f n a = (a', 0).

Require Import Omega.

Property napply'_lt_id:
  ∀ {A : Type} (f : A → option A) n n' a a',
    napply' f n a = (a', n') → n - n' = 0 →
    a = a'.