Qcert.Basic.Util.RList

Section RList.



  Section misc.
    Context {A:Type}.

    Definition singleton {A} (x:A) : list A := x::nil.

    Lemma is_nil_dec (l:list A) : {l = nil} + {l ≠ nil}.

    Fixpoint lflatten (l:list (list A)) : list A :=
      match l with
      | nil ⇒ nil
      | l1 :: l' ⇒
        l1 ++ (lflatten l')
      end.

    Lemma flat_map_app {B} (f:A→list B) l1 l2 :
      flat_map f (l1 ++ l2) = flat_map f l1 ++ flat_map f l2.

    Lemma map_nil f l :
      map f l = (@nil A) ↔ l = (@nil A).

    Lemma eq_means_same_length :
      ∀ (l1 l2:list A),
        l1 = l2 → (length l1) = (length l2).

    Lemma app_cons_middle (l1 l2:list A) (a:A) :
      l1 ++ (a::l2) = (l1 ++ (a::nil))++l2.

  End misc.

  Lemma map_app_break {A B:Type} (f:A→B) {a b c} :
    map f a = b ++ c →
    {b':list A & {c' : list A | a = b' ++ c' ∧ b = map f b' ∧ c = map f c'}}.

  Lemma map_inj_strong {A B} (f g:A→B) (l1 l2:list A)
        (inj:∀ (x y:A), In (f x) (map f l1) → In (g y) (map g l2) → f x = g y → x = y) :
    map f l1 = map g l2 →
    l1 = l2.

  Lemma map_inj {A B} (f g:A→B) (l1 l2:list A)
        (inj:∀ (x y:A), f x = g y → x = y) :
    map f l1 = map g l2 →
    l1 = l2.

  Section folds.
    Context {A B C: Type}.

    Lemma fold_left_map
          (f:A → C → A) (g:B→C) (l:list B) (init:A) :
      fold_left f (map g l) init = fold_left (fun a b ⇒ f a (g b)) l init.

    Lemma fold_left_ext
          (f g:A → B → A) (l:list B) (init:A) :
      (∀ x y, f x y = g x y) →
      fold_left f l init = fold_left g l init.

    Lemma fold_right_app_map_singleton l :
    fold_right (fun a b : list A ⇒ a ++ b) nil
              (map (fun x : A ⇒ (x::nil)) l) = l.

  Lemma fold_right_perm (f : A → A → A)
        (assoc:∀ x y z : A, f x (f y z) = f (f x y) z)
        (comm:∀ x y : A, f x y = f y x) (l1 l2:list A) (unit:A)
        (perm:Permutation l1 l2) :
    fold_right f unit l1 = fold_right f unit l2.

  End folds.

  Section filter.
    Context {A:Type}.

    Lemma filter_length :
      ∀ (p:A → bool), ∀ (l:list A),
          length l ≥ length (filter p l).

    Lemma filter_smaller :
      ∀ (p:A → bool), ∀ (l:list A), ∀ (x:A),
            filter p l ≠ x::l.

    Lemma filter_filter :
      ∀ (p:A → bool), ∀ (s:list A),
          filter p (filter p s) = filter p s.

    Lemma filter_not_filter:
      ∀ (p:A → bool), ∀ (s:list A),
            filter p (filter (fun x ⇒ negb (p x)) s) = nil.

    Lemma filter_id_implies_pred :
      ∀ (p:A → bool), ∀ (l:list A),
          filter p l = l → ∀ (y:A), (In y l → (p y = true)).

    Lemma filter_nil_implies_not_pred :
      ∀ (p:A → bool), ∀ (l:list A),
          filter p l = nil → ∀ (y:A), (In y l → (p y = false)).

    Lemma filter_comm:
      ∀ (x:list A) (p1 p2: A → bool),
        (filter p1 (filter p2 x)) = (filter p2 (filter p1 x)).

    Lemma filter_and:
      ∀ (x:list A) (p1 p2: A → bool),
        (filter p1 (filter p2 x)) = (filter (fun a ⇒ andb (p1 a) (p2 a)) x).

    Lemma filter_eq:
      ∀ (p1 p2:A → bool),
        (∀ x:A, p1 x = p2 x) → (∀ l:list A, filter p1 l = filter p2 l).

    Lemma false_filter_nil {f} {l:list A} :
      (∀ x, In x l → f x = false) → filter f l = nil.

    Lemma filter_app (f:A→bool) l1 l2 :
      filter f (l1 ++ l2) = filter f l1 ++ filter f l2.

    Lemma Forall_filter {P} {l:list A} f :
      Forall P l → Forall P (filter f l).

    Lemma find_filter f (l:list A) : find f l = hd_error (filter f l).

    Lemma filter_ext (f g : A → bool) (l : list A) :
      (∀ x, In x l → f x = g x) →
      filter f l = filter g l.

    Lemma true_filter (f : A → bool) (l : list A) :
      (∀ x : A, In x l → f x = true) → filter f l = l.

  End filter.


        Lemma forall_in_dec {A:Type} P (l:list A)
          (dec:∀ x, In x l → {P x} + {¬ P x}):
      {∀ x, In x l → P x} + {¬ ∀ x, In x l → P x}.

    Lemma exists_in_dec {A:Type} P (l:list A)
          (dec:∀ x, In x l → {P x} + {¬ P x}):
      {∃ x, In x l ∧ P x} + {¬ ∃ x, In x l ∧ P x}.

    Lemma exists_nforall_in_dec {A:Type} P (l:list A)
          (dec:∀ x, In x l → {P x} + {¬ P x}):
      {∃ x, In x l ∧ P x} + {∀ x, In x l → ¬P x}.

      Lemma existsb_ex {A : Type} (f : A → bool) (l : list A) :
       existsb f l = true → {x : A | In x l ∧ f x = true}.

  Section perm_equiv.
    Context {A:Type}.
    Context {eqdec:EqDec A eq}.

    Definition ldeqA := (@Permutation A).

    Definition rbag := list A.

    Global Instance perm_equiv : Equivalence (@Permutation A).
  End perm_equiv.

  Section list2.
    Context {A B:Type}.

    Section fb2.
      Context (f:A→B→bool).
      Fixpoint forallb2 (l1:list A) (l2:list B): bool :=
        match l1,l2 with
          | nil, nil ⇒ true
          | a1::l1, a2::l2 ⇒ f a1 a2 && forallb2 l1 l2
          | _, _ ⇒ false
        end.

      Lemma forallb2_forallb : ∀ (l1:list A) (l2:list B),
                                 (length l1 = length l2) →
                                 forallb (fun xy ⇒ f (fst xy) (snd xy)) (combine l1 l2) = forallb2 l1 l2.

      Lemma forallb2_forallb_true : ∀ (l1:list A) (l2:list B),
                                      (length l1 = length l2 ∧ forallb (fun xy ⇒ f (fst xy) (snd xy)) (combine l1 l2) = true)
                                      ↔
                                      forallb2 l1 l2 = true.

      Lemma forallb2_Forallb : ∀ l1 l2, forallb2 l1 l2 = true ↔ Forall2 (fun x y ⇒ f x y = true) l1 l2.

    End fb2.

    Lemma Forall2_incl : ∀ (f1 f2:A→B→Prop) l1 l2,
                           (∀ x y, In x l1 → In y l2 → f1 x y→ f2 x y) →
                           Forall2 f1 l1 l2 → Forall2 f2 l1 l2.

    Lemma forallb2_eq : ∀ (f1 f2:A→B→bool) l1 l2,
                          (∀ x y, In x l1 → In y l2 → f1 x y = f2 x y) →
                          forallb2 f1 l1 l2 = forallb2 f2 l1 l2.

  End list2.

  Section forall2.

    Lemma forallb2_sym {A B} : ∀ (f:A→B→bool) {l1 l2},
      forallb2 f l1 l2 = forallb2 (fun x y ⇒ f y x) l2 l1.

    Lemma Forall2_map {A B C D} (f:C→D→Prop) (g:A→C) (h:B→D) a b:
      Forall2 (fun x y ⇒ f (g x) (h y)) a b ↔ Forall2 f (map g a) (map h b).

    Lemma Forall2_map_f {A B C D} (f:C→D→Prop) (g:A→C) (h:B→D) a b:
      Forall2 (fun x y ⇒ f (g x) (h y)) a b → Forall2 f (map g a) (map h b).

    Lemma Forall2_map_b {A B C D} (f:C→D→Prop) (g:A→C) (h:B→D) a b:
      Forall2 f (map g a) (map h b) → Forall2 (fun x y ⇒ f (g x) (h y)) a b.

    Lemma Forall2_length {A B} (f:A→B→Prop) a b:
      Forall2 f a b → length a = length b.

    Global Instance Forall2_refl {A} R `{Reflexive A R} : Reflexive (Forall2 R).

    Global Instance Forall2_sym {A} R `{Symmetric A R} : Symmetric (Forall2 R).

    Global Instance Forall2_trans {A} R `{Transitive A R} : Transitive (Forall2 R).

  Global Instance Forall2_pre {A} R `{PreOrder A R} : PreOrder (Forall2 R).

  Global Instance Forall2_part_eq {A} R `{PartialOrder A eq R } :
    PartialOrder eq (Forall2 R).

  Lemma Forall2_trans_relations_weak {A B C}
        (R1:A→B→Prop) (R2:B→C→Prop) (R3:A→C→Prop):
    (∀ a b c, R1 a b → R2 b c → R3 a c) →
    ∀ a b c, Forall2 R1 a b → Forall2 R2 b c → Forall2 R3 a c.

    Lemma Forall2_eq {A} (l1 l2:list A): Forall2 eq l1 l2 ↔ l1 = l2.

    Lemma Forall2_flip {A B} {P:A→B→Prop} {l1 l2} :
      Forall2 P l1 l2 → Forall2 (fun x y ⇒ P y x) l2 l1.

    Lemma Forall2_In_l {A B} {P:A→B→Prop} {l1 l2 a} :
      Forall2 P l1 l2 →
      In a l1 →
      ∃ b,
        In b l2 ∧
        P a b.

    Lemma Forall2_In_r {A B} {P:A→B→Prop} {l1 l2 b} :
      Forall2 P l1 l2 →
      In b l2 →
      ∃ a,
        In a l1 ∧
        P a b.

  Lemma Forall2_app_tail_inv {A B} P l1 l2 a1 a2 :
     @Forall2 A B P (l1 ++ (a1::nil)) (l2 ++ (a2::nil)) →
     Forall2 P l1 l2 ∧ P a1 a2.

  Lemma filter_Forall2_same {A B} P f g (l1:list A) (l2:list B) :
    Forall2 P l1 l2 →
    map f l1 = map g l2 →
    Forall2 P (filter f l1) (filter g l2).

  Lemma Forall2_map_Forall {A B:Type} (P:A→B→Prop) (f:A→B) l :
    Forall2 P l (map f l) ↔ Forall (fun x ⇒ P x (f x)) l.

  End forall2.

  Section forallb_ordpairs.

    Fixpoint forallb_ordpairs {A} f (l:list A)
      := match l with
         | nil ⇒ true
         | x::ls ⇒ forallb (f x) ls && forallb_ordpairs f ls
         end.

    Lemma forallb_ordpairs_ForallOrdPairs {A} f (l:list A) :
      forallb_ordpairs f l = true ↔ (ForallOrdPairs (fun x y ⇒ f x y = true) l).

    Lemma forallb_ordpairs_ext {A} f1 f2 (l:list A) :
      (∀ x y, In x l → In y l → f1 x y = f2 x y) →
      forallb_ordpairs f1 l = forallb_ordpairs f2 l.

    Fixpoint forallb_ordpairs_refl {A} (f:A→A→bool) (l:list A)
      := match l with
         | nil ⇒ true
         | x::ls ⇒ forallb (f x) (x::ls) && forallb_ordpairs_refl f ls
         end.

    Lemma forallb_ordpairs_refl_conj A f (l:list A) :
      forallb_ordpairs_refl f l = forallb_ordpairs f l && forallb (fun x ⇒ f x x) l.

        Lemma forallb_ordpairs_app_cons {A} f (l:list A) x :
    forallb_ordpairs f l = true →
    forallb (fun y ⇒ f y x) l = true →
    forallb_ordpairs f (l ++ x::nil) = true.

  Lemma forallb_ordpairs_refl_app_cons {A} f (l:list A) x :
    forallb_ordpairs_refl f l = true →
    f x x = true →
    forallb (fun y ⇒ f y x) l = true →
    forallb_ordpairs_refl f (l ++ x::nil) = true.

  End forallb_ordpairs.

  Lemma app_cons_cons_expand {A} (l:list A) a b :
    l ++ a::b::nil = (l ++ a ::nil)++b::nil.

  Section remove.
    Context {A:Type}.
    Context {eqdec:EqDec A eq}.

    Lemma remove_in_neq
          (l : list A) (x y : A) : x ≠ y →
                                   (In x l ↔ In x (remove eqdec y l)).

    Lemma list_in_remove_impl_diff x y l:
      In x (remove eqdec y l) → x ≠ y.

    Lemma list_remove_append_distrib:
      ∀ (v:A) (l1 l2:list A),
        remove eqdec v l1 ++ remove eqdec v l2 = remove eqdec v (l1 ++ l2).

    Lemma list_remove_idempotent:
      ∀ v l,
        remove eqdec v (remove eqdec v l) = remove eqdec v l.

    Lemma list_remove_commute:
      ∀ v1 v2 l,
        remove eqdec v1 (remove eqdec v2 l) = remove eqdec v2 (remove eqdec v1 l).

    Remark list_remove_in v1 v2 l1 l2:
      (In v1 l1 → In v1 l2) →
      In v1 (remove eqdec v2 l1) → In v1 (remove eqdec v2 l2).

    Lemma remove_inv v n l:
      In v (remove eqdec n l) → In v l ∧ v ≠ n.

    Lemma not_in_remove_impl_not_in:
      ∀ x v l,
        x ≠ v →
        ¬ In x (remove eqdec v l) →
        ¬ In x l.

    Fixpoint remove_all (x : A) (l : list A) : list A :=
      match l with
      | nil ⇒ nil
      | y::tl ⇒ if (x == y) then (remove_all x tl) else y::(remove_all x tl)
      end.

    Global Instance remove_all_proper : Proper (eq ==> ldeqA ==> ldeqA) remove_all.

    Lemma remove_all_filter x l:
      remove_all x l = filter (nequiv_decb x) l.

    Lemma remove_all_app (v:A) l1 l2
      : remove_all v (l1 ++ l2) = remove_all v l1 ++ remove_all v l2.

    Lemma fold_left_remove_all_In {l init a} :
      In a (fold_left (fun (a : list A) (b : A) ⇒
                       filter (nequiv_decb b) a) l init)
      → In a init ∧ ¬ In a l.

  End remove.

  Lemma nin_remove {A} dec (l:list A) a :
    ¬ In a l → remove dec a l = l.

  Section repall.
    Context {A:Type}.
    Context `{eqdec:EqDec A eq}.

    Definition replace_all l v n
      := map (fun x ⇒ if eqdec x v then n else x) l.

    Lemma replace_all_nin l v n :
      ¬ In v l →
      map (fun x ⇒ if eqdec x v then n else x) l = l.

    Lemma replace_all_remove_neq l v0 v n:
      v ≠ v0 → n ≠ v0 →
      remove eqdec v0
             (map (fun x ⇒ if eqdec x v then n else x)
                  l) =
      (map (fun x ⇒ if eqdec x v then n else x)
           (remove eqdec v0 l)).

    Lemma remove_replace_all_nin l v v' :
      ¬ In v' l →
      remove eqdec v' (replace_all l v v') =
      remove eqdec v l.

    Definition flat_replace_all l (v:A) n
      := flat_map (fun x ⇒ if eqdec x v then n else (x::nil)) l.

    Lemma flat_replace_all_nil l (v:A) :
      flat_replace_all l v nil = @remove_all A eqdec v l.

    Lemma flat_replace_all_app l1 l2 (v:A) n
      : flat_replace_all (l1 ++ l2) v n
        = flat_replace_all l1 v n ++ flat_replace_all l2 v n.

    Lemma fold_left_remove_all_nil_in_inv {B} {x ps l}:
      In x (fold_left
              (fun (h : list nat) (xy : nat × B) ⇒
                 remove_all (fst xy) h)
              ps l) →
      In x l.

    Lemma fold_left_remove_all_nil_in_inv' {x ps l}:
      In x (fold_left
              (fun (h : list nat) (xy : nat) ⇒
                 remove_all xy h)
              ps l) →
      In x l.

    Lemma fold_left_remove_all_nil_in_not_inv' {x ps l}:
      In x (fold_left
              (fun (h : list nat) (xy : nat ) ⇒
                 remove_all xy h)
              ps l) →
      ¬ In x ps.

    Lemma replace_all_remove_eq (l : list A) (v n : A) :
      map (fun x : A ⇒ if eqdec x v then n else x) (remove eqdec v l) = (remove eqdec v l).

  End repall.

  Section incl.

    Definition cut_down_to {A B} {dec:EqDec A eq} (l:list (A×B)) (l2:list A) :=
      filter (fun a ⇒ existsb (fun z ⇒ (fst a) ==b z) l2) l.

    Lemma cut_down_to_in
          {A B} {dec:EqDec A eq}
          (l:list (A×B)) l2 a :
      In a (cut_down_to l l2) ↔ In a l ∧ In (fst a) l2 .

    Lemma cut_down_to_app {A B} {dec:EqDec A eq}
          (l l':list (A×B)) l2 :
      cut_down_to (l++l') l2 = cut_down_to l l2 ++ cut_down_to l' l2.

    Lemma incl_dec {A} {dec:EqDec A eq} (l1 l2:list A) :
      {incl l1 l2} + {¬ incl l1 l2}.

    Global Instance incl_pre A : PreOrder (@incl A).

    Lemma set_inter_contained {A} dec (l l':list A):
      (∀ a, In a l → In a l') →
      set_inter dec l l' = l.

    Lemma set_inter_idempotent {A} dec (l:list A):
      set_inter dec l l = l.

    Lemma set_inter_comm_in {A} dec a b :
      (∀ x, In x (@set_inter A dec a b) → In x (set_inter dec b a)) .

   Lemma nincl_exists {A} {dec:EqDec A eq} (l1 l2:list A) :
     ¬ incl l1 l2 → {x | In x l1 ∧ ¬ In x l2}.

  End incl.

  Section equivlist.
    Context {A:Type}.

    Definition equivlist (l l':list A)
      := ∀ x, In x l ↔ In x l'.

    Global Instance equivlist_equiv : Equivalence equivlist.

    Global Instance Permutation_equivlist :
      subrelation (@Permutation A) equivlist.

    Lemma equivlist_in {l1 l2} : equivlist l1 l2 → (∀ x:A, In x l1 → In x l2).

    Lemma equivlist_incls (l1 l2:list A) :
      equivlist l1 l2 ↔ (incl l1 l2 ∧ incl l2 l1).

    Global Instance equivlist_In_proper : Proper (eq ==> equivlist ==> iff) (@In A).

    Lemma equivlist_dec {dec:EqDec A eq} (l1 l2:list A) :
      {equivlist l1 l2} + {¬ equivlist l1 l2}.

    Lemma equivlist_nil {l:list A} : equivlist l nil → l = nil.

    Lemma app_idempotent_equivlist (l:list A) :
      equivlist (l++l) l.

    Lemma app_commutative_equivlist (l1 l2:list A) :
      equivlist (l1++l2) (l2++l1).

    Lemma app_contained_equivlist (a b:list A) :
      incl b a →
      equivlist (a ++ b) a.

    Lemma set_inter_equivlist dec a b :
      equivlist (@set_inter A dec a b) (set_inter dec b a) .

    Global Instance set_inter_equivlist_proper dec : Proper (equivlist ==> equivlist ==> equivlist) (@set_inter A dec).

  Lemma equivlist_cons l1 l2 (s:A) :
    equivlist l1 l2 →
    equivlist (s::l1) (s::l2).

  Global Instance equivlist_filter :
    Proper (eq ==> equivlist ==> equivlist) (@filter A).

  Global Instance equivlist_remove_all {dec:EqDec A eq} :
    Proper (eq ==> equivlist ==> equivlist) (@remove_all A dec).

    Lemma incl_list_dec (dec:∀ x y:A, {x = y} + {x ≠ y}) (l1 l2:list A) : {(∀ x, In x l1 → In x l2)} + {~(∀ x, In x l1 → In x l2)}.

  End equivlist.

      Lemma set_inter_assoc {A} dec a b c:
        @set_inter A dec (set_inter dec a b) c
        = set_inter dec a (set_inter dec b c).

  Section Assym_over.

    Definition asymmetric_over {A} R (l:list A) :=
      ∀ x y, In x l→ In y l → ¬R x y → ¬R y x → x = y.

    Lemma asymmetric_asymmetric_over {A} {R} :
      (∀ x y:A, ¬R x y → ¬R y x → x = y) →
      ∀ l, asymmetric_over R l .

    Lemma asymmetric_over_incl {A} {R} {l2:list A}
      : asymmetric_over R l2 →
        ∀ l1,
          (∀ x, In x l1 → In x l2) →
          asymmetric_over R l1.

    Lemma asymmetric_over_equivlist {A} {R} {l1 l2:list A} :
      equivlist l1 l2 →
      (asymmetric_over R l1 ↔
       asymmetric_over R l2).

    Lemma asymmetric_over_cons_inv {A} {R} {a:A} {l1} :
      asymmetric_over R (a::l1) →
      asymmetric_over R l1.


    Lemma asymmetric_over_swap {A} R {a b:A} {l1} :
      asymmetric_over R (a::b::l1) →
      asymmetric_over R (b::a::l1).

  End Assym_over.


  Global Instance perm_in {A} : Proper (eq ==> (@Permutation A) ==> iff) (@In A).

  Lemma NoDup_perm' {A:Type} {a b:list A} : NoDup a → Permutation a b → NoDup b.

  Global Instance NoDup_perm {A:Type} :
    Proper (@Permutation A ==> iff) (@NoDup A).

  Lemma NoDup_Permutation' {A : Type} (l l' : list A) :
    NoDup l →
    NoDup l' → equivlist l l' → Permutation l l'.

  Lemma NoDup_rev {A:Type} (l:list A) : NoDup (rev l) ↔ NoDup l.

  Lemma NoDup_app_inv {A:Type} {a b:list A} : NoDup (a++b) → NoDup a.


  Lemma NoDup_app_inv2 {A:Type} {a b:list A} : NoDup (a++b) → NoDup b.

  Lemma NoDup_dec {A:Type} {dec:EqDec A eq} (l:list A): {NoDup l} + {¬NoDup l}.

  Section disj.
    Definition disjoint {A:Type} (l1 l2:list A)
      := ∀ x, In x l1 → In x l2 → False.

    Lemma NoDup_app_dis {A:Type} (a b:list A) :
      NoDup (a++b) → disjoint a b.

    Lemma disjoint_cons_inv1 {A:Type} {a:A} {l1 l2} :
      disjoint (a :: l1) l2 → disjoint l1 l2 ∧ ¬ In a l2.

    Lemma disjoint_app_l {A} (l1 l2 l3:list A) :
    disjoint (l1 ++ l2) l3 ↔ (disjoint l1 l3 ∧ disjoint l2 l3).

   Lemma disjoint_app_r {A} (l1 l2 l3:list A) :
    disjoint l1 (l2 ++ l3) ↔ (disjoint l1 l2 ∧ disjoint l1 l3).

    Lemma NoDup_app {A:Type} {a b:list A} :
      disjoint a b → NoDup a → NoDup b → NoDup (a++b).

    Global Instance disjoint_sym {A:Type} : Symmetric (@disjoint A).

  End disj.

  Lemma unmap_NoDup {A B} (f:A→B) l :
    NoDup (map f l) → NoDup l.

  Lemma map_inj_NoDup {A B} (f:A→B)
            (inj:∀ x y, f x = f y → x = y) (l:list A) :
        NoDup l →
        NoDup (map f l).

  Lemma filter_NoDup {A} (f:A→bool) l :
    NoDup l → NoDup (filter f l).

  Fixpoint zip {A B} (l1:list A) (l2: list B) : option (list (A × B)) :=
    match l1 with
    | nil ⇒
      match l2 with
      | nil ⇒ Some nil
      | _ ⇒ None
      end
    | x1 :: l1' ⇒
      match l2 with
      | nil ⇒ None
      | x2 :: l2' ⇒
        match zip l1' l2' with
        | None ⇒ None
        | Some l3 ⇒
          Some ((x1, x2) :: l3)
        end
      end
    end.

End RList.