Skip to main content

πŸƒΒ List.v

Environment

Gitlab

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

Require TezosOfOCaml.Environment.Structs.V0.Either.
Require TezosOfOCaml.Environment.Structs.V0.Error_monad.
Require TezosOfOCaml.Environment.Structs.V0.Pervasives.
Require TezosOfOCaml.Environment.Structs.V0.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? [].

Definition cons_value : βˆ€ {a : Set}, a β†’ list a β†’ list a :=
  @cons.

Definition is_empty {a : Set} (l : list a) : bool :=
  match l with
  | [] β‡’ true
  | _ :: _ β‡’ false
  end.

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.

Fixpoint find_map {a b : Set} (f : a β†’ option b) (l : list a) : option b :=
  match l with
  | [] β‡’ None
  | x :: l' β‡’
    match f x with
    | Some y β‡’ f x
    | None β‡’ find_map f l'
    end
  end.

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.

(* not definable without decidable equality *)
Parameter assq : βˆ€ {a b : Set}, a β†’ list (a Γ— b) β†’ option b.

(* not definable without decidable equality *)
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.

(* not definable without decidable equality *)
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.

(* not definable without decidable equality *)
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.

Definition rev_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 (rev x)
  | None β‡’ Pervasives.Error er
  end.

Definition split : βˆ€ {a b : Set}, list (a Γ— b) β†’ list a Γ— list b :=
  fun _ _ β‡’
  List.split.

Fixpoint iter2 {a b trace : Set} (er : trace)
  (f : a β†’ b β†’ unit) (l1 : list a) (l2 : list b)
  : Pervasives.result unit trace :=
  match l1,l2 with
  | [], [] β‡’ Pervasives.Ok tt
  | _ :: l1', _ :: l2' β‡’ iter2 er f l1' l2'
  | _, _ β‡’ Pervasives.Error er
  end.

Fixpoint map2 {a b c trace : Set} (er : trace)
  (f : a β†’ b β†’ c) (l1 : list a) (l2 : list b)
  : Pervasives.result (list c) trace :=
  match l1, l2 with
  | [], [] β‡’ Pervasives.Ok []
  | x :: l1', y :: l2' β‡’
    match map2 er f l1' l2' with
    | Pervasives.Ok l3 β‡’ Pervasives.Ok (f x y :: l3)
    | Pervasives.Error e β‡’ Pervasives.Error e
    end
  | _, _ β‡’ Pervasives.Error er
  end.

Definition rev_map2 : βˆ€ {a b c trace : Set},
  trace β†’ (a β†’ b β†’ c) β†’ list a β†’ list b β†’
  Pervasives.result (list c) trace :=
  fun a b c trace er f l1 l2 β‡’
  match map2 er f l1 l2 with
  | Pervasives.Ok l3 β‡’ Pervasives.Ok (List.rev l3)
  | Pervasives.Error _ as e β‡’ e
  end.

Fixpoint fold_left2 {a b c trace : Set} (er : trace)
  (f : a β†’ b β†’ c β†’ a) (acc : a) (l1 : list b) (l2 : list c)
  : Pervasives.result a trace :=
  match l1, l2 with
  | [], [] β‡’ Pervasives.Ok acc
  | x :: l1', y :: l2' β‡’ fold_left2 er f (f acc x y) l1' l2'
  | _, _ β‡’ Pervasives.Error er
  end.

Fixpoint fold_right2 {a b c trace : Set} (er : trace)
  (f : a β†’ b β†’ c β†’ c) (l1 : list a) (l2 : list b) (acc : c)
  : Pervasives.result c trace :=
  match l1, l2 with
  | [], [] β‡’ Pervasives.Ok acc
  | x :: l1', y :: l2' β‡’
    match fold_right2 er f l1' l2' acc with
    | Pervasives.Ok acc' β‡’ Pervasives.Ok (f x y acc')
    | Pervasives.Error _ as e β‡’ e
    end
  | _, _ β‡’ Pervasives.Error er
  end.

Definition for_all2 : βˆ€ {a b trace : Set},
  trace β†’ (a β†’ b β†’ bool) β†’ list a β†’ list b β†’
  Pervasives.result bool trace :=
  fun a b trace er p l1 l2 β‡’ fold_left2 er
    (fun acc x y β‡’ acc && p x y) true l1 l2.

Definition _exists2 : βˆ€ {a b trace : Set},
  trace β†’ (a β†’ b β†’ bool) β†’ list a β†’ list b β†’
  Pervasives.result bool trace :=
  fun a b trace er p l1 l2 β‡’ fold_left2 er
    (fun acc x y β‡’ acc || p x y) false l1 l2.

Fixpoint nat_init_e {a trace : Set} (er : trace) (n : nat)
  (ff : nat β†’ Pervasives.result a trace)
  : Pervasives.result (list a) trace :=
  match n with
  | 0%nat β‡’ Pervasives.Ok []
  | S k β‡’
    match ff 0%nat with
    | Pervasives.Error e β‡’ Pervasives.Error e
    | Pervasives.Ok x β‡’
      match nat_init_e er k (fun v β‡’ ff (S v)) with
      | Pervasives.Error _ as e β‡’ e
      | Pervasives.Ok l β‡’ Pervasives.Ok (x :: l)
      end
    end
  end.

Definition init_e : βˆ€ {a trace : Set},
  trace β†’ int β†’ (int β†’ Pervasives.result a trace) β†’
  Pervasives.result (list a) trace :=
  fun a trace er n ff β‡’
  match n with
  | Zneg _ β‡’ Pervasives.Error er
  | Z0 β‡’ Pervasives.Ok []
  | Zpos _ β‡’ nat_init_e er (Z.to_nat n) (fun x β‡’ ff (Z.of_nat x))
  end.

Definition init_s : βˆ€ {a trace : Set},
  trace β†’ int β†’ (int β†’ a) β†’ Pervasives.result (list a) trace :=
  @init_value.

