Coq Library
PADEC - Coq Library

Library Padec.Tools.ListUtils

A Framework for Certified Self-Stabilization
PADEC Coq Library

Global imports

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import RelationClasses.
From Coq Require Import Omega.
From CoLoR Require Import ListUtil.
Existing Instance relation_equivalence_equivalence.

Local imports

From Padec Require Import SetoidUtil.
From Padec Require Import OptionUtil.

Open Scope signature_scope.
Set Implicit Arguments.

Setoid and Partial Setoid of Lists

Two equalities exist on lists: Both equalities preserve the property of their base-equality (i.e. equivalence or PER).
We chose to define eqlistA as the base equality on list and to instantiate a setoid/partial setoid on it. Namely, in further developments, equiv or pequiv on list refers to the point-wise equality. equivlistA has to be called explicitely.
Instance eqlistA_per {A} {eqA} {eqA_per: @PER A eqA}:
  PER (eqlistA eqA).

Instance List_Setoid {A} `{Setoid A}: Setoid (list A) :=
  {| equiv := eqlistA equiv |}.

Instance List_Partial_Setoid {A} `{PartialSetoid A}: PartialSetoid (list A) :=
  {| pequiv := eqlistA pequiv |}.

Instance eqlistA_eq_is_eq (A: Type):
  subrelation (eqlistA (@eq A)) (@eq (list A)).


Section INA.

InA_compat provides compatibility of InA wrt equivlistA, InA_compat_eqlistA, below, provides compatibility wrt eqlistA
  Global Instance InA_compat_eqlistA {A} `{Setoid A}:
    Proper (equiv ==> eqlistA equiv ==> iff) (InA equiv).

  Lemma InA_app_app A (eqA:relation A): forall x l,
      Proper (eqlistA eqA) l -> InA eqA x l ->
      exists a b, eqlistA eqA (a ++ (x :: nil) ++ b) l.

  Lemma InA_app (A:Type) {SA:Setoid A}: forall (x:A) a b,
      InA equiv x (a ++ b) <-> ((InA equiv x a) \/ (InA equiv x b)).

  Lemma list_app_preserve {A} `{Setoid A}:
    forall (x: A) a1 b1 a2 b2,
      ~ InA equiv x a1 -> ~ InA equiv x b1 ->
      a1 ++ x :: b1 == a2 ++ x :: b2 -> a1 == a2 /\ b1 == b2.

End INA.


Section NoDupA.

  Lemma NoDupA_nil_iff: forall (A: Type) (eqA: A -> A -> Prop),
    NoDupA eqA nil <-> True.

  Lemma NoDupA_cons_iff: forall (A: Type) (eqA: A -> A -> Prop) x q,
      NoDupA eqA (x::q) <-> ~InA eqA x q /\ NoDupA eqA q.

  Global Instance NoDupA_compat {A} `{Setoid A}:
    Proper (eqlistA equiv ==> iff) (NoDupA equiv).

  Lemma NoDupA_app_alt {A} `{Setoid A}:
    forall l1 l2: list A, NoDupA equiv (l1++l2) ->
                          NoDupA equiv l1 /\ NoDupA equiv l2.

End NoDupA.

Tools about ForallA

Section ForallA.

  Context {A: Type} (eqA: relation A).
  Context {eqA_refl: Reflexive eqA}.

  Section FF.

    Context (P: A -> Prop) {P_compat: Proper (eqA ==> iff) P}.

    Lemma Forall_forallA:
      forall (l : list A),
        Forall P l <-> (forall (x : A), InA eqA x l -> P x).

    Definition Forall_hd := Forall_inv.

    Lemma Forall_tl:
      forall a l, Forall P (a :: l) -> Forall P l.

  End FF.

  Global Instance Forall_compat :
    Proper ((eqA ==> iff) ==> (eqlistA eqA) ==> iff) (@Forall A).

  Global Instance Forall_compat_equiv :
    Proper ((eqA ==> iff) ==> (equivlistA eqA) ==> iff) (@Forall A).

  Lemma forall_inv_2:
    forall (P: A -> Prop) (a: A) (l: list A),
      Forall P (a :: l) -> Forall P l.

  Lemma Forall_head_and_tail:
    forall (h: A) t p, Forall p (h :: t) <-> p h /\ Forall p t.

  Lemma forall_app:
    forall (p: A -> Prop) l1 l2,
      Forall p (l1 ++ l2) <-> (Forall p l1) /\ (Forall p l2).

