Library hydras.rpo.more_list

by Evelyne Contejean, LRI

Some additional properties for the Coq lists.

Set Implicit Arguments.

From Coq Require Import List Arith.

Relations between length, map, append, In and nth.

Lemma map_map :
  ∀ (A B C : Set) (l : (list A)) (f : B → C) (g : A →B),
  map f (map g l) = map (fun x ⇒ f (g x)) l.

Lemma list_app_length :
∀ A, ∀ l1 l2 : list A, length (l1 ++ l2) = length l1 + length l2.

Lemma length_map :
∀ (A B : Set) (f : A → B) (l : list A), length (map f l) = length l.

Lemma map_app :
∀ (A B : Set) (f : A → B) l1 l2, map f (l1 ++ l2) = (map f l1 ) ++ (map f l2 ).

Lemma in_in_map :
  ∀ (A B : Set) (f : A → B) a l, In a l → In (f a) (map f l).

Lemma in_map_in :
  ∀ (A B : Set) (f : A → B) b l, In b (map f l) →
  ∃ a , In a l ∧ f a = b.

Lemma nth_error_map :
  ∀ (A B : Set) (f : A → B) (l : list A) i,
  match nth_error (map f l) i with
  | Some f_li ⇒
           match nth_error l i with
            | Some li ⇒ f_li = f li
            | None ⇒ False
            end
  | None ⇒
            match nth_error l i with
            | Some li ⇒ False
            | None ⇒ True
            end
end.

A measure on lists based on a measure on elements.

Fixpoint list_size (A : Set) (size : A → nat) (l : list A) {struct l} : nat :=
  match l with
  | nil ⇒ 0
  | h :: tl ⇒ size h + list_size size tl
  end.

Lemma list_size_tl_compat :
  ∀ (A : Set) (size : A → nat) a b l, size a < size b →
    list_size size (a :: l) < list_size size (b :: l).

Lemma list_size_app:
∀ (A : Set) (size : A → nat) l1 l2,
list_size size (l1 ++ l2) = list_size size l1 + list_size size l2.

Lemma list_size_fold :
  ∀ (A : Set) (size : A → nat) l n,
  fold_left (fun (size_acc : nat) (a : A) ⇒ size_acc + size a) l n =
  n + list_size size l.

Lemma list_size_size_eq :
  ∀ (A : Set) (size1 : A → nat) (size2 : A → nat) l,
(∀ a, In a l → size1 a = size2 a ) → list_size size1 l = list_size size2 l.

Induction principles for list.

Induction on the length.

Definition list_rec2 :
  ∀ A, ∀ P : list A → Type,
    (∀ (n:nat) (l : list A), length l ≤ n → P l ) →
    ∀ l : list A, P l.

Definition o_length (A : Set) (l1 l2 : list A) : Prop := length l1 < length l2.

Theorem well_founded_length : ∀ A, well_founded (o_length (A := A)).

Induction on the the size.

Definition list_rec3 (A : Set) (size : A → nat) :
  ∀ P : list A → Type,
    (∀ (n:nat) (l : list A), list_size size l ≤ n → P l ) →
    ∀ l : list A, P l.

How to remove an element in a list, whenever it is present.