Definition init_es : βˆ€ {a trace : Set},
  trace β†’ int β†’ (int β†’ Pervasives.result a trace) β†’
  Pervasives.result (list a) trace :=
  @init_e.

Definition init_p : βˆ€ {a trace : Set},
  trace β†’ int β†’ (int β†’ a) β†’ Pervasives.result (list a) trace :=
  @init_value.

Fixpoint find_e {a trace : Set}
  (ep : a β†’ Pervasives.result bool trace) (l : list a)
  : Pervasives.result (option a) trace :=
  match l with
  | [] β‡’ Pervasives.Ok None
  | x :: l' β‡’
    match ep x with
    | Pervasives.Error e β‡’ Pervasives.Error e
    | Pervasives.Ok true β‡’ Pervasives.Ok (Some x)
    | Pervasives.Ok false β‡’ find_e ep l'
    end
  end.

Definition find_s : βˆ€ {a : Set},
  (a β†’ bool) β†’ list a β†’ option a :=
  @find.

Definition find_es : βˆ€ {a trace : Set},
  (a β†’ Pervasives.result bool trace) β†’ list a β†’
  Pervasives.result (option a) trace :=
  @find_e.

Fixpoint find_map_e {a b trace : Set}
  (f : a β†’ Pervasives.result (option b) trace) (l : list a)
  : Pervasives.result (option b) trace :=
  match l with
  | [] β‡’ Pervasives.Ok None
  | x :: l' β‡’
    match f x with
    | Pervasives.Error _ as e β‡’ e
    | Pervasives.Ok (Some _) as res β‡’ res
    | Pervasives.Ok None β‡’ find_map_e f l'
    end
  end.

Definition find_map_s : βˆ€ {a b : Set},
  (a β†’ option b) β†’ list a β†’ option b :=
  @find_map.

Definition find_map_es : βˆ€ {a b trace : Set},
  (a β†’ Pervasives.result (option b) trace) β†’ list a β†’
  Pervasives.result (option b) trace :=
  @find_map_e.

Definition filter : βˆ€ {a : Set}, (a β†’ bool) β†’ list a β†’ list a :=
  fun _ β‡’
  List.filter.

Fixpoint filteri_aux {a : Set} (i : int) (p : int β†’ a β†’ bool) (l : list a)
  : list a :=
  match l with
  | [] β‡’ []
  | x :: l' β‡’ if p i x
    then x :: filteri_aux (i+1)%Z p l'
    else filteri_aux (i+1)%Z p l'
  end.

Definition filteri : βˆ€ {a : Set}, (int β†’ a β†’ bool) β†’ list a β†’ list a :=
  fun a β‡’ @filteri_aux a 0.

Definition find_all : βˆ€ {a : Set}, (a β†’ bool) β†’ list a β†’ list a :=
  @filter.

Definition rev_filter : βˆ€ {a : Set}, (a β†’ bool) β†’ list a β†’ list a :=
  fun a p l β‡’ List.rev (filter p l).

Definition rev_filteri : βˆ€ {a : Set},
  (int β†’ a β†’ bool) β†’ list a β†’ list a :=
  fun a p l β‡’ List.rev (filteri p l).

Fixpoint filter_some {a : Set} (l : list (option a)) : list a :=
  match l with
  | [] β‡’ []
  | None :: l' β‡’ filter_some l'
  | Some x :: l' β‡’ x :: filter_some l'
  end.

Definition rev_filter_some : βˆ€ {a : Set}, list (option a) β†’ list a :=
  fun a l β‡’ List.rev (filter_some l).

Fixpoint filter_ok {a b : Set} (l : list (Pervasives.result a b)) : list a :=
  match l with
  | [] β‡’ []
  | Pervasives.Error _ :: l' β‡’ filter_ok l'
  | Pervasives.Ok x :: l' β‡’ x :: filter_ok l'
  end.

Definition rev_filter_ok : βˆ€ {a b : Set},
  list (Pervasives.result a b) β†’ list a :=
  fun a b l β‡’ List.rev (filter_ok l).

Fixpoint filter_error {a b : Set} (l : list (Pervasives.result a b)) : list b :=
  match l with
  | [] β‡’ []
  | Pervasives.Ok _ :: l' β‡’ filter_error l'
  | Pervasives.Error e :: l' β‡’ e :: filter_error l'
  end.

Definition rev_filter_error : βˆ€ {a b : Set},
  list (Pervasives.result a b) β†’ list b :=
  fun a b l β‡’ List.rev (filter_error l).

Fixpoint filter_left {a b : Set} (l : list (Either.t a b)) : list a :=
  match l with
  | [] β‡’ []
  | Either.Left x :: l' β‡’ x :: filter_left l'
  | Either.Right _ :: l' β‡’ filter_left l'
  end.

Definition rev_filter_left : βˆ€ {a b : Set}, list (Either.t a b) β†’ list a :=
  fun a b l β‡’ List.rev (filter_left l).

Fixpoint filter_right {a b : Set} (l : list (Either.t a b)) : list b :=
  match l with
  | [] β‡’ []
  | Either.Right x :: l' β‡’ x :: filter_right l'
  | Either.Left _ :: l' β‡’ filter_right l'
  end.

Definition rev_filter_right : βˆ€ {a b : Set},
  list (Either.t a b) β†’ list b :=
  fun a b l β‡’ List.rev (filter_right l).

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.

Definition rev_filter_e : βˆ€ {a trace : Set},
  (a β†’ Pervasives.result bool trace) β†’ list a β†’
  Pervasives.result (list a) trace :=
  fun a trace f l β‡’
  let? l' := filter_e f l in
  return? List.rev l'.

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.

Definition rev_filter_s : βˆ€ {a : Set},
  (a β†’ bool) β†’ list a β†’ list a :=
  fun a p l β‡’
  List.rev (filter_s p l).

