Library Lib_ListFactsMore

Require Import Lib_Tactic List.

Results on List.map

Lemma list_map_id : forall (A : Set) l,
  List.map (fun t : A => t) l = l.

Lemma list_concat_right : forall (A : Set) (x : A) l1 l2,
  l1 ++ (x :: l2) = (l1 ++ (x :: nil)) ++ l2.

Lemma list_map_nth : forall (A : Set) (f : A -> A) d l n,
  f d = d ->
  f (List.nth n l d) = List.nth n (List.map f l) d.

Results on List.forall

Inductive list_forall (A : Set) (P : A -> Prop) : list A -> Prop :=
  | list_forall_nil : list_forall P nil
  | list_forall_cons : forall L x,
       list_forall P L -> P x -> list_forall P (x::L).

Hint Constructors list_forall.

Lemma list_forall_concat : forall (A : Set) (P : A -> Prop) L1 L2,
  list_forall P L1 ->
  list_forall P L2 ->
  list_forall P (L1 ++ L2).

Results on List.for_n

Definition list_for_n (A : Set) (P : A -> Prop) (n : nat) (L : list A) :=
  n = length L /\ list_forall P L.

Lemma list_for_n_concat : forall (A : Set) (P : A -> Prop) n1 n2 L1 L2,
  list_for_n P n1 L1 ->
  list_for_n P n2 L2 ->
  list_for_n P (n1+n2) (L1 ++ L2).

Hint Extern 1 (?n = length ?xs) =>
 match goal with H: list_for_n _ ?n ?xs |- _ =>
  apply (proj1 H) end.

Hint Extern 1 (length ?xs = ?n) =>
 match goal with H: list_for_n _ ?n ?xs |- _ =>
  apply (sym_eq (proj1 H)) end.