# 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
| NoneNone
| Some xf x
end.

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

Coplist: possibly infinite lists.
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 _ cCSingle _ 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 _ xx
| CCons _ x _x
end.

Definition next {A : Type} (l : coplist A) : option (coplist A) :=
match l with
| CSingle _ _None
| CCons _ _ xsSome 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 _ xCSingle _ (f x)
| CCons _ x xsCCons _ (f x) (map f xs)
end.

Applying a partial function n times, or up to n times

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'.