Definition rev_filter_es : βˆ€ {a trace : Set},
  (a β†’ Pervasives.result bool trace) β†’ list a β†’
  Pervasives.result (list a) trace :=
  @rev_filter_e.

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.

Fixpoint filteri_e_aux {a trace : Set} (i : int)
  (p : int β†’ a β†’ Pervasives.result bool trace) (l : list a)
  : Pervasives.result (list a) trace :=
  match l with
  | [] β‡’ return? []
  | x :: l' β‡’
    let? b := p i x in
    let? res := filteri_e_aux (i + 1)%Z p l' in
    return? (if b then x :: res else res)
  end.

Definition filteri_e : βˆ€ {a trace : Set},
  (int β†’ a β†’ Pervasives.result bool trace) β†’ list a β†’
  Pervasives.result (list a) trace :=
  fun a trace β‡’ @filteri_e_aux a trace 0.

Definition rev_filteri_e : βˆ€ {a trace : Set},
  (int β†’ a β†’ Pervasives.result bool trace) β†’ list a β†’
  Pervasives.result (list a) trace :=
  fun a trace p l β‡’
  let? res := filteri_e p l in
  return? List.rev res.

Definition rev_filteri_s : βˆ€ {a : Set},
  (int β†’ a β†’ bool) β†’ list a β†’ list a :=
  @rev_filteri.

Definition filteri_s : βˆ€ {a : Set},
  (int β†’ a β†’ bool) β†’ list a β†’ list a :=
  @filteri.

Definition rev_filteri_es : βˆ€ {a trace : Set},
  (int β†’ a β†’ Pervasives.result bool trace) β†’ list a β†’
  Pervasives.result (list a) trace :=
  @rev_filteri_e.

Definition filteri_es : βˆ€ {a trace : Set},
  (int β†’ a β†’ Pervasives.result bool trace) β†’ list a β†’
  Pervasives.result (list a) trace :=
  @filteri_e.

Definition filter_p : βˆ€ {a : Set},
  (a β†’ bool) β†’ list a β†’ list a :=
  @filter.

Definition partition : βˆ€ {a : Set},
  (a β†’ bool) β†’ list a β†’ list a Γ— list a :=
  fun _ β‡’
  List.partition.

Definition rev_partition : βˆ€ {a : Set},
  (a β†’ bool) β†’ list a β†’ list a Γ— list a :=
  fun a p l β‡’ partition p (List.rev l).

Fixpoint partition_map {a b c : Set}
  (f : a β†’ Either.t b c) (l : list a)
  : list b Γ— list c :=
  match l with
  | [] β‡’ ([], [])
  | x :: l' β‡’
    let '(l1, l2) := partition_map f l' in
    match f x with
    | Either.Left y β‡’ (y :: l1, l2)
    | Either.Right y β‡’ (l1, y :: l2)
    end
  end.

Definition rev_partition_map : βˆ€ {a b c : Set},
  (a β†’ Either.t b c) β†’ list a β†’ list b Γ— list c :=
  fun a b c f l β‡’
  partition_map f (List.rev l).

Fixpoint partition_result {a b : Set}
  (l : list (Pervasives.result a b)) : list a Γ— list b :=
  match l with
  | [] β‡’ ([], [])
  | x :: l' β‡’
    let '(l1, l2) := partition_result l' in
    match x with
    | Pervasives.Ok x β‡’ (x :: l1, l2)
    | Pervasives.Error e β‡’ (l1, e :: l2)
    end
  end.

Definition rev_partition_result : βˆ€ {a b : Set},
  list (Pervasives.result a b) β†’ list a Γ— list b :=
  fun a b l β‡’ partition_result (List.rev l).

Fixpoint partition_either {a b : Set}
  (l : list (Either.t a b)) : list a Γ— list b :=
  match l with
  | [] β‡’ ([], [])
  | x :: l' β‡’
    let '(l1, l2) := partition_either l' in
    match x with
    | Either.Left y β‡’ (y :: l1, l2)
    | Either.Right y β‡’ (l1, y :: l2)
    end
  end.

Definition rev_partition_either : βˆ€ {a b : Set},
  list (Either.t a b) β†’ list a Γ— list b :=
  fun a b l β‡’ partition_either (List.rev l).

Fixpoint partition_e {a trace : Set}
  (p : a β†’ Pervasives.result bool trace) (l : list a)
  : Pervasives.result (list a Γ— list a) trace :=
  match l with
  | [] β‡’ return? ([], [])
  | x :: l' β‡’
    let? b := p x in
    let? '(l1, l2) := partition_e p l' in
    return? (if b then (x :: l1, l2) else (l1, x :: l2))
  end.

Definition rev_partition_e : βˆ€ {a trace : Set},
  (a β†’ Pervasives.result bool trace) β†’ list a β†’
  Pervasives.result (list a Γ— list a) trace :=
  fun a trace p l β‡’ partition_e p (List.rev l).

Definition rev_partition_s : βˆ€ {a : Set},
  (a β†’ bool) β†’ list a β†’ list a Γ— list a :=
  @rev_partition.

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.

Definition rev_partition_es : βˆ€ {a trace : Set},
  (a β†’ Pervasives.result bool trace) β†’ list a β†’
  Pervasives.result (list a Γ— list a) trace :=
  @rev_partition_e.

Definition partition_es : βˆ€ {a trace : Set},
  (a β†’ Pervasives.result bool trace) β†’ list a β†’
  Pervasives.result (list a Γ— list a) trace :=
  @partition_e.

Definition partition_p : βˆ€ {a : Set},
  (a β†’ bool) β†’ list a β†’ list a Γ— list a :=
  @partition.

