🍃 List.v

Environment

See proofs, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Proto_alpha.Environment.Either.
Require Proto_alpha.Environment.Error_monad.
Require Proto_alpha.Environment.Pervasives.
Require Proto_alpha.Environment.Seq.
Import Error_monad.Notations.
Import Pervasives.Notations.

Definition t (a : Set) : Set := list a.

Definition nil : ∀ {a : Set}, list a :=
  fun _ ⇒
  [].

Definition nil_e : ∀ {a trace : Set}, Pervasives.result (list a) trace :=
  fun _ _ ⇒
  return? [].

Definition nil_s : ∀ {a : Set}, list a :=
  fun _ ⇒
  [].

Definition nil_es : ∀ {a trace : Set},
  Pervasives.result (list a) trace :=
  fun _ _ ⇒
  return? [].

Parameter cons_value : ∀ {a : Set}, a → list a → list a.

Definition hd : ∀ {a : Set}, list a → option a :=
  fun _ l ⇒
    match l with
    | [] ⇒ None
    | x :: _ ⇒ Some x
    end.

Definition tl : ∀ {a : Set}, list a → option (list a) :=
  fun _ l ⇒
    match l with
    | [] ⇒ None
    | _x :: m ⇒ Some m
    end.

Fixpoint nth_z {a : Set} (l : list a) (i : Z.t) {struct l} : option a :=
  match l, i with
  | [], _ ⇒ None
  | x :: _, 0 ⇒ Some x
  | _ :: l, _ ⇒ nth_z l (i - 1)
  end.

Definition nth : ∀ {a : Set}, list a → int → option a :=
  @nth_z.

Definition nth_opt : ∀ {a : Set}, list a → int → option a :=
  @nth_z.

Definition last : ∀ {a : Set}, a → list a → a :=
  fun _ x l ⇒
  List.last l x.

Fixpoint last_opt {a : Set} (l: list a) : option a :=
  match l with
  | [] ⇒ None
  | [z] ⇒ Some z
  | x :: tl ⇒ (last_opt tl)
  end.

Definition find : ∀ {a : Set}, (a → bool) → list a → option a :=
  fun a ⇒
  List.find (A := a).

Definition find_opt : ∀ {a : Set}, (a → bool) → list a → option a :=
  fun _ ⇒
  find.

Parameter find_map : ∀ {a b : Set},
  (a → option b) → list a → option b.

Fixpoint mem {a : Set} (eq_dec : a → a → bool) (v : a) (l : list a) : bool :=
  match l with
  | [] ⇒ false
  | x :: l ⇒ eq_dec v x || mem eq_dec v l
  end.

Fixpoint assoc {a b : Set}
  (eq : a → a → bool)
  (k : a)
  (l : list (a × b))
  : option b :=
  match l with
  | [] ⇒ None
  | (h, x) :: tl ⇒ if eq k h then Some x else assoc eq k tl
  end.

Definition assoc_opt : ∀ {a b : Set},
  (a → a → bool) → a → list (a × b) → option b :=
  fun _ _ ⇒ assoc.

Parameter assq : ∀ {a b : Set}, a → list (a × b) → option b.

Parameter assq_opt : ∀ {a b : Set}, a → list (a × b) → option b.

Fixpoint mem_assoc {a b : Set}
  (eq : a → a → bool)
  (k : a)
  (l : list (a × b))
  : bool :=
  match l with
  | [] ⇒ false
  | (h, x) :: tl ⇒ eq k h || mem_assoc eq k tl
  end.

Parameter mem_assq : ∀ {a b : Set}, a → list (a × b) → bool.

Fixpoint remove_assoc {a b : Set}
  (eq : a → a → bool)
  (k : a)
  (l : list (a × b))
  : list (a × b) :=
  match l with
  | [] ⇒ []
  | (h, x) :: tl ⇒
    if eq k h then
      tl
    else
      (h, x) :: remove_assoc eq k tl
  end.

Parameter remove_assq : ∀ {a b : Set}, a → list (a × b) → list (a × b).

Fixpoint nat_init {a trace : Set} (er : trace) (n : nat) (ff : nat → a)
  : list a :=
  match n with
  | 0%nat ⇒ []
  | S k ⇒ ff 0%nat :: nat_init er k (fun v ⇒ ff (S v))
  end.

