Library CoLoR.Util.List.ListUtil

Set Implicit Arguments.

Require Import LogicUtil NatUtil EqUtil Setoid SetoidList RelMidex Omega
  RelUtil BoolUtil.
Require Export List.
Require Program.


Ltac elt_type l := match type of l with list ?A => A end.

Infix "[=" := incl (at level 70).

Section In.

  Variable A : Type.

  Lemma in_app : forall l m (x : A), In x (l ++ m) <-> In x l \/ In x m.

  Lemma notin_app : forall l m (x : A), ~In x (l ++ m) <-> ~In x l /\ ~In x m.

  Lemma in_appl : forall (x : A) l1 l2, In x l1 -> In x (l1 ++ l2).

  Lemma in_appr : forall (x : A) l1 l2, In x l2 -> In x (l1 ++ l2).

  Lemma in_app_com : forall (x : A) l1 l2 l3,
    In x ((l1 ++ l3) ++ l2) -> In x ((l1 ++ l2) ++ l3).

  Lemma in_elim : forall (x : A) l,
    In x l -> exists l1, exists l2, l = l1 ++ x :: l2.

  Variable eqA_dec : forall x y : A, {x=y}+{~x=y}.

  Lemma in_elim_dec : forall (x : A) l,
    In x l -> exists m, exists p, l = m ++ x :: p /\ ~In x m.

  Lemma In_midex : eq_midex A -> forall (x : A) l, In x l \/ ~In x l.

  Lemma In_elim_right : eq_midex A -> forall (x : A) l,
    In x l -> exists l', exists l'', l = l'++x::l'' /\ ~In x l''.

  Lemma In_cons : forall (x a : A) l, In x (a::l) <-> a=x \/ In x l.

  Lemma In_InA_eq : forall (x : A) l, In x l <-> InA eq x l.

End In.

Implicit Arguments in_elim [A x l].
Implicit Arguments in_elim_dec [A x l].

Ltac intac := repeat (apply in_eq || apply in_cons).

Ltac list_ok := let x := fresh in intro x;
  match goal with
    | |- In _ ?l => vm_compute; destruct x; tauto
  end.

Instance incl_rel A : PreOrder (@incl A).


Instance app_incl A : Proper (incl ==> incl ==> incl) (@app A).