Fixpoint partition_map_e {a b c trace : Set}
  (f : a β†’ Pervasives.result (Either.t b c) trace) (l : list a) :
  Pervasives.result (list b Γ— list c) trace :=
  match l with
  | [] β‡’ return? ([], [])
  | x :: l' β‡’
    let? e := f x in
    let? '(l1, l2) := partition_map_e f l' in
    match e with
    | Either.Left y β‡’ return? (y :: l1, l2)
    | Either.Right y β‡’ return? (l1, y :: l2)
    end
  end.

Definition 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 :=
  fun a b c trace f l β‡’ partition_map_e f (List.rev l).

Definition rev_partition_map_s : βˆ€ {a b c : Set},
  (a β†’ Either.t b c) β†’ list a β†’ list b Γ— list c :=
  @rev_partition_map.

Definition partition_map_s : βˆ€ {a b c : Set},
  (a β†’ Either.t b c) β†’ list a β†’ list b Γ— list c :=
  @partition_map.

Definition 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 :=
  @rev_partition_map_e.

Definition 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 :=
  @partition_map_e.

Definition iter : βˆ€ {a : Set},
  (a β†’ unit) β†’ list a β†’ unit :=
  fun a f l β‡’ tt.

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.

Definition iter_p : βˆ€ {a : Set}, (a β†’ unit) β†’ list a β†’ unit :=
  @iter.

Definition iteri : βˆ€ {a : Set}, (int β†’ a β†’ unit) β†’ list a β†’ unit :=
  fun a f l β‡’ tt.

Fixpoint iteri_e_aux {a trace : Set} (i : int)
  (f : int β†’ a β†’ Pervasives.result unit trace) (l : list a)
  : Pervasives.result unit trace :=
  match l with
  | [] β‡’ return? tt
  | x :: l' β‡’
    let? _ := f i x in
    iteri_e_aux (i + 1)%Z f l'
  end.

Definition iteri_e : βˆ€ {a trace : Set},
  (int β†’ a β†’ Pervasives.result unit trace) β†’ list a β†’
  Pervasives.result unit trace :=
  fun a trace β‡’ @iteri_e_aux a trace 0.

Definition iteri_s : βˆ€ {a : Set},
  (int β†’ a β†’ unit) β†’ list a β†’ unit :=
  @iteri.

Definition iteri_es : βˆ€ {a trace : Set},
  (int β†’ a β†’ Pervasives.result unit trace) β†’ list a β†’
  Pervasives.result unit trace :=
  @iteri_e.

Definition iteri_p : βˆ€ {a : Set},
  (int β†’ a β†’ unit) β†’ list a β†’ unit :=
  @iteri.

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.

Definition map_p : βˆ€ {a b : Set},
  (a β†’ b) β†’ list a β†’ list b :=
  @map.

Definition mapi : βˆ€ {a b : Set}, (int β†’ a β†’ b) β†’ list a β†’ list b :=
  fun _ _ β‡’
  List.mapi.

Fixpoint mapi_e_aux {a b trace : Set} (i : int)
  (f : int β†’ a β†’ Pervasives.result b trace) (l : list a)
  : Pervasives.result (list b) trace :=
  match l with
  | [] β‡’ return? []
  | x :: l' β‡’
    let? y := f i x in
    let? res := mapi_e_aux (i+1)%Z f l' in
    return? (y :: res)
  end.

Definition mapi_e : βˆ€ {a b trace : Set},
  (int β†’ a β†’ Pervasives.result b trace) β†’ list a β†’
  Pervasives.result (list b) trace :=
  fun a b trace β‡’ @mapi_e_aux a b trace 0.

Definition mapi_s : βˆ€ {a b : Set},
  (int β†’ a β†’ b) β†’ list a β†’ list b :=
  @mapi.

Definition mapi_es : βˆ€ {a b trace : Set},
  (int β†’ a β†’ Pervasives.result b trace) β†’ list a β†’
  Pervasives.result (list b) trace :=
  @mapi_e.

Definition mapi_p : βˆ€ {a b : Set},
  (int β†’ a β†’ b) β†’ list a β†’ list b :=
  @mapi.

Definition rev_map : βˆ€ {a b : Set}, (a β†’ b) β†’ list a β†’ list b :=
  fun _ _ β‡’
  List.rev_map.

Definition rev_mapi : βˆ€ {a b : Set}, (int β†’ a β†’ b) β†’ list a β†’ list b :=
  fun a b f l β‡’ List.rev (mapi f l).

Definition rev_map_e : βˆ€ {a b trace : Set},
  (a β†’ Pervasives.result b trace) β†’ list a β†’
  Pervasives.result (list b) trace :=
  fun a b trace f l β‡’
  let? res := map_e f l in
  return? (List.rev res).

Definition rev_map_s : βˆ€ {a b : Set},
  (a β†’ b) β†’ list a β†’ list b :=
  @rev_map.

Definition rev_map_es : βˆ€ {a b trace : Set},
  (a β†’ Pervasives.result b trace) β†’ list a β†’
  Pervasives.result (list b) trace :=
  @rev_map_e.

Definition rev_map_p : βˆ€ {a b : Set},
  (a β†’ b) β†’ list a β†’ list b :=
  @rev_map.

Definition rev_mapi_e : βˆ€ {a b trace : Set},
  (int β†’ a β†’ Pervasives.result b trace) β†’ list a β†’
  Pervasives.result (list b) trace :=
  fun a b trace f l β‡’
  let? res := mapi_e f l in
  return? List.rev res.

Definition rev_mapi_s : βˆ€ {a b : Set},
  (int β†’ a β†’ b) β†’ list a β†’ list b :=
  @rev_mapi.

Definition rev_mapi_es : βˆ€ {a b trace : Set},
  (int β†’ a β†’ Pervasives.result b trace) β†’ list a β†’
  Pervasives.result (list b) trace :=
  @rev_mapi_e.

Definition rev_mapi_p : βˆ€ {a b : Set},
  (int β†’ a β†’ b) β†’ list a β†’ list b :=
  @rev_mapi.

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.