Definition init_value {a trace : Set}
  (er : trace) (n : int) (ff : int → a)
  : Pervasives.result (list a) trace :=
  match n with
  | Zneg _ ⇒ Pervasives.Error er
  | Z0 ⇒ Pervasives.Ok []
  | Zpos x ⇒
    Pervasives.Ok (nat_init er (Z.to_nat n) (fun x ⇒ ff (Z.of_nat x)))
  end.

Fixpoint length {a : Set} (l : list a) : int :=
  match l with
  | [] ⇒ 0
  | _ :: l ⇒ (length l) +i 1
  end.

Definition rev {a : Set} (l : list a) : list a :=
  Lists.List.rev' l.

Definition concat : ∀ {a : Set}, list (list a) → list a :=
  fun _ ⇒
  List.concat.

Definition append : ∀ {a : Set}, list a → list a → list a :=
  fun _ ⇒
  List.append.

Definition rev_append : ∀ {a : Set}, list a → list a → list a :=
  fun _ ⇒
  List.rev_append.

Definition flatten : ∀ {a : Set}, list (list a) → list a :=
  fun _ ⇒
  List.concat.

Fixpoint combine_aux {a b : Set}
  (list1 : list a)
  (list2 :list b)
  (partial : list (a × b))
  : option (list (a × b)) :=
  match list1, list2 with
  | [], _ :: _ | _ :: _, [] ⇒ None
  | [], [] ⇒ Some partial
  | h1 :: tl1 , h2 :: tl2 ⇒ combine_aux tl1 tl2 ((h1, h2) :: partial)
  end.

Definition combine {a b trace : Set} (er : trace)
  (l1 : list a) (l2 : list b)
  : Pervasives.result (list (a × b)) trace :=
  match combine_aux l1 l2 [] with
  | Some x ⇒ Pervasives.Ok x
  | None ⇒ Pervasives.Error er
  end.

Parameter rev_combine : ∀ {a b trace : Set},
  trace → list a → list b → Pervasives.result (list (a × b)) trace.

Definition split : ∀ {a b : Set}, list (a × b) → list a × list b :=
  fun _ _ ⇒
  List.split.

Parameter iter2 : ∀ {a b trace : Set},
  trace → (a → b → unit) → list a → list b →
  Pervasives.result unit trace.

Parameter map2 : ∀ {a b c trace : Set},
  trace → (a → b → c) → list a → list b →
  Pervasives.result (list c) trace.

Parameter rev_map2 : ∀ {a b c trace : Set},
  trace → (a → b → c) → list a → list b →
  Pervasives.result (list c) trace.

Parameter fold_left2 : ∀ {a b c trace : Set},
  trace → (a → b → c → a) → a → list b → list c →
  Pervasives.result a trace.

Parameter fold_right2 : ∀ {a b c trace : Set},
  trace → (a → b → c → c) → list a → list b → c →
  Pervasives.result c trace.

Parameter for_all2 : ∀ {a b trace : Set},
  trace → (a → b → bool) → list a → list b →
  Pervasives.result bool trace.

Parameter _exists2 : ∀ {a b trace : Set},
  trace → (a → b → bool) → list a → list b →
  Pervasives.result bool trace.

Parameter init_e : ∀ {a trace : Set},
  trace → int → (int → Pervasives.result a trace) →
  Pervasives.result (list a) trace.

Parameter init_s : ∀ {a trace : Set},
  trace → int → (int → a) → Pervasives.result (list a) trace.

Parameter init_es : ∀ {a trace : Set},
  trace → int → (int → Pervasives.result a trace) →
  Pervasives.result (list a) trace.

Parameter init_p : ∀ {a trace : Set},
  trace → int → (int → a) → Pervasives.result (list a) trace.

Parameter find_e : ∀ {a trace : Set},
  (a → Pervasives.result bool trace) → list a →
  Pervasives.result (option a) trace.

Parameter find_s : ∀ {a : Set},
  (a → bool) → list a → option a.

Parameter find_es : ∀ {a trace : Set},
  (a → Pervasives.result bool trace) → list a →
  Pervasives.result (option a) trace.