Section incl.

  Variable A : Type.

  Lemma incl_nil_elim : forall l : list A, l [= nil <-> l = nil.

  Lemma incl_nil : forall l : list A, nil [= l.

  Lemma incl_cons_l : forall (a : A) l m, a :: l [= m -> In a m /\ l [= m.

  Lemma incl_cons_l_in : forall (x : A) l m, x :: l [= m -> In x m.

  Lemma incl_cons_l_incl : forall (x : A) l m, x :: l [= m -> l [= m.

  Lemma incl_app_elim : forall l1 l2 l3 : list A,
    l1 ++ l2 [= l3 -> l1 [= l3 /\ l2 [= l3.

  Lemma incl_appr_incl : forall l1 l2 l3 : list A, l1 ++ l2 [= l3 -> l1 [= l3.

  Lemma incl_appl_incl : forall l1 l2 l3 : list A, l1 ++ l2 [= l3 -> l2 [= l3.

  Lemma appl_incl : forall l l2 l2' : list A, l2 [= l2' -> l ++ l2 [= l ++ l2'.

  Lemma appr_incl : forall l l1 l1' : list A, l1 [= l1' -> l1 ++ l [= l1' ++ l.

  Lemma app_com_incl : forall l1 l2 l3 l4 : list A,
    (l1 ++ l3) ++ l2 [= l4 -> (l1 ++ l2) ++ l3 [= l4.

  Lemma incl_cons_r : forall x : A, forall m l, l [= x :: m -> In x l \/ l [= m.

  Variable eqA_dec : forall x y : A, {x=y}+{~x=y}.

  Lemma not_incl : forall l m, ~ l [= m <-> exists x:A, In x l /\ ~In x m.

End incl.

Implicit Arguments incl_app_elim [A l1 l2 l3].

Definition strict_incl A (l m : list A) := l [= m /\ ~m [= l.

Infix "[" := strict_incl (at level 70).

Lemma strict_incl_tran : forall A (l m n : list A), l [ m -> m [ n -> l [ n.

Instance strict_incl_rel A : Transitive (@strict_incl A).

Definition lequiv {A} (l1 l2 : list A) := l1 [= l2 /\ l2 [= l1.

Infix "[=]" := lequiv (at level 70).

Instance lequiv_rel A : Equivalence (@lequiv A).


Instance app_lequiv A : Proper (lequiv ==> lequiv ==> lequiv) (@app A).


Instance incl_lequiv1 A1 B (f : list A1 -> relation B) :
  Proper (incl ==> inclusion) f -> Proper (lequiv ==> same_rel) f.


Instance incl_lequiv2 A1 A2 B (f : list A1 -> list A2 -> relation B) :
  Proper (incl ==> incl ==> inclusion) f ->
  Proper (lequiv ==> lequiv ==> same_rel) f.

Section nil.

  Variable A : Type.

  Lemma list_empty_dec : forall l : list A, {l = nil} + {l <> nil}.

  Definition is_empty (l : list A) : bool :=
    match l with
      | nil => true
      | _ => false
    end.

End nil.

Instance cons_incl A : Proper (Logic.eq ==> incl ==> incl) (@cons A).


Instance cons_lequiv A : Proper (Logic.eq ==> lequiv ==> lequiv) (@cons A).


Section cons.

  Variable A : Type.

  Lemma cons_eq : forall x x' : A, forall l l',
    x = x' -> l = l' -> x :: l = x' :: l'.

  Lemma head_eq : forall x x' : A, forall l, x = x' -> x :: l = x' :: l.

  Lemma tail_eq : forall x : A, forall l l', l = l' -> x :: l = x :: l'.

End cons.

Section app.

  Variable A : Type.

  Lemma length_app : forall l m : list A, length (l ++ m) = length l + length m.

  Lemma app_nil : forall l1 l2 : list A, l1 = nil -> l2 = nil -> l1 ++ l2 = nil.

  Lemma app_eq : forall l1 l2 l1' l2' : list A,
    l1 = l1' -> l2 = l2' -> l1 ++ l2 = l1' ++ l2'.

  Lemma appl_eq : forall l1 l2 l1' : list A, l1 = l1' -> l1 ++ l2 = l1' ++ l2.

  Lemma appr_eq : forall l1 l2 l2' : list A, l2 = l2' -> l1 ++ l2 = l1 ++ l2'.

  Lemma list_app_first_last : forall l m (a : A),
    (l ++ a::nil) ++ m = l ++ a::m.

  Lemma list_app_last : forall l m n (a : A),
    l ++ m = n ++ a::nil -> m <> nil -> In a m.

  Lemma list_drop_last : forall l m n (a : A),
    l ++ m = n ++ a::nil -> m <> nil -> exists2 w, w [= m & l ++ w = n.

  Lemma last_intro : forall l : list A, length l > 0 ->
    exists m, exists a, l = m ++ a :: nil /\ length m = length l - 1.

End app.

Section length.

  Variable A : Type.

  Lemma length_0 : forall l : list A, length l = 0 -> l = nil.

End length.

Implicit Arguments length_0 [A l].

Section head_tail.

  Variable A : Type.

  Lemma head_app : forall (l l': list A) (lne: l <> nil),
    head (l ++ l') = head l.

  Lemma length_tail : forall l : list A, length (tail l) <= length l.

  Lemma tail_in : forall (x: A) l, In x (tail l) -> In x l.

  Lemma tail_cons_tail : forall (l1 l2: list A),
    l1 <> nil -> tail l1 ++ l2 = tail (l1 ++ l2).

  Lemma length_tail_minus : forall (l : list A), length (tail l) = length l - 1.

  Lemma list_decompose_head : forall (l : list A) el (lne: l <> nil),
    head l = Some el -> l = el :: tail l.

  Lemma in_head_tail : forall a (l : list A),
    In a l -> Some a = head l \/ In a (tail l).

  Lemma head_notNil : forall (l : list A) (lne : l <> nil),
    {a : A | head l = Some a}.

  Lemma head_of_notNil : forall (l : list A) a (lne: l <> nil),
    head l = Some a -> proj1_sig (head_notNil lne) = a.

End head_tail.

Hint Resolve tail_in tail_cons_tail head_app : datatypes.
Hint Rewrite head_app length_app : datatypes.

Section tail_nth.

  Variable A : Type.

  Fixpoint tail_nth (l : list A) (n : nat) : option (list A) :=
    match l, n with
      | _, 0 => Some l
      | a :: l', S n' => tail_nth l' n'
      | _, _ => None
    end.

End tail_nth.

Section filter.

  Variables (A : Type) (f : A -> bool).

  Lemma filter_app : forall l m, filter f (l ++ m) = filter f l ++ filter f m.

  Lemma filter_incl : forall l, filter f l [= l.

  Variable eq_dec : forall x y : A, {x=y}+{~x=y}.

  Lemma notIn_filter : forall x l,
    ~In x (filter f l) <-> ~In x l \/ (In x l /\ f x = false).

End filter.

Section filter_opt.

  Variables (A B : Type) (f : A -> option B).

  Fixpoint filter_opt (l : list A) : list B :=
    match l with
      | nil => nil
      | cons a m =>
        match f a with
          | Some b => cons b (filter_opt m)
          | _ => filter_opt m
        end
    end.

End filter_opt.

Section Inb.

  Variables (A : Type) (eq_dec : forall x y : A, {x=y}+{~x=y}).

  Fixpoint Inb (x : A) (l : list A) : bool :=
    match l with
      | nil => false
      | cons y l' =>
        match eq_dec x y with
          | left _ => true
          | _ => Inb x l'
        end
    end.

  Lemma Inb_true : forall x l, Inb x l = true -> In x l.

  Lemma Inb_false : forall x l, Inb x l = false -> In x l -> False.

  Lemma Inb_intro : forall x l, In x l -> Inb x l = true.

  Lemma Inb_elim : forall x l, ~In x l -> Inb x l = false.

  Lemma Inb_correct : forall x l, In x l <-> Inb x l = true.

  Lemma Inb_incl : forall x l l', l [= l' -> Inb x l = true -> Inb x l' = true.

  Lemma Inb_equiv : forall x l l', lequiv l l' -> Inb x l = Inb x l'.

  Definition Inclb (l1 l2 : list A) := forallb (fun x => Inb x l2) l1.

  Lemma Inclb_ok : forall l1 l2, Inclb l1 l2 = true <-> l1 [= l2.

End Inb.

Ltac inbtac :=
  match goal with
    | _ : In ?x ?l |- _ =>
      let H0 := fresh "H" in
        (assert (H0 : Inb x l = true); apply Inb_intro; hyp; rewrite H0)
  end.

Section remove.

  Variables (A : Type) (eq_dec : forall x y : A, {x=y}+{~x=y}).

  Fixpoint remove (y : A) (l : list A) : list A :=
    match l with
      | nil => nil
      | cons x l' =>
        match eq_dec x y with
          | left _ => remove y l'
          | right _ => cons x (remove y l')
        end
    end.

  Lemma length_remove : forall (x : A) l, length (remove x l) <= length l.

  Lemma In_length_remove : forall (x : A) l,
    In x l -> length (remove x l) < length l.

  Lemma In_remove : forall (x y : A) l, x <> y -> In y l -> In y (remove x l).

  Lemma incl_remove : forall (x : A) l m, ~In x l -> l [= m -> l [= remove x m.

  Lemma notin_remove : forall x l, In x (remove x l) -> False.

  Lemma remove_In : forall a x l, In a (remove x l) -> In a l.

  Lemma remove_eq : forall a x l, In a (remove x l) <-> a <> x /\ In a l.

End remove.

Section removes.

  Variable (A : Type) (eqdec : forall x y : A, {x=y}+{x<>y}).

  Notation In_dec := (In_dec eqdec).

  Fixpoint removes (l m : list A) : list A :=
    match m with
      | nil => nil
      | x :: m' =>
        match In_dec x l with
          | left _ => removes l m'
          | right _ => x :: removes l m'
        end
    end.

  Lemma incl_removes : forall l m, removes l m [= m.

  Lemma incl_removes_app : forall l m, m [= removes l m ++ l.

  Lemma In_removes : forall x l m, In x (removes l m) <-> In x m /\ ~In x l.

End removes.

Section map.

  Variable (A B : Type) (f : A->B).

  Lemma map_app : forall l1 l2, map f (l1 ++ l2) = (map f l1) ++ map f l2.

  Lemma in_map_elim : forall x l, In x (map f l) -> exists y, In y l /\ x = f y.

  Lemma map_eq : forall (g : A->B) l,
    (forall x, In x l -> f x = g x) -> map f l = map g l.

End map.

Implicit Arguments in_map_elim [A B f x l].

Lemma map_eq_id : forall A (f:A->A) l,
  (forall x, In x l -> f x = x) -> map f l = l.

Section flat_map.

  Variables (A B : Type) (f : A -> list B).

  Lemma In_flat_map_intro : forall x l y,
    In y l -> In x (f y) -> In x (flat_map f l).

  Lemma In_flat_map_elim : forall l y,
    In y (flat_map f l) -> exists x, In x l /\ In y (f x).

  Lemma flat_map_app : forall l m,
    flat_map f (l ++ m) = flat_map f l ++ flat_map f m.

End flat_map.

Section flat.

  Variable A : Type.

  Fixpoint flat (l : list (list A)) : list A :=
    match l with
      | nil => nil
      | cons x l' => x ++ flat l'
    end.

  Lemma In_incl_flat : forall x l, In x l -> x [= flat l.

  Lemma incl_flat_In : forall x c cs l,
    In x c -> In c cs -> flat cs [= l -> In x l.

End flat.

Implicit Arguments In_incl_flat [A x l].

Section Element_At_List.

  Variable A : Type.

  Fixpoint element_at (l : list A) (p : nat) : option A :=
    match l with
      | nil => None
      | h :: t =>
        match p with
          | 0 => Some h
          | S p' => element_at t p'
        end
    end.

  Notation "l '[' p ']'" := (element_at l p) (at level 50).

  Fixpoint replace_at (l : list A) (p : nat) (a : A) : list A :=
    match l with
      | nil => nil
      | h :: t =>
        match p with
          | 0 => a :: t
          | S p' => h :: (replace_at t p' a)
        end
    end.

  Notation "l '[' p ':=' a ']'" := (replace_at l p a) (at level 50).

  Lemma element_at_exists : forall l p,
    p < length l <-> ex (fun a => l[p] = Some a).

  Lemma element_at_replaced : forall l p a, p < length l -> l[p:=a][p] = Some a.

  Lemma element_at_not_replaced : forall l p q a, p <> q -> l[p] = l[q:=a][p].

  Lemma in_exists_element_at :
    forall l a, In a l -> ex (fun p => l[p] = Some a).

  Lemma exists_element_at_in :
    forall l a, ex (fun p => l[p] = Some a) -> In a l.

  Lemma element_at_in : forall (x:A) l n, l[n] = Some x -> In x l.

  Lemma element_at_in2 :
    forall (x:A) l n, l[n] = Some x -> In x l /\ n < length l.

  Lemma element_at_app_r : forall l l' p,
    p >= length l -> (l ++ l') [p] = l' [p - length l].

  Lemma replace_at_app_r : forall l l' p a,
    p >= length l -> (l ++ l') [p := a] = l ++ l' [p - length l := a].

End Element_At_List.

Implicit Arguments element_at_in [A x l n].
Implicit Arguments element_at_in2 [A x l n].
Implicit Arguments in_exists_element_at [A l a].
Implicit Arguments element_at_exists [A l p].

Notation "l '[' p ']'" := (element_at l p) (at level 50) : list_scope.
Notation "l '[' p ':=' a ']'" := (replace_at l p a) (at level 50) : list_scope.

Section one_less.

  Variables (A : Type) (r : relation A).

  Inductive one_less : relation (list A) :=
    | one_less_cons : forall (l l' : list A) (p : nat) (a a' : A),
      r a a' -> l[p] = Some a -> l' = l[p:=a'] -> one_less l l'.

  Lemma one_less_length : forall l l', one_less l l' -> length l = length l'.

End one_less.

Implicit Arguments one_less [A].
Implicit Arguments one_less_cons [A].

Section reverse.

  Variable A : Type.

  Lemma in_rev : forall (x : A) l, In x l -> In x (rev l).

  Lemma incl_rev : forall l : list A, l [= rev l.

  Lemma rev_incl : forall l : list A, rev l [= l.

  Lemma incl_rev_intro : forall l l' : list A, rev l [= rev l' -> l [= l'.

End reverse.

Section reverse_tail_recursive.

  Variable A : Type.

  Fixpoint rev_append (l' l : list A) : list A :=
    match l with
      | nil => l'
      | a :: l => rev_append (a :: l') l
    end.

  Notation rev' := (rev_append nil).

  Lemma rev_append_rev : forall l l', rev_append l' l = rev l ++ l'.

  Lemma rev_append_app : forall l l' acc : list A,
    rev_append acc (l ++ l') = rev_append (rev_append acc l) l'.

  Lemma rev'_app : forall l l' : list A, rev' (l ++ l') = rev' l' ++ rev' l.

  Lemma rev'_rev : forall l : list A, rev' l = rev l.

  Lemma rev'_rev' : forall l : list A, rev' (rev' l) = l.

  Lemma rev'_cons : forall a (l : list A), rev' (a::l) = rev' l ++ (a::nil).

End reverse_tail_recursive.

Notation rev' := (rev_append nil).

Section split.

  Variable A : Type.

  Fixpoint split_aux (acc l : list A) (n : nat) : option (list A * list A) :=
    match l, n with
      | _, 0 => Some (rev' acc, l)
      | a :: l', S n' => split_aux (a::acc) l' n'
      | _, _ => None
    end.

  Lemma split_aux_correct : forall l n l1 l2 acc,
    split_aux acc l n = Some (l1, l2) -> rev' acc ++ l = l1 ++ l2.

  Implicit Arguments split_aux_correct [l n l1 l2].

  Notation split := (split_aux nil).

  Lemma split_correct : forall l n l1 l2,
    split l n = Some (l1, l2) -> l = l1 ++ l2.

End split.

Notation split := (split_aux nil).

Implicit Arguments split_correct [A l n l1 l2].

Section last.

  Variable A : Type.

  Lemma last_nth : forall (d : A) l, last l d = nth (length l - 1) l d.

  Lemma last_default : forall (d1 : A) d2 l, l <> nil -> last l d1 = last l d2.

End last.

Implicit Arguments last_intro [A l].

Section partition.

  Variables (A : Type) (f : A -> bool) (a : A) (l : list A).

  Lemma partition_complete : let p := partition f l in
    In a l -> In a (fst p) \/ In a (snd p).

  Lemma partition_inleft : In a (fst (partition f l)) -> In a l.

  Lemma partition_inright : In a (snd (partition f l)) -> In a l.

  Lemma partition_left : In a (fst (partition f l)) -> f a = true.

  Lemma partition_right : In a (snd (partition f l)) -> f a = false.

End partition.

Section partition_by_prop.

  Variables (A : Type) (P : A -> Prop) (P_dec : forall x, {P x}+{~P x}).

  Definition partition_by_prop a :=
    match P_dec a with
    | left _ => true
    | right _ => false
    end.

  Lemma partition_by_prop_true : forall a, partition_by_prop a = true -> P a.

End partition_by_prop.

Section partition_by_rel.

  Variables (A : Type) (R : relation A) (R_dec : rel_dec R).

  Definition partition_by_rel p :=
    if R_dec (fst p) (snd p) then true else false.

  Lemma partition_by_rel_true : forall a b,
    partition_by_rel (a, b) = true -> R a b.

End partition_by_rel.

Section ListFilter.

  Variable A : Type.

  Fixpoint listfilter (L : list A) l :=
    match L with
      | nil => nil
      | a :: Q =>
        match l with
          | nil => nil
          | true :: q => a :: listfilter Q q
          | false :: q => listfilter Q q
        end
    end.

  Lemma listfilter_in : forall L l i x,
    L[i]=Some x -> l[i]=Some true -> In x (listfilter L l) .

End ListFilter.

Section ListsNth.

  Variable A: Type.

  Lemma In_nth : forall A d (x : A) l,
    In x l -> exists i, i < length l /\ nth i l d = x.

  Lemma nth_error_In : forall (l : list A) i,
    {a : A | nth_error l i = Some a} + {nth_error l i = None}.

  Lemma nth_some_in :
    forall (l : list A) i a, nth_error l i = Some a -> In a l.

  Lemma list_In_nth : forall (l : list A) a,
    In a l -> exists p: nat, nth_error l p = Some a.

  Lemma nth_app_left : forall (l m: list A) i,
    i < length l -> nth_error (l ++ m) i = nth_error l i.

  Lemma nth_app_right : forall (l m: list A) i, i >= length l ->
     nth_error (l ++ m) i = nth_error m (i - length l).

  Lemma nth_app : forall (l m: list A) a i, nth_error (l ++ m) i = Some a ->
    (nth_error l i = Some a /\ i < length l) \/
    (nth_error m (i - length l) = Some a /\ i >= length l).

  Lemma nth_beyond : forall (l : list A) i,
    i >= length l -> nth_error l i = None.

  Lemma nth_beyond_idx : forall (l : list A) i,
    nth_error l i = None -> i >= length l.

  Lemma nth_in : forall (l : list A) i,
    nth_error l i <> None <-> i < length l.

  Lemma nth_some : forall (l : list A) n a,
    nth_error l n = Some a -> n < length l.

  Lemma nth_map_none : forall (l : list A) i (f: A -> A),
    nth_error l i = None -> nth_error (map f l) i = None.

  Lemma nth_map_none_rev : forall (l : list A) i (f: A -> A),
    nth_error (map f l) i = None -> nth_error l i = None.

  Lemma nth_map_some : forall (l : list A) i (f: A -> A) a,
    nth_error l i = Some a -> nth_error (map f l) i = Some (f a).

  Lemma nth_map_some_rev : forall (l : list A) i (f: A -> A) a,
    nth_error (map f l) i = Some a ->
    exists a', nth_error l i = Some a' /\ f a' = a.

  Lemma nth_error_singleton_in : forall (a b: A) i,
    nth_error (a :: nil) i = Some b -> a = b /\ i = 0.

End ListsNth.

Implicit Arguments In_nth [A x l].

Section ith.

  Variable A : Type.

  Fixpoint ith (l : list A) : forall i, i < length l -> A :=
    match l as l return forall i, i < length l -> A with
      | nil => fun i H => False_rect A (lt_n_O H)
      | cons x m => fun i =>
        match i return i < S (length m) -> A with
          | O => fun _ => x
          | S j => fun H => ith (lt_S_n H)
        end
    end.

  Lemma ith_In : forall l i (h : i < length l), In (ith h) l.

  Lemma ith_eq : forall l i (hi : i < length l) j (hj : j < length l),
    i = j -> ith hi = ith hj.

  Lemma ith_eq_app : forall m l i (hi : i < length (l++m))
    j (hj : j < length l), i = j -> ith hi = ith hj.

End ith.

Implicit Arguments ith_In [A l i].

Section values.

  Variables (A : Type) (f : nat -> A).

  Fixpoint values j : list A :=
    match j with
      | 0 => nil
      | S k => f k :: values k
    end.

End values.

Section pvalues.

  Variable A : Type.

  Fixpoint pvalues n : (forall i, i < n -> A) -> list A :=
    match n as n return (forall i, i < n -> A) -> list A with
      | 0 => fun _ => nil
      | S k => fun f =>
        f 0 (lt_O_Sn k) :: pvalues (fun i h => f (S i) (lt_n_S h))
    end.

  Lemma pvalues_eq : forall n (f g : forall i, i < n -> A),
    (forall i (hi : i < n), f i hi = g i hi) -> pvalues f = pvalues g.

End pvalues.

Section pvalues_map.

  Variables (A B : Type) (f : A -> B).

  Definition f_ith (l : list A) i (hi : i < length l) := f (ith hi).

  Lemma pvalues_ith_eq_map : forall l, pvalues (@f_ith l) = map f l.

End pvalues_map.

Definition nat_lts n := list (nat_lt n).

Lemma in_map_val : forall n (l : nat_lts n) i, In i (map (@val n) l) -> i<n.

Implicit Arguments in_map_val [n l i].

Section mk_nat_lts.

  Variable n : nat.

  Lemma mk_nat_lts_aux1 : forall k', S k' < n -> k' < n.


  Fixpoint mk_nat_lts_aux k :=
    match k as k return k<n -> list (nat_lt n) with
      | 0 => fun h => mk_nat_lt h :: nil
      | S k' => fun h => mk_nat_lt h :: mk_nat_lts_aux k' (mk_nat_lts_aux1 h)
    end.

  Lemma mk_nat_lts_aux_correct : forall x k (h : k<n) i,
    i <= k -> val (nth i (mk_nat_lts_aux h) x) = k - i.

  Lemma mk_nat_lts_aux_complete : forall k (h : k<n) i (p : i<n),
    i <= k -> In (mk_nat_lt p) (mk_nat_lts_aux h).

End mk_nat_lts.

Implicit Arguments mk_nat_lts_aux [].


Definition mk_nat_lts n :=
  match n return list (nat_lt n) with
    | 0 => nil
    | S p => mk_nat_lts_aux (S p) p (le_n (S p))
  end.

Implicit Arguments mk_nat_lts [].

Lemma mk_nat_lts_correct : forall n x i,
  i < n -> val (nth i (mk_nat_lts n) x) = pred n - i.

Lemma mk_nat_lts_complete : forall n i (p : i<n),
  In (mk_nat_lt p) (mk_nat_lts n).

Section first.

  Variable (A : Type) (f : A -> bool).

  Fixpoint first l :=
    match l with
      | nil => None
      | x :: l' => if f x then Some x else first l'
    end.

End first.

Instance transpose_inclusion A B : Proper (inclusion ==> Logic.eq ==> impl)
  (@transpose A B).


Instance transpose_same_rel A B :
  Proper (same_rel ==> Logic.eq ==> iff) (@transpose A B).

Section fold_left.

  Variables (A : Type) (eqA : relation A) (B : Type) (eqB : relation B).

  Definition feq f f' :=
    forall a a', eqA a a' -> forall b b', eqB b b' -> eqA (f a b) (f' a' b').

  Global Instance fold_left_m_ext :
    Proper (feq ==> eqlistA eqB ==> eqA ==> eqA) (@fold_left A B).


End fold_left.

Section fold_left_list.

  Variables (A B : Type) (f : list A -> B -> list A).

  Variable g : B -> list A.

  Variable hyp : forall l b, f l b = g b ++ l.

  Lemma fold_left_flat_map : forall bs l,
    fold_left f bs l = flat_map g (rev bs) ++ l.

  Lemma In_fold_left : forall a bs l,
    In a (fold_left f bs l) <-> (In a l \/ exists b, In b bs /\ In a (g b)).

End fold_left_list.

Implicit Arguments fold_left_flat_map [A B f].
Implicit Arguments In_fold_left [A B f].

Section Check_seq_aux.

  Variables (n : nat) (Pr : nat_lt n -> Prop)
    (P : forall i : nat_lt n, Exc (Pr i)).

  Program Fixpoint check_seq_aux p (H : forall i : nat_lt n, val i < p -> Pr i)
    {measure (n - p)} : Exc (forall i : nat_lt n, Pr i) :=
    match le_lt_dec n p with
      | left _ => value _
      | right cmp =>
        match @P (mk_nat_lt cmp) with
          | error => error
          | value _ => @check_seq_aux (S p) _ _
        end
    end.


End Check_seq_aux.

Program Definition check_seq (n : nat) (Pr : nat_lt n -> Prop)
  (P : forall (i : nat_lt n), Exc (Pr i)) :
  Exc (forall (i : nat_lt n), Pr i) :=
  check_seq_aux P (p:=0) _.