Definition rev_filter_map : βˆ€ {a b : Set},
  (a β†’ option b) β†’ list a β†’ list b :=
  fun a b f l β‡’ List.rev (filter_map f l).

Fixpoint filter_map_e {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
    match y with
    | None β‡’ filter_map_e f l'
    | Some z β‡’ let? res := filter_map_e f l' in return? (z :: res)
    end
  end.

Definition rev_filter_map_e : βˆ€ {a b trace : Set},
  (a β†’ Pervasives.result (option b) trace) β†’ list a β†’
  Pervasives.result (list b) trace :=
  fun a b trace f l β‡’ filter_map_e f (List.rev l).

Definition rev_filter_map_s : βˆ€ {a b : Set},
  (a β†’ option b) β†’ list a β†’ list b :=
  @rev_filter_map.

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.

Definition rev_filter_map_es : βˆ€ {a b trace : Set},
  (a β†’ Pervasives.result (option b) trace) β†’ list a β†’
  Pervasives.result (list b) trace :=
  @rev_filter_map_e.

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.

Definition filter_map_p : βˆ€ {a b : Set},
  (a β†’ option b) β†’ list a β†’ list b :=
  @filter_map.

Definition concat_map : βˆ€ {a b : Set}, (a β†’ list b) β†’ list a β†’ list b :=
  fun a b f l β‡’ List.concat (List.map f l).

Definition concat_map_s : βˆ€ {a b : Set},
  (a β†’ list b) β†’ list a β†’ list b :=
  @concat_map.

Definition concat_map_e : βˆ€ {_error a b : Set},
  (a β†’ Pervasives.result (list b) _error) β†’ list a β†’
  Pervasives.result (list b) _error :=
  fun _error a b f l β‡’
  let? ls := map_e f l in
  return? concat ls.

Definition concat_map_es : βˆ€ {_error a b : Set},
  (a β†’ Pervasives.result (list b) _error) β†’ list a β†’
  Pervasives.result (list b) _error :=
  @concat_map_e.

Definition concat_map_p : βˆ€ {a b : Set},
  (a β†’ list b) β†’ list a β†’ list b :=
  @concat_map.

Definition fold_left {a b : Set} (f : a β†’ b β†’ a) (acc : a) (l : list b) : a :=
  Lists.List.fold_left f l acc.

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.

Definition fold_left_s : βˆ€ {a b : Set},
  (a β†’ b β†’ a) β†’ a β†’ list b β†’ a :=
  fun _ _ β‡’
  fold_left.

Definition fold_left_es : βˆ€ {a b trace : Set},
  (a β†’ b β†’ Pervasives.result a trace) β†’ a β†’ list b β†’
  Pervasives.result a trace :=
  fun _ _ _ β‡’
  fold_left_e.

Fixpoint fold_left_map {a b c : Set} (f : a β†’ b β†’ a Γ— c)
  (acc : a) (l : list b) : a Γ— list c :=
  match l with
  | [] β‡’ (acc, [])
  | x :: l' β‡’
    let '(acc1, y) := f acc x in
    let '(acc2, res) := fold_left_map f acc1 l' in (acc2, y :: res)
  end.

Fixpoint fold_left_map_e {a b c trace : Set}
  (f : a β†’ b β†’ Pervasives.result (a Γ— c) trace) (acc : a) (l : list b) :
  Pervasives.result (a Γ— list c) trace :=
  match l with
  | [] β‡’ return? (acc, [])
  | x :: l' β‡’
    let? '(acc1, y) := f acc x in
    let? '(acc2, res) := fold_left_map_e f acc1 l' in
    return? (acc2, y :: res)
  end.

Definition fold_left_map_s : βˆ€ {a b c : Set},
  (a β†’ b β†’ a Γ— c) β†’ a β†’ list b β†’ a Γ— list c :=
  @fold_left_map.

Definition 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 :=
  @fold_left_map_e.

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.

Fixpoint fold_right_e {a b trace : Set}
  (f : a β†’ b β†’ Pervasives.result b trace) (l : list a) (acc : b) :
  Pervasives.result b trace :=
  match l with
  | [] β‡’ return? acc
  | x :: l' β‡’
    let? acc' := fold_right_e f l' acc in
    f x acc'
  end.

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.

Fixpoint iter2_e {a b trace : Set} (er : trace)
  (f : a β†’ b β†’ Pervasives.result unit trace) (l1 : list a) (l2 : list b)
  : Pervasives.result unit trace :=
  match l1, l2 with
  | [], [] β‡’ return? tt
  | x :: l1', y :: l2' β‡’
    let? _ := f x y in iter2_e er f l1' l2'
  | _, _ β‡’ Pervasives.Error er
  end.

Definition iter2_s : βˆ€ {a b trace : Set},
  trace β†’ (a β†’ b β†’ unit) β†’ list a β†’ list b β†’
  Pervasives.result unit trace :=
  @iter2.

Definition iter2_es : βˆ€ {a b trace : Set},
  trace β†’ (a β†’ b β†’ Pervasives.result unit trace) β†’ list a β†’
  list b β†’ Pervasives.result unit trace :=
  @iter2_e.

Fixpoint map2_e {a b c trace : Set} (er : trace)
  (f : a β†’ b β†’ Pervasives.result c trace) (l1 : list a) (l2 : list b) :
  Pervasives.result (list c) trace :=
  match l1, l2 with
  | [], [] β‡’ return? []
  | x :: l1', y :: l2' β‡’
    let? z := f x y in
    let? res := map2_e er f l1' l2' in return? (z :: res)
  | _, _ β‡’ Pervasives.Error er
  end.

Definition map2_s : βˆ€ {a b c trace : Set},
  trace β†’ (a β†’ b β†’ c) β†’ list a β†’ list b β†’
  Pervasives.result (list c) trace :=
  @map2.

Definition map2_es : βˆ€ {a b c trace : Set},
  trace β†’ (a β†’ b β†’ Pervasives.result c trace) β†’ list a β†’
  list b β†’ Pervasives.result (list c) trace :=
  @map2_e.

Definition rev_map2_e : βˆ€ {a b c trace : Set},
  trace β†’ (a β†’ b β†’ Pervasives.result c trace) β†’ list a β†’ list b β†’
  Pervasives.result (list c) trace :=
  fun a b c trace er f l1 l2 β‡’
  let? res := map2_e er f l1 l2 in return? List.rev res.

Definition rev_map2_s : βˆ€ {a b c trace : Set},
  trace β†’ (a β†’ b β†’ c) β†’ list a β†’ list b β†’
  Pervasives.result (list c) trace :=
  @rev_map2.

Definition rev_map2_es : βˆ€ {a b c trace : Set},
  trace β†’ (a β†’ b β†’ Pervasives.result c trace) β†’ list a β†’
  list b β†’ Pervasives.result (list c) trace :=
  @rev_map2_e.

Fixpoint fold_left2_e {a b c trace : Set} (er : trace)
  (f : a β†’ b β†’ c β†’ Pervasives.result a trace) (acc : a) (l1 : list b) (l2 : list c)
  : Pervasives.result a trace :=
  match l1, l2 with
  | [], [] β‡’ return? acc
  | x :: l1', y :: l2' β‡’
    let? acc' := f acc x y in
    fold_left2_e er f acc' l1' l2'
  | _, _ β‡’ Pervasives.Error er
  end.

Definition fold_left2_s : βˆ€ {a b c trace : Set},
  trace β†’ (a β†’ b β†’ c β†’ a) β†’ a β†’ list b β†’ list c β†’
  Pervasives.result a trace :=
  @fold_left2.

Definition 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 :=
  @fold_left2_e.

Fixpoint fold_right2_e {a b c trace : Set} (er : trace)
  (f : a β†’ b β†’ c β†’ Pervasives.result c trace) (l1 : list a) (l2 : list b) (acc : c)
  : Pervasives.result c trace :=
  match l1, l2 with
  | [], [] β‡’ return? acc
  | x :: l1', y :: l2' β‡’
    let? acc' := fold_right2_e er f l1' l2' acc in
    f x y acc'
  | _, _ β‡’ Pervasives.Error er
  end.

Definition fold_right2_s : βˆ€ {a b c trace : Set},
  trace β†’ (a β†’ b β†’ c β†’ c) β†’ list a β†’ list b β†’ c β†’
  Pervasives.result c trace :=
  @fold_right2.

Definition 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 :=
  @fold_right2_e.

Definition for_all : βˆ€ {a : Set}, (a β†’ bool) β†’ list a β†’ bool :=
  fun a β‡’
  List.forallb (A := a).

(* intended semantics? *)
Fixpoint for_all_e {a trace : Set}
  (p : a β†’ Pervasives.result bool trace) (l : list a)
  : Pervasives.result bool trace :=
  match l with
  | [] β‡’ return? true
  | x :: l' β‡’
    let? b := p x in
    let? res := for_all_e p l' in
    return? (b && res)
  end.

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.

Definition for_all_es : βˆ€ {a trace : Set},
  (a β†’ Pervasives.result bool trace) β†’ list a β†’
  Pervasives.result bool trace :=
  @for_all_e.

Definition for_all_p : βˆ€ {a : Set},
  (a β†’ bool) β†’ list a β†’ bool :=
  @for_all.

Definition _exists : βˆ€ {a : Set}, (a β†’ bool) β†’ list a β†’ bool :=
  fun a β‡’
  List.existsb (A := a).

Fixpoint exists_e {a trace : Set}
  (p : a β†’ Pervasives.result bool trace) (l : list a)
  : Pervasives.result bool trace :=
  match l with
  | [] β‡’ return? false
  | x :: l' β‡’
    let? b := p x in
    let? res := exists_e p l' in
    return? (b || res)
  end.

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.

Definition exists_es : βˆ€ {a trace : Set},
  (a β†’ Pervasives.result bool trace) β†’ list a β†’
  Pervasives.result bool trace :=
  @exists_e.

Definition exists_p : βˆ€ {a : Set},
  (a β†’ bool) β†’ list a β†’ bool :=
  @_exists.

Fixpoint for_all2_e {a b trace : Set} (er : trace)
  (f : a β†’ b β†’ Pervasives.result bool trace) (l1 : list a) (l2 : list b)
  : Pervasives.result bool trace :=
  match l1, l2 with
  | [], [] β‡’ return? true
  | x :: l1', y :: l2' β‡’
    let? b := f x y in
    let? res := for_all2_e er f l1' l2' in
    return? (b && res)
  | _, _ β‡’ Pervasives.Error er
  end.

Definition for_all2_s : βˆ€ {a b trace : Set},
  trace β†’ (a β†’ b β†’ bool) β†’ list a β†’ list b β†’
  Pervasives.result bool trace :=
  @for_all2.

Definition for_all2_es : βˆ€ {a b trace : Set},
  trace β†’ (a β†’ b β†’ Pervasives.result bool trace) β†’ list a β†’
  list b β†’ Pervasives.result bool trace :=
  @for_all2_e.

Fixpoint exists2_e {a b trace : Set} (er : trace)
  (f : a β†’ b β†’ Pervasives.result bool trace) (l1 : list a) (l2 : list b)
  : Pervasives.result bool trace :=
  match l1, l2 with
  | [], [] β‡’ return? false
  | x :: l1', y :: l2' β‡’
    let? b := f x y in
    let? res := exists2_e er f l1' l2' in
    return? (b || res)
  | _, _ β‡’ Pervasives.Error er
  end.

Definition exists2_s : βˆ€ {a b trace : Set},
  trace β†’ (a β†’ b β†’ bool) β†’ list a β†’ list b β†’
  Pervasives.result bool trace :=
  @_exists2.

Definition exists2_es : βˆ€ {a b trace : Set},
  trace β†’ (a β†’ b β†’ Pervasives.result bool trace) β†’ list a β†’
  list b β†’ Pervasives.result bool trace :=
  @exists2_e.

Fixpoint combine_drop {a b : Set} (l1 : list a) (l2 : list b) : list (a Γ— b) :=
  match l1, l2 with
  | [], _ β‡’ []
  | _, [] β‡’ []
  | x :: l1', y :: l2' β‡’ (x, y) :: combine_drop l1' l2'
  end.

Fixpoint combine_with_leftovers {a b : Set} (l1 : list a) (l2 : list b)
  : list (a Γ— b) Γ— option (Either.t (list a) (list b)) :=
  match l1, l2 with
  | [], [] β‡’ ([], None)
  | [], _ β‡’ ([], Some (Either.Right l2))
  | _, [] β‡’ ([], Some (Either.Left l1))
  | x :: l1', y :: l2' β‡’
    let '(combine, leftovers) := combine_with_leftovers l1' l2' in
    ((x, y) :: combine, leftovers)
  end.

Parameter product : βˆ€ {a b : Set}, list a β†’ list b β†’ list (a Γ— b).

Fixpoint compare {a : Set} (cmp : a β†’ a β†’ int) (l1 l2 : list a)
  : int :=
  match l1, l2 with
  | [], [] β‡’ 0
  | [], _ β‡’ -1
  | _, [] β‡’ 1
  | x :: l1', y :: l2' β‡’
    match cmp x y with
    | Z0 β‡’ compare cmp l1' l2'
    | Zpos _ β‡’ 1
    | Zneg _ β‡’ -1
    end
  end.

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.

(* inserts new val just before first value greater than it *)
Fixpoint insert {a : Set} (cmp : a β†’ a β†’ int) (x : a) (l : list a) : list a :=
  match l with
  | [] β‡’ [x]
  | y :: l' β‡’
    match cmp x y with
    | Zpos _ β‡’ y :: insert cmp x l'
    | _ β‡’ x :: l
    end
  end.

Fixpoint sort {a : Set} (cmp : a β†’ a β†’ int) (l : list a) : list a :=
  match l with
  | [] β‡’ []
  | x :: l' β‡’ insert cmp x (sort cmp l')
  end.