Parameter find_map_e : ∀ {a b trace : Set},
  (a → Pervasives.result (option b) trace) → list a →
  Pervasives.result (option b) trace.

Parameter find_map_s : ∀ {a b : Set},
  (a → option b) → list a → option b.

Parameter find_map_es : ∀ {a b trace : Set},
  (a → Pervasives.result (option b) trace) → list a →
  Pervasives.result (option b) trace.

Definition filter : ∀ {a : Set}, (a → bool) → list a → list a :=
  fun _ ⇒
  List.filter.

Parameter filteri : ∀ {a : Set}, (int → a → bool) → list a → list a.

Parameter find_all : ∀ {a : Set}, (a → bool) → list a → list a.

Parameter rev_filter : ∀ {a : Set}, (a → bool) → list a → list a.

Parameter rev_filteri : ∀ {a : Set},
  (int → a → bool) → list a → list a.

Parameter rev_filter_some : ∀ {a : Set}, list (option a) → list a.

Parameter filter_some : ∀ {a : Set}, list (option a) → list a.

Parameter rev_filter_ok : ∀ {a b : Set},
  list (Pervasives.result a b) → list a.

Parameter filter_ok : ∀ {a b : Set},
  list (Pervasives.result a b) → list a.

Parameter rev_filter_error : ∀ {a b : Set},
  list (Pervasives.result a b) → list b.

Parameter filter_error : ∀ {a b : Set},
  list (Pervasives.result a b) → list b.

Parameter rev_filter_left : ∀ {a b : Set}, list (Either.t a b) → list a.

Parameter filter_left : ∀ {a b : Set}, list (Either.t a b) → list a.

Parameter rev_filter_right : ∀ {a b : Set},
  list (Either.t a b) → list b.

Parameter filter_right : ∀ {a b : Set}, list (Either.t a b) → list b.

Parameter rev_filter_e : ∀ {a trace : Set},
  (a → Pervasives.result bool trace) → list a →
  Pervasives.result (list a) trace.

Fixpoint filter_e {a trace : Set}
  (f : a → Pervasives.result bool trace) (l : list a)
  : Pervasives.result (list a) trace :=
  match l with
  | [] ⇒ return? []
  | x :: l ⇒
    let? b := f x in
    let? l := filter_e f l in
    if b then
      return? (x :: l)
    else
      return? l
  end.

Parameter rev_filter_s : ∀ {a : Set},
  (a → bool) → list a → list a.

Fixpoint filter_s {a : Set}
  (f : a → bool) (l : list a) : list a :=
  match l with
  | [] ⇒ []
  | x :: l ⇒
    let b := f x in
    let l := filter_s f l in
    if b then
      x :: l
    else
      l
  end.

Parameter rev_filter_es : ∀ {a trace : Set},
  (a → Pervasives.result bool trace) → list a →
  Pervasives.result (list a) trace.

Fixpoint filter_es {a trace : Set}
  (f : a → Pervasives.result bool trace) (l : list a)
  : Pervasives.result (list a) trace :=
  match l with
  | [] ⇒ return? []
  | x :: l ⇒
    let? b := f x in
    let? l := filter_es f l in
    if b then
      return? (x :: l)
    else
      return? l
  end.

Parameter rev_filteri_e : ∀ {a trace : Set},
  (int → a → Pervasives.result bool trace) → list a →
  Pervasives.result (list a) trace.

Parameter filteri_e : ∀ {a trace : Set},
  (int → a → Pervasives.result bool trace) → list a →
  Pervasives.result (list a) trace.

Parameter rev_filteri_s : ∀ {a : Set},
  (int → a → bool) → list a → list a.

Parameter filteri_s : ∀ {a : Set},
  (int → a → bool) → list a → list a.

Parameter rev_filteri_es : ∀ {a trace : Set},
  (int → a → Pervasives.result bool trace) → list a →
  Pervasives.result (list a) trace.

Parameter filteri_es : ∀ {a trace : Set},
  (int → a → Pervasives.result bool trace) → list a →
  Pervasives.result (list a) trace.

Parameter filter_p : ∀ {a : Set},
  (a → bool) → list a → list a.

Parameter rev_partition : ∀ {a : Set},
  (a → bool) → list a → list a × list a.