End ForallA.

Tools about map compatibility

Section map_compat.

  Context {A: Type} (eqA: relation A).
  Context {B: Type} (eqB: relation B).

  Global Instance map_compat:
    Proper ((eqA ==> eqB) ==> eqlistA eqA ==> eqlistA eqB)
           ( A B).

  Lemma map_eq_locality :
    forall (eqA_refl: Reflexive eqA)
           (eqB_PER: PER eqB)
           (f1: A -> B) (p1: Proper (eqA ==> eqB) f1)
           (f2: A -> B) (p2: Proper (eqA ==> eqB) f2)
           (l1 l2: list A) (el: eqlistA eqA l1 l2),
      (forall a, InA eqA a l1 -> eqB (f1 a) (f2 a)) ->
      eqlistA eqB (map f1 l1) (map f2 l2).

End map_compat.

Section map_compat_equivlist.

  Context {A: Type} `{SA:Setoid A}.
  Context {B: Type} `{SB:Setoid B}.

  Global Instance map_compat_equiv :
    Proper (fequiv ==> equivlistA equiv ==> equivlistA equiv)
           ( A B).

  Lemma InA_map_iff:
    forall (f: A -> B) {f_compat: Proper fequiv f}
           (l: list A) (b: B),
      InA equiv b (map f l) <->
      (exists a : A, (f a) == b /\ InA equiv a l).

End map_compat_equivlist.

Tools about filter

Section filter.

  Context {A: Type} `{SA:Setoid A}.

  Global Instance filter_compat :
    Proper (fequiv ==> eqlistA equiv ==> eqlistA equiv)
           (filter (A:=A)).

  Global Instance filter_compat_equiv :
    Proper (fequiv ==> equivlistA equiv ==> equivlistA equiv)
           (filter (A:=A)).

  Lemma filter_nil:
    forall (f: A -> bool) (l: list A), filter f l = nil
                                       <-> existsb f l = false.

  Lemma filter_eq_locality:
    forall (f1 f2: A -> bool) (l1 l2: list A),
      equivlistA equiv l1 l2 ->
      Proper fequiv f1 -> Proper fequiv f2 ->
      (forall a, InA equiv a l1 -> f1 a = f2 a) ->
      equivlistA equiv (filter f1 l1) (filter f2 l2).

  Lemma filter_InA_locality:
    forall (f: A -> bool),
    forall (l: list A),
      (forall x y, x == y -> InA equiv x l -> f x = f y) ->
      forall x,
        InA equiv x (filter f l) <-> InA equiv x l /\ f x = true.

  Lemma filter_NoDupA:
    forall (f: A -> bool) (f_c: Proper pequiv f)
           (l: list A),
      NoDupA equiv l -> NoDupA equiv (filter f l).

  Lemma filter_app_preserve:
    forall (f: A -> bool) (pf: Proper pequiv f),
    forall l l1 x l2 (hl: l == l1 ++ x :: l2)
           (inx1: ~ InA equiv x l1) (inx2: ~ InA equiv x l2) lf1 lf2,
      filter f l == lf1 ++ x :: lf2 ->
      filter f l1 == lf1 /\ filter f l2 == lf2.

End filter.

Tools about map_filter

map_filter transforms a list into another, by applying to each element of the first list a Some/None function (the resulting element is added to the new list if it is not None).

Tools about RestrictA

RestrictA is a subrelation of equality, conditionned using a compatible predicate.

  Definition RestrictA A (eqA:relation A) (P: A -> Prop) a1 a2 :=
    eqA a1 a2 /\ P a1.

  Instance RestrictA_per {A: Type} `{SA:PartialSetoid A}
           {P: A -> Prop} {P_proper: Proper fequiv P}: PER (RestrictA pequiv P).

  Instance RestrictA_per_s {A: Type} `{SA:Setoid A}
           {P: A -> Prop} {P_proper: Proper fequiv P}: PER (RestrictA equiv P).


Tools about ConsistentA

A list of pairs is consistent whenever for any two pairs in the list, if their first parts are equal, their second parts are also equal.
Section ConsistentA.

  Context {A: Type} `{SA:Setoid A}.
  Context {B: Type} `{SB:Setoid B}.

  Definition ConsistentA (l: list (A*B)) :=
    forall a1 a2 b1 b2, InA equiv (a1,b1) l ->
                        InA equiv (a2,b2) l ->
                        a1 == a2 -> b1 == b2.

  Global Instance ConsistentA_compat:
    Proper (equivlistA equiv ==> iff) ConsistentA .

End ConsistentA.

Tools about assocA

assocA searches into a list of pairs a first part and returns its second part (None if not found).
Section AssocA.

  Context {A: Type} `{SA: Setoid A}.
  Context `{Adec: Decider equiv}.

  Context {B: Type} `{SB: Setoid B}.

  Fixpoint assocA (x: A) (l: list (A * B)): option B :=
    match l with
    | nil => None
    | (y, v)::q => if Adec x y then Some v else
                     assocA x q end.

  Global Instance assocA_compat:
    Proper fequiv assocA.

  Lemma assocA_none:
    forall (l: list(A * B)) (a: A),
      (assocA a l) == None <->
      forall (b: B), ~ InA equiv (a, b) l.

  Lemma assocA_InA:
    forall (l: list(A*B)) (a: A) (b: B),
      (assocA a l) == (Some b) ->
      InA equiv (a, b) l.

  Lemma InA_AssocA:
    forall (l: list(A*B)) (a: A) (b: B),
      ConsistentA l ->
      (InA equiv (a, b) l <->
       (assocA a l) == (Some b)).

  Global Instance assocA_compat2:
    Proper (equiv ==> RestrictA (equivlistA equiv) ConsistentA ==> equiv)

  Lemma assoc_dec:
    forall (eqB_dec: Decider (equiv (A := B))) (a: A) l,
      {b: B | InA equiv (a, b) l}
      {forall b, ~ (InA equiv (a, b) l)}.