Fixpoint split_list (A : Set)
  (eqA : ∀ (a1 a2 : A), {a1 =a2 }+{a1 ≠a2 })
  (l : list A) (t : A) {struct l} : list A × list A :=
  match l with
  | nil ⇒ (nil , nil )
  | a :: l' ⇒
      if eqA t a
      then (nil , l')
      else let (l1,l2) := split_list eqA l' t in (a :: l1 , l2 )
  end.

Lemma split_list_app_cons :
∀ (A : Set) (eqA : ∀ (a1 a2 : A), {a1 =a2 }+{a1 ≠a2 }) t l,
   In t l → let (l1, l2) := split_list eqA l t in l = l1 ++ t :: l2.

Fixpoint remove (A : Set) (eqA : ∀ a1 a2 : A, {a1 =a2 }+{a1 ≠a2 })
  (a : A) (l : list A) {struct l} : (option (list A)) :=
  match l with
  | nil ⇒ None
  | h :: tl ⇒
    if eqA a h
    then Some tl
    else
      match remove eqA a tl with
      | Some rmv ⇒ Some (h :: rmv)
      | None ⇒ None
      end
  end.

Lemma in_remove :
  ∀ (A : Set) (eqA : ∀ a1 a2 : A, {a1 =a2 }+{a1 ≠a2 }) a l,
  match remove eqA a l with
  | None ⇒ ¬In a l
  | Some l' ⇒ In a l ∧ let (l1, l2) := split_list eqA l a in l' = l1 ++ l2
  end.

Fixpoint remove_list (A : Set) (eqA : ∀ (a1 a2 : A), {a1 =a2 }+{a1 ≠a2 })
(la l : list A) {struct l} : option (list A) :=
  match la with
  | nil ⇒ Some l
  | a :: la' ⇒
        match l with
        | nil ⇒ None
        | b :: l' ⇒
           if eqA a b
           then remove_list eqA la' l'
           else
             match remove_list eqA la l' with
             | None ⇒ None
             | Some rmv ⇒ Some (b :: rmv)
             end
        end
  end.

Iterators.

Fixpoint fold_left2 (A B C : Set) (f : A → B → C → A) (a : A) (l1 : list B) (l2 : list C)
  {struct l1} : option A :=
  match l1, l2 with
  | nil, nil ⇒ Some a
  | b :: t1, c :: t2 ⇒ fold_left2 f (f a b c) t1 t2
  | _, _ ⇒ None
  end.

more properties on the nth element.

Lemma nth_error_ok_in :
∀ (A : Set) n (l : list A) (a : A),
nth_error l n = Some a → In a l.

Association lists.

find.

Fixpoint find (A B : Set) (eqA : ∀ (a1 a2 : A), {a1 =a2 }+{a1 ≠a2 })
(a : A) (l : list (A × B)) {struct l} : option (B) :=
match l with
| nil ⇒ None
| (a1,b1) :: l ⇒
     if eqA a a1
     then Some b1
     else find eqA a l
  end.

Lemma find_not_mem :
  ∀ (A B : Set) (eqA : ∀ (a1 a2 : A), {a1 =a2 }+{a1 ≠a2 })
  (a : A) (b : B) (l : list (A × B)) (dom : list A),
  ¬In a dom → (∀ a', In a' dom → find eqA a' ((a ,b ) :: l) = find eqA a' l ).

number of occurences of the first element of a pair.

Fixpoint nb_occ (A B : Set) (eqA : ∀ (a1 a2 : A), {a1 =a2 }+{a1 ≠a2 })
  (a : A) (l : list (A × B)) {struct l} : nat :=
  match l with
  | nil ⇒ 0
  | (a',_) :: tl ⇒
     if (eqA a a') then S (nb_occ eqA a tl) else nb_occ eqA a tl
  end.

Lemma none_nb_occ_O :
  ∀ (A B : Set) (eqA : ∀ (a1 a2 : A), {a1 =a2 }+{a1 ≠a2 })
  (a : A) (l : list (A × B)),
  find eqA a l = None → nb_occ eqA a l = 0.

Lemma some_nb_occ_Sn :
  ∀ (A B : Set) (eqA : ∀ (a1 a2 : A), {a1 =a2 }+{a1 ≠a2 })
  (a : A) (l : list (A × B)) b,
  find eqA a l = Some b → 1 ≤ nb_occ eqA a l.

Lemma nb_occ_app :
  ∀ (A B : Set) (eqA : ∀ (a1 a2 : A), {a1 =a2 }+{a1 ≠a2 })
  a (l1 l2 : list (A × B)),
  nb_occ eqA a (l1 ++l2) = nb_occ eqA a l1 + nb_occ eqA a l2.

Lemma reduce_assoc_list :
  ∀ (A B : Set) (eqA : ∀ (a1 a2 : A), {a1 =a2 }+{a1 ≠a2 }),
  ∀ (l : list (A × B)), ∃ l',
(∀ a, nb_occ eqA a l' ≤ 1) ∧ (∀ a, find eqA a l = find eqA a l').

map_without_repetition applies a function to the elements of a list, but only a single time when there are several consecutive occurences of the same element. Moreover, the function is supposed to return an option as a result, in order to simulate exceptions, and the abnormal results are discarted.

Fixpoint map_without_repetition (A B : Set)
  (eqA : ∀ (a1 a2 : A), {a1 =a2 }+{a1 ≠a2 })
  (f : A → option B) (l : list A) {struct l} : list B :=
    match l with
    | nil ⇒ (nil : list B)
    | h :: nil ⇒
      match f h with
      | None ⇒ nil
      | Some f_h ⇒ f_h :: nil
      end
    | h1 :: ((h2 :: tl) as l1) ⇒
    if (eqA h1 h2)
    then map_without_repetition eqA f l1
    else
      match f h1 with
      | None ⇒ map_without_repetition eqA f l1
      | Some f_h1 ⇒ f_h1 :: (map_without_repetition eqA f l1)
      end
end.

Lemma prop_map_without_repetition :
∀ (A B : Set) (eqA : ∀ (a1 a2 : A), {a1 =a2 }+{a1 ≠a2 })
  (P : B → Prop) f l,
  (∀ a, In a l →
   match f a with
   | None ⇒ True
   | Some f_a ⇒ P f_a
   end) →
   (∀ b, In b (map_without_repetition eqA f l) → P b ).

Lemma exists_map_without_repetition :
  ∀ (A B : Set) (eqA : ∀ (a1 a2 : A), {a1 =a2 }+{a1 ≠a2 })
  (P : B → Prop) f l,
  (∃ a , In a l ∧ match f a with
                        | None ⇒ False
                        | Some f_a ⇒ P f_a
                        end) →
  (∃ b , In b (map_without_repetition eqA f l) ∧ P b ).

map12_without_repetition is similar to map_without_repetition, but the applied function returns two optional results instead of one.

Fixpoint map12_without_repetition (A B : Set)
  (eqA : ∀ (a1 a2 : A), {a1 =a2 }+{a1 ≠a2 })
  (f : A → option B × option B) (l : list A) {struct l} : list B :=
    match l with
    | nil ⇒ (nil : list B)
    | h :: nil ⇒
      match f h with
      | (None , None ) ⇒ nil
      | (Some f_h1, None ) ⇒ f_h1 :: nil
      | (None , Some f_h1) ⇒ f_h1 :: nil
      | (Some f_h1, Some f_h2) ⇒ f_h1 :: f_h2 :: nil
      end
    | h :: ((h' :: tl) as l1) ⇒
    if (eqA h h')
    then map12_without_repetition eqA f l1
    else
      match f h with
      | (None , None ) ⇒ map12_without_repetition eqA f l1
      | (Some f_h1, None ) ⇒ f_h1 :: (map12_without_repetition eqA f l1)
      | (None , Some f_h1) ⇒ f_h1 :: (map12_without_repetition eqA f l1)
      | (Some f_h1, Some f_h2) ⇒ f_h2 :: f_h1 :: (map12_without_repetition eqA f l1)
      end
end.

Lemma prop_map12_without_repetition :
  ∀ (A B : Set) (eqA : ∀ (a1 a2 : A), {a1 =a2 }+{a1 ≠a2 })
  (P : B → Prop) f l,
  (∀ a, In a l →
   match f a with
   | (None , None ) ⇒ True
   | (Some f1_a, None ) ⇒ P f1_a
   | (None , Some f2_a) ⇒ P f2_a
   | (Some f1_a, Some f2_a) ⇒ P f1_a ∧ P f2_a
   end) →
(∀ b, In b (map12_without_repetition eqA f l) → P b ).

Lemma exists_map12_without_repetition :
  ∀ (A B : Set) (eqA : ∀ (a1 a2 : A), {a1 =a2 }+{a1 ≠a2 })
  (P : B → Prop) f l,
  ((∃ a , In a l ∧ match f a with
                        | (None , None ) ⇒ False
                        | (None , Some f2_a) ⇒ P f2_a
                        | (Some f1_a, None ) ⇒ P f1_a
                        | (Some f1_a, Some f2_a) ⇒ P f1_a ∨ P f2_a
                        end) →
  (∃ b , In b (map12_without_repetition eqA f l) ∧ P b )).