Definition partition : ∀ {a : Set},
  (a → bool) → list a → list a × list a :=
  fun _ ⇒
  List.partition.

Parameter rev_partition_map : ∀ {a b c : Set},
  (a → Either.t b c) → list a → list b × list c.

Parameter partition_map : ∀ {a b c : Set},
  (a → Either.t b c) → list a → list b × list c.

Parameter rev_partition_result : ∀ {a b : Set},
  list (Pervasives.result a b) → list a × list b.

Parameter partition_result : ∀ {a b : Set},
  list (Pervasives.result a b) → list a × list b.

Parameter rev_partition_either : ∀ {a b : Set},
  list (Either.t a b) → list a × list b.

Parameter partition_either : ∀ {a b : Set},
  list (Either.t a b) → list a × list b.

Parameter rev_partition_e : ∀ {a trace : Set},
  (a → Pervasives.result bool trace) → list a →
  Pervasives.result (list a × list a) trace.

Parameter partition_e : ∀ {a trace : Set},
  (a → Pervasives.result bool trace) → list a →
  Pervasives.result (list a × list a) trace.

Parameter rev_partition_s : ∀ {a : Set},
  (a → bool) → list a → list a × list a.

Fixpoint partition_s {a : Set}
  (f : a → bool) (l : list a) : list a × list a :=
  match l with
  | [] ⇒ ([], [])
  | x :: l ⇒
    let b := f x in
    let '(yes, no) := partition_s f l in
    if b then
      (x :: yes, no)
    else
    (yes, x :: no)
  end.

Parameter rev_partition_es : ∀ {a trace : Set},
  (a → Pervasives.result bool trace) → list a →
  Pervasives.result (list a × list a) trace.

Parameter partition_es : ∀ {a trace : Set},
  (a → Pervasives.result bool trace) → list a →
  Pervasives.result (list a × list a) trace.

Parameter partition_p : ∀ {a : Set},
  (a → bool) → list a → list a × list a.

Parameter rev_partition_map_e : ∀ {a b c trace : Set},
  (a → Pervasives.result (Either.t b c) trace) → list a →
  Pervasives.result (list b × list c) trace.

Parameter partition_map_e : ∀ {a b c trace : Set},
  (a → Pervasives.result (Either.t b c) trace) → list a →
  Pervasives.result (list b × list c) trace.

Parameter rev_partition_map_s : ∀ {a b c : Set},
  (a → Either.t b c) → list a → list b × list c.

Parameter partition_map_s : ∀ {a b c : Set},
  (a → Either.t b c) → list a → list b × list c.

Parameter rev_partition_map_es : ∀ {a b c trace : Set},
  (a → Pervasives.result (Either.t b c) trace) → list a →
  Pervasives.result (list b × list c) trace.

Parameter partition_map_es : ∀ {a b c trace : Set},
  (a → Pervasives.result (Either.t b c) trace) → list a →
  Pervasives.result (list b × list c) trace.

Parameter iter : ∀ {a : Set}, (a → unit) → list a → unit.

Fixpoint iter_e {a trace : Set}
  (f : a → Pervasives.result unit trace) (l : list a)
  : Pervasives.result unit trace :=
  match l with
  | [] ⇒ return? tt
  | x :: l ⇒
    let? _ := f x in
    iter_e f l
  end.

Fixpoint iter_s {a : Set}
  (f : a → unit) (l : list a) : unit :=
  match l with
  | [] ⇒ tt
  | x :: l ⇒
    let _ := f x in
    iter_s f l
  end.

Fixpoint iter_es {a trace : Set}
  (f : a → Pervasives.result unit trace) (l : list a)
  : Pervasives.result unit trace :=
  match l with
  | [] ⇒ return? tt
  | x :: l ⇒
    let? _ := f x in
    iter_es f l
  end.

Parameter iter_p : ∀ {a : Set}, (a → unit) → list a → unit.

Parameter iteri : ∀ {a : Set}, (int → a → unit) → list a → unit.

Parameter iteri_e : ∀ {a trace : Set},
  (int → a → Pervasives.result unit trace) → list a →
  Pervasives.result unit trace.

Parameter iteri_s : ∀ {a : Set},
  (int → a → unit) → list a → unit.

