include "basics/list.ma".

let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
match l with
[ nil ⇒ None ?
| cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
].

let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
match l with
[ nil ⇒ True
| cons h t ⇒ P h ∧ All A P t
].

lemma All_mp : ∀A,P,Q. (∀a.P a → Q a) → ∀l. All A P l → All A Q l.
#A #P #Q #H #l elim l normalize //
#h #t #IH * /3/
qed.

let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
match l with
[ nil ⇒ false
| cons h t ⇒ orb (p h) (exists A p t)
].

let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
match l with
[ nil ⇒ False
| cons h t ⇒ (P h) ∨ (Exists A P t)
].

lemma Exists_append : ∀A,P,l1,l2.
  Exists A P (l1 @ l2) → Exists A P l1 ∨ Exists A P l2.
#A #P #l1 elim l1
[ normalize /2/
| #h #t #IH #l2 *
  [ #H /3/
  | #H cases (IH l2 H) /3/
  ]
] qed.

lemma map_append : ∀A,B,f,l1,l2.
  (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
#A #B #f #l1 elim l1
[ #l2 @refl
| #h #t #IH #l2 normalize //
] qed.

let rec find (A,B:Type[0]) (f:A → option B) (l:list A) on l : option B ≝
match l with
[ nil ⇒ None B
| cons h t ⇒
    match f h with
    [ None ⇒ find A B f t
    | Some b ⇒ Some B b
    ]
].