End AssocA.

Tools about rev on a list

Section Rev_List.

  Lemma rev_equivlistA {A} `{SA:Setoid A}:
    forall l: list A, equivlistA equiv l (rev l).

  Lemma rev_rev_eqlistA {A} `{SA:Setoid A}:
    forall (l l': list A),
      eqlistA equiv l (rev l') <-> eqlistA equiv (rev l) l'.

  Lemma rev_app_cons {A} `{SA:Setoid A}:
    forall (x: A) (l1 l2: list A),
      rev (l1 ++ x :: l2) == rev l2 ++ x :: rev l1.

End Rev_List.

Existsb Forallb

Section Existsb_Forallb.

  Variable (A: Type).
  Variable (f: A -> bool)
           (notf: A -> bool)
           (H: forall a, f a = negb (notf a)).

  Lemma existsb_forallb:
    forall l, existsb f l = negb (forallb notf l).

  Lemma forallb_existsb:
    forall l, forallb f l = negb (existsb notf l).

End Existsb_Forallb.

Section Existsb_InA.

  Lemma existsb_exists_InA {A: Type} `{SA: Setoid A}:
    forall (f : A -> bool) (f_compat: Proper fequiv f)
           (l : list A),
      existsb f l = true <-> (exists x : A, InA equiv x l /\ f x = true).

End Existsb_InA.

Section Forallb_InA.

  Lemma forallb_forall_InA {A: Type} `{SA: Setoid A}:
    forall (f : A -> bool) (f_compat: Proper fequiv f)
           (l : list A),
      forallb f l = true <-> (forall x : A, InA equiv x l -> f x = true).

End Forallb_InA.

Section Existsb_Forallb_compat.

  Global Instance existsb_compat:
    forall A (eqA: relation A),
      Proper ( (eqA ==> eq) ==> (eqlistA eqA) ==> eq) (existsb (A:=A)).

  Global Instance forallb_compat:
    forall A (eqA: relation A),
      Proper ( (eqA ==> eq) ==> (eqlistA eqA) ==> eq) (forallb (A:=A)).

End Existsb_Forallb_compat.

Section Other_forallb.

  Lemma forallb_compat1:
    forall (A: Type) (eqA: A -> A -> Prop) (refl: Reflexive eqA)
           (f1 f2: A -> bool) (EF: (eqA ==> eq) f1 f2)
           (l : list A),
      forallb f1 l = forallb f2 l.

  Global Instance forallb_compat_equiv:
    forall (A : Type) (SA : Setoid A),
      Proper ((equiv ==> eq) ==> equivlistA equiv ==> eq) (forallb (A:=A)).

End Other_forallb.

Decidability on lists

Section Decidability_on_Lists.

  Lemma eqlistA_dec:
    forall {A: Type} {eqA: relation A},
      Decider eqA -> Decider (eqlistA eqA).

  Lemma equivlistA_dec:
    forall {A: Type} {SA: Setoid A},
      Decider (equiv (A := A)) -> Decider (equivlistA equiv).

End Decidability_on_Lists.

Section Rev.

  Variable (A: Type).

  Lemma rev_intro:
    forall l l': list A, l = l' <-> rev l = rev l'.

  Definition list_rev_destruct:
    forall eqA (eqA_refl: Reflexive eqA) (l:list A),
      {first:list A & {last:A | eqlistA eqA l (first++ last::nil) }}
      + {eqlistA eqA l nil}.

  Global Instance removelast_eqlistA_compat :
    forall eqA, Proper (eqlistA eqA ==> eqlistA eqA) (@removelast A).

End Rev.

Section map_filter.

  Context {A: Type} `{SA: Setoid A}.
  Context {B: Type} `{SB: Setoid B}.

  Section Fixed_fopt.

    Context (fopt: A -> option B).

    Context {fopt_compat: Proper fequiv fopt}.

    Fixpoint map_filter (l: list A) :=
      match l with
        nil => nil
      | a :: q =>
        match fopt a with
          None => map_filter q
        | Some b => b::map_filter q
        end end.

    Lemma InA_map_filter_iff:
      forall (l: list A) (b: B),
        InA equiv b (map_filter l) <->
        (exists a: A, InA equiv a l /\ (fopt a) == (Some b)).

  End Fixed_fopt.

  Global Instance map_filter_compat:
    Proper (fequiv ==> equivlistA equiv ==> equivlistA equiv) map_filter.

  Lemma map_filter_eq_locality:
    forall (f1 f2: A -> option B) (l1 l2: list A),
      equivlistA equiv l1 l2 ->
      Proper fequiv f1 -> Proper fequiv f2 ->
      (forall a, InA equiv a l1 -> f1 a == f2 a) ->
      equivlistA equiv (map_filter f1 l1) (map_filter f2 l2).

  Lemma map_filter_eq_locality_converse:
    Decider (equiv (A := B)) ->
    forall (f1 f2: A -> option B) (l1 l2: list A),
      equivlistA equiv l1 l2 ->
      Proper fequiv f1 -> Proper fequiv f2 ->
      ~ equivlistA equiv (map_filter f1 l1) (map_filter f2 l2) ->
      exists a, InA equiv a l1 /\ ~ f1 a == f2 a.

End map_filter.

Global Instance map_filter_compat_eqlistA:
  forall A B (eqA: relation A) (eqB: relation B),
    Proper ((eqA ==> eqoptionA eqB)
              ==> eqlistA eqA ==> eqlistA eqB) map_filter.

Tools about eqlistA

Section EqlistA_Utils.

  Variable (A : Type) (eqA : relation A).

  Lemma l_eqlistA_nil : forall l, eqlistA eqA l nil <-> l = nil.

  Lemma l_eqlistA_cons : forall l1 h2 t2, eqlistA eqA l1 (h2 :: t2) ->
                                          exists h1 t1, l1 = h1 :: t1.

  Lemma cons_eqlistA_cons :
    forall h1 t1 h2 t2, eqlistA eqA (h1 :: t1) (h2 :: t2) <->
                        eqA h1 h2 /\ eqlistA eqA t1 t2.

End EqlistA_Utils.

Instance nth_compat (A:Type) (SA:PartialSetoid A) : Proper fequiv (nth (A:=A)).

Ltac lsplit pl :=
  hnf in pl;
  match (type of pl) with
  | (eqlistA ?R (cons ?a1 ?l1) (cons ?a2 ?l2)) =>
    let X := fresh "X" in
    assert (X:=proj1 (cons_eqlistA_cons R a1 l1 a2 l2) pl);
    clear pl;rename X into pl
  | (eqlistA ?R nil nil) => clear pl
  | (eqlistA ?R nil (cons _ _)) =>
    inversion pl
  | (eqlistA ?R (cons _ _) nil) =>
    inversion pl

Stutter : copy list with stuttering at element n

Section Stutter.

  Fixpoint stutter A n (l:list A):=
    match l with
      nil => nil
    | i :: q =>
      match n with
        0 => i :: removelast (i::q)
      | S n => i :: stutter n q end end.

  Lemma removelast_length: forall A (l:list A), length (removelast l) = (length l) - 1.

  Lemma stutter_length: forall A n l, length (stutter (A:=A) n l) = length l.

  Lemma removelast_Forall: forall A P (l:list A), Forall P l ->
                                                  Forall P (removelast l).

  Lemma stutter_Forall: forall A P n l,
      Forall P l -> Forall P (stutter (A:=A) n l).

  Lemma stutter_nth_le: forall A a (l:list A) i j,
      i <= j ->
      nth i l a = nth i (stutter j l) a.

  Lemma stutter_nth_gt: forall A a (l:list A) i j,
      j <= i - 1 -> i < length l ->
      nth (i - 1) l a = nth i (stutter j l) a.

  Lemma stutter_nth_gt2: forall A a (l:list A) i j,
      j <= i -> i < length l - 1 ->
      nth i l a = nth (1+i) (stutter j l) a.

  Lemma stutter_last_id:
    forall A (l:list A) j, j = length l - 1 ->
                           stutter j l = l.

  Lemma stutter_app_r:
    forall A (l1 l2:list A) j, j >= length l1 ->
                           stutter j (l1++l2) = l1 ++ stutter (j - length l1) l2.

End Stutter.

Tools for building lists of natural numbers (goins up, down, with repeated patterns)

Section List_builders.

  Fixpoint uc min len :=
    match len with 0 => nil | S n => min :: uc (min+1) n end.

  Lemma uc_length: forall min len, length (uc min len) = len.

  Fixpoint dc min len :=
    match len with 0 => nil | S n => min+n :: dc min n end.

  Lemma dc_length: forall min len, length (dc min len) = len.

  Fixpoint rep cte len : list nat :=
    match len with 0 => nil | S n => cte :: rep cte n end.

  Lemma rep_length: forall cte len, length (rep cte len) = len.

  Fixpoint repl A (lcte:list A) len : list A :=
    match len with 0 => nil | S n => lcte ++ repl lcte n end.

  Lemma repl_length: forall A lcte len, length (repl (A:=A) lcte len) = len * length lcte.

  Fixpoint flatmap A B (f:A -> list B) l : list B :=
    match l with nil => nil | x::q => f x ++ flatmap f q end.

  Lemma flatmap_length:
    forall A B f l, length (flatmap (A:=A) (B:=B) f l) =
                    fold_right plus 0 ( (fun a => length (f a)) l).

  Lemma dc_le: forall min len, Forall (le min) (dc min len).

  Lemma dc_gt: forall min len, Forall (gt (min+len)) (dc min len).

  Lemma dc_nth: forall min len x i, i < len -> nth i (dc min len) x = min + len - i - 1.

  Lemma dc_last: forall min len x, len > 0 -> last (dc min len) x = min.

  Lemma dc_removelast: forall min len,
      len > 0 ->
      removelast (dc min len) = dc (min+1) (len-1).

  Lemma uc_le: forall min len, Forall (le min) (uc min len).

  Lemma uc_gt: forall min len, Forall (gt (min+len)) (uc min len).

  Lemma rep_app: forall x n p, rep x (n+p)=rep x n ++ rep x p.

  Lemma last_cons: forall A x d (l:list A), l <> nil -> last (x::l) d = last l d.

  Lemma last_app: forall A d (l1 l2:list A), l2 <> nil -> last (l1++l2) d=last l2 d.

End List_builders.

Section App.

  Context {A: Type} `{SA: PartialSetoid A}.

  Lemma app_proper_l:
    forall (a b: list A), Proper pequiv (a ++ b) -> Proper pequiv a.

  Lemma app_proper_r:
    forall (a b: list A), Proper pequiv (a ++ b) -> Proper pequiv b.

    Lemma app_cut:
    forall (l1 l2 m1 m2: list A),
      l1 ++ l2 =~= m1 ++ m2 ->
      (exists x, l1 =~= m1 ++ x /\ m2 =~= x ++ l2) \/
      (exists y, m1 =~= l1 ++ y /\ l2 =~= y ++ m2).

End App.

Close Scope signature_scope.
Unset Implicit Arguments.