Definition stable_sort : βˆ€ {a : Set}, (a β†’ a β†’ int) β†’ list a β†’ list a :=
  @sort.

Definition fast_sort : βˆ€ {a : Set}, (a β†’ a β†’ int) β†’ list a β†’ list a :=
  @sort.

Definition sort_uniq : βˆ€ {a : Set}, (a β†’ a β†’ int) β†’ list a β†’ list a :=
  @sort.

Fixpoint to_seq_node {a : Set} (l : list a) : Seq.node a :=
  match l with
  | [] β‡’ Seq.Nil
  | x :: l' β‡’ Seq.Cons x (fun _ β‡’ to_seq_node l')
  end.

Definition to_seq : βˆ€ {a : Set}, list a β†’ Seq.t a :=
  fun a l _ β‡’ to_seq_node l.

Fixpoint of_seq_node {a : Set} (s : Seq.node a) : list a :=
  match s with
  | Seq.Nil β‡’ []
  | Seq.Cons x f β‡’ x :: of_seq_node (f tt)
  end.

Definition of_seq : βˆ€ {a : Set}, Seq.t a β†’ list a :=
  fun a s β‡’ of_seq_node (s tt).

Fixpoint nat_init_ep {a : Set} (n : nat) (ff : nat β†’ M? a) : M? (list a) :=
  match n with
  | 0%nat β‡’ return? []
  | S k β‡’
    match ff 0%nat with
    | Pervasives.Ok x β‡’
        let? res := nat_init_ep k (fun x β‡’ ff (S x)) in return? (x :: res)
    | Pervasives.Error es β‡’
      match nat_init_ep k (fun x β‡’ ff (S x)) with
      | Pervasives.Error es' β‡’ Pervasives.Error (List.app es es')
      | Pervasives.Ok _ β‡’ Pervasives.Error es
      end
    end
  end.