Parameter iteri_es : ∀ {a trace : Set},
  (int → a → Pervasives.result unit trace) → list a →
  Pervasives.result unit trace.

Parameter iteri_p : ∀ {a : Set},
  (int → a → unit) → list a → unit.

Definition map : ∀ {a b : Set}, (a → b) → list a → list b :=
  @Lists.List.map.

Fixpoint map_e {a b trace : Set}
  (f : a → Pervasives.result b trace) (l : list a)
  : Pervasives.result (list b) trace :=
  match l with
  | [] ⇒ return? []
  | x :: l ⇒
    let? y := f x in
    let? l' := map_e f l in
    return? (y :: l')
  end.

Fixpoint map_s {a b : Set}
  (f : a → b) (l : list a) : list b :=
  match l with
  | [] ⇒ []
  | x :: l ⇒
    let x := f x in
    let l := map_s f l in
    x :: l
  end.

Fixpoint map_es {a b trace : Set}
  (f : a → Pervasives.result b trace) (l : list a)
  : Pervasives.result (list b) trace :=
  match l with
  | [] ⇒ return? []
  | x :: l ⇒
    let? y := f x in
    let? l' := map_es f l in
    return? (y :: l')
  end.

Parameter map_p : ∀ {a b : Set},
  (a → b) → list a → list b.

Definition mapi : ∀ {a b : Set}, (int → a → b) → list a → list b :=
  fun _ _ ⇒
  List.mapi.

Parameter mapi_e : ∀ {a b trace : Set},
  (int → a → Pervasives.result b trace) → list a →
  Pervasives.result (list b) trace.

Parameter mapi_s : ∀ {a b : Set},
  (int → a → b) → list a → list b.

Parameter mapi_es : ∀ {a b trace : Set},
  (int → a → Pervasives.result b trace) → list a →
  Pervasives.result (list b) trace.

Parameter mapi_p : ∀ {a b : Set},
  (int → a → b) → list a → list b.

Definition rev_map : ∀ {a b : Set}, (a → b) → list a → list b :=
  fun _ _ ⇒
  List.rev_map.

Parameter rev_mapi : ∀ {a b : Set}, (int → a → b) → list a → list b.

Parameter rev_map_e : ∀ {a b trace : Set},
  (a → Pervasives.result b trace) → list a →
  Pervasives.result (list b) trace.

Parameter rev_map_s : ∀ {a b : Set},
  (a → b) → list a → list b.

Parameter rev_map_es : ∀ {a b trace : Set},
  (a → Pervasives.result b trace) → list a →
  Pervasives.result (list b) trace.

Parameter rev_map_p : ∀ {a b : Set},
  (a → b) → list a → list b.

Parameter rev_mapi_e : ∀ {a b trace : Set},
  (int → a → Pervasives.result b trace) → list a →
  Pervasives.result (list b) trace.

Parameter rev_mapi_s : ∀ {a b : Set},
  (int → a → b) → list a → list b.

Parameter rev_mapi_es : ∀ {a b trace : Set},
  (int → a → Pervasives.result b trace) → list a →
  Pervasives.result (list b) trace.

Parameter rev_mapi_p : ∀ {a b : Set},
  (int → a → b) → list a → list b.

Parameter rev_filter_map : ∀ {a b : Set},
  (a → option b) → list a → list b.

Parameter rev_filter_map_e : ∀ {a b trace : Set},
  (a → Pervasives.result (option b) trace) → list a →
  Pervasives.result (list b) trace.

Parameter filter_map_e : ∀ {a b trace : Set},
  (a → Pervasives.result (option b) trace) → list a →
  Pervasives.result (list b) trace.

Parameter rev_filter_map_s : ∀ {a b : Set},
  (a → option b) → list a → list b.

Fixpoint filter_map {a b : Set} (f : a → option b) (l : list a) : list b :=
  match l with
  | [] ⇒ []
  | x :: l' ⇒
    match f x with
    | None ⇒ filter_map f l'
    | Some y ⇒ y :: filter_map f l'
    end
  end.

Fixpoint filter_map_s {a b : Set}
  (f : a → option b) (l : list a) : list b :=
  match l with
  | [] ⇒ []
  | x :: l ⇒
    let y := f x in
    let l' := filter_map_s f l in
    match y with
    | Some y ⇒ y :: l'
    | None ⇒ l'
    end
  end.

Parameter rev_filter_map_es : ∀ {a b trace : Set},
  (a → Pervasives.result (option b) trace) → list a →
  Pervasives.result (list b) trace.

Fixpoint filter_map_es {a b trace : Set}
  (f : a → Pervasives.result (option b) trace) (l : list a)
  : Pervasives.result (list b) trace :=
  match l with
  | [] ⇒ return? []
  | x :: l ⇒
    let? y := f x in
    let? l' := filter_map_es f l in
    match y with
    | Some y ⇒ return? (y :: l')
    | None ⇒ return? l'
    end
  end.

Parameter filter_map_p : ∀ {a b : Set},
  (a → option b) → list a → list b.

Parameter concat_map : ∀ {a b : Set}, (a → list b) → list a → list b.

Parameter concat_map_s : ∀ {a b : Set},
  (a → list b) → list a → list b.

Parameter concat_map_e : ∀ {_error a b : Set},
  (a → Pervasives.result (list b) _error) → list a →
  Pervasives.result (list b) _error.

Parameter concat_map_es : ∀ {_error a b : Set},
  (a → Pervasives.result (list b) _error) → list a →
  Pervasives.result (list b) _error.

Parameter concat_map_p : ∀ {a b : Set},
  (a → list b) → list a → list b.

Definition fold_left : ∀ {a b : Set}, (a → b → a) → a → list b → a :=
  fun _ _ ⇒
  List.fold_left.

Definition fold_left_e {a b trace : Set}
  (f : a → b → Pervasives.result a trace) (acc : a) (l : list b) :
  Pervasives.result a trace :=
  fold_left (fun acc item ⇒ let? acc := acc in f acc item) (return? acc) l.

Fixpoint fold_left_s {a b : Set}
  (f : a → b → a) (accumulator : a) (l : list b) : a :=
  match l with
  | [] ⇒ accumulator
  | x :: l ⇒
    let accumulator := f accumulator x in
    fold_left_s f accumulator l
  end.

Fixpoint fold_left_es {a b trace : Set}
  (f : a → b → Pervasives.result a trace) (accumulator : a)
  (l : list b) : Pervasives.result a trace :=
  match l with
  | [] ⇒ return? accumulator
  | x :: l ⇒
    let? accumulator := f accumulator x in
    fold_left_es f accumulator l
  end.

Parameter fold_left_map : ∀ {a b c : Set},
  (a → b → a × c) → a → list b → a × list c.

Parameter fold_left_map_e : ∀ {a b c trace : Set},
  (a → b → Pervasives.result (a × c) trace) → a → list b →
  Pervasives.result (a × list c) trace.

Parameter fold_left_map_s : ∀ {a b c : Set},
  (a → b → a × c) → a → list b → a × list c.

Parameter fold_left_map_es : ∀ {a b c trace : Set},
  (a → b → Pervasives.result (a × c) trace) → a → list b →
  Pervasives.result (a × list c) trace.

Definition fold_left_i {a b : Set}
  (f : int → a → b → a) (acc : a) (l : list b) : a :=
  snd (
    fold_left
      (fun '(index, acc) item ⇒
        let acc := f index acc item in
        (index +i 1, acc)
      )
      (0, acc)
      l
  ).

Definition fold_left_i_e {a b trace : Set}
  (f : int → a → b → Pervasives.result a trace) (acc : a) (l : list b) :
  Pervasives.result a trace :=
  fold_left_i
    (fun index acc item ⇒ let? acc := acc in f index acc item)
    (return? acc)
    l.

Definition fold_left_i_s := @fold_left_i.
Arguments fold_left_i_s {a b}.

Definition fold_left_i_es := @fold_left_i_e.
Arguments fold_left_i_es {a b trace}.

Definition fold_right : ∀ {a b : Set}, (a → b → b) → list a → b → b :=
  fun _ _ ⇒
  List.fold_right.

Parameter fold_right_e : ∀ {a b trace : Set},
  (a → b → Pervasives.result b trace) → list a → b →
  Pervasives.result b trace.

Fixpoint fold_right_s {a b : Set}
  (f : a → b → b) (l : list a) (accumulator : b) : b :=
  match l with
  | [] ⇒ accumulator
  | x :: l ⇒
    let accumulator := fold_right_s f l accumulator in
    f x accumulator
  end.

Fixpoint fold_right_es {a b trace : Set}
  (f : a → b → Pervasives.result b trace) (l : list a)
  (accumulator : b) : Pervasives.result b trace :=
  match l with
  | [] ⇒ return? accumulator
  | x :: l ⇒
    let? accumulator := fold_right_es f l accumulator in
    f x accumulator
  end.

Parameter iter2_e : ∀ {a b trace : Set},
  trace → (a → b → Pervasives.result unit trace) → list a → list b →
  Pervasives.result unit trace.

Parameter iter2_s : ∀ {a b trace : Set},
  trace → (a → b → unit) → list a → list b →
  Pervasives.result unit trace.

Parameter iter2_es : ∀ {a b trace : Set},
  trace → (a → b → Pervasives.result unit trace) → list a →
  list b → Pervasives.result unit trace.

Parameter map2_e : ∀ {a b c trace : Set},
  trace → (a → b → Pervasives.result c trace) → list a → list b →
  Pervasives.result (list c) trace.

Parameter map2_s : ∀ {a b c trace : Set},
  trace → (a → b → c) → list a → list b →
  Pervasives.result (list c) trace.

Parameter map2_es : ∀ {a b c trace : Set},
  trace → (a → b → Pervasives.result c trace) → list a →
  list b → Pervasives.result (list c) trace.

Parameter rev_map2_e : ∀ {a b c trace : Set},
  trace → (a → b → Pervasives.result c trace) → list a → list b →
  Pervasives.result (list c) trace.

Parameter rev_map2_s : ∀ {a b c trace : Set},
  trace → (a → b → c) → list a → list b →
  Pervasives.result (list c) trace.

Parameter rev_map2_es : ∀ {a b c trace : Set},
  trace → (a → b → Pervasives.result c trace) → list a →
  list b → Pervasives.result (list c) trace.

Parameter fold_left2_e : ∀ {a b c trace : Set},
  trace → (a → b → c → Pervasives.result a trace) → a → list b →
  list c → Pervasives.result a trace.

Parameter fold_left2_s : ∀ {a b c trace : Set},
  trace → (a → b → c → a) → a → list b → list c →
  Pervasives.result a trace.

Parameter fold_left2_es : ∀ {a b c trace : Set},
  trace → (a → b → c → Pervasives.result a trace) → a →
  list b → list c → Pervasives.result a trace.

Parameter fold_right2_e : ∀ {a b c trace : Set},
  trace → (a → b → c → Pervasives.result c trace) → list a → list b →
  c → Pervasives.result c trace.

Parameter fold_right2_s : ∀ {a b c trace : Set},
  trace → (a → b → c → c) → list a → list b → c →
  Pervasives.result c trace.

Parameter fold_right2_es : ∀ {a b c trace : Set},
  trace → (a → b → c → Pervasives.result c trace) → list a →
  list b → c → Pervasives.result c trace.

Definition for_all : ∀ {a : Set}, (a → bool) → list a → bool :=
  fun a ⇒
  List.forallb (A := a).

Parameter for_all_e : ∀ {a trace : Set},
  (a → Pervasives.result bool trace) → list a →
  Pervasives.result bool trace.

Fixpoint for_all_s {a : Set}
  (f : a → bool) (l : list a) : bool :=
  match l with
  | [] ⇒ true
  | x :: l ⇒
    let b := f x in
    if b then
      for_all_s f l
    else
      false
  end.

Parameter for_all_es : ∀ {a trace : Set},
  (a → Pervasives.result bool trace) → list a →
  Pervasives.result bool trace.

Parameter for_all_p : ∀ {a : Set},
  (a → bool) → list a → bool.

Definition _exists : ∀ {a : Set}, (a → bool) → list a → bool :=
  fun a ⇒
  List.existsb (A := a).

Parameter exists_e : ∀ {a trace : Set},
  (a → Pervasives.result bool trace) → list a →
  Pervasives.result bool trace.

Fixpoint exists_s {a : Set}
  (f : a → bool) (l : list a) : bool :=
  match l with
  | [] ⇒ false
  | x :: l ⇒
    let b := f x in
    if b then
      true
    else
      exists_s f l
  end.

Parameter exists_es : ∀ {a trace : Set},
  (a → Pervasives.result bool trace) → list a →
  Pervasives.result bool trace.

Parameter exists_p : ∀ {a : Set},
  (a → bool) → list a → bool.

Parameter for_all2_e : ∀ {a b trace : Set},
  trace → (a → b → Pervasives.result bool trace) → list a → list b →
  Pervasives.result bool trace.

Parameter for_all2_s : ∀ {a b trace : Set},
  trace → (a → b → bool) → list a → list b →
  Pervasives.result bool trace.

Parameter for_all2_es : ∀ {a b trace : Set},
  trace → (a → b → Pervasives.result bool trace) → list a →
  list b → Pervasives.result bool trace.

Parameter exists2_e : ∀ {a b trace : Set},
  trace → (a → b → Pervasives.result bool trace) → list a → list b →
  Pervasives.result bool trace.

Parameter exists2_s : ∀ {a b trace : Set},
  trace → (a → b → bool) → list a → list b →
  Pervasives.result bool trace.

Parameter exists2_es : ∀ {a b trace : Set},
  trace → (a → b → Pervasives.result bool trace) → list a →
  list b → Pervasives.result bool trace.

Parameter combine_drop : ∀ {a b : Set}, list a → list b → list (a × b).

Parameter combine_with_leftovers : ∀ {a b : Set},
  list a → list b → list (a × b) × option (Either.t (list a) (list b)).

Parameter compare : ∀ {a : Set},
  (a → a → int) → list a → list a → int.

Definition compare_lengths : ∀ {a b : Set}, list a → list b → int :=
  fun _ _ l1 l2 ⇒
  (length l1) -i (length l2).

Definition compare_length_with : ∀ {a : Set}, list a → int → int :=
  fun _ l n ⇒
  length l -i n.

Fixpoint equal {a : Set} (eqb : a → a → bool) (l1 l2 : list a) : bool :=
  match l1, l2 with
  | [], [] ⇒ true
  | x1 :: l1, x2 :: l2 ⇒ eqb x1 x2 && equal eqb l1 l2
  | _, _ ⇒ false
  end.

Parameter sort : ∀ {a : Set}, (a → a → int) → list a → list a.

Parameter stable_sort : ∀ {a : Set}, (a → a → int) → list a → list a.

Parameter fast_sort : ∀ {a : Set}, (a → a → int) → list a → list a.

Parameter sort_uniq : ∀ {a : Set}, (a → a → int) → list a → list a.

Parameter to_seq : ∀ {a : Set}, list a → Seq.t a.

Parameter of_seq : ∀ {a : Set}, Seq.t a → list a.

Parameter init_ep : ∀ {_error a : Set},
  _error → int → (int → M? a) → M? (list a).

Parameter filter_ep : ∀ {a : Set},
  (a → M? bool) → list a → M? (list a).

Parameter partition_ep : ∀ {a : Set},
  (a → M? bool) → list a → M? (list a × list a).

Parameter partition_map_ep : ∀ {a b c : Set},
  (a → M? (Either.t b c)) → list a → M? (list b × list c).

Parameter iter_ep : ∀ {a : Set},
  (a → M? unit) → list a → M? unit.

Parameter iteri_ep : ∀ {a : Set},
  (int → a → M? unit) → list a → M? unit.

Parameter map_ep : ∀ {a b : Set},
  (a → M? b) → list a → M? (list b).

Parameter mapi_ep : ∀ {a b : Set},
  (int → a → M? b) → list a → M? (list b).

Parameter rev_map_ep : ∀ {a b : Set},
  (a → M? b) → list a → M? (list b).

Parameter rev_mapi_ep : ∀ {a b : Set},
  (int → a → M? b) → list a → M? (list b).

Parameter filter_map_ep : ∀ {a b : Set},
  (a → M? (option b)) → list a → M? (list b).

Parameter concat_map_ep : ∀ {a b : Set},
  (a → M? (list b)) → list a → M? (list b).

Parameter for_all_ep : ∀ {a : Set},
  (a → M? bool) → list a → M? bool.

Parameter exists_ep : ∀ {a : Set},
  (a → M? bool) → list a → M? bool.