Definition init_ep : βˆ€ {_error a : Set},
  _error β†’ int β†’ (int β†’ M? a) β†’ M? (list a) :=
  fun _error a er n ff β‡’
  match n with
  | Z0 β‡’ return? []
  | Zpos _ β‡’ nat_init_ep (Z.to_nat n) (fun x β‡’ ff (Z.of_nat x))
  | Zneg _ β‡’ let error := Build_extensible "negative value" _ er in
      Pervasives.Error [error]
  end.

Fixpoint filter_ep {a : Set} (p : a β†’ M? bool) (l : list a)
  : M? (list a) :=
  match l with
  | [] β‡’ return? []
  | x :: l' β‡’
    match p x with
    | Pervasives.Ok b β‡’
        let? res := filter_ep p l' in
        return? (if b then (x :: res) else res)
    | Pervasives.Error es β‡’
      match filter_ep p l' with
      | Pervasives.Error es' β‡’ Pervasives.Error (List.app es es')
      | Pervasives.Ok _ β‡’ Pervasives.Error es
      end
    end
  end.

Fixpoint partition_ep {a : Set}
  (p : a β†’ M? bool) (l : list a) : M? (list a Γ— list a) :=
  match l with
  | [] β‡’ return? ([], [])
  | hd :: tl β‡’
    match p hd with
    | Pervasives.Ok b β‡’
        let? '(res_left, res_right) := partition_ep p tl in
        return? (
          if b
            then (hd :: res_left, res_right)
            else (res_left, hd :: res_right)
          )
    | Pervasives.Error es β‡’
      match partition_ep p tl with
      | Pervasives.Error es' β‡’ Pervasives.Error (List.app es es')
      | Pervasives.Ok _ β‡’ Pervasives.Error es
      end
    end
  end.

Fixpoint partition_map_ep {a b c : Set}
  (p : a β†’ M? (Either.t b c)) (l : list a) : M? (list b Γ— list c) :=
    match l with
    | [] β‡’ return? ([], [])
    | hd :: tl β‡’
      match p hd with
      | Pervasives.Ok b β‡’
          match b with
          | Either.Left b β‡’
            let? '(res_left, res_right) := partition_map_ep p tl in
            return? (b :: res_left, res_right)
          | Either.Right c β‡’
            let? '(res_left, res_right) := partition_map_ep p tl in
            return? (res_left, c :: res_right)
          end
      | Pervasives.Error es β‡’
          match partition_map_ep p tl with
          | Pervasives.Error es' β‡’ Pervasives.Error (List.app es es')
          | Pervasives.Ok _ β‡’ Pervasives.Error es
          end
      end
    end.

Fixpoint iter_ep {a : Set} (p : a β†’ M? unit) (l : list a) : M? unit :=
  match l with
  | [] β‡’ return? tt
  | hd :: tl β‡’
    match p hd with
    | Pervasives.Ok _ β‡’ iter_ep p tl
    | Pervasives.Error es β‡’
        match iter_ep p tl with
        | Pervasives.Error es' β‡’ Pervasives.Error (List.app es es')
        | Pervasives.Ok _ β‡’ Pervasives.Error es
        end
    end
  end.

Definition iteri_ep {a : Set}
  (p : int β†’ a β†’ M? unit) (l : list a) : M? unit :=
  let fix iteri_ep_aux (index : int) (l : list a) : M? unit :=
    match l with
    | [] β‡’ return? tt
    | hd :: tl β‡’
      match p index hd with
      | Pervasives.Ok _ β‡’ iteri_ep_aux (index +i 1) tl
      | Pervasives.Error es β‡’
          match iteri_ep_aux (index +i 1) tl with
          | Pervasives.Error es' β‡’ Pervasives.Error (List.app es es')
          | Pervasives.Ok _ β‡’ Pervasives.Error es
          end
      end
    end
  in
  iteri_ep_aux 0 l.

Fixpoint map_ep {a b : Set}
  (p : a β†’ M? b) (l : list a) : M? (list b) :=
  match l with
  | [] β‡’ return? []
  | hd :: tl β‡’
    match p hd with
    | Pervasives.Ok b β‡’
      let? res := map_ep p tl in
      return? (b :: res)
    | Pervasives.Error es β‡’
        match map_ep p tl with
        | Pervasives.Error es' β‡’ Pervasives.Error (List.app es es')
        | Pervasives.Ok _ β‡’ Pervasives.Error es
        end
    end
  end.

Definition mapi_ep {a b : Set}
  (p : int β†’ a β†’ M? b) (l : list a) : M? (list b) :=
  let fix mapi_ep_aux index l :=
    match l with
    | [] β‡’ return? []
    | hd :: tl β‡’
      match p index hd with
      | Pervasives.Ok b β‡’
        let? res := mapi_ep_aux (index +i 1) tl in
        return? (b :: res)
      | Pervasives.Error es β‡’
          match mapi_ep_aux (index +i 1) tl with
          | Pervasives.Error es' β‡’ Pervasives.Error (List.app es es')
          | Pervasives.Ok _ β‡’ Pervasives.Error es
          end
      end
    end in
  mapi_ep_aux 0 l.

Definition rev_map_ep {a b : Set}
  (p : a β†’ M? b) (l : list a) : M? (list b) :=
  let? res := map_ep p l in
  return? (List.rev res).

Definition rev_mapi_ep {a b : Set}
  (p : int β†’ a β†’ M? b) (l : list a) : M? (list b) :=
  let? res := mapi_ep p l in
  return? (List.rev res).

Fixpoint filter_map_ep {a b : Set}
  (p : a β†’ M? (option b)) (l : list a) : M? (list b) :=
  match l with
  | [] β‡’ return? []
  | hd :: tl β‡’
    match p hd with
    | Pervasives.Ok b β‡’ match b with
                         | None β‡’ filter_map_ep p tl
                         | Some v β‡’
                            let? res := filter_map_ep p tl in
                            return? (v :: res)
                         end
    | Pervasives.Error es β‡’
        match filter_map_ep p tl with
        | Pervasives.Error es' β‡’ Pervasives.Error (List.app es es')
        | Pervasives.Ok _ β‡’ Pervasives.Error es
        end
    end
  end.

Definition concat_map_ep {a b : Set}
  (p : a β†’ M? (list b)) (l : list a) : M? (list b) :=
  let? res := map_ep p l in
  return? (List.concat res).

Fixpoint for_all_ep {a : Set}
  (p : a β†’ M? bool) (l : list a) : M? bool :=
  match l with
  | [] β‡’ return? true
  | hd :: tl β‡’
    match p hd with
    | Pervasives.Ok b β‡’
        let? res := for_all_ep p tl in
        return? (b && res)
    | Pervasives.Error es β‡’
        match for_all_ep p tl with
        | Pervasives.Error es' β‡’ Pervasives.Error (List.app es es')
        | Pervasives.Ok _ β‡’ Pervasives.Error es
        end
    end
  end.

Fixpoint exists_ep {a : Set}
  (p : a β†’ M? bool) (l : list a) : M? bool :=
  match l with
  | [] β‡’ return? false
  | hd :: tl β‡’
    match p hd with
    | Pervasives.Ok b β‡’
        let? res := exists_ep p tl in
        return? (b || res)
    | Pervasives.Error es β‡’
        match exists_ep p tl with
        | Pervasives.Error es' β‡’ Pervasives.Error (List.app es es')
        | Pervasives.Ok _ β‡’ Pervasives.Error es
        end
    end
  end.